#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
qed-.
+
+lemma cpxs_neq_inv_step_sn: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
+[ #H elim H -H //
+| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct
+ [ -H1 -H2 /3 width=1 by/
+ | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *)
+ ]
+]
+qed-.
∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2.
#h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csx_intro #T #HLT2 #HT2
-elim (term_eq_dec T1 T2) #HT12
+elim (eq_term_dec T1 T2) #HT12
[ -IHT1 -HLT12 destruct /3 width=1/
| -HT1 -HT2 /3 width=4/
qed-.
∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2.
#h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csxa_intro #T #HLT2 #HT2
-elim (term_eq_dec T1 T2) #HT12
+elim (eq_term_dec T1 T2) #HT12
[ -IHT1 -HLT12 destruct /3 width=1/
| -HT1 -HT2 /3 width=4/
qed.
[ -H #H destruct #H
elim H //
| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct
- elim (term_eq_dec T0 T) #HT0
+ elim (eq_term_dec T0 T) #HT0
[ -HLT1 -HLT2 -H /3 width=1/
| -IHT -HT12 /4 width=3/
]
elim (cpx_inv_abbr1 … HL) -HL *
[ #V3 #T3 #HV3 #HLT3 #H0 destruct
elim (lift_total V0 0 1) #V4 #HV04
- elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
+ elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
[ -IHVT #H0 destruct
elim (eq_false_inv_tpair_sn … H) -H
[ -HLV10 -HV3 -HLT3 -HVT
include "basic_2/reduction/fpbc.ma".
include "basic_2/computation/fpbs.ma".
-(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************)
+(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************)
inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbg_inj : ∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+| fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 →
+ fpbg h g G1 L1 T1 G1 L2 T2
+| fpbg_fqup: ∀G2,L,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃+ ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 →
fpbg h g G1 L1 T1 G2 L2 T2
-| fpbg_step: ∀G,L,L2,T. fpbg h g G1 L1 T1 G L T → ⦃G, L⦄ ⊢ ➡[h, g] L2 → fpbg h g G1 L1 T1 G L2 T
.
interpretation "'big tree' proper parallel computation (closure)"
'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2).
-(* Basic forvard lemmas *****************************************************)
-
-lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
-/3 width=5 by fpbs_strap1, fpbc_fwd_fpb, fpb_lpx/
-qed-.
-
(* Basic properties *********************************************************)
lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-/3 width=5 by fpbg_inj, fpbg_step/ qed.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/3 width=5 by fpbg_cpxs, fpbg_fqup, fqu_fqup, cpx_cpxs/
+qed.
-lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
-lapply (fpbg_fwd_fpbs … H1) #H0
-elim (fpb_fpbc_or_fpn … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ]
-/2 width=5 by fpbg_inj, fpbg_step/
-qed-.
+axiom fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
+axiom fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2
-/3 width=5 by fpbg_step, fpbg_inj, fpbs_strap2/
-qed-.
lemma fpbg_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(fpbs_ind … HT2) -G2 -L2 -T2
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fpbs_ind … H) -G2 -L2 -T2
/2 width=5 by fpbg_strap1/
qed-.
-lemma fpbs_fpbg_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
- â\88\80G2,L2,T2. â¦\83G, L, Tâ¦\84 >[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >[h, g] â¦\83G2, L2, T2â¦\84.
-#h #g #G1 #G #L1 #L #T1 #T #HT1 @(fpbs_ind … HT1) -G -L -T
+lemma fpbs_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
/3 width=5 by fpbg_strap2/
qed-.
-
-lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … L2 T2 H) -G2 -L2 -T2
-/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu, fpb_fquq, fqu_fquq/
-qed.
-
-lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
-[ #H elim H //
-| #T #T2 #_ #HT2 #IHT1 #HT12
- elim (term_eq_dec T1 T) #H destruct
- [ -IHT1 /4 width=1/
- | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1
- @(fpbg_strap1 … HT1) -HT1 /2 width=1 by fpb_cpx/
- ]
-]
-qed.
-
-lemma cprs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-/3 width=1 by cprs_cpxs, cpxs_fpbg/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/notation/relations/btpredstarproper_8.ma".
-include "basic_2/reduction/fpbc.ma".
-include "basic_2/computation/fpbs.ma".
-
-(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************)
-
-inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 →
- fpbg h g G1 L1 T1 G1 L2 T2
-| fpbg_fqup: ∀G2,L,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃+ ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 →
- fpbg h g G1 L1 T1 G2 L2 T2
-.
-
-interpretation "'big tree' proper parallel computation (closure)"
- 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=5 by fpbg_cpxs, fpbg_fqup, fqu_fqup, cpx_cpxs/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/computation/fpbg.ma".
-
-(* "BIG TREE" ORDER FOR CLOSURES ********************************************)
-
-(* Main properties **********************************************************)
-
-theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g).
-/3 width=5 by fpbg_fwd_fpbs, fpbg_fpbs_trans/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/unfold/lsstas_lift.ma".
-include "basic_2/reduction/fpb_lift.ma".
-include "basic_2/reduction/fpbc_lift.ma".
+include "basic_2/computation/cpxs_lift.ma".
include "basic_2/computation/fpbg.ma".
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************)
(* Advanced properties ******************************************************)
lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) →
∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2
-[ #H elim H //
-| #l2 #T #T2 #HT1 #HT2 #IHT1 #HT12 #l1 #Hl21
- elim (term_eq_dec T1 T) #H destruct [ -IHT1 |]
- [ elim (le_inv_plus_l … Hl21) -Hl21 #_ #Hl1
- >(plus_minus_m_m … Hl1) -Hl1 /3 width=5 by ssta_fpbc, fpbg_inj/
- | #Hl1 >commutative_plus in Hl21; #Hl21
- elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21
- lapply (lsstas_da_conf … HT1 … Hl1) -HT1
- >(plus_minus_m_m … Hl12) -Hl12
- /4 width=5 by ssta_fpb, fpbg_strap1/
- ]
-]
-qed.
+/4 width=5 by fpbg_cpxs, lsstas_cpxs/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/notation/relations/btpredstarrestricted_8.ma".
+include "basic_2/computation/fpbg.ma".
+
+(* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********)
+
+inductive fpbr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
+| fpbr_inj : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbr h g G1 L1 T1 G2 L2 T2
+| fpbr_step: ∀G,G2,L,L2,T,T2. fpbr h g G1 L1 T1 G L T → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ fpbr h g G1 L1 T1 G2 L2 T2
+.
+
+interpretation "restricted 'big tree' proper parallel computation (closure)"
+ 'BTPRedStarRestricted h g G1 L1 T1 G2 L2 T2 = (fpbr h g G1 L1 T1 G2 L2 T2).
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fpbr_fwd_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
+/3 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu/
+qed-.
+
+lemma fpbr_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
+/3 width=5 by fpbs_strap1, fqup_fpbs, fqu_fqup/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fqu_fpbs_fpbr: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fpbs_ind … H) -G2 -L2 -T2
+/2 width=5 by fpbr_inj, fpbr_step/
+qed.
+
+lemma fpbr_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by fqu_fpbs_fpbr, fpbr_fwd_fpbs/ qed-.
+
+(* Note: this is used in the closure proof *)
+lemma fpbr_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(fpbs_ind … HT2) -G2 -L2 -T2
+/2 width=5 by fpbr_step/
+qed-.
+
+lemma fqup_fpbr_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 @(fqup_ind … HT1) -G -L -T
+/3 width=5 by fpbr_strap2/
+qed-.
+
+(* Note: this is used in the closure proof *)
+lemma fqup_fpbr: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
+/3 width=5 by fqu_fpbs_fpbr, fqus_fpbs/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/computation/fpbg_fpbg.ma".
+include "basic_2/computation/fpbr.ma".
+
+(* RESTRICTED "BIG TREE" ORDER FOR CLOSURES *********************************)
+
+(* Advanced forward lemmas **************************************************)
+lemma fpbr_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbr_fwd_fpbg, fpbg_fwd_fpbs/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem fpbr_trans: ∀h,g. tri_transitive … (fpbr h g).
+/3 width=5 by fpbr_fwd_fpbs, fpbr_fpbs_trans/ qed-.
⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
/2 width=5 by tri_TC_strap/ qed-.
+lemma fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+/4 width=5 by fqu_fquq, fpb_fquq, tri_step/
+qed.
+
lemma fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … L2 T2 H) -G2 -L2 -T2
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2
/3 width=5 by fpb_fquq, tri_step/
qed.
⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 →
⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄.
/3 width=5 by fpbs_trans, cpr_lpr_fpbs, ssta_fpbs/ qed.
+
+lemma cpxs_fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
+ ⦃G1, L1, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbs_trans, cpxs_fpbs, fqup_fpbs/ qed.
(* *)
(**************************************************************************)
-include "basic_2/unfold/lsstas_lift.ma".
-include "basic_2/reduction/fpb_lift.ma".
+include "basic_2/computation/cpxs_lift.ma".
include "basic_2/computation/fpbs.ma".
(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
(* Advanced properties ******************************************************)
+lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 →
+ ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
+/3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed.
+
lemma ssta_fpbs: ∀h,g,G,L,T,U,l.
⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U →
⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄.
-/3 width=2 by fpb_fpbs, ssta_fpb/ qed.
-
-lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 →
- ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2 //
-#l2 #T #T2 #HT1 #HT2 #IHT1 #l1 >commutative_plus #Hl21 #Hl1
-elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21
-lapply (lsstas_da_conf … HT1 … Hl1) -HT1
->(plus_minus_m_m … Hl12) -Hl12
-/3 width=5 by ssta_fpb, fpbs_strap1/
-qed.
+/3 width=5 by lsstas_fpbs, ssta_lsstas/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/notation/relations/predsnstar_8.ma".
-include "basic_2/reduction/fpn.ma".
-include "basic_2/computation/lpxs.ma".
-
-(* ORDERED "BIG TREE" NORMAL FORMS ******************************************)
-
-definition fpns: ∀h. sd h → tri_relation genv lenv term ≝
- λh,g,G1,L1,T1,G2,L2,T2.
- ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & T1 = T2.
-
-interpretation
- "ordered 'big tree' normal forms (closure)"
- 'PRedSnStar h g G1 L1 T1 G2 L2 T2 = (fpns h g G1 L1 T1 G2 L2 T2).
-
-(* Basic_properties *********************************************************)
-
-lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g).
-/2 width=1 by and3_intro/ qed.
-
-lemma fpn_fpns: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=1 by lpx_lpxs, and3_intro/
-qed.
-
-lemma fpns_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * #H1G #H1L #G1T *
-/3 width=3 by lpxs_strap1, and3_intro/
-qed-.
-
-lemma fpns_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * #H1G #H1L #G1T *
-/3 width=3 by lpxs_strap2, and3_intro/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fpns_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpxs_fwd_length, and3_intro/
-qed-.
"'big tree' strong normalization (closure)"
'BTSN h g G L T = (fsb h g G L T).
-(* Basic eliminators ********************************************************)
-
-theorem fsb_ind_alt: ∀h,g. ∀R: relation3 …. (
- ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h,g] T1 → (
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
- (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → R G2 L2 T2
- ) → R G1 L1 T1
- ) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T.
-#h #g #R #IH #G #L #T #H elim H -G -L -T
-/5 width=1 by fpb_fpbc, fsb_intro/
-qed-.
-
(* Basic inversion lemmas ***************************************************)
lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
(**************************************************************************)
include "basic_2/notation/relations/btsnalt_5.ma".
-include "basic_2/computation/fpbg_alt.ma".
+include "basic_2/computation/fpbg.ma".
include "basic_2/computation/fsb.ma".
-(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
+(* GENERAL "BIG TREE" STRONGLY NORMALIZING TERMS ****************************)
(* Note: alternative definition of fsb *)
inductive fsba (h) (g): relation3 genv lenv term ≝
include "basic_2/unfold/lsstas_lsstas.ma".
include "basic_2/computation/fpbs_lift.ma".
-include "basic_2/computation/fpbg.ma".
+include "basic_2/computation/fpbr.ma".
include "basic_2/equivalence/cpes_cpds.ma".
include "basic_2/dynamic/snv.ma".
(* Properties for the preservation results **********************************)
fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
+@(cprs_ind … H) -T2 /4 width=6 by fpbr_fpbs_trans, cprs_fpbs/
qed-.
fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
+@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbr_fpbs_trans, cprs_fpbs/
qed-.
fact da_cpcs_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2.
#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H
qed-.
fact ssta_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 →
∀U1. ⦃G, L1⦄ ⊢ T1 •[h, g] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
qed-.
fact lsstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l2] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
[2: /3 width=12 by da_cprs_lpr_aux/
|3: /3 width=10 by snv_cprs_lpr_aux/
-|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
+|4: /3 width=5 by fpbr_fpbs_trans, cprs_fpbs/
] -G0 -L0 -T0 -T1 -T -l1 #U2 #HTU2 #HU2
/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
qed-.
fact lsstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l] U1 →
- ∀T2. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+ ∀T2. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, g, l] U2 →
⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
qed-.
fact snv_ssta_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- ∀G,L,T. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ ∀G,L,T. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
∀U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ¡[h, g].
/3 width=8 by lsstas_inv_SO, ssta_lsstas/ qed-.
fact lsstas_cpds_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
∀U1. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 →
∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, g, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2.
| lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l
lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1
elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L)
- /3 width=8 by fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12
+ /3 width=8 by fpbr_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12
/3 width=5 by cpcs_cpes, ex3_2_intro/
]
qed-.
fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
(* Properties on degree assignment for terms ********************************)
fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1
lapply (fqup_lref … G1 … HLK1)
elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- /4 width=10 by da_ldef, da_ldec, fqup_fpbg/
+ /4 width=10 by da_ldef, da_ldec, fqup_fpbr/
|2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
lapply (ldrop_mono … H … HLK1) -H #H destruct
lapply (fqup_lref … G1 … HLK1)
elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -V2
- /4 width=7 by da_lift, fqup_fpbg/
+ /4 width=7 by da_lift, fqup_fpbr/
]
| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
lapply (da_inv_bind … H2) -H2
elim (cpr_inv_bind1 … H3) -H3 *
[ #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
+ /4 width=9 by da_bind, fqup_fpbr, lpr_pair/
| #T2 #HT12 #HT2 #H1 #H2 destruct
- /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/
+ /4 width=11 by da_inv_lift, fqup_fpbr, lpr_pair, ldrop_ldrop/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct
elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
lapply (da_inv_flat … H2) -H2 #Hl
elim (cpr_inv_appl1 … H3) -H3 *
- [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/
+ [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbr/
| #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct
elim (snv_inv_bind … HT1) -HT1 #HW #HU1
lapply (da_inv_bind … Hl) -Hl #Hl
lapply (cprs_div … HW3 … HW10) -W3 #HWW1
lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #H
elim (snv_fwd_da … HW) #l1 #Hl1
- lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbg, ssta_lsstas/ #HW1
+ lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbr, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
- lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbg/ ] #Hl0
- lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbg/ -HW
- lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
+ /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, ssta_fpbs/ #H destruct
+ lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbr/ ] #Hl0
+ lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbr/ -HW
+ lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbr, lpr_pair/ ] -HL12 -HW2
/4 width=6 by da_bind, lsubd_da_trans, lsubd_abbr/
| #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH3 -IH2 -V -W0 -T0 -l0 -HV1 -HVW1
elim (snv_inv_bind … HT1) -HT1 #_
lapply (da_inv_bind … Hl) -Hl
- /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/
+ /5 width=9 by da_bind, da_flat, fqup_fpbr, lpr_pair/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1
lapply (da_inv_flat … H2) -H2 #Hl
elim (cpr_inv_cast1 … H3) -H3
- [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
- | /3 width=7 by fqup_fpbg/
+ [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbr/
+ | /3 width=7 by fqup_fpbr/
]
]
qed-.
(* Properties on context-free parallel reduction for local environments *****)
fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
lapply (fqup_lref … G1 … HLK1) #HKL
elim (cpr_inv_lref1 … H2) -H2
- [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
+ [ #H destruct -HLK1 /4 width=10 by fqup_fpbr, snv_lref/
| * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
+ lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbr, snv_lift/
]
| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
elim (snv_inv_bind … H1) -H1 #HV1 #HT1
elim (cpr_inv_bind1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbr, snv_bind, lpr_pair/
| #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
- /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/
+ /4 width=10 by fqup_fpbr, snv_inv_lift, lpr_pair, ldrop_ldrop/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1
elim (cpr_inv_appl1 … H2) -H2 *
[ #V2 #T2 #HV12 #HT12 #H destruct -IH4
- lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12
- elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HV2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ #HT2
+ lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #H2l0
+ elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbr/ -HV1 #W2 #HVW2 #HW12
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ -HT12 -HTU1 #X #HTU2 #H
elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct
lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10
lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
lapply (cprs_div … HW10 … HW230) -W30 #HW120
- lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10
+ lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbr/ #HW10
lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #HlW10
elim (snv_fwd_da … HW20) #l #Hl
lapply (da_cpcs_aux … IH1 IH2 … HlW10 … Hl … HW120) // -HlW10
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HlV2
- lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fqup_fpbg/ #HlW2
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #W3 #HV2W3 #HW103
+ /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, ssta_fpbs/ #H destruct
+ lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HlV2
+ lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fqup_fpbr/ #HlW2
+ elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #W3 #HV2W3 #HW103
lapply (ssta_da_conf … HV2W3 … HlV2) <minus_plus_m_m #HlW3
lapply (cpcs_cpr_strap1 … HW120 … HW202) -HW120 #HW102
lapply (lpr_cpcs_conf … HL12 … HW102) -HW102 #HW102
lapply (cpcs_canc_sn … HW103 … HW102) -W10 #HW32
- lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 #HV2
- lapply (IH1 … HW202 … HL12) /2 width=1 by fqup_fpbg/ -HW20 #HW2
- lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT20 #HT2
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbr/ -HV1 #HV2
+ lapply (IH1 … HW202 … HL12) /2 width=1 by fqup_fpbr/ -HW20 #HW2
+ lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fqup_fpbr, lpr_pair/ -HT20 #HT2
lapply (snv_ssta_aux … IH4 … HlV2 … HV2W3)
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW3
+ /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/ #HW3
lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
- @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
+ @(lsubsv_abbr … l) /3 width=7 by fqup_fpbr/ #W #W0 #l0 #Hl0 #HV2W #HW20
lapply (lsstas_ssta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
@(lsstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
- [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_ssta_fpbs/
- | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
+ [ /3 width=9 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_ssta_fpbs/
+ | /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/
]
| #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
lapply (lpr_cprs_conf … HL12 … HW10) -HW10 #HW10
- elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbr, lpr_pair/ -HTU0 #X #HTU2 #H
elim (cprs_inv_abst1 … H) -H #W #U2 #HW1 #_ #H destruct -U3
- elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2
+ elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbr/ -IH3 -HVW1 #X #H1 #H2
lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
elim (lift_total X 0 1) #W20 #H3
lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1 by ldrop_ldrop/ -H1 #HVW20
lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
- lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
+ lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbr/ -IH2 -Hl0 #Hl0
lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 by ldrop_ldrop/ -Hl0 #Hl0
- lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
- lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
- lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
+ lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbr/ -HW0 #HW2
+ lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbr/ -HV1 -HV10 #HV0
+ lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbr, lpr_pair/ -L1 #HT2
lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_ldrop/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
elim (cpr_inv_cast1 … H2) -H2
[ * #W2 #T2 #HW12 #HT12 #H destruct
lapply (cpcs_cprs_strap1 … HUW1 W2 ?) /2 width=1 by cpr_cprs/ -HUW1 #H1
- lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ -HW1 -HW12 #HW2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH1 #HT2
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HTU1 #U2 #HTU2 #HU12
- lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -HT1 -HT12 -Hl0 #Hl0
+ lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbr/ -HW1 -HW12 #HW2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ -IH1 #HT2
+ elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fqup_fpbr/ -IH3 -HTU1 #U2 #HTU2 #HU12
+ lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fqup_fpbr/ -IH2 -HT1 -HT12 -Hl0 #Hl0
/4 width=7 by snv_cast, lpr_cpcs_conf, cpcs_canc_sn/
| #H -IH3 -IH2 -HW1 -HTU1 -HUW1
- lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/
+ lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbr/
]
]
qed-.
(* Properties on nat-iterated stratified static type assignment for terms ***)
fact snv_lsstas_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lsstas h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #HG0 #HL0 #HT0 #_ #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct
[ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ]
lapply (fqup_lref … G1 … HLK1) #H
- lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
+ lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbr, snv_lift/
| #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2
elim (snv_inv_bind … H1) -H1 #HV1 #HT1
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
- elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/
+ elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbr, snv_bind/
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct
elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
lapply (da_inv_flat … Hl1) -Hl1 #Hl1
elim (lsstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
- lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1
- elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2
+ lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbr/ #HU1
+ elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbr/ -T1 -l1 #X #l #_ #H #HU10 -l2
elim (lsstas_inv_bind1 … H) -H #U0 #_ #H destruct -T0 -l
elim (cpes_inv_abst2 … HU10) -HU10 #W2 #U2 #HU12 #HU02
elim (cprs_inv_abst … HU02) -HU02 #HW02 #_
[ lapply (lsstas_inv_O … H2) -H2 #H destruct // ]
elim (snv_inv_cast … H1) -H1
lapply (da_inv_flat … Hl1) -Hl1
- lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/
+ lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbr/
]
qed-.
(* Properties on sn parallel reduction for local environments ***************)
fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lsstas_cpr_lpr h g G1 L1 T1.
#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1
|2,4: * #K0 #V0 #X0 #H #HVX0 #HX0
lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct
]
- [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
+ [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbr/ #V2 #HWV2 #HV2
elim (lift_total V2 0 (i+1))
- /6 width=11 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
- | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
+ /6 width=11 by fqup_fpbr, cpcs_lift, lsstas_ldec, ex2_intro/
+ | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbr/ #W2 #HVW2 #HW02
elim (lift_total W2 0 (i+1))
/4 width=11 by cpcs_lift, lsstas_ldef, ex2_intro/
- | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02
+ | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbr/ -l1 #W2 #HXW2 #HW02
elim (lift_total W2 0 (i+1))
/3 width=11 by cpcs_lift, lsstas_lift, ex2_intro/
]
elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
elim (cpr_inv_bind1 … H3) -H3 *
[ #V2 #T2 #HV12 #HT12 #H destruct
- elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1
+ elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbr, lpr_pair/ -T1
/4 width=5 by cpcs_bind2, lpr_cpr_conf, lsstas_bind, ex2_intro/
| #T3 #HT13 #HXT3 #H1 #H2 destruct
- elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
+ elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbr, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
elim (lsstas_inv_lift1 … HTU3 L2 … HXT3) -T3
/5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_ldrop, ex2_intro/
]
elim (cpr_inv_appl1 … H3) -H3 *
[ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH4 -IH3 -IH2
elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1
- /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/
+ /4 width=5 by fqup_fpbr, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/
| #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct
elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
lapply (cprs_div … HW10 … HW20) -W0 #HW12
lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #H
elim (snv_fwd_da … HW2) #l #Hl
- lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbg, ssta_lsstas/ #HW1
+ lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbr, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, ssta_fpbs/ #H destruct
- lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2l
- elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fqup_fpbg, ssta_lsstas/ -HVW1 #W4 #H #HW14
+ /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, ssta_fpbs/ #H destruct
+ lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HV2
+ lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HV2l
+ elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fqup_fpbr, ssta_lsstas/ -HVW1 #W4 #H #HW14
lapply (lsstas_inv_SO … H) #HV2W4
lapply (ssta_da_conf … HV2W4 … HV2l) <minus_plus_m_m #HW4l
- lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW4
- lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
- lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3l
- elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23
+ lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/ #HW4
+ lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbr/ #HW3
+ lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbr/ #HW3l
+ elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbr, lpr_pair/ #U3 #HTU3 #HU23
lapply (cpcs_cpr_strap1 … HW12 … HW23) #H
lapply (lpr_cpcs_conf … HL12 … H) -H #H
lapply (cpcs_canc_sn … HW14 H) -H #HW43
@(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/
/4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
| -U3
- @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/
+ @(lsubsv_abbr … l) /3 width=7 by fqup_fpbr/
#W #W0 #l0 #Hl0 #HV2W #HW30
lapply (lsstas_ssta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W
@(lsstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) //
- [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_ssta_fpbs/
- | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
+ [ /3 width=9 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_ssta_fpbs/
+ | /3 width=5 by fpbr_fpbs_trans, fqup_fpbr, cpr_lpr_fpbs/
]
- | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
+ | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbr, lpr_pair/
]
| #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH4 -IH3 -IH2
elim (snv_inv_bind … HT1) -HT1 #_ #HT0
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
elim (lsstas_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
- elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
+ elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbr, lpr_pair/ -T0 #U2 #HTU2 #HU02
lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02
elim (cpr_inv_cast1 … H3) -H3
[ * #U2 #T2 #_ #HT12 #H destruct
elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 -HL12
- /3 width=3 by fqup_fpbg, lsstas_cast, ex2_intro/
+ /3 width=3 by fqup_fpbr, lsstas_cast, ex2_intro/
| #HT1X3
elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12
- /2 width=3 by fqup_fpbg, ex2_intro/
+ /2 width=3 by fqup_fpbr, ex2_intro/
]
]
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/notation/relations/bteq_6.ma".
+include "basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/genv.ma".
+
+(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
+
+definition bteq: tri_relation genv lenv term ≝
+ λG1,L1,T1,G2,L2,T2.
+ ∧∧ G1 = G2 & |L1| = |L2| & T1 = T2.
+
+interpretation
+ "equivalent 'big tree' normal forms (closure)"
+ 'BTEq G1 L1 T1 G2 L2 T2 = (bteq G1 L1 T1 G2 L2 T2).
+
+(* Basic_properties *********************************************************)
+
+lemma bteq_refl: tri_reflexive … bteq.
+/2 width=1 by and3_intro/ qed.
+
+lemma bteq_sym: tri_symmetric … bteq.
+#G1 #G2 #L1 #L2 #T1 #T2 * //
+qed-.
+
+lemma bteq_dec: ∀G1,G2,L1,L2,T1,T2. Decidable (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄).
+#G1 #G2 #L1 #L2 #T1 #T2 elim (genv_eq_dec G1 G2)
+#H1G [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
+elim (eq_nat_dec (|L1|) (|L2|))
+#H1L [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
+elim (term_eq_dec T1 T2)
+#H1T [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
+/3 width=1 by and3_intro, or_introl/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'BTEq $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/grammar/bteq.ma".
+
+(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
+
+(* Main properties **********************************************************)
+
+theorem bteq_trans: tri_transitive … bteq.
+#G1 #G #L1 #L #T1 #T * //
+qed-.
+
+theorem bteq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. ⦃G, L, T⦄ ⋕ ⦃G1, L1, T1⦄ →
+ ⦃G, L, T⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
+/3 width=5 by bteq_trans, bteq_sym/ qed-.
+
+theorem bteq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. ⦃G1, L1, T1⦄ ⋕ ⦃G, L, T⦄ →
+ ⦃G2, L2, T2⦄ ⋕ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
+/3 width=5 by bteq_trans, bteq_sym/ qed-.
--- /dev/null
+include "basic_2/reduction/fpn.ma".
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fpb_bteq_fwd_fpn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/
+[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H
+ [ #H1 #H2 elim (fqu_fwd_bteq … H1 H2)
+ | * #HG #HL #HT #_ destruct //
+ ]
+| #T2 #HT12 * //
+]
+qed-.
--- /dev/null
+lemma fpb_fpbc_or_fpn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
+ ⦃G1, L1, T1⦄ ⊢ ➡[h,g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/3 width=1 by and3_intro, or_intror/
+[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H [| * ]
+ /3 width=1 by fpbc_fqu, and3_intro, or_introl, or_intror/
+| #T2 #HT12 elim (eq_term_dec T1 T2) #H destruct
+ /4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/
+]
+qed-.
+
+lemma fpb_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) →
+ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #H0 elim (fpb_fpbc_or_fpn … H) -H //
+#H elim H0 -H0 /2 width=3 by fpn_fwd_bteq/
+qed.
+
+lemma fpbc_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=8 by fqu_fwd_bteq/
+#T2 #_ #HT12 * /2 width=1 by/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/notation/relations/predsn_8.ma".
+include "basic_2/grammar/bteq.ma".
+include "basic_2/reduction/lpx.ma".
+
+(* ADJACENT "BIG TREE" NORMAL FORMS *****************************************)
+
+definition fpn: ∀h. sd h → tri_relation genv lenv term ≝
+ λh,g,G1,L1,T1,G2,L2,T2.
+ ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2.
+
+interpretation
+ "adjacent 'big tree' normal forms (closure)"
+ 'PRedSn h g G1 L1 T1 G2 L2 T2 = (fpn h g G1 L1 T1 G2 L2 T2).
+
+(* Basic_properties *********************************************************)
+
+lemma fpn_refl: ∀h,g. tri_reflexive … (fpn h g).
+/2 width=1 by and3_intro/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fpn_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢➡[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpx_fwd_length, and3_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/notation/relations/predsnstar_8.ma".
+include "basic_2/reduction/fpn.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* ORDERED "BIG TREE" NORMAL FORMS ******************************************)
+
+definition fpns: ∀h. sd h → tri_relation genv lenv term ≝
+ λh,g,G1,L1,T1,G2,L2,T2.
+ ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & T1 = T2.
+
+interpretation
+ "ordered 'big tree' normal forms (closure)"
+ 'PRedSnStar h g G1 L1 T1 G2 L2 T2 = (fpns h g G1 L1 T1 G2 L2 T2).
+
+(* Basic_properties *********************************************************)
+
+lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g).
+/2 width=1 by and3_intro/ qed.
+
+lemma fpn_fpns: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=1 by lpx_lpxs, and3_intro/
+qed.
+
+lemma fpns_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * #H1G #H1L #G1T *
+/3 width=3 by lpxs_strap1, and3_intro/
+qed-.
+
+lemma fpns_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * #H1G #H1L #G1T *
+/3 width=3 by lpxs_strap2, and3_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fpns_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpxs_fwd_length, and3_intro/
+qed-.
--- /dev/null
+include "basic_2/grammar/bteq.ma".
+
+lemma fqu_fwd_bteq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #V * #_ #H elim (plus_xSy_x_false … H)
+| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_x … H)
+| #a #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H)
+| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H)
+| #G #L #K #T #U #e #HLK #_ * #_ #H
+ lapply (ldrop_fwd_length_lt4 … HLK ?) // >H -L #H
+ elim (lt_refl_false … H)
+]
+qed-.
--- /dev/null
+(* Basic eliminators ********************************************************)
+
+theorem fsb_ind_alt: ∀h,g. ∀R: relation3 …. (
+ ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h,g] T1 → (
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → R G2 L2 T2
+ ) → R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T.
+#h #g #R #IH #G #L #T #H elim H -G -L -T
+/5 width=1 by fpb_fpbc, fsb_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedSn $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedSnStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
(* Basic properties *********************************************************)
-lemma aarity_eq_dec: ∀A1,A2:aarity. Decidable (A1 = A2).
+lemma eq_aarity_dec: ∀A1,A2:aarity. Decidable (A1 = A2).
#A1 elim A1 -A1
[ #A2 elim A2 -A2 /2 width=1/
#B2 #A2 #_ #_ @or_intror #H destruct
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/notation/relations/bteq_6.ma".
-include "basic_2/grammar/lenv_length.ma".
-include "basic_2/grammar/genv.ma".
-
-(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
-
-definition bteq: tri_relation genv lenv term ≝
- λG1,L1,T1,G2,L2,T2.
- ∧∧ G1 = G2 & |L1| = |L2| & T1 = T2.
-
-interpretation
- "equivalent 'big tree' normal forms (closure)"
- 'BTEq G1 L1 T1 G2 L2 T2 = (bteq G1 L1 T1 G2 L2 T2).
-
-(* Basic_properties *********************************************************)
-
-lemma bteq_refl: tri_reflexive … bteq.
-/2 width=1 by and3_intro/ qed.
-
-lemma bteq_sym: tri_symmetric … bteq.
-#G1 #G2 #L1 #L2 #T1 #T2 * //
-qed-.
-
-lemma bteq_dec: ∀G1,G2,L1,L2,T1,T2. Decidable (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄).
-#G1 #G2 #L1 #L2 #T1 #T2 elim (genv_eq_dec G1 G2)
-#H1G [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
-elim (eq_nat_dec (|L1|) (|L2|))
-#H1L [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
-elim (term_eq_dec T1 T2)
-#H1T [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
-/3 width=1 by and3_intro, or_introl/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/grammar/bteq.ma".
-
-(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
-
-(* Main properties **********************************************************)
-
-theorem bteq_trans: tri_transitive … bteq.
-#G1 #G #L1 #L #T1 #T * //
-qed-.
-
-theorem bteq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. ⦃G, L, T⦄ ⋕ ⦃G1, L1, T1⦄ →
- ⦃G, L, T⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
-/3 width=5 by bteq_trans, bteq_sym/ qed-.
-
-theorem bteq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. ⦃G1, L1, T1⦄ ⋕ ⦃G, L, T⦄ →
- ⦃G2, L2, T2⦄ ⋕ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
-/3 width=5 by bteq_trans, bteq_sym/ qed-.
(* Basic properties *********************************************************)
-axiom genv_eq_dec: ∀G1,G2:genv. Decidable (G1 = G2).
+axiom eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2).
(* Basic properties *********************************************************)
-axiom item0_eq_dec: ∀I1,I2:item0. Decidable (I1 = I2).
+axiom eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
(* Basic_1: was: bind_dec *)
-axiom bind2_eq_dec: ∀I1,I2:bind2. Decidable (I1 = I2).
+axiom eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2).
(* Basic_1: was: flat_dec *)
-axiom flat2_eq_dec: ∀I1,I2:flat2. Decidable (I1 = I2).
+axiom eq_flat2_dec: ∀I1,I2:flat2. Decidable (I1 = I2).
(* Basic_1: was: kind_dec *)
-axiom item2_eq_dec: ∀I1,I2:item2. Decidable (I1 = I2).
+axiom eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2).
(* Basic_1: removed theorems 21:
s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc
(* Basic properties *********************************************************)
-axiom lenv_eq_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
(* Basic inversion lemmas ***************************************************)
(* Basic properties *********************************************************)
(* Basic_1: was: term_dec *)
-axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2).
+axiom eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
(* Basic inversion lemmas ***************************************************)
(②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
(V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)).
#I #V1 #T1 #V2 #T2 #H
-elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct
+elim (eq_term_dec V1 V2) /3 width=1/ #HV12 destruct
@or_intror @conj // #HT12 destruct /2 width=1/
qed-.
(②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
(T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)).
#I #V1 #T1 #V2 #T2 #H
-elim (term_eq_dec T1 T2) /3 width=1/ #HT12 destruct
+elim (eq_term_dec T1 T2) /3 width=1/ #HT12 destruct
@or_intror @conj // #HT12 destruct /2 width=1/
qed-.
lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2).
* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ]
-[ elim (item2_eq_dec I1 I2) #HI12
+[ elim (eq_item2_dec I1 I2) #HI12
[ destruct /2 width=1/
| @or_intror #H
elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1/
lapply (tstc_inv_atom1 … H) -H #H destruct
| @or_intror #H
lapply (tstc_inv_atom2 … H) -H #H destruct
-| elim (item0_eq_dec I1 I2) #HI12
+| elim (eq_item0_dec I1 I2) #HI12
[ destruct /2 width=1/
| @or_intror #H
lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1/
c: conversion
d: decomposed extended reduction
e: decomposed extended conversion
-n: order on "big tree" normal forms
q: restricted reduction
r: reduction
s: substitution
c: proper single step (successor)
e: reflexive transitive closure to normal form (evaluation)
-g: proper multiple step (greater)
+g: proper multiple step (general) (greater)
p: non-reflexive transitive closure (plus)
q: reflexive closure (question)
+r: proper multiple step (restricted) (restricted)
s: reflexive transitive closure (star)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTEq $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊃≥ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'BTPRedStarRestricted $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PRedSn $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PRedSnStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
include "basic_2/notation/relations/btpred_8.ma".
include "basic_2/relocation/fquq_alt.ma".
-include "basic_2/reduction/fpn.ma".
+include "basic_2/reduction/lpx.ma".
(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄.
/3 width=1 by fpb_lpx, lpr_lpx/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fpb_bteq_fwd_fpn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊢ ➡[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/
-[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H
- [ #H1 #H2 elim (fqu_fwd_bteq … H1 H2)
- | * #HG #HL #HT #_ destruct //
- ]
-| #T2 #HT12 * //
-]
-qed-.
⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
/3 width=1 by fpbc_cpx, cpr_cpx/ qed.
-lemma fpb_fpbc_or_fpn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
- ⦃G1, L1, T1⦄ ⊢ ➡[h,g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=1 by and3_intro, or_intror/
-[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H [| * ]
- /3 width=1 by fpbc_fqu, and3_intro, or_introl, or_intror/
-| #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct
- /4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/
-]
-qed-.
-
-lemma fpb_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
- (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) →
- ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #H0 elim (fpb_fpbc_or_fpn … H) -H //
-#H elim H0 -H0 /2 width=3 by fpn_fwd_bteq/
-qed.
-
(* Basic forward lemmas *****************************************************)
lemma fpbc_fwd_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
/3 width=1 by fpb_fquq, fpb_cpx, fqu_fquq/
qed-.
-
-lemma fpbc_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=8 by fqu_fwd_bteq/
-#T2 #_ #HT12 * /2 width=1 by/
-qed-.
lemma ssta_fpbc: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (term_eq_dec T1 T2)
+#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2)
/3 width=5 by fpbc_cpx, ssta_cpx/ #H destruct
elim (ssta_inv_refl_pos … HT1 … HT12)
qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/notation/relations/predsn_8.ma".
-include "basic_2/grammar/bteq.ma".
-include "basic_2/reduction/lpx.ma".
-
-(* ADJACENT "BIG TREE" NORMAL FORMS *****************************************)
-
-definition fpn: ∀h. sd h → tri_relation genv lenv term ≝
- λh,g,G1,L1,T1,G2,L2,T2.
- ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2.
-
-interpretation
- "adjacent 'big tree' normal forms (closure)"
- 'PRedSn h g G1 L1 T1 G2 L2 T2 = (fpn h g G1 L1 T1 G2 L2 T2).
-
-(* Basic_properties *********************************************************)
-
-lemma fpn_refl: ∀h,g. tri_reflexive … (fpn h g).
-/2 width=1 by and3_intro/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fpn_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢➡[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpx_fwd_length, and3_intro/
-qed-.
include "basic_2/notation/relations/supterm_6.ma".
include "basic_2/grammar/cl_weight.ma".
-include "basic_2/grammar/bteq.ma".
include "basic_2/relocation/ldrop.ma".
(* SUPCLOSURE ***************************************************************)
/2 width=7 by fqu_fwd_length_lref1_aux/
qed-.
-lemma fqu_fwd_bteq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #V * #_ #H elim (plus_xSy_x_false … H)
-| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_x … H)
-| #a #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H)
-| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H)
-| #G #L #K #T #U #e #HLK #_ * #_ #H
- lapply (ldrop_fwd_length_lt4 … HLK ?) // >H -L #H
- elim (lt_refl_false … H)
-]
-qed-.
-
(* Advanced eliminators *****************************************************)
lemma fqu_wf_ind: ∀R:relation3 …. (
lemma gget_dec: ∀G1,G2,e. Decidable (⇩[e] G1 ≡ G2).
#G1 #G2 #e
elim (gget_total e G1) #G #HG1
-elim (genv_eq_dec G G2) #HG2
+elim (eq_genv_dec G G2) #HG2
[ destruct /2 width=1/
| @or_intror #HG12
lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/
#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -L2 -T2
/3 width=3 by fquq_fwd_fw, transitive_le/
qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fqup_inv_step_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 /2 width=5 by ex2_3_intro/
+#G1 #G #L1 #L #T1 #T #H1 #_ * /4 width=9 by fqus_strap2, fqu_fquq, ex2_3_intro/
+qed-.
/2 width=5 by fqus_strap1_fqu, fqup_strap1/
qed-.
-lemma fqup_fqus_trans: ∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ →
- â\88\80G2,L2,T2. â¦\83G, L, Tâ¦\84 â\8a\83* â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\8a\83+ â¦\83G2, L2, T2â¦\84.
-#G1 #G #L1 #L #T1 #T #H1 @(fqup_ind_dx … H1) -H1 -G1 -L1 -T1
+lemma fqup_fqus_trans: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
+#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 @(fqup_ind_dx … H1) -H1 -G1 -L1 -T1
/3 width=5 by fqus_strap2_fqu, fqup_strap2/
qed-.
}
]
[ { "\"big tree\" parallel computation" * } {
- [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_alt" "fpbg_lift" + "fpbg_fpbg" * ]
+ [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ]
+ [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ]
[ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
}
]
}
]
[ { "iterated structural successor for closures" * } {
- [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" "fqus_fqus" * ]
+ [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ]
[ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
}
]
}
]
[ { "closures" * } {
-(* [ "bteq ( ⦃?,?,?⦄ ⪴ ⦃?,?,?⦄ )" "bteq_bteq" * ] *)
[ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ]
}
]
projects / helm.git / commitdiff