From 606dab57f31b66eb3f30f603185124b88dfad4c1 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 29 Jan 2014 18:55:32 +0000
Subject: [PATCH] bug fix in the notation of normal forms, now we specify that
they are normal forms for reduction. This will allow to enable normal forms
for substitution ...
---
.../lambdadelta/basic_2/computation/cpre.ma | 9 ++-
.../lambdadelta/basic_2/computation/cprs.ma | 48 ++++++++--------
.../lambdadelta/basic_2/computation/cpxe.ma | 9 ++-
.../lambdadelta/basic_2/computation/cpxs.ma | 2 +-
.../basic_2/computation/cpxs_cpys.ma | 57 -------------------
.../basic_2/computation/cpxs_tstc.ma | 2 +-
.../basic_2/computation/cpxs_tstc_vector.ma | 2 +-
.../lambdadelta/basic_2/computation/csx.ma | 2 +-
.../basic_2/computation/csx_tstc_vector.ma | 2 +-
.../basic_2/computation/lpxs_lleq.ma | 57 +++++++++++++++----
.../basic_2/notation/relations/normal_3.ma | 2 +-
.../basic_2/notation/relations/normal_5.ma | 2 +-
.../notation/relations/notreducible_3.ma | 2 +-
.../notation/relations/notreducible_5.ma | 2 +-
.../basic_2/notation/relations/reducible_3.ma | 2 +-
.../basic_2/notation/relations/reducible_5.ma | 2 +-
.../lambdadelta/basic_2/reduction/cir.ma | 32 +++++------
.../basic_2/reduction/cir_append.ma | 8 +--
.../lambdadelta/basic_2/reduction/cir_lift.ma | 8 +--
.../lambdadelta/basic_2/reduction/cix.ma | 40 ++++++-------
.../basic_2/reduction/cix_append.ma | 8 +--
.../lambdadelta/basic_2/reduction/cix_lift.ma | 10 ++--
.../lambdadelta/basic_2/reduction/cnr.ma | 20 +++----
.../lambdadelta/basic_2/reduction/cnr_cir.ma | 4 +-
.../lambdadelta/basic_2/reduction/cnr_crr.ma | 2 +-
.../lambdadelta/basic_2/reduction/cnr_lift.ma | 12 ++--
.../lambdadelta/basic_2/reduction/cnx.ma | 44 +++++++-------
.../lambdadelta/basic_2/reduction/cnx_cix.ma | 4 +-
.../lambdadelta/basic_2/reduction/cnx_crx.ma | 10 ++--
.../lambdadelta/basic_2/reduction/cnx_lift.ma | 10 ++--
.../lambdadelta/basic_2/reduction/cpr_cir.ma | 8 +--
.../lambdadelta/basic_2/reduction/cpx_cix.ma | 12 ++--
.../lambdadelta/basic_2/reduction/crr.ma | 30 +++++-----
.../basic_2/reduction/crr_append.ma | 12 ++--
.../lambdadelta/basic_2/reduction/crr_lift.ma | 8 +--
.../lambdadelta/basic_2/reduction/crx.ma | 32 +++++------
.../basic_2/reduction/crx_append.ma | 9 +--
.../lambdadelta/basic_2/reduction/crx_lift.ma | 8 +--
.../lambdadelta/basic_2/web/basic_2_src.tbl | 26 ++++-----
39 files changed, 268 insertions(+), 291 deletions(-)
delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma
index 61dadbcde..2e81a1a0a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma
@@ -19,7 +19,7 @@ include "basic_2/computation/csx.ma".
(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
definition cpre: relation4 genv lenv term term â
- λG,L,T1,T2. â¦G, L⦠⢠T1 â¡* T2 ⧠â¦G, L⦠⢠ðâ¦T2â¦.
+ λG,L,T1,T2. â¦G, L⦠⢠T1 â¡* T2 ⧠â¦G, L⦠⢠⡠ðâ¦T2â¦.
interpretation "context-sensitive parallel evaluation (term)"
'PEval G L T1 T2 = (cpre G L T1 T2).
@@ -29,8 +29,7 @@ interpretation "context-sensitive parallel evaluation (term)"
(* Basic_1: was just: nf2_sn3 *)
lemma csx_cpre: âh,g,G,L,T1. â¦G, L⦠⢠â¬*[h, g] T1 â âT2. â¦G, L⦠⢠T1 â¡* ðâ¦T2â¦.
#h #g #G #L #T1 #H @(csx_ind ⦠H) -T1
-#T1 #_ #IHT1
-elim (cnr_dec G L T1) /3 width=3/
-* #T #H1T1 #H2T1
-elim (IHT1 ⦠H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/
+#T1 #_ #IHT1 elim (cnr_dec G L T1) /3 width=3 by ex_intro, conj/
+* #T #H1T1 #H2T1 elim (IHT1 ⦠H2T1) -IHT1 -H2T1 /2 width=2 by cpr_cpx/
+#T2 * /4 width=3 by cprs_strap2, ex_intro, conj/
qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index 640f4dbfc..45c8cfe7d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -44,20 +44,20 @@ qed-.
(* Basic_1: was: pr3_pr2 *)
lemma cpr_cprs: âG,L,T1,T2. â¦G, L⦠⢠T1 â¡ T2 â â¦G, L⦠⢠T1 â¡* T2.
-/2 width=1/ qed.
+/2 width=1 by inj/ qed.
(* Basic_1: was: pr3_refl *)
lemma cprs_refl: âG,L,T. â¦G, L⦠⢠T â¡* T.
-/2 width=1/ qed.
+/2 width=1 by cpr_cprs/ qed.
lemma cprs_strap1: âG,L,T1,T,T2.
â¦G, L⦠⢠T1 â¡* T â â¦G, L⦠⢠T â¡ T2 â â¦G, L⦠⢠T1 â¡* T2.
-normalize /2 width=3/ qed.
+normalize /2 width=3 by step/ qed.
(* Basic_1: was: pr3_step *)
lemma cprs_strap2: âG,L,T1,T,T2.
â¦G, L⦠⢠T1 â¡ T â â¦G, L⦠⢠T â¡* T2 â â¦G, L⦠⢠T1 â¡* T2.
-normalize /2 width=3/ qed.
+normalize /2 width=3 by TC_strap/ qed.
lemma lsubr_cprs_trans: âG. lsub_trans ⦠(cprs G) lsubr.
/3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/
@@ -65,51 +65,49 @@ qed-.
(* Basic_1: was: pr3_pr1 *)
lemma tprs_cprs: âG,L,T1,T2. â¦G, â⦠⢠T1 â¡* T2 â â¦G, L⦠⢠T1 â¡* T2.
-#G #L #T1 #T2 #H @(lsubr_cprs_trans ⦠H) -H //
-qed.
+/2 width=3 by lsubr_cprs_trans/ qed.
lemma cprs_bind_dx: âG,L,V1,V2. â¦G, L⦠⢠V1 â¡ V2 â âI,T1,T2. â¦G, L.â{I}V1⦠⢠T1 â¡* T2 â
âa. â¦G, L⦠⢠â{a,I}V1. T1 â¡* â{a,I}V2. T2.
#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx ⦠HT12) -T1
-/3 width=1/ /3 width=3/
-qed.
+/3 width=3 by cprs_strap2, cpr_cprs, cpr_pair_sn, cpr_bind/ qed.
(* Basic_1: was only: pr3_thin_dx *)
lemma cprs_flat_dx: âI,G,L,V1,V2. â¦G, L⦠⢠V1 â¡ V2 â âT1,T2. â¦G, L⦠⢠T1 â¡* T2 â
â¦G, L⦠⢠â{I} V1. T1 â¡* â{I} V2. T2.
-#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind ⦠HT12) -T2 /3 width=1/
-#T #T2 #_ #HT2 #IHT1
-@(cprs_strap1 ⦠IHT1) -V1 -T1 /2 width=1/
+#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind ⦠HT12) -T2
+/3 width=5 by cprs_strap1, cpr_flat, cpr_cprs, cpr_pair_sn/
qed.
lemma cprs_flat_sn: âI,G,L,T1,T2. â¦G, L⦠⢠T1 â¡ T2 â âV1,V2. â¦G, L⦠⢠V1 â¡* V2 â
â¦G, L⦠⢠â{I} V1. T1 â¡* â{I} V2. T2.
-#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind ⦠H) -V2 /3 width=1/
-#V #V2 #_ #HV2 #IHV1
-@(cprs_strap1 ⦠IHV1) -V1 -T1 /2 width=1/
+#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind ⦠H) -V2
+/3 width=3 by cprs_strap1, cpr_cprs, cpr_pair_sn, cpr_flat/
qed.
lemma cprs_zeta: âG,L,V,T1,T,T2. â§[0, 1] T2 â¡ T â
â¦G, L.âV⦠⢠T1 â¡* T â â¦G, L⦠⢠+âV.T1 â¡* T2.
-#G #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx ⦠T1 H) -T1 /3 width=3/
+#G #L #V #T1 #T #T2 #HT2 #H @(cprs_ind_dx ⦠H) -T1
+/3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/
qed.
lemma cprs_tau: âG,L,T1,T2. â¦G, L⦠⢠T1 â¡* T2 â âV. â¦G, L⦠⢠âV.T1 â¡* T2.
-#G #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
+#G #L #T1 #T2 #H @(cprs_ind ⦠H) -T2
+/3 width=3 by cprs_strap1, cpr_cprs, cpr_tau/
qed.
lemma cprs_beta_dx: âa,G,L,V1,V2,W1,W2,T1,T2.
â¦G, L⦠⢠V1 â¡ V2 â â¦G, L⦠⢠W1 â¡ W2 â â¦G, L.âW1⦠⢠T1 â¡* T2 â
â¦G, L⦠⢠âV1.â{a}W1.T1 â¡* â{a}âW2.V2.T2.
-#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2 /3 width=1/
-/4 width=7 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_beta/ (**) (* auto too slow without trace *)
+#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2
+/4 width=7 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_beta/
qed.
lemma cprs_theta_dx: âa,G,L,V1,V,V2,W1,W2,T1,T2.
â¦G, L⦠⢠V1 â¡ V â â§[0, 1] V â¡ V2 â â¦G, L.âW1⦠⢠T1 â¡* T2 â
â¦G, L⦠⢠W1 â¡ W2 â â¦G, L⦠⢠âV1.â{a}W1.T1 â¡* â{a}W2.âV2.T2.
-#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
-/4 width=9 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_theta/ (**) (* auto too slow without trace *)
+#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
+/4 width=9 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_theta/
qed.
(* Basic inversion lemmas ***************************************************)
@@ -125,17 +123,17 @@ qed-.
lemma cprs_inv_cast1: âG,L,W1,T1,U2. â¦G, L⦠⢠âW1.T1 â¡* U2 â â¦G, L⦠⢠T1 â¡* U2 â¨
ââW2,T2. â¦G, L⦠⢠W1 â¡* W2 & â¦G, L⦠⢠T1 â¡* T2 & U2 = âW2.T2.
#G #L #W1 #T1 #U2 #H @(cprs_ind ⦠H) -U2 /3 width=5/
-#U2 #U #_ #HU2 * /3 width=3/ *
+#U2 #U #_ #HU2 * /3 width=3 by cprs_strap1, or_introl/ *
#W #T #HW1 #HT1 #H destruct
-elim (cpr_inv_cast1 ⦠HU2) -HU2 /3 width=3/ *
-#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+elim (cpr_inv_cast1 ⦠HU2) -HU2 /3 width=3 by cprs_strap1, or_introl/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5 by cprs_strap1, ex3_2_intro, or_intror/
qed-.
(* Basic_1: was: nf2_pr3_unfold *)
-lemma cprs_inv_cnr1: âG,L,T,U. â¦G, L⦠⢠T â¡* U â â¦G, L⦠⢠ðâ¦T⦠â T = U.
+lemma cprs_inv_cnr1: âG,L,T,U. â¦G, L⦠⢠T â¡* U â â¦G, L⦠⢠⡠ðâ¦T⦠â T = U.
#G #L #T #U #H @(cprs_ind_dx ⦠H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
-lapply (H2T0 ⦠H1T0) -H1T0 #H destruct /2 width=1/
+lapply (H2T0 ⦠H1T0) -H1T0 #H destruct /2 width=1 by/
qed-.
(* Basic_1: removed theorems 13:
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma
index 3d67c002c..e2975c54a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma
@@ -19,7 +19,7 @@ include "basic_2/computation/csx.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************)
definition cpxe: âh. sd h â relation4 genv lenv term term â
- λh,g,G,L,T1,T2. â¦G, L⦠⢠T1 â¡*[h, g] T2 ⧠â¦G, L⦠⢠ð[h, g]â¦T2â¦.
+ λh,g,G,L,T1,T2. â¦G, L⦠⢠T1 â¡*[h, g] T2 ⧠â¦G, L⦠⢠â¡[h, g] ðâ¦T2â¦.
interpretation "context-sensitive extended parallel evaluation (term)"
'PEval h g G L T1 T2 = (cpxe h g G L T1 T2).
@@ -28,8 +28,7 @@ interpretation "context-sensitive extended parallel evaluation (term)"
lemma csx_cpxe: âh,g,G,L,T1. â¦G, L⦠⢠â¬*[h, g] T1 â âT2. â¦G, L⦠⢠T1 â¡*[h, g] ðâ¦T2â¦.
#h #g #G #L #T1 #H @(csx_ind ⦠H) -T1
-#T1 #_ #IHT1
-elim (cnx_dec h g G L T1) /3 width=3/
-* #T #H1T1 #H2T1
-elim (IHT1 ⦠H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/
+#T1 #_ #IHT1 elim (cnx_dec h g G L T1) /3 width=3 by ex_intro, conj/
+* #T #H1T1 #H2T1 elim (IHT1 ⦠H1T1 H2T1) -IHT1 -H2T1
+#T2 * /4 width=3 by cpxs_strap2, ex_intro, conj/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index a3f8e8316..36ef1b2a1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
@@ -152,7 +152,7 @@ lapply (cpxs_strap1 ⦠HW1 ⦠HW2) -W
lapply (cpxs_strap1 ⦠HT1 ⦠HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/
qed-.
-lemma cpxs_inv_cnx1: âh,g,G,L,T,U. â¦G, L⦠⢠T â¡*[h, g] U â â¦G, L⦠⢠ð[h, g]â¦T⦠â T = U.
+lemma cpxs_inv_cnx1: âh,g,G,L,T,U. â¦G, L⦠⢠T â¡*[h, g] U â â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â T = U.
#h #g #G #L #T #U #H @(cpxs_ind_dx ⦠H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 ⦠H1T0) -H1T0 #H destruct /2 width=1 by/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma
deleted file mode 100644
index 2b4eadd6e..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma
+++ /dev/null
@@ -1,57 +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/substitution/cpys_cpys.ma".
-include "basic_2/reduction/cpx_cpys.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Main properties **********************************************************)
-
-axiom cpys_split_down: âG,L,T1,T2,d,e. â¦G, L⦠⢠T1 â¶*Ã[d, e] T2 â
- âi. d ⤠i â i ⤠d + e â
- ââT. â¦G, L⦠⢠T1 â¶*Ã[i, d+e-i] T & â¦G, L⦠⢠T â¶*Ã[d, i-d] T2.
-
-lemma cpys_tpxs_trans: âh,g,G,L,T1,T,d,e. â¦G, L⦠⢠T1 â¶*Ã[d, e] T â
- âT2. â¦G, â⦠⢠T â¡*[h, g] T2 â â¦G, L⦠⢠T1 â¡*[h, g] T2.
-#h #g #G #L #T1 #T #d #e #HT1 #T2 #H @(cpxs_ind ⦠H) -T2
-/3 width=5 by cpxs_strap1, cpys_cpx, lsubr_cpx_trans, cpx_cpxs/
-qed-.
-
-lemma cpx_fwd_cpys_tpxs: âh,g,G,L,T1,T2. â¦G, L⦠⢠T1 â¡[h, g] T2 â
- ââT. â¦G, L⦠⢠T1 â¶*Ã[0, â] T & â¦G, â⦠⢠T â¡*[h, g] T2.
-#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
-[ /2 width=3 by ex2_intro/
-| /4 width=3 by cpx_cpxs, cpx_sort, ex2_intro/
-| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 * #V #HV1 #HV2
- elim (lift_total V 0 (i+1)) #W #HVW
- lapply (cpxs_lift ⦠HV2 (â) (â) ⦠HVW ⦠HVW2)
- [ @ldrop_atom #H destruct | /3 width=7 by cpys_subst_Y2, ex2_intro/ ]
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * #T #HT1 #HT2
- @(ex2_intro ⦠(â{a,I}V1.T))
- [ @cpys_bind //
- | @cpxs_bind //
-
- elim (cpys_split_down ⦠HT1 1) -HT1 // #T0 #HT10 #HT0
- @(ex2_intro ⦠(â{a,I}V.T0))
- [ @cpys_bind //
- | @(cpxs_trans ⦠(â{a,I}V.T)) @cpxs_bind // -HT10
-
-
-(*
- lapply (lsuby_cpys_trans ⦠HT10 (L.â{I}V) ?) -HT10 /2 width=1 by lsuby_succ/ #HT10
-*)
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 *
- /3 width=5 by cpys_flat, cpxs_flat, ex2_intro/
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index ec36d47f1..eed76daea 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -19,7 +19,7 @@ include "basic_2/computation/lpxs_cpxs.ma".
(* Forward lemmas involving same top term constructor ***********************)
-lemma cpxs_fwd_cnx: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â âU. â¦G, L⦠⢠T â¡*[h, g] U â T â U.
+lemma cpxs_fwd_cnx: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â âU. â¦G, L⦠⢠T â¡*[h, g] U â T â U.
#h #g #G #L #T #HT #U #H
>(cpxs_inv_cnx1 ⦠H HT) -G -L -T //
qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
index 08cf4d2cd..41bd98df3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
@@ -21,7 +21,7 @@ include "basic_2/computation/cpxs_tstc.ma".
(* Vector form of forward lemmas involving same top term constructor ********)
(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: âh,g,G,L,T. ðâ¦T⦠â â¦G, L⦠⢠ð[h, g]â¦T⦠â
+lemma cpxs_fwd_cnx_vector: âh,g,G,L,T. ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â
âVs,U. â¦G, L⦠⢠â¶Vs.T â¡*[h, g] U â â¶Vs.T â U.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx ⦠H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
#V #Vs #IHVs #U #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
index 6d55772c4..cd28a524b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
@@ -51,7 +51,7 @@ elim (eq_term_dec T1 T2) #HT12 destruct /3 width=4 by/
qed-.
(* Basic_1: was just: sn3_nf2 *)
-lemma cnx_csx: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠â¬*[h, g] T.
+lemma cnx_csx: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠â¬*[h, g] T.
/2 width=1 by NF_to_SN/ qed.
lemma csx_sort: âh,g,G,L,k. â¦G, L⦠⢠â¬*[h, g] âk.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
index 21431dc3b..5e9ea06c7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
@@ -22,7 +22,7 @@ include "basic_2/computation/csx_vector.ma".
(* Advanced properties ******************************************************)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: âh,g,G,L,T. ðâ¦T⦠â â¦G, L⦠⢠ð[h, g]â¦T⦠â
+lemma csx_applv_cnx: âh,g,G,L,T. ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â
âVs. â¦G, L⦠⢠â¬*[h, g] Vs â â¦G, L⦠⢠â¬*[h, g] â¶Vs.T.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx ⦠H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
index 730604ddb..a78d6c70d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
@@ -23,11 +23,25 @@ include "basic_2/computation/lpxs_cpxs.ma".
fact le_repl_sn_aux: âx,y,z:nat. x ⤠z â x = y â y ⤠z.
// qed-.
-fact pippo_aux: âh,g,G,L1,T,T1,d,e. â¦G, L1⦠⢠T â¶Ã[d, e] T1 â e = â â
+axiom cpxs_cpys_conf_lpxs: âh,g,G,d,e.
+ âL0,T0,T1. â¦G, L0⦠⢠T0 â¡*[h, g] T1 â
+ âT2. â¦G, L0⦠⢠T0 â¶*Ã[d, e] T2 â
+ âL1. â¦G, L0⦠⢠â¡*[h, g] L1 â
+ ââT. â¦G, L1⦠⢠T1 â¶*Ã[d, e] T & â¦G, L0⦠⢠T2 â¡*[h, g] T.
+
+axiom cpxs_conf_lpxs_lpys: âh,g,G,d,e.
+ âI,L0,V0,T0,T1. â¦G, L0.â{I}V0⦠⢠T0 â¡*[h, g] T1 â
+ âL1. â¦G, L0⦠⢠â¡*[h, g] L1 â âV2. â¦G, L0⦠⢠V0 â¶*Ã[d, e] V2 â
+ ââT. â¦G, L1.â{I}V0⦠⢠T1 â¶*Ã[⫯d, e] T & â¦G, L0.â{I}V2⦠⢠T0 â¡*[h, g] T.
+
+
+include "basic_2/reduction/cpx_cpys.ma".
+
+fact pippo_aux: âh,g,G,L1,T,T1,d,e. â¦G, L1⦠⢠T â¶*Ã[d, e] T1 â e = â â
âL2. â¦G, L1⦠⢠â¡*[h, g] L2 â
- ââT2. â¦G, L2⦠⢠T â¶Ã[d, e] T2 & â¦G, L1⦠⢠T1 â¡*[h, g] T2 &
+ ââT2. â¦G, L2⦠⢠T â¶*Ã[d, e] T2 & â¦G, L1⦠⢠T1 â¡*[h, g] T2 &
L1 â[T, d] L2 â T1 = T2.
-#h #g #G #L1 #T #T1 #d #e #H elim H -G -L1 -T -T1 -d -e [ * ]
+#h #g #G #L1 #T #T1 #d #e #H @(cpys_ind_alt ⦠H) -G -L1 -T -T1 -d -e [ * ]
[ /5 width=5 by lpxs_fwd_length, lleq_sort, ex3_intro, conj/
| #i #G #L1 elim (lt_or_ge i (|L1|)) [2: /6 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux, ex3_intro, conj/ ]
#Hi #d elim (ylt_split i d) [ /5 width=5 by lpxs_fwd_length, lleq_skip, ex3_intro, conj/ ]
@@ -36,19 +50,42 @@ fact pippo_aux: âh,g,G,L1,T,T1,d,e. â¦G, L1⦠⢠T â¶Ã[d, e] T1 â e =
elim (lpxs_ldrop_conf ⦠HLK1 ⦠HL12) -HL12 #X #H #HLK2
elim (lpxs_inv_pair1 ⦠H) -H #K2 #V2 #HK12 #HV12 #H destruct
elim (lift_total V2 0 (i+1)) #W2 #HVW2
- @(ex3_intro ⦠W2) /2 width=7 by cpxs_delta, cpy_subst/ -I -K1 -V1 -Hdi
+ @(ex3_intro ⦠W2) /2 width=7 by cpxs_delta, cpys_subst/ -I -K1 -V1 -Hdi
@conj #H [ elim HnL12 // | destruct elim (lift_inv_lref2_be ⦠HVW2) // ]
| /5 width=5 by lpxs_fwd_length, lleq_gref, ex3_intro, conj/
-| #I #G #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #He #L2 #HL12 destruct
+| #I #G #L1 #K1 #V #V1 #T1 #i #d #e #Hdi #Hide #HLK1 #HV1 #HVT1 #_ #He #L2 #HL12 destruct
elim (lpxs_ldrop_conf ⦠HLK1 ⦠HL12) -HL12 #X #H #HLK2
- elim (lpxs_inv_pair1 ⦠H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ elim (lpxs_inv_pair1 ⦠H) -H #K2 #W #HK12 #HVW #H destruct
+ elim (cpxs_cpys_conf_lpxs ⦠HVW ⦠HV1 ⦠HK12) -HVW -HV1 -HK12 #W1 #HW1 #VW1
+ elim (lift_total W1 0 (i+1)) #U1 #HWU1
lapply (ldrop_fwd_drop2 ⦠HLK1) -HLK1 #HLK1
- elim (lift_total V2 0 (i+1)) #W2 #HVW2
- @(ex3_intro ⦠W2) /2 width=10 by cpxs_lift, cpy_subst/
+ @(ex3_intro ⦠U1) /2 width=10 by cpxs_lift, cpys_subst/
+| #a #I #G #L #V #V1 #T #T1 #d #e #HV1 #_ #IHV1 #IHT1 #He #L2 #HL12
+ elim (IHV1 ⦠HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V
+ elim (IHT1 ⦠(L2.â{I}V2)) /4 width=3 by lpxs_cpx_trans, lpxs_pair, cpys_cpx/ -IHT1 -He #T2 #HT2 #HT12 * #H1T #H2T
+ elim (cpxs_conf_lpxs_lpys ⦠HT12 ⦠HL12 ⦠HV1) -HT12 -HL12 -HV1 #T0 #HT20 #HT10
+ @(ex3_intro ⦠(â{a,I}V2.T0))
+ [ @cpys_bind // @(cpys_trans_eq ⦠T2) /3 width=5 by lsuby_cpys_trans, lsuby_succ/
+ | /2 width=1 by cpxs_bind/
+ | @conj #H destruct
+ [ elim (lleq_inv_bind ⦠H) -H #HV #HT >H1V -H1V //
+ | @lleq_bind /2 width=1/
+
+
+ /3 width=5 by lsuby_cpys_trans, lsuby_succ/
+| #I #G #L #V #V1 #T #T1 #d #e #HV1 #HT1 #IHV1 #IHT1 #He #L2 #HL12
+ elim (IHV1 ⦠HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V
+ elim (IHT1 ⦠HL12) // -IHT1 #T2 #HT2 #HT12 * #H1T #H2T -He -HL12
+ @(ex3_intro ⦠(â{I}V2.T2)) /2 width=1 by cpxs_flat, cpys_flat/
+ @conj #H destruct [2: /3 width=1 by lleq_flat/ ]
+ elim (lleq_inv_flat ⦠H) -H /3 width=1 by eq_f2/
+]
+
- elim (lleq_dec (#i) L1 L2 d)
-
+ [
+ | @cpxs_bind //
+ @(lpx_cpxs_trans ⦠HT12)
|
]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma
index c720a11c0..e94aea008 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma
@@ -14,6 +14,6 @@
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦠term 46 G , break term 46 L ⦠⢠ð break ⦠term 46 T ⦠)"
+notation "hvbox( ⦠term 46 G , break term 46 L ⦠⢠⡠ð break ⦠term 46 T ⦠)"
non associative with precedence 45
for @{ 'Normal $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma
index 56ae56448..20844ce63 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma
@@ -14,6 +14,6 @@
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦠term 46 G, break term 46 L ⦠⢠ð break [ term 46 h , break term 46 g ] break ⦠term 46 T ⦠)"
+notation "hvbox( ⦠term 46 G, break term 46 L ⦠⢠⡠break [ term 46 h , break term 46 g ] ð break ⦠term 46 T ⦠)"
non associative with precedence 45
for @{ 'Normal $h $g $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma
index 627be72ac..4cebc3027 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma
@@ -14,6 +14,6 @@
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦠term 46 G , break term 46 L ⦠⢠ð break ⦠term 46 T ⦠)"
+notation "hvbox( ⦠term 46 G , break term 46 L ⦠⢠⡠ð break ⦠term 46 T ⦠)"
non associative with precedence 45
for @{ 'NotReducible $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma
index ad1d1187f..4a4e3f3a9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma
@@ -14,6 +14,6 @@
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦠term 46 G, break term 46 L ⦠⢠ð break [ term 46 h , break term 46 g ] break ⦠term 46 T ⦠)"
+notation "hvbox( ⦠term 46 G, break term 46 L ⦠⢠⡠break [ term 46 h , break term 46 g ] ð break ⦠term 46 T ⦠)"
non associative with precedence 45
for @{ 'NotReducible $h $g $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma
index c8473ccc3..d1b688b8c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma
@@ -14,6 +14,6 @@
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦠term 46 G , break term 46 L ⦠⢠ð break ⦠term 46 T ⦠)"
+notation "hvbox( ⦠term 46 G , break term 46 L ⦠⢠⡠ð break ⦠term 46 T ⦠)"
non associative with precedence 45
for @{ 'Reducible $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma
index ac8033449..c63231648 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma
@@ -14,6 +14,6 @@
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦠term 46 G, break term 46 L ⦠⢠ð break [ term 46 h , break term 46 g ] break ⦠term 46 T ⦠)"
+notation "hvbox( ⦠term 46 G, break term 46 L ⦠⢠⡠break [ term 46 h , break term 46 g ] ð break ⦠term 46 T ⦠)"
non associative with precedence 45
for @{ 'Reducible $h $g $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
index 35a28700a..a8a5bcc9c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
@@ -17,39 +17,39 @@ include "basic_2/reduction/crr.ma".
(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
-definition cir: relation3 genv lenv term â λG,L,T. â¦G, L⦠⢠ðâ¦T⦠â â¥.
+definition cir: relation3 genv lenv term â λG,L,T. â¦G, L⦠⢠⡠ðâ¦T⦠â â¥.
interpretation "context-sensitive irreducibility (term)"
'NotReducible G L T = (cir G L T).
(* Basic inversion lemmas ***************************************************)
-lemma cir_inv_delta: âG,L,K,V,i. â©[i] L â¡ K.âV â â¦G, L⦠⢠ðâ¦#i⦠â â¥.
+lemma cir_inv_delta: âG,L,K,V,i. â©[i] L â¡ K.âV â â¦G, L⦠⢠⡠ðâ¦#i⦠â â¥.
/3 width=3 by crr_delta/ qed-.
-lemma cir_inv_ri2: âI,G,L,V,T. ri2 I â â¦G, L⦠⢠ðâ¦â¡{I}V.T⦠â â¥.
+lemma cir_inv_ri2: âI,G,L,V,T. ri2 I â â¦G, L⦠⢠⡠ðâ¦â¡{I}V.T⦠â â¥.
/3 width=1 by crr_ri2/ qed-.
-lemma cir_inv_ib2: âa,I,G,L,V,T. ib2 a I â â¦G, L⦠⢠ðâ¦â{a,I}V.T⦠â
- â¦G, L⦠⢠ðâ¦V⦠⧠â¦G, L.â{I}V⦠⢠ðâ¦Tâ¦.
+lemma cir_inv_ib2: âa,I,G,L,V,T. ib2 a I â â¦G, L⦠⢠⡠ðâ¦â{a,I}V.T⦠â
+ â¦G, L⦠⢠⡠ðâ¦V⦠⧠â¦G, L.â{I}V⦠⢠⡠ðâ¦Tâ¦.
/4 width=1 by crr_ib2_sn, crr_ib2_dx, conj/ qed-.
-lemma cir_inv_bind: âa,I,G,L,V,T. â¦G, L⦠⢠ðâ¦â{a,I}V.T⦠â
- â§â§ â¦G, L⦠⢠ðâ¦V⦠& â¦G, L.â{I}V⦠⢠ðâ¦T⦠& ib2 a I.
+lemma cir_inv_bind: âa,I,G,L,V,T. â¦G, L⦠⢠⡠ðâ¦â{a,I}V.T⦠â
+ â§â§ â¦G, L⦠⢠⡠ðâ¦V⦠& â¦G, L.â{I}V⦠⢠⡠ðâ¦T⦠& ib2 a I.
#a * [ elim a -a ]
#G #L #V #T #H [ elim H -H /3 width=1 by crr_ri2, or_introl/ ]
elim (cir_inv_ib2 ⦠H) -H /3 width=1 by and3_intro, or_introl/
qed-.
-lemma cir_inv_appl: âG,L,V,T. â¦G, L⦠⢠ðâ¦âV.T⦠â
- â§â§ â¦G, L⦠⢠ðâ¦V⦠& â¦G, L⦠⢠ðâ¦T⦠& ðâ¦Tâ¦.
+lemma cir_inv_appl: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦âV.T⦠â
+ â§â§ â¦G, L⦠⢠⡠ðâ¦V⦠& â¦G, L⦠⢠⡠ðâ¦T⦠& ðâ¦Tâ¦.
#G #L #V #T #HVT @and3_intro /3 width=1/
generalize in match HVT; -HVT elim T -T //
* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/
qed-.
-lemma cir_inv_flat: âI,G,L,V,T. â¦G, L⦠⢠ðâ¦â{I}V.T⦠â
- â§â§ â¦G, L⦠⢠ðâ¦V⦠& â¦G, L⦠⢠ðâ¦T⦠& ðâ¦T⦠& I = Appl.
+lemma cir_inv_flat: âI,G,L,V,T. â¦G, L⦠⢠⡠ðâ¦â{I}V.T⦠â
+ â§â§ â¦G, L⦠⢠⡠ðâ¦V⦠& â¦G, L⦠⢠⡠ðâ¦T⦠& ðâ¦T⦠& I = Appl.
* #G #L #V #T #H
[ elim (cir_inv_appl ⦠H) -H /2 width=1 by and4_intro/
| elim (cir_inv_ri2 ⦠H) -H //
@@ -58,22 +58,22 @@ qed-.
(* Basic properties *********************************************************)
-lemma cir_sort: âG,L,k. â¦G, L⦠⢠ðâ¦âkâ¦.
+lemma cir_sort: âG,L,k. â¦G, L⦠⢠⡠ðâ¦âkâ¦.
/2 width=4 by crr_inv_sort/ qed.
-lemma cir_gref: âG,L,p. â¦G, L⦠⢠ðâ¦Â§pâ¦.
+lemma cir_gref: âG,L,p. â¦G, L⦠⢠⡠ðâ¦Â§pâ¦.
/2 width=4 by crr_inv_gref/ qed.
-lemma tir_atom: âG,I. â¦G, â⦠⢠ðâ¦âª{I}â¦.
+lemma tir_atom: âG,I. â¦G, â⦠⢠⡠ðâ¦âª{I}â¦.
/2 width=3 by trr_inv_atom/ qed.
lemma cir_ib2: âa,I,G,L,V,T.
- ib2 a I â â¦G, L⦠⢠ðâ¦V⦠â â¦G, L.â{I}V⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦â{a,I}V.Tâ¦.
+ ib2 a I â â¦G, L⦠⢠⡠ðâ¦V⦠â â¦G, L.â{I}V⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦â{a,I}V.Tâ¦.
#a #I #G #L #V #T #HI #HV #HT #H
elim (crr_inv_ib2 ⦠HI H) -HI -H /2 width=1 by/
qed.
-lemma cir_appl: âG,L,V,T. â¦G, L⦠⢠ðâ¦V⦠â â¦G, L⦠⢠ðâ¦T⦠â ðâ¦T⦠â â¦G, L⦠⢠ðâ¦âV.Tâ¦.
+lemma cir_appl: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦V⦠â â¦G, L⦠⢠⡠ðâ¦T⦠â ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦âV.Tâ¦.
#G #L #V #T #HV #HT #H1 #H2
elim (crr_inv_appl ⦠H2) -H2 /2 width=1 by/
qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
index bf68aedee..2f0461191 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
@@ -19,16 +19,16 @@ include "basic_2/reduction/cir.ma".
(* Advanved properties ******************************************************)
-lemma cir_labst_last: âG,L,T,W. â¦G, L⦠⢠ðâ¦T⦠â â¦G, â.âW @@ L⦠⢠ðâ¦Tâ¦.
+lemma cir_labst_last: âG,L,T,W. â¦G, L⦠⢠⡠ðâ¦T⦠â â¦G, â.âW @@ L⦠⢠⡠ðâ¦Tâ¦.
/3 width=2 by crr_inv_labst_last/ qed.
-lemma cir_tif: âG,T,W. â¦G, â⦠⢠ðâ¦T⦠â â¦G, â.âW⦠⢠ðâ¦Tâ¦.
+lemma cir_tif: âG,T,W. â¦G, â⦠⢠⡠ðâ¦T⦠â â¦G, â.âW⦠⢠⡠ðâ¦Tâ¦.
/3 width=2 by crr_inv_trr/ qed.
(* Advanced inversion lemmas ************************************************)
-lemma cir_inv_append_sn: âG,L,K,T. â¦G, K @@ L⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦Tâ¦.
+lemma cir_inv_append_sn: âG,L,K,T. â¦G, K @@ L⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
/3 width=1/ qed-.
-lemma cir_inv_tir: âG,T,W. â¦G, â.âW⦠⢠ðâ¦T⦠â â¦G, â⦠⢠ðâ¦Tâ¦.
+lemma cir_inv_tir: âG,T,W. â¦G, â.âW⦠⢠⡠ðâ¦T⦠â â¦G, â⦠⢠⡠ðâ¦Tâ¦.
/3 width=1/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
index 0c518239a..0cea0de9c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
@@ -19,10 +19,10 @@ include "basic_2/reduction/cir.ma".
(* Properties on relocation *************************************************)
-lemma cir_lift: âG,K,T. â¦G, K⦠⢠ðâ¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
- âU. â§[d, e] T â¡ U â â¦G, L⦠⢠ðâ¦Uâ¦.
+lemma cir_lift: âG,K,T. â¦G, K⦠⢠⡠ðâ¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
+ âU. â§[d, e] T â¡ U â â¦G, L⦠⢠⡠ðâ¦Uâ¦.
/3 width=8 by crr_inv_lift/ qed.
-lemma cir_inv_lift: âG,L,U. â¦G, L⦠⢠ðâ¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
- âT. â§[d, e] T â¡ U â â¦G, K⦠⢠ðâ¦Tâ¦.
+lemma cir_inv_lift: âG,L,U. â¦G, L⦠⢠⡠ðâ¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
+ âT. â§[d, e] T â¡ U â â¦G, K⦠⢠⡠ðâ¦Tâ¦.
/3 width=8 by crr_lift/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
index d7da41971..ad3c60831 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
@@ -19,42 +19,42 @@ include "basic_2/reduction/crx.ma".
(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************)
definition cix: âh. sd h â relation3 genv lenv term â
- λh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¥.
+ λh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¥.
interpretation "context-sensitive extended irreducibility (term)"
'NotReducible h g G L T = (cix h g G L T).
(* Basic inversion lemmas ***************************************************)
-lemma cix_inv_sort: âh,g,G,L,k,l. deg h g k (l+1) â â¦G, L⦠⢠ð[h, g]â¦âk⦠â â¥.
+lemma cix_inv_sort: âh,g,G,L,k,l. deg h g k (l+1) â â¦G, L⦠⢠â¡[h, g] ðâ¦âk⦠â â¥.
/3 width=2 by crx_sort/ qed-.
-lemma cix_inv_delta: âh,g,I,G,L,K,V,i. â©[i] L â¡ K.â{I}V â â¦G, L⦠⢠ð[h, g]â¦#i⦠â â¥.
+lemma cix_inv_delta: âh,g,I,G,L,K,V,i. â©[i] L â¡ K.â{I}V â â¦G, L⦠⢠â¡[h, g] ðâ¦#i⦠â â¥.
/3 width=4 by crx_delta/ qed-.
-lemma cix_inv_ri2: âh,g,I,G,L,V,T. ri2 I â â¦G, L⦠⢠ð[h, g]â¦â¡{I}V.T⦠â â¥.
+lemma cix_inv_ri2: âh,g,I,G,L,V,T. ri2 I â â¦G, L⦠⢠â¡[h, g] ðâ¦â¡{I}V.T⦠â â¥.
/3 width=1 by crx_ri2/ qed-.
-lemma cix_inv_ib2: âh,g,a,I,G,L,V,T. ib2 a I â â¦G, L⦠⢠ð[h, g]â¦â{a,I}V.T⦠â
- â¦G, L⦠⢠ð[h, g]â¦V⦠⧠â¦G, L.â{I}V⦠⢠ð[h, g]â¦Tâ¦.
+lemma cix_inv_ib2: âh,g,a,I,G,L,V,T. ib2 a I â â¦G, L⦠⢠â¡[h, g] ðâ¦â{a,I}V.T⦠â
+ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠⧠â¦G, L.â{I}V⦠⢠â¡[h, g] ðâ¦Tâ¦.
/4 width=1 by crx_ib2_sn, crx_ib2_dx, conj/ qed-.
-lemma cix_inv_bind: âh,g,a,I,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦â{a,I}V.T⦠â
- â§â§ â¦G, L⦠⢠ð[h, g]â¦V⦠& â¦G, L.â{I}V⦠⢠ð[h, g]â¦T⦠& ib2 a I.
+lemma cix_inv_bind: âh,g,a,I,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦â{a,I}V.T⦠â
+ â§â§ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠& â¦G, L.â{I}V⦠⢠â¡[h, g] ðâ¦T⦠& ib2 a I.
#h #g #a * [ elim a -a ]
#G #L #V #T #H [ elim H -H /3 width=1 by crx_ri2, or_introl/ ]
elim (cix_inv_ib2 ⦠H) -H /3 width=1 by and3_intro, or_introl/
qed-.
-lemma cix_inv_appl: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦âV.T⦠â
- â§â§ â¦G, L⦠⢠ð[h, g]â¦V⦠& â¦G, L⦠⢠ð[h, g]â¦T⦠& ðâ¦Tâ¦.
-#h #g #G #L #V #T #HVT @and3_intro /3 width=1/
+lemma cix_inv_appl: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦âV.T⦠â
+ â§â§ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠& â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠& ðâ¦Tâ¦.
+#h #g #G #L #V #T #HVT @and3_intro /3 width=1 by crx_appl_sn, crx_appl_dx/
generalize in match HVT; -HVT elim T -T //
* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crx_beta, crx_theta/
qed-.
-lemma cix_inv_flat: âh,g,I,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦â{I}V.T⦠â
- â§â§ â¦G, L⦠⢠ð[h, g]â¦V⦠& â¦G, L⦠⢠ð[h, g]â¦T⦠& ðâ¦T⦠& I = Appl.
+lemma cix_inv_flat: âh,g,I,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦â{I}V.T⦠â
+ â§â§ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠& â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠& ðâ¦T⦠& I = Appl.
#h #g * #G #L #V #T #H
[ elim (cix_inv_appl ⦠H) -H /2 width=1 by and4_intro/
| elim (cix_inv_ri2 ⦠H) -H //
@@ -63,31 +63,31 @@ qed-.
(* Basic forward lemmas *****************************************************)
-lemma cix_inv_cir: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠ðâ¦Tâ¦.
+lemma cix_inv_cir: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
/3 width=1 by crr_crx/ qed-.
(* Basic properties *********************************************************)
-lemma cix_sort: âh,g,G,L,k. deg h g k 0 â â¦G, L⦠⢠ð[h, g]â¦âkâ¦.
+lemma cix_sort: âh,g,G,L,k. deg h g k 0 â â¦G, L⦠⢠â¡[h, g] ðâ¦âkâ¦.
#h #g #G #L #k #Hk #H elim (crx_inv_sort ⦠H) -L #l #Hkl
lapply (deg_mono ⦠Hk Hkl) -h -k <plus_n_Sm #H destruct
qed.
-lemma tix_lref: âh,g,G,i. â¦G, â⦠⢠ð[h, g]â¦#iâ¦.
+lemma tix_lref: âh,g,G,i. â¦G, â⦠⢠â¡[h, g] ðâ¦#iâ¦.
#h #g #G #i #H elim (trx_inv_atom ⦠H) -H #k #l #_ #H destruct
qed.
-lemma cix_gref: âh,g,G,L,p. â¦G, L⦠⢠ð[h, g]â¦Â§pâ¦.
+lemma cix_gref: âh,g,G,L,p. â¦G, L⦠⢠â¡[h, g] ðâ¦Â§pâ¦.
#h #g #G #L #p #H elim (crx_inv_gref ⦠H)
qed.
-lemma cix_ib2: âh,g,a,I,G,L,V,T. ib2 a I â â¦G, L⦠⢠ð[h, g]â¦V⦠â â¦G, L.â{I}V⦠⢠ð[h, g]â¦T⦠â
- â¦G, L⦠⢠ð[h, g]â¦â{a,I}V.Tâ¦.
+lemma cix_ib2: âh,g,a,I,G,L,V,T. ib2 a I â â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠â â¦G, L.â{I}V⦠⢠â¡[h, g] ðâ¦T⦠â
+ â¦G, L⦠⢠â¡[h, g] ðâ¦â{a,I}V.Tâ¦.
#h #g #a #I #G #L #V #T #HI #HV #HT #H
elim (crx_inv_ib2 ⦠HI H) -HI -H /2 width=1 by/
qed.
-lemma cix_appl: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦V⦠â â¦G, L⦠⢠ð[h, g]â¦T⦠â ðâ¦T⦠â â¦G, L⦠⢠ð[h, g]â¦âV.Tâ¦.
+lemma cix_appl: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦âV.Tâ¦.
#h #g #G #L #V #T #HV #HT #H1 #H2
elim (crx_inv_appl ⦠H2) -H2 /2 width=1 by/
qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma
index 7702f384f..ba1eb8b2a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma
@@ -19,8 +19,8 @@ include "basic_2/reduction/cix.ma".
(* Advanced inversion lemmas ************************************************)
-lemma cix_inv_append_sn: âh,g,G,L,K,T. â¦G, K @@ L⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠ð[h, g]â¦Tâ¦.
-/3 width=1/ qed-.
+lemma cix_inv_append_sn: âh,g,G,L,K,T. â¦G, K @@ L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦Tâ¦.
+/3 width=1 by crx_append_sn/ qed-.
-lemma cix_inv_tix: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, â⦠⢠ð[h, g]â¦Tâ¦.
-/3 width=1/ qed-.
+lemma cix_inv_tix: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, â⦠⢠â¡[h, g] ðâ¦Tâ¦.
+/3 width=1 by trx_crx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
index 72d5dbaac..64a17731b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
@@ -19,17 +19,17 @@ include "basic_2/reduction/cix.ma".
(* Advanced properties ******************************************************)
-lemma cix_lref: âh,g,G,L,i. â©[i] L â¡ â â â¦G, L⦠⢠ð[h, g]â¦#iâ¦.
+lemma cix_lref: âh,g,G,L,i. â©[i] L â¡ â â â¦G, L⦠⢠â¡[h, g] ðâ¦#iâ¦.
#h #g #G #L #i #HL #H elim (crx_inv_lref ⦠H) -h #I #K #V #HLK
lapply (ldrop_mono ⦠HLK ⦠HL) -L -i #H destruct
qed.
(* Properties on relocation *************************************************)
-lemma cix_lift: âh,g,G,K,T. â¦G, K⦠⢠ð[h, g]â¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
- âU. â§[d, e] T â¡ U â â¦G, L⦠⢠ð[h, g]â¦Uâ¦.
+lemma cix_lift: âh,g,G,K,T. â¦G, K⦠⢠â¡[h, g] ðâ¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
+ âU. â§[d, e] T â¡ U â â¦G, L⦠⢠â¡[h, g] ðâ¦Uâ¦.
/3 width=8 by crx_inv_lift/ qed.
-lemma cix_inv_lift: âh,g,G,L,U. â¦G, L⦠⢠ð[h, g]â¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
- âT. â§[d, e] T â¡ U â â¦G, K⦠⢠ð[h, g]â¦Tâ¦.
+lemma cix_inv_lift: âh,g,G,L,U. â¦G, L⦠⢠â¡[h, g] ðâ¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
+ âT. â§[d, e] T â¡ U â â¦G, K⦠⢠â¡[h, g] ðâ¦Tâ¦.
/3 width=8 by crx_lift/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
index 34d95faae..26bb268ee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
@@ -25,28 +25,28 @@ interpretation
(* Basic inversion lemmas ***************************************************)
-lemma cnr_inv_delta: âG,L,K,V,i. â©[i] L â¡ K.âV â â¦G, L⦠⢠ðâ¦#i⦠â â¥.
+lemma cnr_inv_delta: âG,L,K,V,i. â©[i] L â¡ K.âV â â¦G, L⦠⢠⡠ðâ¦#i⦠â â¥.
#G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct
elim (lift_inv_lref2_be ⦠HVW) -HVW //
qed-.
-lemma cnr_inv_abst: âa,G,L,V,T. â¦G, L⦠⢠ðâ¦â{a}V.T⦠â â¦G, L⦠⢠ðâ¦V⦠⧠â¦G, L.âV⦠⢠ðâ¦Tâ¦.
+lemma cnr_inv_abst: âa,G,L,V,T. â¦G, L⦠⢠⡠ðâ¦â{a}V.T⦠â â¦G, L⦠⢠⡠ðâ¦V⦠⧠â¦G, L.âV⦠⢠⡠ðâ¦Tâ¦.
#a #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (â{a}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (â{a}V1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnr_inv_abbr: âG,L,V,T. â¦G, L⦠⢠ðâ¦-âV.T⦠â â¦G, L⦠⢠ðâ¦V⦠⧠â¦G, L.âV⦠⢠ðâ¦Tâ¦.
+lemma cnr_inv_abbr: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦-âV.T⦠â â¦G, L⦠⢠⡠ðâ¦V⦠⧠â¦G, L.âV⦠⢠⡠ðâ¦Tâ¦.
#G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (-âV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (-âV1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnr_inv_zeta: âG,L,V,T. â¦G, L⦠⢠ðâ¦+âV.T⦠â â¥.
+lemma cnr_inv_zeta: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦+âV.T⦠â â¥.
#G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3 by cpr_zeta/ #H destruct
@@ -58,7 +58,7 @@ lemma cnr_inv_zeta: âG,L,V,T. â¦G, L⦠⢠ðâ¦+âV.T⦠â â¥.
]
qed-.
-lemma cnr_inv_appl: âG,L,V,T. â¦G, L⦠⢠ðâ¦âV.T⦠â â§â§ â¦G, L⦠⢠ðâ¦V⦠& â¦G, L⦠⢠ðâ¦T⦠& ðâ¦Tâ¦.
+lemma cnr_inv_appl: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦âV.T⦠â â§â§ â¦G, L⦠⢠⡠ðâ¦V⦠& â¦G, L⦠⢠⡠ðâ¦T⦠& ðâ¦Tâ¦.
#G #L #V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (âV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (âV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct //
@@ -69,7 +69,7 @@ lemma cnr_inv_appl: âG,L,V,T. â¦G, L⦠⢠ðâ¦âV.T⦠â â§â§ â¦G,
]
qed-.
-lemma cnr_inv_tau: âG,L,V,T. â¦G, L⦠⢠ðâ¦âV.T⦠â â¥.
+lemma cnr_inv_tau: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦âV.T⦠â â¥.
#G #L #V #T #H lapply (H T ?) -H
/2 width=4 by cpr_tau, discr_tpair_xy_y/
qed-.
@@ -77,27 +77,27 @@ qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: nf2_sort *)
-lemma cnr_sort: âG,L,k. â¦G, L⦠⢠ðâ¦âkâ¦.
+lemma cnr_sort: âG,L,k. â¦G, L⦠⢠⡠ðâ¦âkâ¦.
#G #L #k #X #H
>(cpr_inv_sort1 ⦠H) //
qed.
(* Basic_1: was: nf2_abst *)
-lemma cnr_abst: âa,G,L,W,T. â¦G, L⦠⢠ðâ¦W⦠â â¦G, L.âW⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦â{a}W.Tâ¦.
+lemma cnr_abst: âa,G,L,W,T. â¦G, L⦠⢠⡠ðâ¦W⦠â â¦G, L.âW⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦â{a}W.Tâ¦.
#a #G #L #W #T #HW #HT #X #H
elim (cpr_inv_abst1 ⦠H) -H #W0 #T0 #HW0 #HT0 #H destruct
>(HW ⦠HW0) -W0 >(HT ⦠HT0) -T0 //
qed.
(* Basic_1: was only: nf2_appl_lref *)
-lemma cnr_appl_simple: âG,L,V,T. â¦G, L⦠⢠ðâ¦V⦠â â¦G, L⦠⢠ðâ¦T⦠â ðâ¦T⦠â â¦G, L⦠⢠ðâ¦âV.Tâ¦.
+lemma cnr_appl_simple: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦V⦠â â¦G, L⦠⢠⡠ðâ¦T⦠â ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦âV.Tâ¦.
#G #L #V #T #HV #HT #HS #X #H
elim (cpr_inv_appl1_simple ⦠H) -H // #V0 #T0 #HV0 #HT0 #H destruct
>(HV ⦠HV0) -V0 >(HT ⦠HT0) -T0 //
qed.
(* Basic_1: was: nf2_dec *)
-axiom cnr_dec: âG,L,T1. â¦G, L⦠⢠ðâ¦T1⦠â¨
+axiom cnr_dec: âG,L,T1. â¦G, L⦠⢠⡠ðâ¦T1⦠â¨
ââT2. â¦G, L⦠⢠T1 â¡ T2 & (T1 = T2 â â¥).
(* Basic_1: removed theorems 1: nf2_abst_shift *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma
index 487fd68bb..7c596245f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma
@@ -19,10 +19,10 @@ include "basic_2/reduction/cnr_crr.ma".
(* Main properties on context-sensitive irreducible terms *******************)
-theorem cir_cnr: âG,L,T. â¦G, L⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦Tâ¦.
+theorem cir_cnr: âG,L,T. â¦G, L⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
/2 width=4 by cpr_fwd_cir/ qed.
(* Main inversion lemmas on context-sensitive irreducible terms *************)
-theorem cnr_inv_cir: âG,L,T. â¦G, L⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦Tâ¦.
+theorem cnr_inv_cir: âG,L,T. â¦G, L⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
/2 width=5 by cnr_inv_crr/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
index 7ee9e1f29..c72c3315e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
@@ -20,7 +20,7 @@ include "basic_2/reduction/cnr.ma".
(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
(* Note: this property is unusual *)
-lemma cnr_inv_crr: âG,L,T. â¦G, L⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦T⦠â â¥.
+lemma cnr_inv_crr: âG,L,T. â¦G, L⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦T⦠â â¥.
#G #L #T #H elim H -L -T
[ #L #K #V #i #HLK #H
elim (cnr_inv_delta ⦠HLK H)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
index 9f29fe9a8..48fa090bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
@@ -20,7 +20,7 @@ include "basic_2/reduction/cnr.ma".
(* Advanced properties ******************************************************)
(* Basic_1: was only: nf2_csort_lref *)
-lemma cnr_lref_atom: âG,L,i. â©[i] L â¡ â â â¦G, L⦠⢠ðâ¦#iâ¦.
+lemma cnr_lref_atom: âG,L,i. â©[i] L â¡ â â â¦G, L⦠⢠⡠ðâ¦#iâ¦.
#G #L #i #HL #X #H
elim (cpr_inv_lref1 ⦠H) -H // *
#K #V1 #V2 #HLK #_ #_
@@ -28,7 +28,7 @@ lapply (ldrop_mono ⦠HL ⦠HLK) -L #H destruct
qed.
(* Basic_1: was: nf2_lref_abst *)
-lemma cnr_lref_abst: âG,L,K,V,i. â©[i] L â¡ K. âV â â¦G, L⦠⢠ðâ¦#iâ¦.
+lemma cnr_lref_abst: âG,L,K,V,i. â©[i] L â¡ K. âV â â¦G, L⦠⢠⡠ðâ¦#iâ¦.
#G #L #K #V #i #HLK #X #H
elim (cpr_inv_lref1 ⦠H) -H // *
#K0 #V1 #V2 #HLK0 #_ #_
@@ -38,8 +38,8 @@ qed.
(* Relocation properties ****************************************************)
(* Basic_1: was: nf2_lift *)
-lemma cnr_lift: âG,L0,L,T,T0,s,d,e. â¦G, L⦠⢠ðâ¦T⦠â
- â©[s, d, e] L0 â¡ L â â§[d, e] T â¡ T0 â â¦G, L0⦠⢠ðâ¦T0â¦.
+lemma cnr_lift: âG,L0,L,T,T0,s,d,e. â¦G, L⦠⢠⡠ðâ¦T⦠â
+ â©[s, d, e] L0 â¡ L â â§[d, e] T â¡ T0 â â¦G, L0⦠⢠⡠ðâ¦T0â¦.
#G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
elim (cpr_inv_lift1 ⦠H ⦠HL0 ⦠HT0) -L0 #T1 #HT10 #HT1
<(HLT ⦠HT1) in HT0; -L #HT0
@@ -47,8 +47,8 @@ elim (cpr_inv_lift1 ⦠H ⦠HL0 ⦠HT0) -L0 #T1 #HT10 #HT1
qed.
(* Note: this was missing in basic_1 *)
-lemma cnr_inv_lift: âG,L0,L,T,T0,s,d,e. â¦G, L0⦠⢠ðâ¦T0⦠â
- â©[s, d, e] L0 â¡ L â â§[d, e] T â¡ T0 â â¦G, L⦠⢠ðâ¦Tâ¦.
+lemma cnr_inv_lift: âG,L0,L,T,T0,s,d,e. â¦G, L0⦠⢠⡠ðâ¦T0⦠â
+ â©[s, d, e] L0 â¡ L â â§[d, e] T â¡ T0 â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
#G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
elim (lift_total X d e) #X0 #HX0
lapply (cpr_lift ⦠H ⦠HL0 ⦠HT0 ⦠HX0) -L #HTX0
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
index d423f119e..61e6e6cc6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
@@ -27,37 +27,37 @@ interpretation
(* Basic inversion lemmas ***************************************************)
-lemma cnx_inv_sort: âh,g,G,L,k. â¦G, L⦠⢠ð[h, g]â¦âk⦠â deg h g k 0.
+lemma cnx_inv_sort: âh,g,G,L,k. â¦G, L⦠⢠â¡[h, g] ðâ¦âk⦠â deg h g k 0.
#h #g #G #L #k #H elim (deg_total h g k)
#l @(nat_ind_plus ⦠l) -l // #l #_ #Hkl
lapply (H (â(next h k)) ?) -H /2 width=2 by cpx_sort/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false ⦠H)
qed-.
-lemma cnx_inv_delta: âh,g,I,G,L,K,V,i. â©[i] L â¡ K.â{I}V â â¦G, L⦠⢠ð[h, g]â¦#i⦠â â¥.
+lemma cnx_inv_delta: âh,g,I,G,L,K,V,i. â©[i] L â¡ K.â{I}V â â¦G, L⦠⢠â¡[h, g] ðâ¦#i⦠â â¥.
#h #g #I #G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct
elim (lift_inv_lref2_be ⦠HVW) -HVW //
qed-.
-lemma cnx_inv_abst: âh,g,a,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦â{a}V.T⦠â
- â¦G, L⦠⢠ð[h, g]â¦V⦠⧠â¦G, L.âV⦠⢠ð[h, g]â¦Tâ¦.
+lemma cnx_inv_abst: âh,g,a,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦â{a}V.T⦠â
+ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠⧠â¦G, L.âV⦠⢠â¡[h, g] ðâ¦Tâ¦.
#h #g #a #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (â{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (â{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnx_inv_abbr: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦-âV.T⦠â
- â¦G, L⦠⢠ð[h, g]â¦V⦠⧠â¦G, L.âV⦠⢠ð[h, g]â¦Tâ¦.
+lemma cnx_inv_abbr: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦-âV.T⦠â
+ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠⧠â¦G, L.âV⦠⢠â¡[h, g] ðâ¦Tâ¦.
#h #g #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (-âV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (-âV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnx_inv_zeta: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦+âV.T⦠â â¥.
+lemma cnx_inv_zeta: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦+âV.T⦠â â¥.
#h #g #G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3 by cpx_zeta/ #H destruct
@@ -69,56 +69,56 @@ lemma cnx_inv_zeta: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦+âV.T⦠â
]
qed-.
-lemma cnx_inv_appl: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦âV.T⦠â
- â§â§ â¦G, L⦠⢠ð[h, g]â¦V⦠& â¦G, L⦠⢠ð[h, g]â¦T⦠& ðâ¦Tâ¦.
+lemma cnx_inv_appl: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦âV.T⦠â
+ â§â§ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠& â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠& ðâ¦Tâ¦.
#h #g #G #L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (âV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (âV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (âV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (âV1.T2) ?) -HVT1 /2 width=1 by cpx_flat/ -HT2 #H destruct //
| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
[ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (â{a}W1.âV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
- | lapply (H (â{a}âW1.V1.U1) ?) -H /3 width=1/ #H destruct
+ lapply (H (â{a}W1.âV2.U1) ?) -H /3 width=3 by cpr_cpx, cpr_theta/ -HV12 #H destruct
+ | lapply (H (â{a}âW1.V1.U1) ?) -H /3 width=1 by cpr_cpx, cpr_beta/ #H destruct
]
]
qed-.
-lemma cnx_inv_tau: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦âV.T⦠â â¥.
+lemma cnx_inv_tau: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦âV.T⦠â â¥.
#h #g #G #L #V #T #H lapply (H T ?) -H
/2 width=4 by cpx_tau, discr_tpair_xy_y/
qed-.
(* Basic forward lemmas *****************************************************)
-lemma cnx_fwd_cnr: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠ðâ¦Tâ¦.
+lemma cnx_fwd_cnr: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
#h #g #G #L #T #H #U #HTU
@H /2 width=1 by cpr_cpx/ (**) (* auto fails because a δ-expansion gets in the way *)
qed-.
(* Basic properties *********************************************************)
-lemma cnx_sort: âh,g,G,L,k. deg h g k 0 â â¦G, L⦠⢠ð[h, g]â¦âkâ¦.
+lemma cnx_sort: âh,g,G,L,k. deg h g k 0 â â¦G, L⦠⢠â¡[h, g] ðâ¦âkâ¦.
#h #g #G #L #k #Hk #X #H elim (cpx_inv_sort1 ⦠H) -H // * #l #Hkl #_
lapply (deg_mono ⦠Hkl Hk) -h -L <plus_n_Sm #H destruct
qed.
-lemma cnx_sort_iter: âh,g,G,L,k,l. deg h g k l â â¦G, L⦠⢠ð[h, g]â¦â((next h)^l k)â¦.
+lemma cnx_sort_iter: âh,g,G,L,k,l. deg h g k l â â¦G, L⦠⢠â¡[h, g] ðâ¦â((next h)^l k)â¦.
#h #g #G #L #k #l #Hkl
lapply (deg_iter ⦠l Hkl) -Hkl <minus_n_n /2 width=6 by cnx_sort/
qed.
-lemma cnx_abst: âh,g,a,G,L,W,T. â¦G, L⦠⢠ð[h, g]â¦W⦠â â¦G, L.âW⦠⢠ð[h, g]â¦T⦠â
- â¦G, L⦠⢠ð[h, g]â¦â{a}W.Tâ¦.
+lemma cnx_abst: âh,g,a,G,L,W,T. â¦G, L⦠⢠â¡[h, g] ðâ¦W⦠â â¦G, L.âW⦠⢠â¡[h, g] ðâ¦T⦠â
+ â¦G, L⦠⢠â¡[h, g] ðâ¦â{a}W.Tâ¦.
#h #g #a #G #L #W #T #HW #HT #X #H
elim (cpx_inv_abst1 ⦠H) -H #W0 #T0 #HW0 #HT0 #H destruct
>(HW ⦠HW0) -W0 >(HT ⦠HT0) -T0 //
qed.
-lemma cnx_appl_simple: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦V⦠â â¦G, L⦠⢠ð[h, g]â¦T⦠â ðâ¦T⦠â
- â¦G, L⦠⢠ð[h, g]â¦âV.Tâ¦.
+lemma cnx_appl_simple: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â ðâ¦T⦠â
+ â¦G, L⦠⢠â¡[h, g] ðâ¦âV.Tâ¦.
#h #g #G #L #V #T #HV #HT #HS #X #H
elim (cpx_inv_appl1_simple ⦠H) -H // #V0 #T0 #HV0 #HT0 #H destruct
>(HV ⦠HV0) -V0 >(HT ⦠HT0) -T0 //
qed.
-axiom cnx_dec: âh,g,G,L,T1. â¦G, L⦠⢠ð[h, g]â¦T1⦠â¨
+axiom cnx_dec: âh,g,G,L,T1. â¦G, L⦠⢠â¡[h, g] ðâ¦T1⦠â¨
ââT2. â¦G, L⦠⢠T1 â¡[h, g] T2 & (T1 = T2 â â¥).
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
index 3e62a5c60..18dc60e3e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
@@ -19,10 +19,10 @@ include "basic_2/reduction/cnx_crx.ma".
(* Main properties on context-sensitive extended irreducible terms **********)
-theorem cix_cnr: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠ð[h, g]â¦Tâ¦.
+theorem cix_cnr: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦Tâ¦.
/2 width=6 by cpx_fwd_cix/ qed.
(* Main inversion lemmas on context-sensitive extended irreducible terms ****)
-theorem cnr_inv_cix: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠ð[h, g]â¦Tâ¦.
+theorem cnr_inv_cix: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦Tâ¦.
/2 width=7 by cnx_inv_crx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
index ec9abbd33..c6d51c630 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
@@ -20,7 +20,7 @@ include "basic_2/reduction/cnx.ma".
(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
(* Note: this property is unusual *)
-lemma cnx_inv_crx: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠ð[h, g]â¦T⦠â â¥.
+lemma cnx_inv_crx: âh,g,G,L,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¥.
#h #g #G #L #T #H elim H -L -T
[ #L #k #l #Hkl #H
lapply (cnx_inv_sort ⦠H) -H #H
@@ -28,16 +28,16 @@ lemma cnx_inv_crx: âh,g,G,L,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, Lâ¦
| #I #L #K #V #i #HLK #H
elim (cnx_inv_delta ⦠HLK H)
| #L #V #T #_ #IHV #H
- elim (cnx_inv_appl ⦠H) -H /2 width=1/
+ elim (cnx_inv_appl ⦠H) -H /2 width=1 by/
| #L #V #T #_ #IHT #H
- elim (cnx_inv_appl ⦠H) -H /2 width=1/
+ elim (cnx_inv_appl ⦠H) -H /2 width=1 by/
| #I #L #V #T * #H1 #H2 destruct
[ elim (cnx_inv_zeta ⦠H2)
| elim (cnx_inv_tau ⦠H2)
]
|6,7: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
- [1,3: elim (cnx_inv_abbr ⦠H2) -H2 /2 width=1/
- |*: elim (cnx_inv_abst ⦠H2) -H2 /2 width=1/
+ [1,3: elim (cnx_inv_abbr ⦠H2) -H2 /2 width=1 by/
+ |*: elim (cnx_inv_abst ⦠H2) -H2 /2 width=1 by/
]
| #a #L #V #W #T #H
elim (cnx_inv_appl ⦠H) -H #_ #_ #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
index f52149d5b..65c035f4a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
@@ -19,7 +19,7 @@ include "basic_2/reduction/cnx.ma".
(* Advanced properties ******************************************************)
-lemma cnx_lref_atom: âh,g,G,L,i. â©[i] L â¡ â â â¦G, L⦠⢠ð[h, g]â¦#iâ¦.
+lemma cnx_lref_atom: âh,g,G,L,i. â©[i] L â¡ â â â¦G, L⦠⢠â¡[h, g] ðâ¦#iâ¦.
#h #g #G #L #i #HL #X #H
elim (cpx_inv_lref1 ⦠H) -H // *
#I #K #V1 #V2 #HLK #_ #_
@@ -28,16 +28,16 @@ qed.
(* Relocation properties ****************************************************)
-lemma cnx_lift: âh,g,G,L0,L,T,T0,s,d,e. â¦G, L⦠⢠ð[h, g]â¦T⦠â â©[s, d, e] L0 â¡ L â
- â§[d, e] T â¡ T0 â â¦G, L0⦠⢠ð[h, g]â¦T0â¦.
+lemma cnx_lift: âh,g,G,L0,L,T,T0,s,d,e. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â©[s, d, e] L0 â¡ L â
+ â§[d, e] T â¡ T0 â â¦G, L0⦠⢠â¡[h, g] ðâ¦T0â¦.
#h #g #G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
elim (cpx_inv_lift1 ⦠H ⦠HL0 ⦠HT0) -L0 #T1 #HT10 #HT1
<(HLT ⦠HT1) in HT0; -L #HT0
>(lift_mono ⦠HT10 ⦠HT0) -T1 -X //
qed.
-lemma cnx_inv_lift: âh,g,G,L0,L,T,T0,s,d,e. â¦G, L0⦠⢠ð[h, g]â¦T0⦠â â©[s, d, e] L0 â¡ L â
- â§[d, e] T â¡ T0 â â¦G, L⦠⢠ð[h, g]â¦Tâ¦.
+lemma cnx_inv_lift: âh,g,G,L0,L,T,T0,s,d,e. â¦G, L0⦠⢠â¡[h, g] ðâ¦T0⦠â â©[s, d, e] L0 â¡ L â
+ â§[d, e] T â¡ T0 â â¦G, L⦠⢠â¡[h, g] ðâ¦Tâ¦.
#h #g #G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
elim (lift_total X d e) #X0 #HX0
lapply (cpx_lift ⦠H ⦠HL0 ⦠HT0 ⦠HX0) -L #HTX0
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma
index 5cee2e207..d0e1e19ac 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma
@@ -19,7 +19,7 @@ include "basic_2/reduction/cpr.ma".
(* Advanced forward lemmas on context-sensitive irreducible terms ***********)
-lemma cpr_fwd_cir: âG,L,T1,T2. â¦G, L⦠⢠T1 â¡ T2 â â¦G, L⦠⢠ðâ¦T1⦠â T2 = T1.
+lemma cpr_fwd_cir: âG,L,T1,T2. â¦G, L⦠⢠T1 â¡ T2 â â¦G, L⦠⢠⡠ðâ¦T1⦠â T2 = T1.
#G #L #T1 #T2 #H elim H -G -L -T1 -T2
[ //
| #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
@@ -28,15 +28,15 @@ lemma cpr_fwd_cir: âG,L,T1,T2. â¦G, L⦠⢠T1 â¡ T2 â â¦G, L⦠â¢
[ elim (cir_inv_bind ⦠H) -H #HV1 #HT1 * #H destruct
lapply (IHV1 ⦠HV1) -IHV1 -HV1 #H destruct
lapply (IHT1 ⦠HT1) -IHT1 #H destruct //
- | elim (cir_inv_ib2 ⦠H) -H /2 width=1/ /3 width=2/
+ | elim (cir_inv_ib2 ⦠H) -H /3 width=2 by or_introl, eq_f2/
]
| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
[ elim (cir_inv_appl ⦠H) -H #HV1 #HT1 #_
>IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (cir_inv_ri2 ⦠H) /2 width=1/
+ | elim (cir_inv_ri2 ⦠H) /2 width=1 by/
]
| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
- elim (cir_inv_ri2 ⦠H) /2 width=1/
+ elim (cir_inv_ri2 ⦠H) /2 width=1 by or_introl/
| #G #L #V1 #T1 #T2 #_ #_ #H
elim (cir_inv_ri2 ⦠H) /2 width=1/
| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
index 196cdadb0..ce54e9a7e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
@@ -19,7 +19,7 @@ include "basic_2/reduction/cpx.ma".
(* Advanced forward lemmas on context-sensitive extended irreducible terms **)
-lemma cpx_fwd_cix: âh,g,G,L,T1,T2. â¦G, L⦠⢠T1 â¡[h, g] T2 â â¦G, L⦠⢠ð[h, g]â¦T1⦠â T2 = T1.
+lemma cpx_fwd_cix: âh,g,G,L,T1,T2. â¦G, L⦠⢠T1 â¡[h, g] T2 â â¦G, L⦠⢠â¡[h, g] ðâ¦T1⦠â T2 = T1.
#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
[ //
| #G #L #k #l #Hkl #H elim (cix_inv_sort ⦠Hkl H)
@@ -29,19 +29,19 @@ lemma cpx_fwd_cix: âh,g,G,L,T1,T2. â¦G, L⦠⢠T1 â¡[h, g] T2 â â¦G, L
[ elim (cix_inv_bind ⦠H) -H #HV1 #HT1 * #H destruct
lapply (IHV1 ⦠HV1) -IHV1 -HV1 #H destruct
lapply (IHT1 ⦠HT1) -IHT1 #H destruct //
- | elim (cix_inv_ib2 ⦠H) -H /2 width=1/ /3 width=2/
+ | elim (cix_inv_ib2 ⦠H) -H /3 width=2 by or_introl, eq_f2/
]
| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
[ elim (cix_inv_appl ⦠H) -H #HV1 #HT1 #_
>IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (cix_inv_ri2 ⦠H) /2 width=1/
+ | elim (cix_inv_ri2 ⦠H) /2 width=1 by/
]
| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
- elim (cix_inv_ri2 ⦠H) /2 width=1/
+ elim (cix_inv_ri2 ⦠H) /2 width=1 by or_introl/
| #G #L #V1 #T1 #T2 #_ #_ #H
- elim (cix_inv_ri2 ⦠H) /2 width=1/
+ elim (cix_inv_ri2 ⦠H) /2 width=1 by/
| #G #L #V1 #V2 #T #_ #_ #H
- elim (cix_inv_ri2 ⦠H) /2 width=1/
+ elim (cix_inv_ri2 ⦠H) /2 width=1 by/
| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
elim (cix_inv_appl ⦠H) -H #_ #_ #H
elim (simple_inv_bind ⦠H)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
index 79d9269b3..02aaa8209 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
@@ -45,7 +45,7 @@ interpretation
(* Basic inversion lemmas ***************************************************)
-fact crr_inv_sort_aux: âG,L,T,k. â¦G, L⦠⢠ðâ¦T⦠â T = âk â â¥.
+fact crr_inv_sort_aux: âG,L,T,k. â¦G, L⦠⢠⡠ðâ¦T⦠â T = âk â â¥.
#G #L #T #k0 * -L -T
[ #L #K #V #i #HLK #H destruct
| #L #V #T #_ #H destruct
@@ -58,10 +58,10 @@ fact crr_inv_sort_aux: âG,L,T,k. â¦G, L⦠⢠ðâ¦T⦠â T = âk â
]
qed-.
-lemma crr_inv_sort: âG,L,k. â¦G, L⦠⢠ðâ¦âk⦠â â¥.
+lemma crr_inv_sort: âG,L,k. â¦G, L⦠⢠⡠ðâ¦âk⦠â â¥.
/2 width=6 by crr_inv_sort_aux/ qed-.
-fact crr_inv_lref_aux: âG,L,T,i. â¦G, L⦠⢠ðâ¦T⦠â T = #i â
+fact crr_inv_lref_aux: âG,L,T,i. â¦G, L⦠⢠⡠ðâ¦T⦠â T = #i â
ââK,V. â©[i] L â¡ K.âV.
#G #L #T #j * -L -T
[ #L #K #V #i #HLK #H destruct /2 width=3 by ex1_2_intro/
@@ -75,10 +75,10 @@ fact crr_inv_lref_aux: âG,L,T,i. â¦G, L⦠⢠ðâ¦T⦠â T = #i â
]
qed-.
-lemma crr_inv_lref: âG,L,i. â¦G, L⦠⢠ðâ¦#i⦠â ââK,V. â©[i] L â¡ K.âV.
+lemma crr_inv_lref: âG,L,i. â¦G, L⦠⢠⡠ðâ¦#i⦠â ââK,V. â©[i] L â¡ K.âV.
/2 width=4 by crr_inv_lref_aux/ qed-.
-fact crr_inv_gref_aux: âG,L,T,p. â¦G, L⦠⢠ðâ¦T⦠â T = §p â â¥.
+fact crr_inv_gref_aux: âG,L,T,p. â¦G, L⦠⢠⡠ðâ¦T⦠â T = §p â â¥.
#G #L #T #q * -L -T
[ #L #K #V #i #HLK #H destruct
| #L #V #T #_ #H destruct
@@ -91,10 +91,10 @@ fact crr_inv_gref_aux: âG,L,T,p. â¦G, L⦠⢠ðâ¦T⦠â T = §p â
]
qed-.
-lemma crr_inv_gref: âG,L,p. â¦G, L⦠⢠ðâ¦Â§p⦠â â¥.
+lemma crr_inv_gref: âG,L,p. â¦G, L⦠⢠⡠ðâ¦Â§p⦠â â¥.
/2 width=6 by crr_inv_gref_aux/ qed-.
-lemma trr_inv_atom: âG,I. â¦G, â⦠⢠ðâ¦âª{I}⦠â â¥.
+lemma trr_inv_atom: âG,I. â¦G, â⦠⢠⡠ðâ¦âª{I}⦠â â¥.
#G * #i #H
[ elim (crr_inv_sort ⦠H)
| elim (crr_inv_lref ⦠H) -H #L #V #H
@@ -103,8 +103,8 @@ lemma trr_inv_atom: âG,I. â¦G, â⦠⢠ðâ¦âª{I}⦠â â¥.
]
qed-.
-fact crr_inv_ib2_aux: âa,I,G,L,W,U,T. ib2 a I â â¦G, L⦠⢠ðâ¦T⦠â T = â{a,I}W.U â
- â¦G, L⦠⢠ðâ¦W⦠⨠â¦G, L.â{I}W⦠⢠ðâ¦Uâ¦.
+fact crr_inv_ib2_aux: âa,I,G,L,W,U,T. ib2 a I â â¦G, L⦠⢠⡠ðâ¦T⦠â T = â{a,I}W.U â
+ â¦G, L⦠⢠⡠ðâ¦W⦠⨠â¦G, L.â{I}W⦠⢠⡠ðâ¦Uâ¦.
#G #b #J #L #W0 #U #T #HI * -L -T
[ #L #K #V #i #_ #H destruct
| #L #V #T #_ #H destruct
@@ -119,12 +119,12 @@ fact crr_inv_ib2_aux: âa,I,G,L,W,U,T. ib2 a I â â¦G, L⦠⢠ðâ¦Tâ¦
]
qed-.
-lemma crr_inv_ib2: âa,I,G,L,W,T. ib2 a I â â¦G, L⦠⢠ðâ¦â{a,I}W.T⦠â
- â¦G, L⦠⢠ðâ¦W⦠⨠â¦G, L.â{I}W⦠⢠ðâ¦Tâ¦.
+lemma crr_inv_ib2: âa,I,G,L,W,T. ib2 a I â â¦G, L⦠⢠⡠ðâ¦â{a,I}W.T⦠â
+ â¦G, L⦠⢠⡠ðâ¦W⦠⨠â¦G, L.â{I}W⦠⢠⡠ðâ¦Tâ¦.
/2 width=5 by crr_inv_ib2_aux/ qed-.
-fact crr_inv_appl_aux: âG,L,W,U,T. â¦G, L⦠⢠ðâ¦T⦠â T = âW.U â
- â¨â¨ â¦G, L⦠⢠ðâ¦W⦠| â¦G, L⦠⢠ðâ¦U⦠| (ðâ¦U⦠â â¥).
+fact crr_inv_appl_aux: âG,L,W,U,T. â¦G, L⦠⢠⡠ðâ¦T⦠â T = âW.U â
+ â¨â¨ â¦G, L⦠⢠⡠ðâ¦W⦠| â¦G, L⦠⢠⡠ðâ¦U⦠| (ðâ¦U⦠â â¥).
#G #L #W0 #U #T * -L -T
[ #L #K #V #i #_ #H destruct
| #L #V #T #HV #H destruct /2 width=1 by or3_intro0/
@@ -140,6 +140,6 @@ fact crr_inv_appl_aux: âG,L,W,U,T. â¦G, L⦠⢠ðâ¦T⦠â T = âW.U
]
qed-.
-lemma crr_inv_appl: âG,L,V,T. â¦G, L⦠⢠ðâ¦âV.T⦠â
- â¨â¨ â¦G, L⦠⢠ðâ¦V⦠| â¦G, L⦠⢠ðâ¦T⦠| (ðâ¦T⦠â â¥).
+lemma crr_inv_appl: âG,L,V,T. â¦G, L⦠⢠⡠ðâ¦âV.T⦠â
+ â¨â¨ â¦G, L⦠⢠⡠ðâ¦V⦠| â¦G, L⦠⢠⡠ðâ¦T⦠| (ðâ¦T⦠â â¥).
/2 width=3 by crr_inv_appl_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma
index 36cf60341..8b4cfb336 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma
@@ -19,21 +19,21 @@ include "basic_2/reduction/crr.ma".
(* Advanved properties ******************************************************)
-lemma crr_append_sn: âG,L,K,T. â¦G, L⦠⢠ðâ¦T⦠â â¦G, K @@ L⦠⢠ðâ¦Tâ¦.
+lemma crr_append_sn: âG,L,K,T. â¦G, L⦠⢠⡠ðâ¦T⦠â â¦G, K @@ L⦠⢠⡠ðâ¦Tâ¦.
#G #L #K0 #T #H elim H -L -T /2 width=1/
#L #K #V #i #HLK
lapply (ldrop_fwd_length_lt2 ⦠HLK) #Hi
lapply (ldrop_O1_append_sn_le ⦠HLK ⦠K0) -HLK /2 width=2/ -Hi /2 width=3/
qed.
-lemma trr_crr: âG,L,T. â¦G, â⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦Tâ¦.
+lemma trr_crr: âG,L,T. â¦G, â⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
#G #L #T #H lapply (crr_append_sn ⦠H) //
qed.
(* Advanced inversion lemmas ************************************************)
-fact crr_inv_labst_last_aux: âG,L1,T,W. â¦G, L1⦠⢠ðâ¦T⦠â
- âL2. L1 = â.âW @@ L2 â â¦G, L2⦠⢠ðâ¦Tâ¦.
+fact crr_inv_labst_last_aux: âG,L1,T,W. â¦G, L1⦠⢠⡠ðâ¦T⦠â
+ âL2. L1 = â.âW @@ L2 â â¦G, L2⦠⢠⡠ðâ¦Tâ¦.
#G #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
lapply (ldrop_fwd_length_lt2 ⦠HLK1)
@@ -49,8 +49,8 @@ fact crr_inv_labst_last_aux: âG,L1,T,W. â¦G, L1⦠⢠ðâ¦T⦠â
]
qed.
-lemma crr_inv_labst_last: âG,L,T,W. â¦G, â.âW @@ L⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ðâ¦Tâ¦.
+lemma crr_inv_labst_last: âG,L,T,W. â¦G, â.âW @@ L⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠⡠ðâ¦Tâ¦.
/2 width=4/ qed-.
-lemma crr_inv_trr: âG,T,W. â¦G, â.âW⦠⢠ðâ¦T⦠â â¦G, â⦠⢠ðâ¦Tâ¦.
+lemma crr_inv_trr: âG,T,W. â¦G, â.âW⦠⢠⡠ðâ¦T⦠â â¦G, â⦠⢠⡠ðâ¦Tâ¦.
/2 width=4/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
index 4b28fc1dc..41f626cee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
@@ -19,8 +19,8 @@ include "basic_2/reduction/crr.ma".
(* Properties on relocation *************************************************)
-lemma crr_lift: âG,K,T. â¦G, K⦠⢠ðâ¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
- âU. â§[d, e] T â¡ U â â¦G, L⦠⢠ðâ¦Uâ¦.
+lemma crr_lift: âG,K,T. â¦G, K⦠⢠⡠ðâ¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
+ âU. â§[d, e] T â¡ U â â¦G, L⦠⢠⡠ðâ¦Uâ¦.
#G #K #T #H elim H -K -T
[ #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H
elim (lift_inv_lref1 ⦠H) -H * #Hid #H destruct
@@ -46,8 +46,8 @@ lemma crr_lift: âG,K,T. â¦G, K⦠⢠ðâ¦T⦠â âL,s,d,e. â©[s, d, e
]
qed.
-lemma crr_inv_lift: âG,L,U. â¦G, L⦠⢠ðâ¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
- âT. â§[d, e] T â¡ U â â¦G, K⦠⢠ðâ¦Tâ¦.
+lemma crr_inv_lift: âG,L,U. â¦G, L⦠⢠⡠ðâ¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
+ âT. â§[d, e] T â¡ U â â¦G, K⦠⢠⡠ðâ¦Tâ¦.
#G #L #U #H elim H -L -U
[ #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H
elim (lift_inv_lref2 ⦠H) -H * #Hid #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
index 8c26803ad..86796ae0b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
@@ -38,14 +38,14 @@ interpretation
(* Basic properties *********************************************************)
-lemma crr_crx: âh,g,G,L,T. â¦G, L⦠⢠ðâ¦T⦠â â¦G, L⦠⢠ð[h, g]â¦Tâ¦.
+lemma crr_crx: âh,g,G,L,T. â¦G, L⦠⢠⡠ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦Tâ¦.
#h #g #G #L #T #H elim H -L -T
/2 width=4 by crx_delta, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
qed.
(* Basic inversion lemmas ***************************************************)
-fact crx_inv_sort_aux: âh,g,G,L,T,k. â¦G, L⦠⢠ð[h, g]â¦T⦠â T = âk â
+fact crx_inv_sort_aux: âh,g,G,L,T,k. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â T = âk â
âl. deg h g k (l+1).
#h #g #G #L #T #k0 * -L -T
[ #L #k #l #Hkl #H destruct /2 width=2 by ex_intro/
@@ -60,10 +60,10 @@ fact crx_inv_sort_aux: âh,g,G,L,T,k. â¦G, L⦠⢠ð[h, g]â¦T⦠â T =
]
qed-.
-lemma crx_inv_sort: âh,g,G,L,k. â¦G, L⦠⢠ð[h, g]â¦âk⦠â âl. deg h g k (l+1).
+lemma crx_inv_sort: âh,g,G,L,k. â¦G, L⦠⢠â¡[h, g] ðâ¦âk⦠â âl. deg h g k (l+1).
/2 width=5 by crx_inv_sort_aux/ qed-.
-fact crx_inv_lref_aux: âh,g,G,L,T,i. â¦G, L⦠⢠ð[h, g]â¦T⦠â T = #i â
+fact crx_inv_lref_aux: âh,g,G,L,T,i. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â T = #i â
ââI,K,V. â©[i] L â¡ K.â{I}V.
#h #g #G #L #T #j * -L -T
[ #L #k #l #_ #H destruct
@@ -78,10 +78,10 @@ fact crx_inv_lref_aux: âh,g,G,L,T,i. â¦G, L⦠⢠ð[h, g]â¦T⦠â T =
]
qed-.
-lemma crx_inv_lref: âh,g,G,L,i. â¦G, L⦠⢠ð[h, g]â¦#i⦠â ââI,K,V. â©[i] L â¡ K.â{I}V.
+lemma crx_inv_lref: âh,g,G,L,i. â¦G, L⦠⢠â¡[h, g] ðâ¦#i⦠â ââI,K,V. â©[i] L â¡ K.â{I}V.
/2 width=6 by crx_inv_lref_aux/ qed-.
-fact crx_inv_gref_aux: âh,g,G,L,T,p. â¦G, L⦠⢠ð[h, g]â¦T⦠â T = §p â â¥.
+fact crx_inv_gref_aux: âh,g,G,L,T,p. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â T = §p â â¥.
#h #g #G #L #T #q * -L -T
[ #L #k #l #_ #H destruct
| #I #L #K #V #i #HLK #H destruct
@@ -95,10 +95,10 @@ fact crx_inv_gref_aux: âh,g,G,L,T,p. â¦G, L⦠⢠ð[h, g]â¦T⦠â T =
]
qed-.
-lemma crx_inv_gref: âh,g,G,L,p. â¦G, L⦠⢠ð[h, g]â¦Â§p⦠â â¥.
+lemma crx_inv_gref: âh,g,G,L,p. â¦G, L⦠⢠â¡[h, g] ðâ¦Â§p⦠â â¥.
/2 width=8 by crx_inv_gref_aux/ qed-.
-lemma trx_inv_atom: âh,g,I,G. â¦G, â⦠⢠ð[h, g]â¦âª{I}⦠â
+lemma trx_inv_atom: âh,g,I,G. â¦G, â⦠⢠â¡[h, g] ðâ¦âª{I}⦠â
ââk,l. deg h g k (l+1) & I = Sort k.
#h #g * #i #G #H
[ elim (crx_inv_sort ⦠H) -H /2 width=4 by ex2_2_intro/
@@ -108,8 +108,8 @@ lemma trx_inv_atom: âh,g,I,G. â¦G, â⦠⢠ð[h, g]â¦âª{I}⦠â
]
qed-.
-fact crx_inv_ib2_aux: âh,g,a,I,G,L,W,U,T. ib2 a I â â¦G, L⦠⢠ð[h, g]â¦T⦠â
- T = â{a,I}W.U â â¦G, L⦠⢠ð[h, g]â¦W⦠⨠â¦G, L.â{I}W⦠⢠ð[h, g]â¦Uâ¦.
+fact crx_inv_ib2_aux: âh,g,a,I,G,L,W,U,T. ib2 a I â â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â
+ T = â{a,I}W.U â â¦G, L⦠⢠â¡[h, g] ðâ¦W⦠⨠â¦G, L.â{I}W⦠⢠â¡[h, g] ðâ¦Uâ¦.
#h #g #b #J #G #L #W0 #U #T #HI * -L -T
[ #L #k #l #_ #H destruct
| #I #L #K #V #i #_ #H destruct
@@ -125,12 +125,12 @@ fact crx_inv_ib2_aux: âh,g,a,I,G,L,W,U,T. ib2 a I â â¦G, L⦠⢠ð[h, g
]
qed-.
-lemma crx_inv_ib2: âh,g,a,I,G,L,W,T. ib2 a I â â¦G, L⦠⢠ð[h, g]â¦â{a,I}W.T⦠â
- â¦G, L⦠⢠ð[h, g]â¦W⦠⨠â¦G, L.â{I}W⦠⢠ð[h, g]â¦Tâ¦.
+lemma crx_inv_ib2: âh,g,a,I,G,L,W,T. ib2 a I â â¦G, L⦠⢠â¡[h, g] ðâ¦â{a,I}W.T⦠â
+ â¦G, L⦠⢠â¡[h, g] ðâ¦W⦠⨠â¦G, L.â{I}W⦠⢠â¡[h, g] ðâ¦Tâ¦.
/2 width=5 by crx_inv_ib2_aux/ qed-.
-fact crx_inv_appl_aux: âh,g,G,L,W,U,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â T = âW.U â
- â¨â¨ â¦G, L⦠⢠ð[h, g]â¦W⦠| â¦G, L⦠⢠ð[h, g]â¦U⦠| (ðâ¦U⦠â â¥).
+fact crx_inv_appl_aux: âh,g,G,L,W,U,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â T = âW.U â
+ â¨â¨ â¦G, L⦠⢠â¡[h, g] ðâ¦W⦠| â¦G, L⦠⢠â¡[h, g] ðâ¦U⦠| (ðâ¦U⦠â â¥).
#h #g #G #L #W0 #U #T * -L -T
[ #L #k #l #_ #H destruct
| #I #L #K #V #i #_ #H destruct
@@ -147,6 +147,6 @@ fact crx_inv_appl_aux: âh,g,G,L,W,U,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â T
]
qed-.
-lemma crx_inv_appl: âh,g,G,L,V,T. â¦G, L⦠⢠ð[h, g]â¦âV.T⦠â
- â¨â¨ â¦G, L⦠⢠ð[h, g]â¦V⦠| â¦G, L⦠⢠ð[h, g]â¦T⦠| (ðâ¦T⦠â â¥).
+lemma crx_inv_appl: âh,g,G,L,V,T. â¦G, L⦠⢠â¡[h, g] ðâ¦âV.T⦠â
+ â¨â¨ â¦G, L⦠⢠â¡[h, g] ðâ¦V⦠| â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠| (ðâ¦T⦠â â¥).
/2 width=3 by crx_inv_appl_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma
index 8f5286c54..ca86ad11e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma
@@ -19,13 +19,14 @@ include "basic_2/reduction/crx.ma".
(* Advanved properties ******************************************************)
-lemma crx_append_sn: âh,g,G,L,K,T. â¦G, L⦠⢠ð[h, g]â¦T⦠â â¦G, K @@ L⦠⢠ð[h, g]â¦Tâ¦.
-#h #g #G #L #K0 #T #H elim H -L -T /2 width=1/ /2 width=2/
+lemma crx_append_sn: âh,g,G,L,K,T. â¦G, L⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, K @@ L⦠⢠â¡[h, g] ðâ¦Tâ¦.
+#h #g #G #L #K0 #T #H elim H -L -T
+/2 width=2 by crx_sort, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
#I #L #K #V #i #HLK
lapply (ldrop_fwd_length_lt2 ⦠HLK) #Hi
-lapply (ldrop_O1_append_sn_le ⦠HLK ⦠K0) -HLK /2 width=2/ -Hi /2 width=4/
+lapply (ldrop_O1_append_sn_le ⦠HLK ⦠K0) -HLK /2 width=4 by crx_delta, lt_to_le/
qed.
-lemma trx_crx: âh,g,G,L,T. â¦G, â⦠⢠ð[h, g]â¦T⦠â â¦G, L⦠⢠ð[h, g]â¦Tâ¦.
+lemma trx_crx: âh,g,G,L,T. â¦G, â⦠⢠â¡[h, g] ðâ¦T⦠â â¦G, L⦠⢠â¡[h, g] ðâ¦Tâ¦.
#h #g #G #L #T #H lapply (crx_append_sn ⦠H) //
qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
index 9e1bc9f81..9c268927a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
@@ -19,8 +19,8 @@ include "basic_2/reduction/crx.ma".
(* Properties on relocation *************************************************)
-lemma crx_lift: âh,g,G,K,T. â¦G, K⦠⢠ð[h, g]â¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
- âU. â§[d, e] T â¡ U â â¦G, L⦠⢠ð[h, g]â¦Uâ¦.
+lemma crx_lift: âh,g,G,K,T. â¦G, K⦠⢠â¡[h, g] ðâ¦T⦠â âL,s,d,e. â©[s, d, e] L â¡ K â
+ âU. â§[d, e] T â¡ U â â¦G, L⦠⢠â¡[h, g] ðâ¦Uâ¦.
#h #g #G #K #T #H elim H -K -T
[ #K #k #l #Hkl #L #s #d #e #_ #X #H
>(lift_inv_sort1 ⦠H) -X /2 width=2 by crx_sort/
@@ -48,8 +48,8 @@ lemma crx_lift: âh,g,G,K,T. â¦G, K⦠⢠ð[h, g]â¦T⦠â âL,s,d,e.
]
qed.
-lemma crx_inv_lift: âh,g,G,L,U. â¦G, L⦠⢠ð[h, g]â¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
- âT. â§[d, e] T â¡ U â â¦G, K⦠⢠ð[h, g]â¦Tâ¦.
+lemma crx_inv_lift: âh,g,G,L,U. â¦G, L⦠⢠â¡[h, g] ðâ¦U⦠â âK,s,d,e. â©[s, d, e] L â¡ K â
+ âT. â§[d, e] T â¡ U â â¦G, K⦠⢠â¡[h, g] ðâ¦Tâ¦.
#h #g #G #L #U #H elim H -L -U
[ #L #k #l #Hkl #K #s #d #e #_ #X #H
>(lift_inv_sort2 ⦠H) -X /2 width=2 by crx_sort/
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 506fa910b..7b7c453e4 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
@@ -106,7 +106,7 @@ table {
]
[ { "context-sensitive extended computation" * } {
[ "lpxs ( â¦?,?⦠⢠â¡*[?,?] ? )" "lpxs_alt ( â¦?,?⦠⢠â¡â¡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs ( â¦?,?⦠⢠? â¡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_cpys" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "cpxs ( â¦?,?⦠⢠? â¡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
@@ -130,8 +130,8 @@ table {
[ "fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠)" "fpb_lift" + "fpb_aaa" * ]
}
]
- [ { "context-sensitive extended normal forms" * } {
- [ "cnx ( â¦?,?⦠⢠ð[?,?]â¦?⦠)" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
+ [ { "normal forms for context-sensitive extended reduction" * } {
+ [ "cnx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠)" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
}
]
[ { "context-sensitive extended reduction" * } {
@@ -139,16 +139,16 @@ table {
[ "cpx ( â¦?,?⦠⢠? â¡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ]
}
]
- [ { "context-sensitive extended irreducible forms" * } {
- [ "cix ( â¦?,?⦠⢠ð[?,?]â¦?⦠)" "cix_append" + "cix_lift" * ]
+ [ { "irreducible forms for context-sensitive extended reduction" * } {
+ [ "cix ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠)" "cix_append" + "cix_lift" * ]
}
]
- [ { "context-sensitive extended reducible forms" * } {
- [ "crx ( â¦?,?⦠⢠ð[?,?]â¦?⦠)" "crx_append" + "crx_lift" * ]
+ [ { "reducible forms for context-sensitive extended reduction" * } {
+ [ "crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠)" "crx_append" + "crx_lift" * ]
}
]
- [ { "context-sensitive normal forms" * } {
- [ "cnr ( â¦?,?⦠⢠ðâ¦?⦠)" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
+ [ { "normal forms for context-sensitive reduction" * } {
+ [ "cnr ( â¦?,?⦠⢠⡠ðâ¦?⦠)" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
}
]
[ { "context-sensitive reduction" * } {
@@ -156,12 +156,12 @@ table {
[ "cpr ( �,?⦠⢠? ⡠? )" "cpr_lift" + "cpr_cir" * ]
}
]
- [ { "context-sensitive irreducible forms" * } {
- [ "cir ( â¦?,?⦠⢠ðâ¦?⦠)" "cir_append" + "cir_lift" * ]
+ [ { "irreducible forms for context-sensitive reduction" * } {
+ [ "cir ( â¦?,?⦠⢠⡠ðâ¦?⦠)" "cir_append" + "cir_lift" * ]
}
]
- [ { "context-sensitive reducible forms" * } {
- [ "crr ( â¦?,?⦠⢠ðâ¦?⦠)" "crr_append" + "crr_lift" * ]
+ [ { "reducible forms for context-sensitive reduction" * } {
+ [ "crr ( â¦?,?⦠⢠⡠ðâ¦?⦠)" "crr_append" + "crr_lift" * ]
}
]
}
--
2.39.5