From 156d974ad89aa04a086fdf9d332c8b04adf279fd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 18 Oct 2021 21:04:56 +0200 Subject: [PATCH] partial update in static_2 + ground library propagated in static/syntax + additions in ground --- .../lambdadelta/ground/arith/pnat_lt_plus.ma | 42 ++++++++ .../lambdadelta/ground/arith/wf1_ind_plt.ma | 29 ++++++ .../lambdadelta/ground/web/ground_src.tbl | 3 +- .../lambdadelta/static_2/syntax/append.ma | 2 +- .../static_2/syntax/append_length.ma | 33 ++++--- .../static_2/syntax/bind_weight.ma | 14 ++- .../static_2/syntax/cl_restricted_weight.ma | 21 ++-- .../lambdadelta/static_2/syntax/cl_weight.ma | 18 ++-- .../lambdadelta/static_2/syntax/fold.ma | 6 +- .../static_2/syntax/genv_length.ma | 3 +- .../static_2/syntax/genv_weight.ma | 10 +- .../static_2/syntax/lenv_length.ma | 20 ++-- .../static_2/syntax/lenv_weight.ma | 10 +- .../lambdadelta/static_2/syntax/lveq.ma | 96 ++++++++++++------- .../static_2/syntax/lveq_length.ma | 41 ++++---- .../lambdadelta/static_2/syntax/lveq_lveq.ma | 15 +-- .../lambdadelta/static_2/syntax/teq.ma | 2 +- .../lambdadelta/static_2/syntax/teq_ext.ma | 4 +- .../lambdadelta/static_2/syntax/teqw.ma | 3 +- .../static_2/syntax/term_vector.ma | 8 +- .../static_2/syntax/term_weight.ma | 17 ++-- 21 files changed, 264 insertions(+), 133 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat_lt_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/wf1_ind_plt.ma diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_lt_plus.ma new file mode 100644 index 000000000..bcbb0c000 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_lt_plus.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/arith/pnat_le_plus.ma". +include "ground/arith/pnat_lt.ma". + +(* STRICT ORDER FOR POSITIVE INTEGERS ***************************************) + +(* Constructions with pplus *************************************************) + +lemma plt_plus_bi_dx (p) (q1) (q2): q1 < q2 → q1 + p < q2 + p. +#p #q1 #q2 #H +@plt_i >pplus_succ_sn /2 width=1 by ple_plus_bi_dx/ +qed. + +lemma plt_plus_bi_sn (p) (q1) (q2): q1 < q2 → p + q1 < p + q2. +#p #q1 #q2 #H +@plt_i >pplus_succ_dx /2 width=1 by ple_plus_bi_sn/ +qed. + +lemma plt_plus_dx_dx_refl (p) (q): p < p + q. +/2 width=1 by ple_plus_bi_sn/ qed. + +lemma plt_plus_dx_sn_refl (p) (q): p < q + p. +/2 width=1 by ple_plus_bi_dx/ qed. + +lemma plt_plus_dx_sn (r) (p) (q): q ≤ p → q < r + p. +/2 width=3 by ple_plt_trans/ qed. + +lemma plt_plus_dx_dx (r) (p) (q): q ≤ p → q < p + r. +/2 width=3 by ple_plt_trans/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/wf1_ind_plt.ma b/matita/matita/contribs/lambdadelta/ground/arith/wf1_ind_plt.ma new file mode 100644 index 000000000..9547dad0c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/wf1_ind_plt.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/arith/pnat_lt.ma". + +(* WELL-FOUNDED INDUCTION ***************************************************) + +fact wf1_ind_plt_aux (A1) (f:A1→pnat) (Q:predicate …): + (∀p. (∀a1. f a1 < p → Q a1) → ∀a1. f a1 = p → Q a1) → + ∀p,a1. f a1 = p → Q a1. +#A1 #f #Q #H #p @(pnat_ind_lt … p) -p /3 width=3 by/ +qed-. + +lemma wf1_ind_plt (A1) (f:A1→pnat) (Q:predicate …): + (∀p. (∀a1. f a1 < p → Q a1) → ∀a1. f a1 = p → Q a1) → + ∀a1. Q a1. +#A #f #Q #H #a1 @(wf1_ind_plt_aux … H) -H // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index 638b1441c..a84e3e1a3 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -81,6 +81,7 @@ table { [ { "well-founded induction" * } { [ "wf1_ind_ylt" * ] [ "wf1_ind_nlt" "wf2_ind_nlt" "wf3_ind_nlt.ma" * ] + [ "wf1_ind_plt" * ] } ] [ { "non-negative integers with infinity" * } { @@ -106,7 +107,7 @@ table { } ] [ { "positive integers" * } { - [ "nat_lt ( ?<? )" "pnat_lt_pred" * ] + [ "nat_lt ( ?<? )" "pnat_lt_pred" "pnat_lt_plus" * ] [ "pnat_le ( ?≤? )" "pnat_le_pred" "pnat_le_plus" * ] [ "pnat_plus ( ?+? )" * ] [ "nat_pred ( ↓? )" * ] diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma index 0377292d6..220944f49 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/append.ma @@ -28,7 +28,7 @@ rec definition append L K on K ≝ match K with | LBind K I ⇒ (append L K).ⓘ[I] ]. -interpretation "append (local environment)" 'nplus L1 L2 = (append L1 L2). +interpretation "append (local environment)" 'plus L1 L2 = (append L1 L2). interpretation "local environment tail binding construction (generic)" 'SnItem I L = (append (LBind LAtom I) L). diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma index 2222c52ff..1e0de051b 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/append_length.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "ground/arith/nat_plus.ma". +include "ground/arith/wf1_ind_nlt.ma". include "static_2/syntax/lenv_length.ma". include "static_2/syntax/append.ma". @@ -34,31 +36,36 @@ qed. lemma length_inv_succ_dx_ltail: ∀L,n. |L| = ↑n → ∃∃I,K. |K| = n & L = ⓘ[I].K. #Y #n #H elim (length_inv_succ_dx … H) -H #I #L #Hn #HLK destruct -elim (lenv_case_tail … L) [2: * #K #J ] -#H destruct /2 width=4 by ex2_2_intro/ +elim (lenv_case_tail … L) [| * #K #J ] #H destruct +/2 width=4 by ex2_2_intro/ +@(ex2_2_intro … (J) (K.ⓘ[I])) // (**) (* auto fails *) +>ltail_length >length_bind // qed-. (* Basic_2A1: was: length_inv_pos_sn_ltail *) lemma length_inv_succ_sn_ltail: ∀L,n. ↑n = |L| → ∃∃I,K. n = |K| & L = ⓘ[I].K. #Y #n #H elim (length_inv_succ_sn … H) -H #I #L #Hn #HLK destruct -elim (lenv_case_tail … L) [2: * #K #J ] -#H destruct /2 width=4 by ex2_2_intro/ +elim (lenv_case_tail … L) [| * #K #J ] #H destruct +/2 width=4 by ex2_2_intro/ +@(ex2_2_intro … (J) (K.ⓘ[I])) // (**) (* auto fails *) +>ltail_length >length_bind // qed-. (* Inversion lemmas with length for local environments **********************) (* Basic_2A1: was: append_inj_sn *) lemma append_inj_length_sn: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |K1| = |K2| → - L1 = L2 ∧ K1 = K2. + ∧∧ L1 = L2 & K1 = K2. #K1 elim K1 -K1 [ * /2 width=1 by conj/ #K2 #I2 #L1 #L2 #_ >length_atom >length_bind - #H destruct + #H elim (eq_inv_zero_nsucc … H) | #K1 #I1 #IH * [ #L1 #L2 #_ >length_atom >length_bind - #H destruct + #H elim (eq_inv_nsucc_zero … H) | #K2 #I2 #L1 #L2 #H1 >length_bind >length_bind #H2 + lapply (eq_inv_nsucc_bi … H2) -H2 #H2 elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *) elim (IH … H1) -IH -H1 /3 width=4 by conj/ ] @@ -68,16 +75,16 @@ qed-. (* Note: lemma 750 *) (* Basic_2A1: was: append_inj_dx *) lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |L1| = |L2| → - L1 = L2 ∧ K1 = K2. + ∧∧ L1 = L2 & K1 = K2. #K1 elim K1 -K1 [ * /2 width=1 by conj/ #K2 #I2 #L1 #L2 >append_atom >append_bind #H destruct - >length_bind >append_length >nplus_succ_dx - #H elim (succ_nplus_refl_sn … H) + >length_bind >append_length #H + elim (succ_nplus_refl_sn (|L2|) (|K2|) ?) // | #K1 #I1 #IH * [ #L1 #L2 >append_bind >append_atom #H destruct - >length_bind >append_length >nplus_succ_dx #H - lapply (nplus_refl_sn … H) -H #H destruct + >length_bind >append_length #H + elim (succ_nplus_refl_sn … H) | #K2 #I2 #L1 #L2 >append_bind >append_bind #H1 #H2 elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *) elim (IH … H1) -IH -H1 /2 width=1 by conj/ @@ -107,6 +114,6 @@ lemma lenv_ind_tail: ∀Q:predicate lenv. Q (⋆) → (∀I,L. Q L → Q (ⓘ[I].L)) → ∀L. Q L. #Q #IH1 #IH2 #L @(wf1_ind_nlt … length … L) -L #x #IHx * // #L #I -IH1 #H destruct -elim (lenv_case_tail … L) [2: * #K #J ] +elim (lenv_case_tail … L) [| * #K #J ] #H destruct /3 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/bind_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/bind_weight.ma index 2cf1bc170..caab2538a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/bind_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/bind_weight.ma @@ -18,14 +18,18 @@ include "static_2/syntax/bind.ma". (* WEIGHT OF A BINDER FOR LOCAL ENVIRONMENTS *******************************) rec definition bw I ≝ match I with -[ BUnit _ ⇒ 1 +[ BUnit _ ⇒ 𝟏 | BPair _ V ⇒ ♯❨V❩ ]. -interpretation "weight (binder for local environments)" 'Weight I = (bw I). +interpretation + "weight (binder for local environments)" + 'Weight I = (bw I). (* Basic properties *********************************************************) -lemma bw_pos: ∀I. 1 ≤ ♯❨I❩. -* // -qed. +lemma bw_unit_unfold (I): 𝟏 = ♯❨BUnit I❩. +// qed. + +lemma bw_pair_unfold (I) (V): ♯❨V❩ = ♯❨BPair I V❩. +// qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma index 62ce9d6fc..879af21b2 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_restricted_weight.ma @@ -23,30 +23,27 @@ interpretation "weight (restricted closure)" 'Weight L T = (rfw L T). (* Basic properties *********************************************************) +lemma rfw_unfold (L) (T): ♯❨L❩ + ♯❨T❩ = ♯❨L,T❩. +// qed. + (* Basic_1: was: flt_shift *) lemma rfw_shift: ∀p,I,K,V,T. ♯❨K.ⓑ[I]V,T❩ < ♯❨K,ⓑ[p,I]V.T❩. -normalize /2 width=1 by nle_plus_bi_sn/ -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma rfw_clear: ∀p,I1,I2,K,V,T. ♯❨K.ⓤ[I1],T❩ < ♯❨K,ⓑ[p,I2]V.T❩. -normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/ -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma rfw_tpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L,②[I]V.T❩. -normalize in ⊢ (?→?→?→?→?%%); // -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma rfw_tpair_dx: ∀I,L,V,T. ♯❨L,T❩ < ♯❨L,②[I]V.T❩. -normalize in ⊢ (?→?→?→?→?%%); // -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma rfw_lpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L.ⓑ[I]V,T❩. -normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/ -qed. +// qed. lemma rfw_lpair_dx: ∀I,L,V,T. ♯❨L,T❩ < ♯❨L.ⓑ[I]V,T❩. -normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/ -qed. +/2 width=1 by plt_plus_bi_dx/ qed. (* Basic_1: removed theorems 7: flt_thead_sx flt_thead_dx flt_trans diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma index e87996c23..515e72a9f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/cl_weight.ma @@ -25,26 +25,24 @@ interpretation "weight (closure)" 'Weight G L T = (fw G L T). (* Basic properties *********************************************************) +lemma fw_unfold (G) (L) (T): ♯❨L❩ + ♯❨T❩ = ♯❨G,L,T❩. +// qed. + (* Basic_1: was: flt_shift *) lemma fw_shift: ∀p,I,G,K,V,T. ♯❨G,K.ⓑ[I]V,T❩ < ♯❨G,K,ⓑ[p,I]V.T❩. -normalize /2 width=1 by nle_plus_bi_sn/ -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma fw_clear: ∀p,I1,I2,G,K,V,T. ♯❨G,K.ⓤ[I1],T❩ < ♯❨G,K,ⓑ[p,I2]V.T❩. -normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/ -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma fw_tpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L,②[I]V.T❩. -normalize in ⊢ (?→?→?→?→?→?%%); // -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma fw_tpair_dx: ∀I,G,L,V,T. ♯❨G,L,T❩ < ♯❨G,L,②[I]V.T❩. -normalize in ⊢ (?→?→?→?→?→?%%); // -qed. +/2 width=1 by plt_plus_bi_sn/ qed. lemma fw_lpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L.ⓑ[I]V,T❩. -normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/ -qed. +// qed. (* Basic_1: removed theorems 7: flt_thead_sx flt_thead_dx flt_trans diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma index 061ef6ed9..37c715067 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/fold.ma @@ -19,19 +19,19 @@ include "static_2/syntax/lenv.ma". rec definition fold L T on L ≝ match L with [ LAtom ⇒ T | LBind L I ⇒ match I with - [ BUnit _ ⇒ fold L (-ⓛ⋆0.T) + [ BUnit _ ⇒ fold L (-ⓛ⋆𝟎.T) | BPair I V ⇒ fold L (-ⓑ[I]V.T) ] ]. -interpretation "fold (restricted closure)" 'nplus L T = (fold L T). +interpretation "fold (restricted closure)" 'plus L T = (fold L T). (* Basic properties *********************************************************) lemma fold_atom: ∀T. ⋆ + T = T. // qed. -lemma fold_unit: ∀I,L,T. L.ⓤ[I]+T = L+(-ⓛ⋆0.T). +lemma fold_unit: ∀I,L,T. L.ⓤ[I]+T = L+(-ⓛ⋆𝟎.T). // qed. lemma fold_pair: ∀I,L,V,T. (L.ⓑ[I]V)+T = L+(-ⓑ[I]V.T). diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma index afd36af9c..41e22b52c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_length.ma @@ -12,12 +12,13 @@ (* *) (**************************************************************************) +include "ground/arith/nat_succ.ma". include "static_2/syntax/genv.ma". (* LENGTH OF A GLOBAL ENVIRONMENT *******************************************) rec definition glength G on G ≝ match G with -[ GAtom ⇒ 0 +[ GAtom ⇒ 𝟎 | GPair G _ _ ⇒ ↑(glength G) ]. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma index 88dcbc185..6cda4db4f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/genv_weight.ma @@ -18,7 +18,7 @@ include "static_2/syntax/genv.ma". (* WEIGHT OF A GLOBAL ENVIRONMENT *******************************************) rec definition gw G ≝ match G with -[ GAtom ⇒ 0 +[ GAtom ⇒ 𝟏 | GPair G I T ⇒ gw G + ♯❨T❩ ]. @@ -26,5 +26,11 @@ interpretation "weight (global environment)" 'Weight G = (gw G). (* Basic properties *********************************************************) +lemma gw_atom_unfold: 𝟏 = ♯❨⋆❩. +// qed. + +lemma gw_pair_unfold (I) (G) (T): ♯❨G❩ + ♯❨T❩ = ♯❨G.ⓑ[I]T❩. +// qed. + lemma gw_pair: ∀I,G,T. ♯❨G❩ < ♯❨G.ⓑ[I]T❩. -normalize /2 width=1 by nle_plus_bi_sn/ qed. +// qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma index 5f4b5dcb7..164aab500 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_length.ma @@ -12,12 +12,13 @@ (* *) (**************************************************************************) +include "ground/arith/nat_succ.ma". include "static_2/syntax/lenv.ma". (* LENGTH OF A LOCAL ENVIRONMENT ********************************************) rec definition length L ≝ match L with -[ LAtom ⇒ 0 +[ LAtom ⇒ 𝟎 | LBind L _ ⇒ ↑(length L) ]. @@ -25,7 +26,7 @@ interpretation "length (local environment)" 'card L = (length L). (* Basic properties *********************************************************) -lemma length_atom: |⋆| = 0. +lemma length_atom: |⋆| = 𝟎. // qed. (* Basic_2A1: uses: length_pair *) @@ -34,20 +35,23 @@ lemma length_bind: ∀I,L. |L.ⓘ[I]| = ↑|L|. (* Basic inversion lemmas ***************************************************) -lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆. -* // #L #I >length_bind -#H destruct +lemma length_inv_zero_dx: ∀L. |L| = 𝟎 → L = ⋆. +* // #L #I +>length_bind #H +elim (eq_inv_nsucc_zero … H) qed-. -lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆. +lemma length_inv_zero_sn: ∀L. 𝟎 = |L| → L = ⋆. /2 width=1 by length_inv_zero_dx/ qed-. (* Basic_2A1: was: length_inv_pos_dx *) lemma length_inv_succ_dx: ∀n,L. |L| = ↑n → ∃∃I,K. |K| = n & L = K. ⓘ[I]. #n * -[ >length_atom #H destruct -| #L #I >length_bind /3 width=4 by ex2_2_intro, eq_inv_nsucc_bi/ +[ >length_atom #H + elim (eq_inv_zero_nsucc … H) +| #L #I >length_bind + /3 width=4 by ex2_2_intro, eq_inv_nsucc_bi/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma index 66d46a41f..f406ed9d0 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lenv_weight.ma @@ -18,7 +18,7 @@ include "static_2/syntax/lenv.ma". (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************) rec definition lw L ≝ match L with -[ LAtom ⇒ 0 +[ LAtom ⇒ 𝟏 | LBind L I ⇒ lw L + ♯❨I❩ ]. @@ -26,9 +26,15 @@ interpretation "weight (local environment)" 'Weight L = (lw L). (* Basic properties *********************************************************) +lemma lw_atom_unfold: 𝟏 = ♯❨⋆❩. +// qed. + +lemma lw_bind_unfold (I) (L): ♯❨L❩ + ♯❨I❩ = ♯❨L.ⓘ[I]❩. +// qed. + (* Basic_2A1: uses: lw_pair *) lemma lw_bind: ∀I,L. ♯❨L❩ < ♯❨L.ⓘ[I]❩. -normalize /2 width=1 by nle_plus_bi_sn/ qed. +// qed. (* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *) (* Basic_1: removed local theorems 1: clt_wf__q_ind *) diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma index e127fa236..43d4e636f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma @@ -12,21 +12,23 @@ (* *) (**************************************************************************) +include "ground/xoa/ex_3_1.ma". include "ground/xoa/ex_3_4.ma". include "ground/xoa/ex_4_1.ma". +include "ground/arith/nat_succ.ma". include "static_2/notation/relations/voidstareq_4.ma". include "static_2/syntax/lenv.ma". (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************) inductive lveq: bi_relation nat lenv ≝ -| lveq_atom : lveq 0 (⋆) 0 (⋆) -| lveq_bind : ∀I1,I2,K1,K2. lveq 0 K1 0 K2 → - lveq 0 (K1.ⓘ[I1]) 0 (K2.ⓘ[I2]) -| lveq_void_sn: ∀K1,K2,n1. lveq n1 K1 0 K2 → - lveq (↑n1) (K1.ⓧ) 0 K2 -| lveq_void_dx: ∀K1,K2,n2. lveq 0 K1 n2 K2 → - lveq 0 K1 (↑n2) (K2.ⓧ) +| lveq_atom : lveq 𝟎 (⋆) 𝟎 (⋆) +| lveq_bind : ∀I1,I2,K1,K2. lveq 𝟎 K1 𝟎 K2 → + lveq 𝟎 (K1.ⓘ[I1]) 𝟎 (K2.ⓘ[I2]) +| lveq_void_sn: ∀K1,K2,n1. lveq n1 K1 𝟎 K2 → + lveq (↑n1) (K1.ⓧ) 𝟎 K2 +| lveq_void_dx: ∀K1,K2,n2. lveq 𝟎 K1 n2 K2 → + lveq 𝟎 K1 (↑n2) (K2.ⓧ) . interpretation "equivalence up to exclusion binders (local environment)" @@ -34,7 +36,7 @@ interpretation "equivalence up to exclusion binders (local environment)" (* Basic properties *********************************************************) -lemma lveq_refl: ∀L. L ≋ⓧ*[0,0] L. +lemma lveq_refl: ∀L. L ≋ⓧ*[𝟎,𝟎] L. #L elim L -L /2 width=1 by lveq_atom, lveq_bind/ qed. @@ -46,37 +48,41 @@ qed-. (* Basic inversion lemmas ***************************************************) fact lveq_inv_zero_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → - 0 = n1 → 0 = n2 → + (𝟎 = n1) → 𝟎 = n2 → ∨∨ ∧∧ ⋆ = L1 & ⋆ = L2 - | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[0,0] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2. + | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[𝟎,𝟎] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2. #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2 [1: /3 width=1 by or_introl, conj/ |2: /3 width=7 by ex3_4_intro, or_intror/ -|*: #K1 #K2 #n #_ #H1 #H2 destruct +|*: #K1 #K2 #n #_ [ #H #_ | #_ #H ] + elim (eq_inv_zero_nsucc … H) ] qed-. -lemma lveq_inv_zero: ∀L1,L2. L1 ≋ⓧ*[0,0] L2 → +lemma lveq_inv_zero: ∀L1,L2. L1 ≋ⓧ*[𝟎,𝟎] L2 → ∨∨ ∧∧ ⋆ = L1 & ⋆ = L2 - | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[0,0] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2. + | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[𝟎,𝟎] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2. /2 width=5 by lveq_inv_zero_aux/ qed-. fact lveq_inv_succ_sn_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → ∀m1. ↑m1 = n1 → - ∃∃K1. K1 ≋ⓧ*[m1,0] L2 & K1.ⓧ = L1 & 0 = n2. + ∃∃K1. K1 ≋ⓧ*[m1,𝟎] L2 & K1.ⓧ = L1 & 𝟎 = n2. #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2 -[1: #m #H destruct -|2: #I1 #I2 #K1 #K2 #_ #m #H destruct -|*: #K1 #K2 #n #HK #m #H destruct /2 width=3 by ex3_intro/ +[1: #m #H elim (eq_inv_nsucc_zero … H) +|2: #I1 #I2 #K1 #K2 #_ #m #H elim (eq_inv_nsucc_zero … H) +|*: #K1 #K2 #n #HK #m #H + [ >(eq_inv_nsucc_bi … H) -m /2 width=3 by ex3_intro/ + | elim (eq_inv_nsucc_zero … H) + ] ] qed-. lemma lveq_inv_succ_sn: ∀L1,K2,n1,n2. L1 ≋ⓧ*[↑n1,n2] K2 → - ∃∃K1. K1 ≋ⓧ*[n1,0] K2 & K1.ⓧ = L1 & 0 = n2. + ∃∃K1. K1 ≋ⓧ*[n1,𝟎] K2 & K1.ⓧ = L1 & 𝟎 = n2. /2 width=3 by lveq_inv_succ_sn_aux/ qed-. lemma lveq_inv_succ_dx: ∀K1,L2,n1,n2. K1 ≋ⓧ*[n1,↑n2] L2 → - ∃∃K2. K1 ≋ⓧ*[0,n2] K2 & K2.ⓧ = L2 & 0 = n1. + ∃∃K2. K1 ≋ⓧ*[𝟎,n2] K2 & K2.ⓧ = L2 & 𝟎 = n1. #K1 #L2 #n1 #n2 #H lapply (lveq_sym … H) -H #H elim (lveq_inv_succ_sn … H) -H /3 width=3 by lveq_sym, ex3_intro/ @@ -85,9 +91,10 @@ qed-. fact lveq_inv_succ_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → ∀m1,m2. ↑m1 = n1 → ↑m2 = n2 → ⊥. #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2 -[1: #m1 #m2 #H1 #H2 destruct -|2: #I1 #I2 #K1 #K2 #_ #m1 #m2 #H1 #H2 destruct -|*: #K1 #K2 #n #_ #m1 #m2 #H1 #H2 destruct +[1: #m1 #m2 #H #_ elim (eq_inv_nsucc_zero … H) +|2: #I1 #I2 #K1 #K2 #_ #m1 #m2 #H #_ elim (eq_inv_nsucc_zero … H) +|*: #K1 #K2 #n #_ #m1 #m2 [ #_ #H | #H #_ ] + elim (eq_inv_nsucc_zero … H) ] qed-. @@ -96,13 +103,15 @@ lemma lveq_inv_succ: ∀L1,L2,n1,n2. L1 ≋ⓧ*[↑n1,↑n2] L2 → ⊥. (* Advanced inversion lemmas ************************************************) -lemma lveq_inv_bind_O: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[0,0] K2.ⓘ[I2] → K1 ≋ⓧ*[0,0] K2. +lemma lveq_inv_bind_O: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[𝟎,𝟎] K2.ⓘ[I2] → K1 ≋ⓧ*[𝟎,𝟎] K2. #I1 #I2 #K1 #K2 #H elim (lveq_inv_zero … H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct // qed-. -lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1,n2] ⋆ → ∧∧ 0 = n1 & 0 = n2. -* [2: #n1 ] * [2,4: #n2 ] #H +lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1,n2] ⋆ → ∧∧ 𝟎 = n1 & 𝟎 = n2. +#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ] +#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ] +#H [ elim (lveq_inv_succ … H) | elim (lveq_inv_succ_dx … H) -H #Y #_ #H1 #H2 destruct | elim (lveq_inv_succ_sn … H) -H #Y #_ #H1 #H2 destruct @@ -111,8 +120,11 @@ lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1,n2] ⋆ → ∧∧ 0 = n1 & 0 qed-. lemma lveq_inv_bind_atom: ∀I1,K1,n1,n2. K1.ⓘ[I1] ≋ⓧ*[n1,n2] ⋆ → - ∃∃m1. K1 ≋ⓧ*[m1,0] ⋆ & BUnit Void = I1 & ↑m1 = n1 & 0 = n2. -#I1 #K1 * [2: #n1 ] * [2,4: #n2 ] #H + ∃∃m1. K1 ≋ⓧ*[m1,𝟎] ⋆ & BUnit Void = I1 & ↑m1 = n1 & 𝟎 = n2. +#I1 #K1 +#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ] +#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ] +#H [ elim (lveq_inv_succ … H) | elim (lveq_inv_succ_dx … H) -H #Y #_ #H1 #H2 destruct | elim (lveq_inv_succ_sn … H) -H #Y #HY #H1 #H2 destruct /2 width=3 by ex4_intro/ @@ -124,7 +136,7 @@ lemma lveq_inv_bind_atom: ∀I1,K1,n1,n2. K1.ⓘ[I1] ≋ⓧ*[n1,n2] ⋆ → qed-. lemma lveq_inv_atom_bind: ∀I2,K2,n1,n2. ⋆ ≋ⓧ*[n1,n2] K2.ⓘ[I2] → - ∃∃m2. ⋆ ≋ⓧ*[0,m2] K2 & BUnit Void = I2 & 0 = n1 & ↑m2 = n2. + ∃∃m2. ⋆ ≋ⓧ*[𝟎,m2] K2 & BUnit Void = I2 & 𝟎 = n1 & ↑m2 = n2. #I2 #K2 #n1 #n2 #H lapply (lveq_sym … H) -H #H elim (lveq_inv_bind_atom … H) -H @@ -132,8 +144,11 @@ elim (lveq_inv_bind_atom … H) -H qed-. lemma lveq_inv_pair_pair: ∀I1,I2,K1,K2,V1,V2,n1,n2. K1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] K2.ⓑ[I2]V2 → - ∧∧ K1 ≋ⓧ*[0,0] K2 & 0 = n1 & 0 = n2. -#I1 #I2 #K1 #K2 #V1 #V2 * [2: #n1 ] * [2,4: #n2 ] #H + ∧∧ K1 ≋ⓧ*[𝟎,𝟎] K2 & 𝟎 = n1 & 𝟎 = n2. +#I1 #I2 #K1 #K2 #V1 #V2 +#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ] +#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ] +#H [ elim (lveq_inv_succ … H) | elim (lveq_inv_succ_dx … H) -H #Y #_ #H1 #H2 destruct | elim (lveq_inv_succ_sn … H) -H #Y #_ #H1 #H2 destruct @@ -145,13 +160,13 @@ lemma lveq_inv_pair_pair: ∀I1,I2,K1,K2,V1,V2,n1,n2. K1.ⓑ[I1]V1 ≋ⓧ*[n1,n2 qed-. lemma lveq_inv_void_succ_sn: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[↑n1,n2] L2 → - ∧∧ L1 ≋ ⓧ*[n1,0] L2 & 0 = n2. + ∧∧ L1 ≋ ⓧ*[n1,𝟎] L2 & 𝟎 = n2. #L1 #L2 #n1 #n2 #H elim (lveq_inv_succ_sn … H) -H #Y #HY #H1 #H2 destruct /2 width=1 by conj/ qed-. lemma lveq_inv_void_succ_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,↑n2] L2.ⓧ → - ∧∧ L1 ≋ ⓧ*[0,n2] L2 & 0 = n1. + ∧∧ L1 ≋ ⓧ*[𝟎,n2] L2 & 𝟎 = n1. #L1 #L2 #n1 #n2 #H lapply (lveq_sym … H) -H #H elim (lveq_inv_void_succ_sn … H) -H @@ -161,18 +176,25 @@ qed-. (* Advanced forward lemmas **************************************************) lemma lveq_fwd_gen: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → - ∨∨ 0 = n1 | 0 = n2. -#L1 #L2 * [2: #n1 ] * [2,4: #n2 ] #H + ∨∨ 𝟎 = n1 | 𝟎 = n2. +#L1 #L2 +#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ] +#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ] +#H [ elim (lveq_inv_succ … H) ] /2 width=1 by or_introl, or_intror/ qed-. -lemma lveq_fwd_pair_sn: ∀I1,K1,L2,V1,n1,n2. K1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2 → 0 = n1. -#I1 #K1 #L2 #V1 * [2: #n1 ] // * [2: #n2 ] #H +lemma lveq_fwd_pair_sn: + ∀I1,K1,L2,V1,n1,n2. K1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2 → 𝟎 = n1. +#I1 #K1 #L2 #V1 +#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ] // +#n2 @(nat_ind_succ … n2) -n2 [2: #n2 #_ ] #H [ elim (lveq_inv_succ … H) | elim (lveq_inv_succ_sn … H) -H #Y #_ #H1 #H2 destruct ] qed-. -lemma lveq_fwd_pair_dx: ∀I2,L1,K2,V2,n1,n2. L1 ≋ⓧ*[n1,n2] K2.ⓑ[I2]V2 → 0 = n2. +lemma lveq_fwd_pair_dx: + ∀I2,L1,K2,V2,n1,n2. L1 ≋ⓧ*[n1,n2] K2.ⓑ[I2]V2 → 𝟎 = n2. /3 width=6 by lveq_fwd_pair_sn, lveq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma index da13d1248..3154290eb 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground/arith/nat_le_minus_plus.ma". include "static_2/syntax/lenv_length.ma". include "static_2/syntax/lveq.ma". @@ -19,7 +20,7 @@ include "static_2/syntax/lveq.ma". (* Properties with length for local environments ****************************) -lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[0,0] L2. +lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[𝟎,𝟎] L2. #L1 elim L1 -L1 [ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/ | #K1 #I1 #IH #Y2 #H @@ -31,35 +32,40 @@ qed. (* Forward lemmas with length for local environments ************************) lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n1 ≤ |L1|. -#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize +#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by nle_succ_bi/ qed-. lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n2 ≤ |L2|. -#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize +#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by nle_succ_bi/ qed-. lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → ∧∧ |L1|-|L2| = n1 & |L2|-|L1| = n2. -#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by conj/ -#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by nminus_succ_sn, conj/ +#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 +[ /2 width=1 by conj/ +| #I1 #I2 #K1 #K2 #_ #IH >length_bind >length_bind // +] +#K1 #K2 #n #_ * #H1 #H2 destruct +>length_bind (nle_inv_eq_zero_minus … HL) // qed-. -lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 0 = n2. +lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 𝟎 = n2. #L1 #L2 #n1 #n2 #H #HL elim (lveq_fwd_length … H) -H >(nle_inv_eq_zero_minus … HL) // qed-. lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → - |L1| = |L2| → ∧∧ 0 = n1 & 0 = n2. + |L1| = |L2| → ∧∧ 𝟎 = n1 & 𝟎 = n2. #L1 #L2 #n1 #n2 #H #HL elim (lveq_fwd_length … H) -H >HL -HL /2 width=1 by conj/ @@ -67,11 +73,11 @@ qed-. lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| + n2 = |L2| + n1. -#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize -/2 width=2 by eq_inv_nplus_bi_sn/ +#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 // +#k1 #K2 #n #_ #IH length_bind >length_bind // +elim (lveq_fwd_length … HL) -HL >length_bind >length_bind +nplus_succ_dx #H0 +lapply (lveq_fwd_length_plus … H) >length_bind >nplus_succ_shift #H0 lapply (nplus_2_des_le_sn_sn … H0 HL12) -H0 -HL12 #H0 -elim (nle_inv_succ_sn … H0) -H0 #m2 #_ #H0 destruct +elim (nle_inv_succ_sn … H0) -H0 #_ #H0 >H0 in H; -H0 #H elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/ qed-. +(**) (* state with m1 ≝ ↓n1 *) lemma lveq_inv_void_sn_length: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → - ∃∃m1. L1 ≋ ⓧ*[m1,n2] L2 & ↑m1 = n1 & 0 = n2. + ∃∃m1. L1 ≋ ⓧ*[m1,n2] L2 & ↑m1 = n1 & 𝟎 = n2. #L1 #L2 #n1 #n2 #H #HL lapply (lveq_sym … H) -H #H elim (lveq_inv_void_dx_length … H HL) -H -HL diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma index 6966715c4..83b9bc787 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma @@ -18,12 +18,12 @@ include "static_2/syntax/lveq_length.ma". (* Main inversion lemmas ****************************************************) -theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[0,0] K2 → +theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[𝟎,𝟎] K2 → ∀I1,I2,m1,m2. K1.ⓘ[I1] ≋ⓧ*[m1,m2] K2.ⓘ[I2] → - ∧∧ 0 = m1 & 0 = m2. + ∧∧ 𝟎 = m1 & 𝟎 = m2. #K1 #K2 #HK #I1 #I2 #m1 #m2 #H lapply (lveq_fwd_length_eq … HK) -HK #HK -elim (lveq_inj_length … H) -H normalize /3 width=1 by conj, eq_f/ +elim (lveq_inj_length … H) -H /3 width=1 by conj/ qed-. theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → @@ -38,16 +38,17 @@ qed-. theorem lveq_inj_void_sn_ge: ∀K1,K2. |K2| ≤ |K1| → ∀n1,n2. K1 ≋ⓧ*[n1,n2] K2 → ∀m1,m2. K1.ⓧ ≋ⓧ*[m1,m2] K2 → - ∧∧ ↑n1 = m1 & 0 = m2 & 0 = n2. + ∧∧ ↑n1 = m1 & 𝟎 = m2 & 𝟎 = n2. #L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct ->length_bind >nminus_succ_dx >(nle_inv_eq_zero_minus … HL) -/3 width=4 by nminus_plus_comm_23, and3_intro/ +>length_bind