From: Ferruccio Guidi Date: Wed, 22 Nov 2017 21:19:18 +0000 (+0000) Subject: - equivalene of tc_lfxs and lex + lfeq proved X-Git-Tag: make_still_working~401 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=775106f04b47236bf47e4321d745ec360ab4ebb4 - equivalene of tc_lfxs and lex + lfeq proved - bug fixed in fqu_lref_S --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma index bc7061ba7..d802f6e1a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma @@ -30,6 +30,13 @@ lemma tc_lfxs_pair_refl: ∀R. c_reflexive … R → /3 width=3 by tc_lfxs_step_dx, lfxs_pair_refl, inj/ qed. +lemma tc_lfxs_tc: ∀R,L1,L2,T,f. 𝐈⦃f⦄ → TC … (lexs cfull (cext2 R) f) L1 L2 → + L1 ⪤**[R, T] L2. +#R #L1 #L2 #T #f #Hf #H elim H -L2 +[ elim (frees_total L1 T) | #L elim (frees_total L T) ] +/5 width=7 by lexs_sdj, tc_lfxs_step_dx, sdj_isid_sn, inj, ex2_intro/ +qed. + (* Advanced eliminators *****************************************************) lemma tc_lfxs_ind_sn: ∀R. c_reflexive … R → diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma new file mode 100644 index 000000000..dbcf5fe44 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/syntax/ext2_tc.ma". +include "basic_2/relocation/lexs_tc.ma". +include "basic_2/relocation/lex.ma". +include "basic_2/static/lfeq_fqup.ma". +include "basic_2/static/lfeq_lfeq.ma". +include "basic_2/i_static/tc_lfxs_fqup.ma". + +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +(* Properties with generic extension of a context sensitive relation ********) + +lemma tc_lfxs_lex: ∀R. c_reflexive … R → + ∀L1,L2,T. L1 ⪤[LTC … R] L2 → L1 ⪤**[R, T] L2. +#R #HR #L1 #L2 #T * +/5 width=7 by tc_lfxs_tc, lexs_inv_tc_dx, lexs_co, ext2_inv_tc, ext2_refl/ +qed. + +lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R → + ∀L1,L. L1 ⪤[LTC … R] L → ∀L2,T. L ≡[T] L2 → + L1 ⪤**[R, T] L2. +/3 width=3 by tc_lfxs_lex, tc_lfxs_step_dx, lfeq_fwd_lfxs/ qed. + +(* Inversion lemmas with generic extension of a context sensitive relation **) + +lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R → + lexs_frees_confluent (cext2 R) cfull → + s_rs_transitive_isid cfull (cext2 R) → + lfeq_transitive R → + ∀L1,L2,T. L1 ⪤**[R, T] L2 → + ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2. +#R #H1R #H2R #H3R #H4R #L1 #L2 #T #H +@(tc_lfxs_ind_sn … H1R … H) -H -L2 +[ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/ +| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0 + lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 // * #f1 #Hf1 #HL2 + elim (lexs_sdj_split … ceq_ext … HL2 f0 ?) -HL2 + [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] + lapply (lexs_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H + elim (H2R … Hf1 … H) -H #f2 #Hf2 #Hf21 + lapply (sle_lexs_trans … HL02 … Hf21) -f1 // #HL02 + lapply (lexs_co ?? cfull (LTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1 + /8 width=11 by lexs_inv_tc_dx, lexs_tc_dx, lexs_co, ext2_tc, ext2_refl, step, ex2_intro/ (**) (* full auto too slow *) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma deleted file mode 100644 index 64e38fc48..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma +++ /dev/null @@ -1,46 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "basic_2/syntax/ext2_tc.ma". -include "basic_2/relocation/lexs_tc.ma". -include "basic_2/relocation/lex.ma". -include "basic_2/static/lfeq_fqup.ma". -include "basic_2/static/lfxs_lfxs.ma". -include "basic_2/i_static/tc_lfxs_fqup.ma". - -(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) - -lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R → - (lexs_frees_confluent (cext2 R) cfull) → - (∀f. 𝐈⦃f⦄ → s_rs_transitive … (cext2 R) (λ_.lexs cfull (cext2 R) f)) → - ∀L1,L2,T. L1 ⪤**[R, T] L2 → - ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2. -#R #H1R #H2R #H3R #L1 #L2 #T #H -@(tc_lfxs_ind_sn … H1R … H) -H -L2 -[ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/ -| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0 - lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 * #f1 #Hf1 #HL2 - elim (lexs_sdj_split … ceq_ext … HL2 f0 ?) -HL2 - [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] - lapply (lexs_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H - elim (H2R … Hf1 … H) -H #f2 #Hf2 #Hf21 - lapply (sle_lexs_trans … HL02 … Hf21) -f1 // #HL02 - lapply (lexs_co ?? cfull (LTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1 - lapply (lexs_inv_tc_dx … HL1) -HL1 /2 width=1 by ext2_refl/ #HL1 - lapply (step ????? HL1 … HL0) -L #HL10 - lapply (lexs_tc_dx … H3R … HL10) -HL10 // #HL10 - lapply (lexs_co … cfull (cext2 (LTC … R)) … HL10) -HL10 /2 width=1 by ext2_tc/ #HL10 - /3 width=5 by ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma index b9cd6c4ab..3ec8b4164 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -40,6 +40,16 @@ theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP → Transitive … (lexs RN RP f). /2 width=9 by lexs_trans_gen/ qed-. +theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ → + ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2. +#R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f +[ #f #Hf #L2 #H >(lexs_inv_atom1 … H) -L2 // ] +#f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H +[ elim (isid_inv_next … Hf) | lapply (isid_inv_push … Hf ??) ] -Hf [5: |*: // ] #Hf +elim (lexs_inv_push1 … H) -H #I2 #K2 #HK2 #_ #H destruct +/3 width=1 by lexs_push/ +qed-. + (* Basic_2A1: includes: lpx_sn_conf *) theorem lexs_conf (RN1) (RP1) (RN2) (RP2): ∀L,f. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma index 46a31fe94..24d8d9fcf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma @@ -17,6 +17,9 @@ include "basic_2/relocation/lexs.ma". (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) +definition s_rs_transitive_isid: relation (relation3 lenv bind bind) ≝ λRN,RP. + ∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f). + (* Properties with transitive closure ***************************************) lemma lexs_tc_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → @@ -78,7 +81,7 @@ theorem lexs_tc_push: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → qed. (* Basic_2A1: uses: TC_lpx_sn_ind *) -theorem lexs_tc_step_dx: ∀RN,RP. (∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f)) → +theorem lexs_tc_step_dx: ∀RN,RP. s_rs_transitive_isid RN RP → ∀f,L1,L. L1 ⪤*[RN, RP, f] L → 𝐈⦃f⦄ → ∀L2. L ⪤*[RN, LTC … RP, f] L2 → L1⪤* [RN, LTC … RP, f] L2. #RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L @@ -96,7 +99,7 @@ qed-. (* Advanced properties ******************************************************) (* Basic_2A1: uses: TC_lpx_sn_inv_lpx_sn_LTC *) -lemma lexs_tc_dx: ∀RN,RP. (∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f)) → +lemma lexs_tc_dx: ∀RN,RP. s_rs_transitive_isid RN RP → ∀f. 𝐈⦃f⦄ → ∀L1,L2. TC … (lexs RN RP f) L1 L2 → L1 ⪤*[RN, LTC … RP, f] L2. #RN #RP #HRP #f #Hf #L1 #L2 #H @(TC_ind_dx ??????? H) -L1 /3 width=3 by lexs_tc_step_dx, lexs_tc_inj_dx/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma index 8dcfa103d..0f5feb7fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma @@ -44,7 +44,13 @@ interpretation (* Basic properties *********************************************************) -lemma fqu_lref_S: ∀b,I,G,L,V,i. ⦃G, L.ⓑ{I}V, #⫯i⦄ ⊐[b] ⦃G, L, #i⦄. +lemma fqu_sort: ∀b,I,G,L,s. ⦃G, L.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G, L, ⋆s⦄. +/2 width=1 by fqu_drop/ qed. + +lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G, L.ⓘ{I}, #⫯i⦄ ⊐[b] ⦃G, L, #i⦄. +/2 width=1 by fqu_drop/ qed. + +lemma fqu_gref: ∀b,I,G,L,l. ⦃G, L.ⓘ{I}, §l⦄ ⊐[b] ⦃G, L, §l⦄. /2 width=1 by fqu_drop/ qed. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index df8af706d..f55500bd1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -28,10 +28,7 @@ interpretation interpretation "degree-based ranged equivalence (local environment)" 'StarEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2). -(* -definition lfdeq_transitive: predicate (relation3 lenv term term) ≝ - λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≛[h, o, T1] L2 → R L1 T1 T2. -*) + (* Basic properties ***********************************************************) lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≛[h, o] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma index cc3fce365..1b6257520 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma @@ -25,10 +25,29 @@ interpretation "syntactic equivalence on referred entries (local environment)" 'LazyEqSn T L1 L2 = (lfeq T L1 L2). -(***************************************************) +(* Basic_2A1: uses: lleq_transitive *) +definition lfeq_transitive: predicate (relation3 lenv term term) ≝ + λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2. -axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L → - ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. +(* Basic_properties *********************************************************) + +lemma lfxs_transitive_lfeq: ∀R. lfxs_transitive ceq R R → lfeq_transitive R. +/2 width=5 by/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lfeq_transitive_inv_lfxs: ∀R. lfeq_transitive R → lfxs_transitive ceq R R. +/2 width=3 by/ qed-. + +(* Basic forward lemmas *****************************************************) + +(* Basic_2A1: was: llpx_sn_lrefl *) +(* Note: this should have been lleq_fwd_llpx_sn *) +lemma lfeq_fwd_lfxs: ∀R. c_reflexive … R → + ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤*[R, T] L2. +#R #HR #L1 #L2 #T * #f #Hf #HL12 +/4 width=7 by lexs_co, cext2_co, ex2_intro/ +qed-. (* Basic_2A1: removed theorems 10: lleq_ind lleq_fwd_lref diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma new file mode 100644 index 000000000..8fd1f2f4f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/static/lfxs_lfxs.ma". +include "basic_2/static/lfeq.ma". + +(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) + +(* Advanced forward lemmas **************************************************) + +(* Note: the proof should may invoke lfeq_transitive_inv_lfxs *) +lemma lfeq_lfxs_trans: ∀R. c_reflexive … R → lfeq_transitive R → + ∀L1,L,T. L1 ≡[T] L → + ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. +/3 width=9 by lfxs_trans_gen/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 9c0cc9c4a..80ed1c081 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -44,6 +44,16 @@ definition R_confluent2_lfxs: relation4 (relation3 lenv term term) ∀L1. L0 ⪤*[RP1, T0] L1 → ∀L2. L0 ⪤*[RP2, T0] L2 → ∃∃T. R2 L1 T1 T & R1 L2 T2 T. +definition lfxs_confluent: relation … ≝ + λR1,R2. + ∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V → + ∀K2. K ⪤*[R2, V] K2 → K ⪤*[R2, V1] K2. + +definition lfxs_transitive: relation3 ? (relation3 ?? term) ? ≝ + λR1,R2,R3. + ∀K1,K,V1. K1 ⪤*[R1, V1] K → + ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2. + (* Basic inversion lemmas ***************************************************) lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index c1d816668..89949c4b0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -165,6 +165,59 @@ elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] ] qed-. +theorem lfxs_trans_gen: ∀R1,R2,R3. + c_reflexive … R1 → c_reflexive … R2 → + lfxs_confluent R1 R2 → lfxs_transitive R1 R2 R3 → + ∀L1,T,L. L1 ⪤*[R1, T] L → + ∀L2. L ⪤*[R2, T] L2 → L1 ⪤*[R3, T] L2. +#R1 #R2 #R3 #H1R #H2R #H3R #H4R #L1 #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L1 T) -L1 -T +#G0 #L0 #T0 #IH #G #L1 * * +[ #s #HG #HL #HT #L #H1 #L2 #H2 destruct + elim (lfxs_inv_sort … H1) -H1 * + [ #H1 #H0 destruct + >(lfxs_inv_atom_sn … H2) -L2 // + | #I1 #I #K1 #K #HK1 #H1 #H0 destruct + elim (lfxs_inv_sort_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct + /4 width=3 by lfxs_sort, fqu_fqup/ + ] +| * [ | #i ] #HG #HL #HT #L #H1 #L2 #H2 destruct + [ elim (lfxs_inv_zero … H1) -H1 * + [ #H1 #H0 destruct + >(lfxs_inv_atom_sn … H2) -L2 // + | #I #K1 #K #V1 #V #HK1 #H1 #H0 #H destruct + elim (lfxs_inv_zero_pair_sn … H2) -H2 #K2 #V2 #HK2 #HV2 #H destruct + /4 width=7 by lfxs_pair, fqu_fqup, fqu_lref_O/ + | #f1 #I #K1 #K #Hf1 #HK1 #H1 #H0 destruct + elim (lfxs_inv_zero_unit_sn … H2) -H2 #f2 #K2 #Hf2 #HK2 #H destruct + /5 width=8 by lfxs_unit, lexs_trans_id_cfull, lexs_eq_repl_back, isid_inv_eq_repl/ + ] + | elim (lfxs_inv_lref … H1) -H1 * + [ #H1 #H0 destruct + >(lfxs_inv_atom_sn … H2) -L2 // + | #I1 #I #K1 #K #HK1 #H1 #H0 destruct + elim (lfxs_inv_lref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct + /4 width=3 by lfxs_lref, fqu_fqup/ + ] + ] +| #l #HG #HL #HT #L #H1 #L2 #H2 destruct + elim (lfxs_inv_gref … H1) -H1 * + [ #H1 #H0 destruct + >(lfxs_inv_atom_sn … H2) -L2 // + | #I1 #I #K1 #K #HK1 #H1 #H0 destruct + elim (lfxs_inv_gref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct + /4 width=3 by lfxs_gref, fqu_fqup/ + ] +| #p #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct + elim (lfxs_inv_bind … V1 V1 … H1) -H1 // #H1V #H1T + elim (lfxs_inv_bind … V1 V1 … H2) -H2 // #H2V #H2T + /3 width=4 by lfxs_bind/ +| #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct + elim (lfxs_inv_flat … H1) -H1 #H1V #H1T + elim (lfxs_inv_flat … H2) -H2 #H2V #H2T + /3 width=3 by lfxs_flat/ +] +qed-. + (* Negated inversion lemmas *************************************************) (* Basic_2A1: uses: nllpx_sn_inv_bind nllpx_sn_inv_bind_O *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 7737099cc..c2bfdf883 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -150,7 +150,7 @@ table { class "water" [ { "iterated static typing" * } { [ { "iterated extension on referred entries" * } { - [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] + [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] } ] } @@ -174,7 +174,7 @@ table { } ] [ { "syntactic equivalence on referred entries" * } { - [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" * ] + [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ] } ] [ { "generic extension on referred entries" * } {