(* *)
(**************************************************************************)
-include "basic_2/substitution/fsups_fsups.ma".
+include "basic_2/substitution/fqus_fqus.ma".
include "basic_2/unfold/lsstas_lift.ma".
include "basic_2/reduction/cpx_lift.ma".
include "basic_2/computation/cpxs.ma".
(* Properties on supclosure *************************************************)
-lemma fsupq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
- ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+lemma fquq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
+ ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2
-[ /3 width=3 by fsupq_fsups, ex2_intro/
+[ /3 width=3 by fquq_fqus, ex2_intro/
| #T #T2 #HT2 #_ #IHTU2 #T1 #HT1
- elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
+ elim (fquq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/
]
qed-.
-lemma fsupq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
- ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-/3 width=5 by fsupq_cpxs_trans, lsstas_cpxs/ qed-.
+lemma fquq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
+ ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+/3 width=5 by fquq_cpxs_trans, lsstas_cpxs/ qed-.
-lemma fsups_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2
+lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2
[ /2 width=3 by ex2_intro/
| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
- elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
- elim (IHT1 … HT2) -T /3 width=7 by fsups_trans, ex2_intro/
+ elim (fquq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
+ elim (IHT1 … HT2) -T /3 width=7 by fqus_trans, ex2_intro/
]
qed-.
-lemma fsups_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
- ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-/3 width=7 by fsups_cpxs_trans, lsstas_cpxs/ qed-.
+lemma fqus_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 →
+ ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+/3 width=7 by fqus_cpxs_trans, lsstas_cpxs/ qed-.
-lemma fsups_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2
+lemma fqus_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2
[ /2 width=3 by ex2_intro/
| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
- elim (fsupq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
- elim (IHT1 … HT2) -T /3 width=7 by fsups_strap1, ex2_intro/
+ elim (fquq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
+ elim (IHT1 … HT2) -T /3 width=7 by fqus_strap1, ex2_intro/
]
-qed-.
\ No newline at end of file
+qed-.
(**************************************************************************)
include "basic_2/notation/relations/btpredstarproper_8.ma".
-include "basic_2/substitution/fsupp.ma".
+include "basic_2/substitution/fqup.ma".
include "basic_2/reduction/fpbc.ma".
include "basic_2/computation/fpbs.ma".
/3 width=5 by fpbg_strap2/
qed-.
-lemma fsupp_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 @(fsupp_ind … L2 T2 H) -G2 -L2 -T2
-/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fsup, fpb_fsupq, fsup_fsupq/
+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 → ⊥) →
(**************************************************************************)
include "basic_2/notation/relations/btpredstar_8.ma".
-include "basic_2/substitution/fsups.ma".
+include "basic_2/substitution/fqus.ma".
include "basic_2/reduction/fpb.ma".
include "basic_2/computation/cpxs.ma".
include "basic_2/computation/lpxs.ma".
⦃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 fsups_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 @(fsups_ind … L2 T2 H) -G2 -L2 -T2
-/3 width=5 by fpb_fsupq, tri_step/
+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
+/3 width=5 by fpb_fquq, tri_step/
qed.
lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ]
#G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #HL02
-[ elim (fsupq_cpxs_trans … HT0 … HG1) -T
- /3 width=7 by fsups_trans, ex3_2_intro/
+[ elim (fquq_cpxs_trans … HT0 … HG1) -T
+ /3 width=7 by fqus_trans, ex3_2_intro/
| /3 width=5 by cpxs_strap2, ex3_2_intro/
| lapply (lpx_cpxs_trans … HT0 … HL1) -HT0
- elim (lpx_fsups_trans … HG2 … HL1) -L
+ elim (lpx_fqus_trans … HG2 … HL1) -L
/3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
]
qed-.
theorem fpbsa_inv_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 *
-/4 width=5 by fpbs_trans, fsups_fpbs, cpxs_fpbs, lpxs_fpbs/
+/4 width=5 by fpbs_trans, fqus_fpbs, cpxs_fpbs, lpxs_fpbs/
qed-.
(* Properties on supclosure *************************************************)
-lemma lpxs_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
[ /2 width=5 by ex3_2_intro/
| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
- elim (lpx_fsupq_trans … HT2 … HK1) -K
+ elim (lpx_fquq_trans … HT2 … HK1) -K
/3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
]
qed-.
-lemma lpxs_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fsupq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpxs_trans … HT0 … HT3) -T
-/3 width=7 by cpxs_trans, fsups_strap1, ex3_2_intro/
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
qed-.
-lemma lpx_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fsupq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpx_trans … HT0 … HT3) -T
-/3 width=7 by cpxs_strap1, fsups_strap1, ex3_2_intro/
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
qed-.
lapply (ldrop_mono … H … HLK1) -H #H destruct
elim (cpr_inv_lref1 … H3) -H3
[1,3: #H destruct
- lapply (fsupp_lref … G1 … HLK1)
+ 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, fsupp_fpbg/
+ /4 width=10 by da_ldef, da_ldec, fqup_fpbg/
|2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
lapply (ldrop_mono … H … HLK1) -H #H destruct
- lapply (fsupp_lref … G1 … HLK1)
+ 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, fsupp_fpbg/
+ /4 width=7 by da_lift, fqup_fpbg/
]
| #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, fsupp_fpbg, lpr_pair/
+ /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
| #T2 #HT12 #HT2 #H1 #H2 destruct
- /4 width=11 by da_inv_lift, fsupp_fpbg, lpr_pair, ldrop_ldrop/
+ /4 width=11 by da_inv_lift, fqup_fpbg, 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, fsupp_fpbg/
+ [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/
| #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 fsupp_fpbg, ssta_lsstas/ #HW1
+ lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbg, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
- /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, ssta_fpbs/ #H destruct
- lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fsupp_fpbg/ ] #Hl0
- lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fsupp_fpbg/ -HW
- lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fsupp_fpbg, lpr_pair/ ] -HL12 -HW2
+ /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
/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, fsupp_fpbg, lpr_pair/
+ /5 width=9 by da_bind, da_flat, fqup_fpbg, 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, fsupp_fpbg/
- | /3 width=7 by fsupp_fpbg/
+ [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
+ | /3 width=7 by fqup_fpbg/
]
]
qed-.
(* Advanced properties ******************************************************)
-lemma snv_fsup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g].
+lemma snv_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g].
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I1 #G1 #L1 #V1 #H
elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- lapply (fsupp_lref … G1 … HLK1) #HKL
+ lapply (fqup_lref … G1 … HLK1) #HKL
elim (cpr_inv_lref1 … H2) -H2
- [ #H destruct -HLK1 /4 width=10 by fsupp_fpbg, snv_lref/
+ [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, 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 fsupp_fpbg, snv_lift/
+ lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, 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 fsupp_fpbg, snv_bind, lpr_pair/
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/
| #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
- /4 width=10 by fsupp_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/
+ /4 width=10 by fqup_fpbg, 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 fsupp_fpbg/ #HV2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ #HT2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #H2l0
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fsupp_fpbg/ -HV1 #W2 #HVW2 #HW12
- elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ -HT12 -HTU1 #X #HTU2 #H
+ 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
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 fsupp_fpbg/ #HW10
+ lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #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, fsupp_fpbg, ssta_fpbs/ #H destruct
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HlV2
- lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fsupp_fpbg/ #HlW2
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #W3 #HV2W3 #HW103
+ /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
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 fsupp_fpbg/ -HV1 #HV2
- lapply (IH1 … HW202 … HL12) /2 width=1 by fsupp_fpbg/ -HW20 #HW2
- lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fsupp_fpbg, lpr_pair/ -HT20 #HT2
+ 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 (snv_ssta_aux … IH4 … HlV2 … HV2W3)
- /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/ #HW3
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, 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 fsupp_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
+ @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #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, fsupp_fpbg, cpr_lpr_ssta_fpbs/
- | /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/
+ [ /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/
]
| #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 fsupp_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, 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 fsupp_fpbg/ -IH3 -HVW1 #X #H1 #H2
+ elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -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 fsupp_fpbg/ -IH2 -Hl0 #Hl0
+ lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -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 fsupp_fpbg/ -HW0 #HW2
- lapply (IH1 … HV10 … HL12) /2 width=1 by fsupp_fpbg/ -HV1 -HV10 #HV0
- lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fsupp_fpbg, lpr_pair/ -L1 #HT2
+ 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 (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 fsupp_fpbg/ -HW1 -HW12 #HW2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ -IH1 #HT2
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fsupp_fpbg/ -IH3 -HTU1 #U2 #HTU2 #HU12
- lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ -IH2 -HT1 -HT12 -Hl0 #Hl0
+ 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
/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 fsupp_fpbg/
+ lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/
]
]
qed-.
elim (lsstas_inv_lref1 … H2) -H2 * #K0 #Y0 #X0 [2,4: #l0 ] #HLK0 [1,2: #HYl0 ] #HYX0 #HX0
lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct
[ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ]
- lapply (fsupp_lref … G1 … HLK1) #H
- lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fsupp_fpbg, snv_lift/
+ lapply (fqup_lref … G1 … HLK1) #H
+ lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, 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 fsupp_fpbg, snv_bind/
+ elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, 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 fsupp_fpbg/ #HU1
- elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fsupp_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2
+ 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
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 fsupp_fpbg/
+ lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/
]
qed-.
[ lapply (da_mono … Hl … HWl1) -Hl #H destruct
lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21
]
- lapply (fsupp_lref … G1 … HLK1) #HKV1
+ lapply (fqup_lref … G1 … HLK1) #HKV1
elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) #H2
|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 fsupp_fpbg/ #V2 #HWV2 #HV2
+ [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
elim (lift_total V2 0 (i+1))
- /6 width=11 by fsupp_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
- | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fsupp_fpbg/ #W2 #HVW2 #HW02
+ /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
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 fsupp_fpbg/ -l1 #W2 #HXW2 #HW02
+ | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -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 fsupp_fpbg, lpr_pair/ -T1
+ elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, 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 fsupp_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
+ 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 (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 fsupp_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/
+ /4 width=5 by fqup_fpbg, 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 fsupp_fpbg, ssta_lsstas/ #HW1
+ lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbg, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
- /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, ssta_fpbs/ #H destruct
- lapply (IH3 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HV2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HV2l
- elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fsupp_fpbg, ssta_lsstas/ -HVW1 #W4 #H #HW14
+ /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
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, fsupp_fpbg, cpr_lpr_fpbs/ #HW4
- lapply (IH3 … HW23 … HL12) /2 width=1 by fsupp_fpbg/ #HW3
- lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fsupp_fpbg/ #HW3l
- elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fsupp_fpbg, lpr_pair/ #U3 #HTU3 #HU23
+ 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 (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 fsupp_fpbg/
+ @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/
#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, fsupp_fpbg, cpr_lpr_ssta_fpbs/
- | /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/
+ [ /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/
]
- | -IH1 -IH3 -IH4 /3 width=9 by fsupp_fpbg, lpr_pair/
+ | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, 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 fsupp_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
+ elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbg, 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 fsupp_fpbg, lsstas_cast, ex2_intro/
+ /3 width=3 by fqup_fpbg, lsstas_cast, ex2_intro/
| #HT1X3
elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12
- /2 width=3 by fsupp_fpbg, ex2_intro/
+ /2 width=3 by fqup_fpbg, ex2_intro/
]
]
qed-.
(* Basic_1: removed theorems 9:
clear_pc3_trans pc3_ind_left
pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
- pc3_pr2_fsubst0 pc3_pr2_fsubst0_back pc3_fsubst0
+ pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0
pc3_gen_abst pc3_gen_abst_shift
*)
(* Basic_1: removed local theorems 6:
q: restricted reduction
r: reduction
s: substitution
+u: supclosure
x: extended reduction
- forth letter (if present)
(**************************************************************************)
include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/relocation/fsupq_alt.ma".
+include "basic_2/relocation/fquq_alt.ma".
include "basic_2/static/ssta.ma".
include "basic_2/reduction/cpx.ma".
(* Properties on supclosure *************************************************)
-lemma fsup_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+lemma fqu_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=3 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
+/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
[ #I #G #L #V2 #U2 #HVU2
elim (lift_total U2 0 1)
- /4 width=9 by fsup_drop, cpx_append, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
+ /4 width=9 by fqu_drop, cpx_append, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
elim (lift_total T2 0 (e+1))
- /3 width=11 by cpx_lift, fsup_drop, ex2_intro/
+ /3 width=11 by cpx_lift, fqu_drop, ex2_intro/
]
qed-.
-lemma fsup_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
- ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
-/3 width=5 by fsup_cpx_trans, ssta_cpx/ qed-.
+lemma fqu_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
+ ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+/3 width=5 by fqu_cpx_trans, ssta_cpx/ qed-.
-lemma fsupq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (fsup_cpx_trans … HT12 … HTU2) /3 width=3 by fsup_fsupq, ex2_intro/
+lemma fquq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpx_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma fsupq_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
- ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-/3 width=5 by fsupq_cpx_trans, ssta_cpx/ qed-.
+lemma fquq_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
+ ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+/3 width=5 by fquq_cpx_trans, ssta_cpx/ qed-.
(**************************************************************************)
include "basic_2/notation/relations/btpred_8.ma".
-include "basic_2/relocation/fsupq.ma".
+include "basic_2/relocation/fquq.ma".
include "basic_2/reduction/lpx.ma".
(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpb_fsupq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2
-| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2
-| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1
+| fpb_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2
+| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2
+| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1
.
interpretation
(**************************************************************************)
include "basic_2/notation/relations/btpredproper_8.ma".
-include "basic_2/relocation/fsupq_alt.ma".
+include "basic_2/relocation/fquq_alt.ma".
include "basic_2/reduction/fpb.ma".
(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
inductive fpbc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbc_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2
-| fpbc_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2
+| fpbc_fqu: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2
+| fpbc_cpx: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2
.
interpretation
(* Basic properties *********************************************************)
lemma fpbc_fpb: ∀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 fpb_fsupq, fpb_cpx, fsup_fsupq/
+/3 width=1 by fpb_fquq, fpb_cpx, fqu_fquq/
qed.
lemma cpr_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
+ ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
/3 width=1 by fpbc_cpx, cpr_cpx/ qed.
(* Inversion lemmas on "big tree" parallel reduction for closures ***********)
lemma fpb_inv_fpbc: ∀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 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2.
+ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
+ ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = 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 (fsupq_inv_gen … H) -H [| * ]
- /3 width=1 by fpbc_fsup, and3_intro, or_introl, 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/
]
(* *)
(**************************************************************************)
-include "basic_2/relocation/fsupq_alt.ma".
+include "basic_2/relocation/fquq_alt.ma".
include "basic_2/relocation/ldrop_lpx_sn.ma".
include "basic_2/reduction/cpr_lift.ma".
include "basic_2/reduction/lpr.ma".
(* Properties on context-sensitive parallel reduction for terms *************)
-lemma fsup_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
- ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+lemma fqu_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
#G #L #K #U #T #e #HLK #HUT #U2 #HU2
elim (lift_total U2 0 (e+1)) #T2 #HUT2
-lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fsup_drop, ex3_2_intro/
+lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/
qed-.
-lemma fsupq_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
- ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (fsup_cpr_trans … HT12 … HTU2) /3 width=5 by fsup_fsupq, ex3_2_intro/
+lemma fquq_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_cpr_trans … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/
| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
]
qed-.
(**************************************************************************)
include "basic_2/grammar/lpx_sn_lpx_sn.ma".
-include "basic_2/substitution/fsupp.ma".
+include "basic_2/substitution/fqup.ma".
include "basic_2/reduction/lpr_ldrop.ma".
(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
-lapply (fsupp_lref … G … HLK0) -HLK0 #HLK0
+lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
-lapply (fsupp_lref … G … HLK0) -HLK0 #HLK0
+lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
qed-.
theorem cpr_conf_lpr: ∀G. lpx_sn_confluent (cpr G) (cpr G).
-#G #L0 #T0 @(fsupp_wf_ind … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [|*]
+#G #L0 #T0 @(fqup_wf_ind … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [|*]
[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpr_inv_atom1 … H1) -H1
elim (cpr_inv_atom1 … H2) -H2
(* Properties on supclosure *************************************************)
-lemma fsup_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
+lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_flat_dx, lpx_pair, ex3_2_intro/
+/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
#K2 #W2 #HLK2 #HVW2 #H destruct
- /3 width=5 by fsup_fsupq, cpx_pair_sn, fsup_bind_dx, ex3_2_intro/
+ /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
- /3 width=7 by fsup_drop, ex3_2_intro/
+ /3 width=7 by fqu_drop, ex3_2_intro/
]
qed-.
-lemma fsupq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (fsup_lpx_trans … HT12 … HLK2) /3 width=5 by fsup_fsupq, ex3_2_intro/
+lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma lpx_fsup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=7 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpx_pair, ex3_2_intro/
+/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
#K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
- /4 width=7 by cpx_delta, fsup_drop, ldrop_ldrop, ex3_2_intro/
+ /4 width=7 by cpx_delta, fqu_drop, ldrop_ldrop, ex3_2_intro/
| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
- /3 width=5 by fsup_drop, ex3_2_intro/
+ /3 width=5 by fqu_drop, ex3_2_intro/
]
qed-.
-lemma lpx_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fsupq_inv_gen … H) -H
-[ #HT12 elim (lpx_fsup_trans … HT12 … HKL1) /3 width=5 by fsup_fsupq, ex3_2_intro/
+lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
+[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_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/supterm_6.ma".
+include "basic_2/grammar/cl_weight.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+(* activate genv *)
+inductive fqu: tri_relation genv lenv term ≝
+| fqu_lref_O : ∀I,G,L,V. fqu G (L.ⓑ{I}V) (#0) G L V
+| fqu_pair_sn: ∀I,G,L,V,T. fqu G L (②{I}V.T) G L V
+| fqu_bind_dx: ∀a,I,G,L,V,T. fqu G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
+| fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T
+| fqu_drop : ∀G,L,K,T,U,e.
+ ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fqu G L U G K T
+.
+
+interpretation
+ "structural successor (closure)"
+ 'SupTerm G1 L1 T1 G2 L2 T2 = (fqu G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fqu_drop_lt: ∀G,L,K,T,U,e. 0 < e →
+ ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fqu G L U G K T.
+#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fqu_drop/
+qed.
+
+lemma fqu_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄.
+/3 width=3 by fqu_drop, ldrop_ldrop, lift_lref_ge_minus/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fqu_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
+#G #L #K #T #U #e #HLK #HTU
+lapply (ldrop_fwd_lw_lt … HLK ?) -HLK // #HKL
+lapply (lift_fwd_tw … HTU) -e #H
+normalize in ⊢ (?%%); /2 width=1 by lt_minus_to_plus/
+qed-.
+
+fact fqu_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀i. T1 = #i → |L2| < |L1|.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[1: normalize //
+|3: #a
+|5: /2 width=4 by ldrop_fwd_length_lt4/
+] #I #G #L #V #T #j #H destruct
+qed-.
+
+lemma fqu_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, T2⦄ → |L2| < |L1|.
+/2 width=7 by fqu_fwd_length_lref1_aux/
+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/suptermopt_6.ma".
+include "basic_2/relocation/fqu.ma".
+
+(* OPTIONAL SUPCLOSURE ******************************************************)
+
+(* activate genv *)
+inductive fquq: tri_relation genv lenv term ≝
+| fquq_lref_O : ∀I,G,L,V. fquq G (L.ⓑ{I}V) (#0) G L V
+| fquq_pair_sn: ∀I,G,L,V,T. fquq G L (②{I}V.T) G L V
+| fquq_bind_dx: ∀a,I,G,L,V,T. fquq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
+| fquq_flat_dx: ∀I,G, L,V,T. fquq G L (ⓕ{I}V.T) G L T
+| fquq_drop : ∀G,L,K,T,U,e.
+ ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T
+.
+
+interpretation
+ "optional structural successor (closure)"
+ 'SupTermOpt G1 L1 T1 G2 L2 T2 = (fquq G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fquq_refl: tri_reflexive … fquq.
+/2 width=3 by fquq_drop/ qed.
+
+lemma fqu_fquq: ∀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 -L1 -L2 -T1 -T2 // /2 width=3 by fquq_drop/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fquq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /2 width=1 by lt_to_le/
+#G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1
+lapply (ldrop_fwd_lw … HLK1) -HLK1
+lapply (lift_fwd_tw … HTU1) -HTU1
+/2 width=1 by le_plus, le_n/
+qed-.
+
+fact fquq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀i. T1 = #i → |L2| ≤ |L1|.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
+[ #a #I #G #L #V #T #j #H destruct
+| #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #i #H destruct
+ /2 width=3 by ldrop_fwd_length_le4/
+]
+qed-.
+
+lemma fquq_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃⸮ ⦃G2, L2, T2⦄ → |L2| ≤ |L1|.
+/2 width=7 by fquq_fwd_length_lref1_aux/
+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/suptermoptalt_6.ma".
+include "basic_2/relocation/fquq.ma".
+
+(* OPTIONAL SUPCLOSURE ******************************************************)
+
+(* alternative definition of fquq *)
+definition fquqa: tri_relation genv lenv term ≝ tri_RC … fqu.
+
+interpretation
+ "optional structural successor (closure) alternative"
+ 'SupTermOptAlt G1 L1 T1 G2 L2 T2 = (fquqa G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fquqa_refl: tri_reflexive … fquqa.
+// qed.
+
+lemma fquqa_drop: ∀G,L,K,T,U,e.
+ ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
+#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
+/3 width=5 by fqu_drop_lt, or_introl/ #H destruct
+>(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
+qed.
+
+(* Main properties **********************************************************)
+
+theorem fquq_fquqa: ∀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
+/2 width=3 by fquqa_drop, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, or_introl/
+qed.
+
+(* Main inversion properties ************************************************)
+
+theorem fquqa_inv_fquq: ∀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 -H /2 width=1 by fqu_fquq/
+* #H1 #H2 #H3 destruct //
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fquq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2).
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_fquqa … H) -H [| * ]
+/2 width=1 by 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/notation/relations/supterm_6.ma".
-include "basic_2/grammar/cl_weight.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* SUPCLOSURE ***************************************************************)
-
-(* activate genv *)
-inductive fsup: tri_relation genv lenv term ≝
-| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V
-| fsup_pair_sn: ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V
-| fsup_bind_dx: ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
-| fsup_flat_dx: ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T
-| fsup_drop : ∀G,L,K,T,U,e.
- ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fsup G L U G K T
-.
-
-interpretation
- "structural successor (closure)"
- 'SupTerm G1 L1 T1 G2 L2 T2 = (fsup G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fsup_drop_lt: ∀G,L,K,T,U,e. 0 < e →
- ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsup G L U G K T.
-#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fsup_drop/
-qed.
-
-lemma fsup_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄.
-/3 width=3 by fsup_drop, ldrop_ldrop, lift_lref_ge_minus/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fsup_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
-#G #L #K #T #U #e #HLK #HTU
-lapply (ldrop_fwd_lw_lt … HLK ?) -HLK // #HKL
-lapply (lift_fwd_tw … HTU) -e #H
-normalize in ⊢ (?%%); /2 width=1 by lt_minus_to_plus/
-qed-.
-
-fact fsup_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀i. T1 = #i → |L2| < |L1|.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[1: normalize //
-|3: #a
-|5: /2 width=4 by ldrop_fwd_length_lt4/
-] #I #G #L #V #T #j #H destruct
-qed-.
-
-lemma fsup_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, T2⦄ → |L2| < |L1|.
-/2 width=7 by fsup_fwd_length_lref1_aux/
-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/suptermopt_6.ma".
-include "basic_2/relocation/fsup.ma".
-
-(* OPTIONAL SUPCLOSURE ******************************************************)
-
-(* activate genv *)
-inductive fsupq: tri_relation genv lenv term ≝
-| fsupq_lref_O : ∀I,G,L,V. fsupq G (L.ⓑ{I}V) (#0) G L V
-| fsupq_pair_sn: ∀I,G,L,V,T. fsupq G L (②{I}V.T) G L V
-| fsupq_bind_dx: ∀a,I,G,L,V,T. fsupq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
-| fsupq_flat_dx: ∀I,G, L,V,T. fsupq G L (ⓕ{I}V.T) G L T
-| fsupq_drop : ∀G,L,K,T,U,e.
- ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsupq G L U G K T
-.
-
-interpretation
- "optional structural successor (closure)"
- 'SupTermOpt G1 L1 T1 G2 L2 T2 = (fsupq G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fsupq_refl: tri_reflexive … fsupq.
-/2 width=3 by fsupq_drop/ qed.
-
-lemma fsup_fsupq: ∀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 -L1 -L2 -T1 -T2 // /2 width=3 by fsupq_drop/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fsupq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /2 width=1 by lt_to_le/
-#G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1
-lapply (ldrop_fwd_lw … HLK1) -HLK1
-lapply (lift_fwd_tw … HTU1) -HTU1
-/2 width=1 by le_plus, le_n/
-qed-.
-
-fact fsupq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀i. T1 = #i → |L2| ≤ |L1|.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
-[ #a #I #G #L #V #T #j #H destruct
-| #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #i #H destruct
- /2 width=3 by ldrop_fwd_length_le4/
-]
-qed-.
-
-lemma fsupq_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃⸮ ⦃G2, L2, T2⦄ → |L2| ≤ |L1|.
-/2 width=7 by fsupq_fwd_length_lref1_aux/
-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/suptermoptalt_6.ma".
-include "basic_2/relocation/fsupq.ma".
-
-(* OPTIONAL SUPCLOSURE ******************************************************)
-
-(* alternative definition of fsupq *)
-definition fsupqa: tri_relation genv lenv term ≝ tri_RC … fsup.
-
-interpretation
- "optional structural successor (closure) alternative"
- 'SupTermOptAlt G1 L1 T1 G2 L2 T2 = (fsupqa G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fsupqa_refl: tri_reflexive … fsupqa.
-// qed.
-
-lemma fsupqa_drop: ∀G,L,K,T,U,e.
- ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
-#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
-/3 width=5 by fsup_drop_lt, or_introl/ #H destruct
->(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
-qed.
-
-(* Main properties **********************************************************)
-
-theorem fsupq_fsupqa: ∀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
-/2 width=3 by fsupqa_drop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/
-qed.
-
-(* Main inversion properties ************************************************)
-
-theorem fsupqa_inv_fsupq: ∀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 -H /2 width=1 by fsup_fsupq/
-* #H1 #H2 #H3 destruct //
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma fsupq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2).
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fsupq_fsupqa … H) -H [| * ]
-/2 width=1 by 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/notation/relations/suptermplus_6.ma".
+include "basic_2/relocation/fqu.ma".
+
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
+
+definition fqup: tri_relation genv lenv term ≝ tri_TC … fqu.
+
+interpretation "plus-iterated structural successor (closure)"
+ 'SupTermPlus G1 L1 T1 G2 L2 T2 = (fqup G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fqu_fqup: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
+/2 width=1 by tri_inj/ qed.
+
+lemma fqup_strap1: ∀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⦄.
+/2 width=5 by tri_step/ qed.
+
+lemma fqup_strap2: ∀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⦄.
+/2 width=5 by tri_TC_strap/ qed.
+
+lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+ ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct
+[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 //
+| /3 width=5 by fqup_strap2, fqu_drop_lt/
+]
+qed-.
+
+lemma fqup_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄.
+/3 width=6 by fqu_lref_O, fqu_fqup, lift_lref_ge, fqup_ldrop/ qed.
+
+lemma fqup_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄.
+/2 width=1 by fqu_pair_sn, fqu_fqup/ qed.
+
+lemma fqup_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄.
+/2 width=1 by fqu_bind_dx, fqu_fqup/ qed.
+
+lemma fqup_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄.
+/2 width=1 by fqu_flat_dx, fqu_fqup/ qed.
+
+lemma fqup_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄.
+/2 width=5 by fqu_pair_sn, fqup_strap1/ qed.
+
+lemma fqup_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄.
+/2 width=5 by fqu_flat_dx, fqup_strap1/ qed.
+
+lemma fqup_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄.
+/2 width=5 by fqu_bind_dx, fqup_strap1/ qed.
+
+(* Basic eliminators ********************************************************)
+
+lemma fqup_ind: ∀G1,L1,T1. ∀R:relation3 ….
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2.
+#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+@(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
+qed-.
+
+lemma fqup_ind_dx: ∀G2,L2,T2. ∀R:relation3 ….
+ (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G1 L1 T1) →
+ (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G1 L1 T1.
+#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fqup_fwd_fw: ∀G1,G2,L1,L2,T1,T2.
+ ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+/3 width=3 by fqu_fwd_fw, transitive_lt/
+qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma fqup_wf_ind: ∀R:relation3 …. (
+ ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
+ ) → ∀G1,L1,T1. R G1 L1 T1.
+#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/
+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/substitution/fqup.ma".
+
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
+
+(* Main propertis ***********************************************************)
+
+theorem fqup_trans: tri_transitive … fqup.
+/2 width=5 by tri_TC_transitive/ 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/suptermstar_6.ma".
+include "basic_2/relocation/fquq.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+definition fqus: tri_relation genv lenv term ≝ tri_TC … fquq.
+
+interpretation "star-iterated structural successor (closure)"
+ 'SupTermStar G1 L1 T1 G2 L2 T2 = (fqus G1 L1 T1 G2 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fqus_ind: ∀G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 →
+ (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2.
+#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+@(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) //
+qed-.
+
+lemma fqus_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 →
+ (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G1 L1 T1.
+#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fqus_refl: tri_reflexive … fqus.
+/2 width=1 by tri_inj/ qed.
+
+lemma fquq_fqus: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
+/2 width=1 by tri_inj/ qed.
+
+lemma fqus_strap1: ∀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⦄.
+/2 width=5 by tri_step/ qed.
+
+lemma fqus_strap2: ∀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⦄.
+/2 width=5 by tri_TC_strap/ qed.
+
+lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
+ ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+ ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
+#G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind … H) -G2 -K2 -T2
+/3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fqus_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -L2 -T2
+/3 width=3 by fquq_fwd_fw, transitive_le/
+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/substitution/fqus.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+(* Main properties **********************************************************)
+
+theorem fqus_trans: tri_transitive … fqus.
+/2 width=5 by tri_TC_transitive/ 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/suptermplus_6.ma".
-include "basic_2/relocation/fsup.ma".
-
-(* PLUS-ITERATED SUPCLOSURE *************************************************)
-
-definition fsupp: tri_relation genv lenv term ≝ tri_TC … fsup.
-
-interpretation "plus-iterated structural successor (closure)"
- 'SupTermPlus G1 L1 T1 G2 L2 T2 = (fsupp G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fsup_fsupp: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-/2 width=1 by tri_inj/ qed.
-
-lemma fsupp_strap1: ∀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⦄.
-/2 width=5 by tri_step/ qed.
-
-lemma fsupp_strap2: ∀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⦄.
-/2 width=5 by tri_TC_strap/ qed.
-
-lemma fsupp_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
- ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄.
-#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct
-[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 //
-| /3 width=5 by fsupp_strap2, fsup_drop_lt/
-]
-qed-.
-
-lemma fsupp_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄.
-/3 width=6 by fsup_lref_O, fsup_fsupp, lift_lref_ge, fsupp_ldrop/ qed.
-
-lemma fsupp_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄.
-/2 width=1 by fsup_pair_sn, fsup_fsupp/ qed.
-
-lemma fsupp_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄.
-/2 width=1 by fsup_bind_dx, fsup_fsupp/ qed.
-
-lemma fsupp_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄.
-/2 width=1 by fsup_flat_dx, fsup_fsupp/ qed.
-
-lemma fsupp_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄.
-/2 width=5 by fsup_pair_sn, fsupp_strap1/ qed.
-
-lemma fsupp_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄.
-/2 width=5 by fsup_flat_dx, fsupp_strap1/ qed.
-
-lemma fsupp_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄.
-/2 width=5 by fsup_bind_dx, fsupp_strap1/ qed.
-
-(* Basic eliminators ********************************************************)
-
-lemma fsupp_ind: ∀G1,L1,T1. ∀R:relation3 ….
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
-@(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
-qed-.
-
-lemma fsupp_ind_dx: ∀G2,L2,T2. ∀R:relation3 ….
- (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G1 L1 T1) →
- (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
-@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fsupp_fwd_fw: ∀G1,G2,L1,L2,T1,T2.
- ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
-/3 width=3 by fsup_fwd_fw, transitive_lt/
-qed-.
-
-(* Advanced eliminators *****************************************************)
-
-lemma fsupp_wf_ind: ∀R:relation3 …. (
- ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
- ) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fsupp_fwd_fw/
-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/substitution/fsupp.ma".
-
-(* PLUS-ITERATED SUPCLOSURE *************************************************)
-
-(* Main propertis ***********************************************************)
-
-theorem fsupp_trans: tri_transitive … fsupp.
-/2 width=5 by tri_TC_transitive/ 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/suptermstar_6.ma".
-include "basic_2/relocation/fsupq.ma".
-
-(* STAR-ITERATED SUPCLOSURE *************************************************)
-
-definition fsups: tri_relation genv lenv term ≝ tri_TC … fsupq.
-
-interpretation "star-iterated structural successor (closure)"
- 'SupTermStar G1 L1 T1 G2 L2 T2 = (fsups G1 L1 T1 G2 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma fsups_ind: ∀G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 →
- (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
-@(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) //
-qed-.
-
-lemma fsups_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 →
- (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
-@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma fsups_refl: tri_reflexive … fsups.
-/2 width=1 by tri_inj/ qed.
-
-lemma fsupq_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=1 by tri_inj/ qed.
-
-lemma fsups_strap1: ∀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⦄.
-/2 width=5 by tri_step/ qed.
-
-lemma fsups_strap2: ∀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⦄.
-/2 width=5 by tri_TC_strap/ qed.
-
-lemma fsups_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
- ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
- ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
-#G1 #G2 #K1 #K2 #T1 #T2 #H @(fsups_ind … H) -G2 -K2 -T2
-/3 width=5 by fsups_strap1, fsupq_fsups, fsupq_drop/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fsups_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2
-/3 width=3 by fsupq_fwd_fw, transitive_le/
-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/substitution/fsups.ma".
-
-(* STAR-ITERATED SUPCLOSURE *************************************************)
-
-(* Main properties **********************************************************)
-
-theorem fsups_trans: tri_transitive … fsups.
-/2 width=5 by tri_TC_transitive/ qed-.
}
]
[ { "iterated structural successor for closures" * } {
- [ "fsups ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fsups_fsups" * ]
- [ "fsupp ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fsupp_fsupp" * ]
+ [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_fqus" * ]
+ [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
}
]
[ { "generic local env. slicing" * } {
class "orange"
[ { "relocation" * } {
[ { "structural successor for closures" * } {
- [ "fsup ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fsupq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fsupq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
+ [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
}
]
[ { "global env. slicing" * } {
projects / helm.git / commitdiff