@printf ' SUMMARY $(1)\n'
@printf 'name "$$(basename $$(@F))"\n\n' > $$@
@printf 'table {\n' >> $$@
- @printf ' class "gray" [ "category"\n' >> $$@
+ @printf ' class "gray" [ "category"\n' >> $$@
@printf ' [ "objects" * ]\n' >> $$@
@printf ' ]\n' >> $$@
- @printf ' class "water" [ "sizes"\n' >> $$@
+ @printf ' class "water" [ "sizes"\n' >> $$@
@printf ' [ "files" "$$(S1)" ]\n' >> $$@
@printf ' [ "characters" "$$(S2)" ]\n' >> $$@
@printf ' [ "nodes" "$$(S4)" ]\n' >> $$@
@printf ' ]\n' >> $$@
- @printf ' class "grass" [ "propositions"\n' >> $$@
+ @printf ' class "green" [ "propositions"\n' >> $$@
@printf ' [ "theorems" "$$(P1)" ]\n' >> $$@
@printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@
@printf ' [ "total" "$$(P3)" ]\n' >> $$@
@printf ' ]\n' >> $$@
- @printf ' class "yellow" [ "concepts"\n' >> $$@
+ @printf ' class "grass" [ "concepts"\n' >> $$@
@printf ' [ "declared" "$$(C1)" ]\n' >> $$@
@printf ' [ "defined" "$$(C2)" ]\n' >> $$@
@printf ' [ "total" "$$(C3)" ]\n' >> $$@
--- /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/rt_transition/lfpx.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+
+
+
+(* Properties on supclosure *************************************************)
+
+lemma lpx_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
+ /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+ #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
+ #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
+ /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
+#h #o #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_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-.
+
+lemma lpxs_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2.
+#h #o #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_fquq_trans … HT2 … HK1) -K
+ /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpxs_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2.
+#h #o #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_fqup_trans … HT2 … HK1) -K
+ /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
+]
+qed-.
+
+lemma lpxs_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2.
+#h #o #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_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
+/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
+qed-.
+
+lemma lpxs_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1
+ #K0 #V0 #H1KL1 #_ #H destruct
+ elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
+ #K1 #H #H2KL1 lapply (drop_inv_O2 … H) -H #H destruct
+ /2 width=4 by fqu_lref_O, ex3_intro/
+| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
+ [ elim (lleq_inv_bind … H)
+ | elim (lleq_inv_flat … H)
+ ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
+| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/
+| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
+ /2 width=4 by fqu_flat_dx, ex3_intro/
+| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1
+ elim (drop_O1_le (Ⓕ) (k+1) K1)
+ [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
+ #H2KL elim (lpxs_drop_trans_O1 … H1KL1 … HL1) -L1
+ #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct
+ /3 width=4 by fqu_drop, ex3_intro/
+ | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o
+ lapply (lleq_fwd_length … H2KL1) //
+ ]
+]
+qed-.
+
+lemma lpxs_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fquq_inv_gen … H) -H
+[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqu_fquq, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
+
+lemma lpxs_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqu_fqup, ex3_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
+ #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L
+ /3 width=5 by fqup_strap1, ex3_intro/
+]
+qed-.
+
+lemma lpxs_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
+elim (fqus_inv_gen … H) -H
+[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
+ /3 width=4 by fqup_fqus, ex3_intro/
+| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
+]
+qed-.
(* Basic_1: was just: sn3_abbr *)
(* Basic_2A1: was: csx_lref_bind *)
-lemma csx_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V →
- ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄.
+lemma csx_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V →
+ ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄.
#h #o #I #G #L #K #V #i #HLK #HV
@csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H
[ #H destruct elim Hi //
(* Basic_1: was: sn3_gen_def *)
(* Basic_2A1: was: csx_inv_lref_bind *)
-lemma csx_inv_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V →
- ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄.
+lemma csx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V →
+ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄.
#h #o #I #G #L #K #V #i #HLK #Hi
elim (lifts_total V (𝐔❴⫯i❵))
/4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/
∀V2. ⬆*[⫯i] V1 ≡ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.V2⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.#i⦄.
#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
-[ /4 width=11 by csx_inv_lifts, csx_lref_drops, drops_isuni_fwd_drop2/
+[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn … H1T) #HV
lapply (csx_fwd_flat_dx … H1T) #H2T
+++ /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/fpbs.ma".
-include "basic_2/computation/csx_lleq.ma".
-include "basic_2/computation/csx_lpx.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Advanced properties ******************************************************)
-
-lemma csx_fpb_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2.
-#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
-/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_lleq_conf/
-qed-.
-
-lemma csx_fpbs_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2.
-#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
-/2 width=5 by csx_fpb_conf/
-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/fpbs.ma".
+include "basic_2/computation/csx_lleq.ma".
+include "basic_2/computation/csx_lpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Advanced properties ******************************************************)
+
+lemma csx_fpb_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2.
+#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
+/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_lleq_conf/
+qed-.
+
+lemma csx_fpbs_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, o] T2.
+#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
+/2 width=5 by csx_fpb_conf/
+qed-.
+++ /dev/null
-(* Properties on supclosure *************************************************)
-
-lemma lpx_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
- /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
-| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
- #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
- #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
- /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
-#h #o #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_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-.
-
-lemma lpxs_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2.
-#h #o #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_fquq_trans … HT2 … HK1) -K
- /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
-]
-qed-.
-
-lemma lpxs_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2.
-#h #o #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_fqup_trans … HT2 … HK1) -K
- /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
-]
-qed-.
-
-lemma lpxs_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, o] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2.
-#h #o #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_fquq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
-/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
-qed-.
-
-lemma lpxs_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1
- #K0 #V0 #H1KL1 #_ #H destruct
- elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
- #K1 #H #H2KL1 lapply (drop_inv_O2 … H) -H #H destruct
- /2 width=4 by fqu_lref_O, ex3_intro/
-| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
- [ elim (lleq_inv_bind … H)
- | elim (lleq_inv_flat … H)
- ] -H /2 width=4 by fqu_pair_sn, ex3_intro/
-| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H
- /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/
-| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
- /2 width=4 by fqu_flat_dx, ex3_intro/
-| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1
- elim (drop_O1_le (Ⓕ) (k+1) K1)
- [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
- #H2KL elim (lpxs_drop_trans_O1 … H1KL1 … HL1) -L1
- #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct
- /3 width=4 by fqu_drop, ex3_intro/
- | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o
- lapply (lleq_fwd_length … H2KL1) //
- ]
-]
-qed-.
-
-lemma lpxs_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fquq_inv_gen … H) -H
-[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqu_fquq, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
-
-lemma lpxs_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqu_fqup, ex3_intro/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1
- #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L
- /3 width=5 by fqup_strap1, ex3_intro/
-]
-qed-.
-
-lemma lpxs_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
-elim (fqus_inv_gen … H) -H
-[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
- /3 width=4 by fqup_fqus, ex3_intro/
-| * #HG #HL #HT destruct /2 width=4 by ex3_intro/
-]
-qed-.
#h #o #G #L1 #s @lfsx_intro
#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
[ #H1 #H2 destruct //
-| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
- /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort_gen, frees_inv_sort/
+| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct
+ /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort, frees_inv_sort/
]
qed.
#h #o #G #L1 #s @lfsx_intro
#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H *
[ #H1 #H2 destruct //
-| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
- /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref_gen, frees_inv_gref/
+| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct
+ /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref, frees_inv_gref/
]
qed.
-cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
/2 width=1 by lfxs_atom/ qed.
(* Basic_2A1: uses: lleq_sort *)
-lemma lfdeq_sort: ∀h,o,I,L1,L2,V1,V2,s.
- L1 â\89¡[h, o, â\8b\86s] L2 â\86\92 L1.â\93\91{I}V1 â\89¡[h, o, â\8b\86s] L2.â\93\91{I}V2.
+lemma lfdeq_sort: ∀h,o,I1,I2,L1,L2,s.
+ L1 â\89¡[h, o, â\8b\86s] L2 â\86\92 L1.â\93\98{I1} â\89¡[h, o, â\8b\86s] L2.â\93\98{I2}.
/2 width=1 by lfxs_sort/ qed.
-lemma lfdeq_pair: ∀h,o,I,L1,L2,V.
- L1 ≡[h, o, V] L2 → L1.ⓑ{I}V ≡[h, o, #0] L2.ⓑ{I}V.
+lemma lfdeq_pair: ∀h,o,I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 → V1 ≡[h, o] V2 →
+ L1.ⓑ{I}V1 ≡[h, o, #0] L2.ⓑ{I}V2.
/2 width=1 by lfxs_pair/ qed.
-
+(*
lemma lfdeq_unit: ∀h,o,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 →
L1.ⓤ{I} ≡[h, o, #0] L2.ⓤ{I}.
/2 width=3 by lfxs_unit/ qed.
-
-lemma lfdeq_lref: ∀h,o,I,L1,L2,V1,V2,i.
- L1 â\89¡[h, o, #i] L2 â\86\92 L1.â\93\91{I}V1 â\89¡[h, o, #⫯i] L2.â\93\91{I}V2.
+*)
+lemma lfdeq_lref: ∀h,o,I1,I2,L1,L2,i.
+ L1 â\89¡[h, o, #i] L2 â\86\92 L1.â\93\98{I1} â\89¡[h, o, #⫯i] L2.â\93\98{I2}.
/2 width=1 by lfxs_lref/ qed.
(* Basic_2A1: uses: lleq_gref *)
-lemma lfdeq_gref: ∀h,o,I,L1,L2,V1,V2,l.
- L1 â\89¡[h, o, §l] L2 â\86\92 L1.â\93\91{I}V1 â\89¡[h, o, §l] L2.â\93\91{I}V2.
+lemma lfdeq_gref: ∀h,o,I1,I2,L1,L2,l.
+ L1 â\89¡[h, o, §l] L2 â\86\92 L1.â\93\98{I1} â\89¡[h, o, §l] L2.â\93\98{I2}.
/2 width=1 by lfxs_gref/ qed.
lemma lfdeq_bind_repl_dx: ∀h,o,I,I1,L1,L2.∀T:term.
lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≡[h, o, T] ⋆ → Y1 = ⋆.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
-
+(*
lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 →
∨∨ Y1 = ⋆ ∧ Y2 = ⋆
| ∃∃I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 &
#h #o #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H *
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
qed-.
-
+*)
lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≡[h, o, #⫯i] Y2 →
(Y1 = ⋆ ∧ Y2 = ⋆) ∨
∃∃I1,I2,L1,L2. L1 ≡[h, o, #i] L2 &
]
[ { "strongly normalizing rt-computation" * } {
[ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
- [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
- [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_theq_vector" + "csx_aaa" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ]
+ [ "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
+ [ "csx_lleq" + "csx_lpxs" + "csx_fpbs" * ]
}
]
[ { "parallel qrst-computation" * } {
]
*)
[ { "uncounted context-sensitive rt-computation" * } {
-(*
- [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
-*)
-(*
[ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
-*)
+ [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
[ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
projects / helm.git / commitdiff