TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib
-PACKAGES := ground_2 basic_2 apps_2
+PACKAGES := ground_2 basic_2 apps_2 alpha_1
+XPACKAGES := ground_2 basic_2
LDWS := $(shell find -name "*.ldw.xml")
TBLS := $(shell find -name "*.tbl")
$(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG))))
+# XMAS #######################################################################
+
+define XMAS_TEMPLATE
+ XMAS += $$(MAS_$(1))
+endef
+
+$(foreach PKG, $(XPACKAGES), $(eval $(call XMAS_TEMPLATE,$(PKG))))
+
# xoa ########################################################################
xoa: $(XOA_TARGETS)
contrib:
@echo " TAR -czf $(CONTRIB).tar.gz root *.ma"
- $(H)tar -czf $(CONTRIB).tar.gz root $(MAS)
+ $(H)tar -czf $(CONTRIB).tar.gz root $(XMAS)
##############################################################################
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* THE FORMAL SYSTEM α: MATITA SOURCE FILES
+ * Initial invocation : - Patience on me to gain peace and perfection! -
+ * Developed since : 2014 July 25
+ *)
+
+include "ground_2/lib/bool.ma".
+include "ground_2/lib/arith.ma".
+
+(* ITEMS ********************************************************************)
+
+(* unary items *)
+inductive item1: Type[0] ≝
+ | Char: nat → item1 (* character: starting at 0 *)
+ | LRef: nat → item1 (* reference by index: starting at 0 *)
+ | GRef: nat → item1 (* reference by position: starting at 0 *)
+ | Decl: item1 (* global abstraction *)
+.
+
+(* binary items *)
+inductive item2: Type[0] ≝
+ | Abst: item2 (* local abstraction *)
+ | Abbr: bool → item2 (* local (Ⓣ) or global (Ⓕ) abbreviation *)
+ | Proj: bool → item2 (* local (Ⓣ) or global (Ⓕ) projection *)
+.
--- /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/constructors/snitem2_3.ma".
+include "basic_2/notation/constructors/star_0.ma".
+include "basic_2/notation/constructors/snabstpos_2.ma".
+include "basic_2/notation/constructors/snabbr_3.ma".
+include "basic_2/notation/constructors/snabbrpos_2.ma".
+include "basic_2/notation/constructors/snabbrneg_2.ma".
+include "alpha_1/notation/constructors/snitem1_2.ma".
+include "alpha_1/notation/constructors/snstar_2.ma".
+include "alpha_1/notation/constructors/snlref_2.ma".
+include "alpha_1/notation/constructors/sngref_2.ma".
+include "alpha_1/notation/constructors/snabstneg_1.ma".
+include "alpha_1/notation/constructors/snproj_3.ma".
+include "alpha_1/notation/constructors/snprojpos_2.ma".
+include "alpha_1/notation/constructors/snprojneg_2.ma".
+include "alpha_1/grammar/item.ma".
+
+(* TERMS ********************************************************************)
+
+(* terms *)
+inductive term: Type[0] ≝
+ | TAtom: term (* atomic item construction *)
+ | TUnit: item1 → term → term (* unary item construction *)
+ | TPair: item2 → term → term → term (* binary item construction *)
+.
+
+interpretation "top (term)"
+ 'Star = TAtom.
+
+interpretation "term construction (unary)"
+ 'SnItem1 I T = (TUnit I T).
+
+interpretation "term construction (binary)"
+ 'SnItem2 I T1 T2 = (TPair I T1 T2).
+
+interpretation "character (term)"
+ 'SnStar k T = (TUnit (Char k) T).
+
+interpretation "local reference (term)"
+ 'SnLRef i T = (TUnit (LRef i) T).
+
+interpretation "global reference (term)"
+ 'SnGRef p T = (TUnit (GRef p) T).
+
+interpretation "negative abbreviation (term)"
+ 'SnAbbrNeg T = (TUnit Decl T).
+
+interpretation "positive abstraction (term)"
+ 'SnAbstPos T1 T2 = (TPair Abst T1 T2).
+
+interpretation "abbreviation (term)"
+ 'SnAbbr a T1 T2 = (TPair (Abbr a) T1 T2).
+
+interpretation "positive abbreviation (term)"
+ 'SnAbbrPos T1 T2 = (TPair (Abbr true) T1 T2).
+
+interpretation "negative abbreviation (term)"
+ 'SnAbbrNeg T1 T2 = (TPair (Abbr false) T1 T2).
+
+interpretation "projection (term)"
+ 'SnProj a T1 T2 = (TPair (Proj a) T1 T2).
+
+interpretation "positive projection (term)"
+ 'SnProjPos T1 T2 = (TPair (Proj true) T1 T2).
+
+interpretation "negative projection (term)"
+ 'SnProjNeg T1 T2 = (TPair (Proj false) T1 T2).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "alpha_1/grammar/term.ma".
+
+(* TERMS ********************************************************************)
+
+let rec tappend T U on T ≝ match T with
+[ TAtom ⇒ U
+| TUnit I T ⇒ ①{I}.(tappend T U)
+| TPair I V T ⇒ ②{I}V.(tappend T U)
+].
+
+interpretation "append (term)" 'Append T U = (tappend T U).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( - 𝛌 . break term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnAbstNeg $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( § term 90 p . break term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnGRef $p $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( ① { term 46 I } . break term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnItem1 $I $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( # term 90 i . break term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnLRef $i $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( 𝛑 { term 46 a } break term 55 T1 . break term 55 T2 )"
+ non associative with precedence 55
+ for @{ 'SnProj $a $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( - 𝛑 term 55 T1 . break term 55 T2 )"
+ non associative with precedence 55
+ for @{ 'SnProjNeg $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( + 𝛑 term 55 T1 . break term 55 T2 )"
+ non associative with precedence 55
+ for @{ 'SnProjPos $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM α *****************************************)
+
+notation "hvbox( ⋆ term 90 k . break term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnStar $k $T }.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/dpredstar_6.ma".
+include "basic_2/notation/relations/dpredstar_7.ma".
include "basic_2/static/da.ma".
include "basic_2/unfold/lstas.ma".
include "basic_2/computation/cprs.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-definition cpds: ∀h. sd h → relation4 genv lenv term term ≝
- λh,g,G,L,T1,T2.
- ∃∃T,l1,l2. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2.
+definition cpds: ∀h. sd h → nat → relation4 genv lenv term term ≝
+ λh,g,l2,G,L,T1,T2.
+ ∃∃T,l1. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2.
interpretation "decomposed extended parallel computation (term)"
- 'DPRedStar h g G L T1 T2 = (cpds h g G L T1 T2).
+ 'DPRedStar h g l G L T1 T2 = (cpds h g l G L T1 T2).
(* Basic properties *********************************************************)
lemma sta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T →
- ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-/3 width=7 by sta_lstas, ex4_3_intro/ qed.
+ ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 1] T2.
+/3 width=6 by sta_lstas, ex4_2_intro/ qed.
-lemma lstas_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-/2 width=7 by ex4_3_intro/ qed.
+lemma lstas_cpds: ∀h,g,G,L,T1,T2,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
+ ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2] T2.
+/2 width=6 by ex4_2_intro/ qed.
-lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-/2 width=7 by lstar_O, ex4_3_intro/ qed.
+lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 →
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2.
+/2 width=6 by lstar_O, ex4_2_intro/ qed.
-lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g] T.
+lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g, 0] T.
/2 width=2 by cprs_cpds/ qed.
-lemma cpds_strap1: ∀h,g,G,L,T1,T,T2.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #G #L #T1 #T #T2 * /3 width=9 by cprs_strap1, ex4_3_intro/
+lemma cpds_strap1: ∀h,g,G,L,T1,T,T2,l.
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2.
+#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_strap1, ex4_2_intro/
qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpds_fwd_cprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2 →
+ ⦃G, L⦄ ⊢ T1 ➡* T2.
+#h #g #G #L #T1 #T2 *
+#T #l #_ #_ #H lapply (lstas_inv_O … H) -l -H
+#H destruct //
+qed-.
(* Properties on atomic arity assignment for terms **************************)
-lemma cpds_aaa_conf: ∀h,g,G,L. Conf3 … (aaa G L) (cpds h g G L).
-#h #g #G #L #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/
+lemma cpds_aaa_conf: ∀h,g,G,L,l. Conf3 … (aaa G L) (cpds h g l G L).
+#h #g #G #L #l #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/
qed.
(* Advanced properties ******************************************************)
-lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
- ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #G #L #T1 #T #T2 #l #Hl #HT1 *
-#T0 #l0 #l1 #Hl10 #HT #HT0 #HT02
-lapply (da_sta_conf … HT1 … Hl) <minus_plus_m_m #H0T
-lapply (da_mono … H0T … HT) -HT -H0T #H destruct
-/3 width=7 by lstas_step_sn, le_S_S, ex4_3_intro/
+lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l1,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1+1 →
+ ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 →
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l+1] T2.
+#h #g #G #L #T1 #T #T2 #l1 #l #Hl1 #HT1 *
+#T0 #l0 #Hl0 #HTl0 #HT0 #HT02
+lapply (da_sta_conf … HT1 … Hl1) <minus_plus_m_m #HTl1
+lapply (da_mono … HTl0 … HTl1) -HTl0 -HTl1 #H destruct
+/3 width=6 by lstas_step_sn, le_S_S, ex4_2_intro/
qed.
-lemma cpds_cprs_trans: ∀h,g,G,L,T1,T,T2.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #G #L #T1 #T #T2 * /3 width=9 by cprs_trans, ex4_3_intro/
+lemma cpds_cprs_trans: ∀h,g,G,L,T1,T,T2,l.
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2.
+#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_trans, ex4_2_intro/
qed-.
-lemma lstas_cpds_trans: ∀h,g,G,L,T1,T,T2,l1,l2.
+lemma lstas_cpds_trans: ∀h,g,G,L,T1,T,T2,l1,l2,l.
l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
- ⦃G, L⦄ ⊢ T1 •*[h, l2] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2.
-#h #g #G #L #T1 #T #T2 #l1 #l2 #Hl21 #Hl1 #HT1 * #T0 #l3 #l4 #Hl43 #Hl3 #HT0 #HT02
-lapply (lstas_da_conf … HT1 … Hl1) #H0T
-lapply (da_mono … H0T … Hl3) -H0T -Hl3 #H destruct
-lapply (le_minus_to_plus_r … Hl21 Hl43) -Hl21 -Hl43
-/3 width=8 by lstas_trans, ex4_3_intro/
+ ⦃G, L⦄ ⊢ T1 •*[h, l2] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2+l] T2.
+#h #g #G #L #T1 #T #T2 #l1 #l2 #l #Hl21 #HTl1 #HT1 * #T0 #l0 #Hl0 #HTl0 #HT0 #HT02
+lapply (lstas_da_conf … HT1 … HTl1) #HTl12
+lapply (da_mono … HTl12 … HTl0) -HTl12 -HTl0 #H destruct
+lapply (le_minus_to_plus_r … Hl21 Hl0) -Hl21 -Hl0
+/3 width=7 by lstas_trans, ex4_2_intro/
qed-.
(* Advanced inversion lemmas ************************************************)
-lemma cpds_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, g] U2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, g] T2 &
+lemma cpds_inv_abst1: ∀h,g,a,G,L,V1,T1,U2,l. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, g, l] U2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, g, l] T2 &
U2 = ⓛ{a}V2.T2.
-#h #g #a #G #L #V1 #T1 #U2 * #X #l1 #l2 #Hl21 #Hl1 #H1 #H2
+#h #g #a #G #L #V1 #T1 #U2 #l2 * #X #l1 #Hl21 #Hl1 #H1 #H2
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
-/3 width=7 by ex4_3_intro, ex3_2_intro/
+/3 width=6 by ex4_2_intro, ex3_2_intro/
qed-.
-lemma cpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g] ⓛ{a2}W2.T2 →
- ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, g] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
-#h #g #a1 #a2 #G #L #V1 #W2 #T1 #T2 * #X #l1 #l2 #Hl21 #Hl1 #H1 #H2
+lemma cpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2,l. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g, l] ⓛ{a2}W2.T2 →
+ ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, g, l] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
+#h #g #a1 #a2 #G #L #V1 #W2 #T1 #T2 #l2 * #X #l1 #Hl21 #Hl1 #H1 #H2
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
elim (cprs_inv_abbr1 … H2) -H2 *
[ #V2 #U2 #HV12 #HU12 #H destruct
-| /3 width=7 by ex4_3_intro, ex3_intro/
+| /3 width=6 by ex4_2_intro, ex3_intro/
]
qed-.
+lemma cpds_inv_lstas_eq: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 →
+ ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l] T → ⦃G, L⦄ ⊢ T ➡* T2.
+#h #g #G #L #T1 #T2 #l2 *
+#T0 #l1 #_ #_ #HT10 #HT02 #T #HT1
+lapply (lstas_mono … HT10 … HT1) #H destruct //
+qed-.
+
(* Advanced forward lemmas **************************************************)
-lemma cpds_fwd_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
-#h #g #G #L #T1 #T2 * /3 width=5 by cpxs_trans, lstas_cpxs, cprs_cpxs/
+lemma cpds_fwd_cpxs: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 #l * /3 width=5 by cpxs_trans, lstas_cpxs, cprs_cpxs/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem cpds_conf_eq: ∀h,g,G,L,T0,T1,l. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, l] T1 →
+ ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, l] T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
+#h #g #G #L #T0 #T1 #l0 * #U1 #l1 #_ #_ #H1 #HUT1 #T2 * #U2 #l2 #_ #_ #H2 #HUT2 -l1 -l2
+lapply (lstas_mono … H1 … H2) #H destruct -h -l0 /2 width=3 by cprs_conf/
qed-.
(* Relocation properties ****************************************************)
-lemma cpds_lift: ∀h,g,G. l_liftable (cpds h g G).
-#h #g #G #K #T1 #T2 * #T #l1 #l2 #Hl12 #Hl1 #HT1 #HT2 #L #s #d #e
+lemma cpds_lift: ∀h,g,G,l. l_liftable (cpds h g l G).
+#h #g #G #l2 #K #T1 #T2 * #T #l1 #Hl21 #Hl1 #HT1 #HT2 #L #s #d #e
elim (lift_total T d e)
-/3 width=16 by cprs_lift, da_lift, lstas_lift, ex4_3_intro/
+/3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/
qed.
-lemma cpds_inv_lift1: ∀h,g,G. l_deliftable_sn (cpds h g G).
-#h #g #G #L #U1 #U2 * #U #l1 #l2 #Hl12 #Hl1 #HU1 #HU2 #K #s #d #e #HLK #T1 #HTU1
+lemma cpds_inv_lift1: ∀h,g,G,l. l_deliftable_sn (cpds h g l G).
+#h #g #G #l2 #L #U1 #U2 * #U #l1 #Hl21 #Hl1 #HU1 #HU2 #K #s #d #e #HLK #T1 #HTU1
lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1
elim (lstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L
-/3 width=9 by ex4_3_intro, ex2_intro/
+/3 width=8 by ex4_2_intro, ex2_intro/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/nativevalid_6.ma".
+include "basic_2/equivalence/cpes.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* HIGHER ORDER STRATIFIED NATIVE VALIDITY FOR TERMS ************************)
+
+inductive hsnv (h) (g) (l1) (G) (L): predicate term ≝
+| hsnv_cast: ∀U,T. ⦃G, L⦄ ⊢ U ¡[h, g] → ⦃G, L⦄ ⊢ T ¡[h, g] →
+ (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T) →
+ hsnv h g l1 G L (ⓝU.T)
+.
+
+interpretation "higher order stratified native validity (term)"
+ 'NativeValid h g l G L T = (hsnv h g l G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact hsnv_inv_cast_aux: ∀h,g,G,L,X,l1. ⦃G, L⦄ ⊢ X ¡[h, g, l1] → ∀U,T. X = ⓝU.T →
+ ∧∧ ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g]
+ & (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T).
+#h #g #G #L #X #l1 * -X
+#U #T #HU #HT #HUT #U1 #T1 #H destruct /3 width=1 by and3_intro/
+qed-.
+
+lemma hsnv_inv_cast: ∀h,g,G,L,U,T,l1. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, l1] →
+ ∧∧ ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g]
+ & (∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ U •*⬌*[h, g, l2, l2+1] T).
+/2 width=3 by hsnv_inv_cast_aux/ qed-.
+
+lemma hsnv_inv_snv: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ¡[h, g, l] → ⦃G, L⦄ ⊢ T ¡[h, g].
+#h #g #G #L #T #l * -T
+#U #T #HU #HT #HUT elim (HUT 0) -HUT
+/3 width=3 by snv_cast, cpds_fwd_cprs/
+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/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/hsnv.ma".
+
+(* HIGHER ORDER STRATIFIED NATIVE VALIDITY FOR TERMS ************************)
+
+(* Advanced properties ******************************************************)
+
+lemma snv_hsnv_cast: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g, 0].
+#h #g #G #L #U #T #H elim (snv_inv_cast … H) -H
+#U0 #HU #HT #HU0 #HTU0 @hsnv_cast // -HT
+#l #H <(le_n_O_to_eq … H) -l
+elim (snv_fwd_da … HU) -HU /3 width=3 by cprs_cpds, cpds_div/
+qed.
(**************************************************************************)
include "basic_2/notation/relations/lrsubeqv_5.ma".
-include "basic_2/dynamic/snv.ma".
+include "basic_2/dynamic/hsnv.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
| lsubsv_atom: lsubsv h g G (⋆) (⋆)
| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g G L1 L2 →
lsubsv h g G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubsv_beta: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ W ¡[h, g] → ⦃G, L1⦄ ⊢ V ¡[h, g] →
- scast h g l G L1 V W → ⦃G, L2⦄ ⊢ W ¡[h, g] →
- ⦃G, L1⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l →
+| lsubsv_beta: ∀L1,L2,W,V,l1. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, g, l1] → ⦃G, L2⦄ ⊢ W ¡[h, g] →
+ ⦃G, L1⦄ ⊢ V ▪[h, g] l1+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l1 →
lsubsv h g G L1 L2 → lsubsv h g G (L1.ⓓⓝW.V) (L2.ⓛW)
.
#h #g #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #W #V #l #_ #_ #_ #_ #_ #_ #_ #H destruct
+| #L1 #L2 #W #V #l1 #_ #_ #_ #_ #_ #H destruct
]
qed-.
fact lsubsv_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀I,K1,X. L1 = K1.ⓑ{I}X →
(∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
- ∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
- scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
- ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ⫃¡[h, g] K2 &
- I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+ ∃∃K2,W,V,l1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g, l1] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+ ⦃G, K1⦄ ⊢ V ▪[h, g] l1+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l1 &
+ G ⊢ K1 ⫃¡[h, g] K2 &
+ I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
#h #g #G #L1 #L2 * -L1 -L2
[ #J #K1 #X #H destruct
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
-| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #HL12 #J #K1 #X #H destruct /3 width=13/
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #l1 #HWV #HW #HVl1 #HWl1 #HL12 #J #K1 #X #H destruct /3 width=11 by or_intror, ex8_4_intro/
]
qed-.
lemma lsubsv_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃¡[h, g] L2 →
(∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
- ∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
- scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
- ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ⫃¡[h, g] K2 &
- I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+ ∃∃K2,W,V,l1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g, l1] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+ ⦃G, K1⦄ ⊢ V ▪[h, g] l1+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l1 &
+ G ⊢ K1 ⫃¡[h, g] K2 &
+ I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
fact lsubsv_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L2 = ⋆ → L1 = ⋆.
#h #g #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #W #V #l #_ #_ #_ #_ #_ #_ #_ #H destruct
+| #L1 #L2 #W #V #l1 #_ #_ #_ #_ #_ #H destruct
]
qed-.
fact lsubsv_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀I,K2,W. L2 = K2.ⓑ{I}W →
(∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
- ∃∃K1,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
- scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
- ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+ ∃∃K1,V,l1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g, l1] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+ ⦃G, K1⦄ ⊢ V ▪[h, g] l1+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l1 &
+ G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
#h #g #G #L1 #L2 * -L1 -L2
[ #J #K2 #U #H destruct
-| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3/
-| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #HL12 #J #K2 #U #H destruct /3 width=10/
+| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #l1 #HWV #HW #HVl1 #HWl1 #HL12 #J #K2 #U #H destruct /3 width=8 by or_intror, ex7_3_intro/
]
qed-.
lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, g] K2.ⓑ{I}W →
(∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
- ∃∃K1,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
- scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
- ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+ ∃∃K1,V,l1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g, l1] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+ ⦃G, K1⦄ ⊢ V ▪[h, g] l1+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l1 &
+ G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
(* Basic forward lemmas *****************************************************)
lemma lsubsv_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L1 ⫃ L2.
-#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
qed-.
(* Basic properties *********************************************************)
lemma lsubsv_refl: ∀h,g,G,L. G ⊢ L ⫃¡[h, g] L.
-#h #g #G #L elim L -L // /2 width=1/
+#h #g #G #L elim L -L /2 width=1 by lsubsv_pair/
qed.
lemma lsubsv_cprs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
<(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
| elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
]
-| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K1 #s #e #H
+| #L1 #L2 #W #V #l1 #HWV #HW #HVl1 #HWl1 #_ #IHL12 #K1 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK1
[ destruct
elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H
<(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
| elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
]
-| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K2 #s #e #H
+| #L1 #L2 #W #V #l1 #HWV #HW #HVl1 #HWl1 #_ #IHL12 #K2 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK2
[ destruct
elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H
(* Properties on decomposed extended parallel computation on terms **********)
-lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 →
+lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2,l. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g, l] T2 →
∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
-#h #g #G #L2 #T1 #T2 * #T #l1 #l2 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
+#h #g #G #L2 #T1 #T2 #l2 * #T #l1 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12
lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
elim (lsubsv_lstas_trans … HT1 … Hl1 … HL12) // #T0 #HT10 #HT0
-lapply (lsubsv_fwd_lsubd … HL12) -HL12 #HL12
-lapply (lsubd_da_trans … Hl1 … HL12) -L2 #Hl1
lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02
-elim (cpcs_inv_cprs … HT02) -HT02 /3 width=7 by ex2_intro, ex4_3_intro/
+elim (cpcs_inv_cprs … HT02) -HT02
+/5 width=5 by lsubsv_fwd_lsubd, lsubd_da_trans, ex4_2_intro, ex2_intro/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/static/da_sta.ma".
include "basic_2/static/lsubd_da.ma".
include "basic_2/unfold/lstas_alt.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/equivalence/cpes_cpcs.ma".
include "basic_2/dynamic/lsubsv_lsubd.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
(* Properties on nat-iterated static type assignment ************************)
-lemma lsubsv_lstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, l1] U2 →
- ∀l2. l1 ≤ l2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l2 →
+lemma lsubsv_lstas_trans: ∀h,g,G,L2,T,U2,l2. ⦃G, L2⦄ ⊢ T •*[h, l2] U2 →
+ ∀l1. l2 ≤ l1 → ⦃G, L2⦄ ⊢ T ▪[h, g] l1 →
∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
- ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, l1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L2 #T #U #l1 #H @(lstas_ind_alt … H) -G -L2 -T -U -l1
+ ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, l2] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L2 #T #U #l2 #H @(lstas_ind_alt … H) -G -L2 -T -U -l2
[1,2: /2 width=3 by ex2_intro/
-| #G #L2 #K2 #X #Y #U #i #l1 #HLK2 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12
- elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0
+| #G #L2 #K2 #X #Y #U #i #l2 #HLK2 #_ #HYU #IHXY #l1 #Hl21 #Hl1 #L1 #HL12
+ elim (da_inv_lref … Hl1) -Hl1 * #K0 #V0 [| #l0 ] #HK0 #HV0
lapply (drop_mono … HK0 … HLK2) -HK0 #H destruct
elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HYU -IHXY -HLK1 ]
[ #HK12 #H destruct
- elim (IHXY … Hl12 HV0 … HK12) -K2 -l2 #T #HXT #HTY
+ elim (IHXY … Hl21 HV0 … HK12) -K2 -l1 #T #HXT #HTY
lapply (drop_fwd_drop2 … HLK1) #H
elim (lift_total T 0 (i+1))
/3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/
- | #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct
+ | #V #l0 #_ #_ #_ #_ #_ #H destruct
]
-| #G #L2 #K2 #X #Y #Y0 #U #i #l1 #HLK2 #HXY0 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12
- elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 [| #H1 ]
+| #G #L2 #K2 #X #Y #Y0 #U #i #l2 #HLK2 #HXY0 #_ #HYU #IHXY #l1 #Hl21 #Hl1 #L1 #HL12
+ elim (da_inv_lref … Hl1) -Hl1 * #K0 #V0 [| #l0 ] #HK0 #HV0 [| #H1 ]
lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
- lapply (le_plus_to_le_r … Hl12) -Hl12 #Hl12
+ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21
elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
elim (lsubsv_inv_pair2 … H) -H * #K1
[ #HK12 #H destruct
lapply (lsubsv_fwd_lsubd … HK12) #H
lapply (lsubd_da_trans … HV0 … H) -H #H
elim (da_inv_sta … H) -H
- elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y1
+ elim (IHXY … Hl21 HV0 … HK12) -K2 -Hl21 #Y1
lapply (drop_fwd_drop2 … HLK1)
elim (lift_total Y1 0 (i+1))
/3 width=12 by lstas_ldec, cpcs_lift, ex2_intro/
- | #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct
- lapply (da_mono … HX … HV0) -HX #H destruct
- elim (IHXY … Hl12 HV0 … HK12) -K2 #Y0 #HXY0 #HY0
+ | #V #l1 #HXV #_ #HV #HX #HK12 #_ #H destruct
+ lapply (da_mono … HV0 … HX) -HX #H destruct
+ elim (hsnv_inv_cast … HXV) -HXV #_ #_ #H
+ lapply (H … Hl21) -H #HXV
+ elim (IHXY … Hl21 HV0 … HK12) -K2 -Hl21 #Y0 #HXY0 #HY0
elim (da_inv_sta … HV) -HV #W #HVW
- elim (lstas_total … HVW (l1+1)) -W #W #HVW
- lapply (HVX … Hl12 HVW HXY0) -HVX -Hl12 -HXY0 #HWY0
- lapply (cpcs_trans … HWY0 … HY0) -Y0
- lapply (drop_fwd_drop2 … HLK1)
+ elim (lstas_total … HVW (l2+1)) -W #W #HVW
+ lapply (cpes_inv_lstas_eq … HXV … HXY0 … HVW) -HXV -HXY0 #HY0W
+ lapply (cpcs_canc_sn … HY0W … HY0) -Y0 #HYW
elim (lift_total W 0 (i+1))
- /4 width=12 by lstas_ldef, lstas_cast, cpcs_lift, ex2_intro/
+ lapply (drop_fwd_drop2 … HLK1)
+ /4 width=12 by cpcs_lift, lstas_cast, lstas_ldef, ex2_intro/
]
| #a #I #G #L2 #V2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12
lapply (da_inv_bind … Hl2) -Hl2 #Hl2
(* *)
(**************************************************************************)
+include "basic_2/equivalence/cpes_aaa.ma".
include "basic_2/dynamic/snv_aaa.ma".
include "basic_2/dynamic/lsubsv.ma".
lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃⁝ L2.
#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_pair/
-#L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #_ #_ #IHL12
-lapply (snv_scast … HV H1W HVW H1l) -HV -H1W -HVW -H1l #HV
+#L1 #L2 #W #V #l1 #H #_ #_ #_ #_ #IHL12
+elim (hsnv_inv_cast … H) -H #HW #HV #H
+lapply (H 0 ?) // -l1 #HWV
+elim (snv_fwd_aaa … HW) -HW #B #HW
elim (snv_fwd_aaa … HV) -HV #A #HV
-elim (snv_fwd_aaa … H2W) -H2W #B #HW
-elim (aaa_inv_cast … HV) #HWA #_
-lapply (lsuba_aaa_trans … HW … IHL12) #HWB
-lapply (aaa_mono … HWB … HWA) -HWB -HWA #H destruct /2 width=3 by lsuba_beta/
+lapply (cpes_aaa_mono … HWV … HW … HV) #H destruct
+/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/cpds_cpds.ma".
-include "basic_2/dynamic/snv_aaa.ma".
include "basic_2/dynamic/lsubsv_cpds.ma".
-include "basic_2/dynamic/lsubsv_cpcs.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
elim (lsubsv_inv_pair2 … H) -H * #K1
[ #HK12 #H destruct /3 width=5 by snv_lref/
- | #W #l #H1V #H1W #HWV #_ #HWl #_ #_ #H1 #H2 destruct -IHV
- /3 width=10 by snv_scast, snv_lref/
+ | #W #l #HVW #_ #_ #_ #_ #H1 #H2 destruct -IHV
+ /3 width=6 by hsnv_inv_snv, snv_lref/
]
| #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct
/4 width=1 by snv_bind, lsubsv_pair/
-| #a #G #L2 #V #W #W0 #T #U #l #_ #_ #HVl #HVW #HW0 #HTU #IHV #IHT #L1 #HL12
- lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0
- elim (lsubsv_sta_trans … HVW … HVl … HL12) -HVW #W1 #HVW1 #HW1
- lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10
- lapply (lsubd_da_trans … HVl L1 ?) -HVl /2 width=1 by lsubsv_fwd_lsubd/ #HVl
- elim (lsubsv_cpds_trans … HTU … HL12) -HTU #X #HTU #H
- elim (cprs_inv_abst1 … H) -H #W #U2 #HW0 #_ #H destruct
- lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H
- elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0
- /4 width=11 by snv_appl, cpds_cprs_trans, cprs_bind/
-| #G #L2 #W #T #U #l #_ #_ #HTl #HTU #HUW #IHW #IHT #L1 #HL12
- lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW
- elim (lsubsv_sta_trans … HTU … HTl … HL12) -HTU #U0 #HTU0 #HU0
- lapply (lsubd_da_trans … HTl L1 ?) -HTl
- /4 width=5 by lsubsv_fwd_lsubd, snv_cast, cpcs_trans/
+| #a #G #L2 #V #W0 #T #U0 #l #_ #_ #HVW0 #HTU0 #IHV #IHT #L1 #HL12
+ elim (lsubsv_cpds_trans … HVW0 … HL12) -HVW0 #V0 #HV0 #HWV0
+ elim (lsubsv_cpds_trans … HTU0 … HL12) -HTU0 #X #HT0 #H
+ elim (cprs_inv_abst1 … H) -H #W #T0 #HW0 #_ #H destruct
+ elim (cprs_conf … HWV0 … HW0) -W0
+ /4 width=10 by snv_appl, cpds_cprs_trans, cprs_bind/
+| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
+ elim (lsubsv_cpds_trans … HTU0 … HL12) -HTU0
+ /4 width=5 by lsubsv_cprs_trans, snv_cast, cprs_trans/
]
qed-.
include "basic_2/notation/relations/nativevalid_5.ma".
include "basic_2/computation/cpds.ma".
-include "basic_2/equivalence/cpcs.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-definition scast: ∀h. sd h → nat → relation4 genv lenv term term ≝
- λh,g,l,G,L,V,W. ∀V0,W0,l0.
- l0 ≤ l → ⦃G, L⦄ ⊢ V •*[h, l0+1] V0 → ⦃G, L⦄ ⊢ W •*[h, l0] W0 → ⦃G, L⦄ ⊢ V0 ⬌* W0.
-
(* activate genv *)
-inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝
+inductive snv (h) (g): relation3 genv lenv term ≝
| snv_sort: ∀G,L,k. snv h g G L (⋆k)
| snv_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i)
| snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T)
-| snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T →
- ⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h] W → ⦃G, L⦄ ⊢ W ➡* W0 →
- ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g G L (ⓐV.T)
-| snv_cast: ∀G,L,W,T,U,l. snv h g G L W → snv h g G L T →
- ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T)
+| snv_appl: ∀a,G,L,V,W0,T,U0,l. snv h g G L V → snv h g G L T →
+ ⦃G, L⦄ ⊢ V •*➡*[h, g, 1] W0 → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] ⓛ{a}W0.U0 → snv h g G L (ⓐV.T)
+| snv_cast: ∀G,L,U,T,U0. snv h g G L U → snv h g G L T →
+ ⦃G, L⦄ ⊢ U ➡* U0 → ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0 → snv h g G L (ⓝU.T)
.
interpretation "stratified native validity (term)"
[ #G #L #k #i #H destruct
| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5 by ex2_3_intro/
| #a #I #G #L #V #T #_ #_ #i #H destruct
-| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #i #H destruct
-| #G #L #W #T #U #l #_ #_ #_ #_ #_ #i #H destruct
+| #a #G #L #V #W0 #T #U0 #l #_ #_ #_ #_ #i #H destruct
+| #G #L #U #T #U0 #_ #_ #_ #_ #i #H destruct
]
qed-.
[ #G #L #k #p #H destruct
| #I #G #L #K #V #i #_ #_ #p #H destruct
| #a #I #G #L #V #T #_ #_ #p #H destruct
-| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #p #H destruct
-| #G #L #W #T #U #l #_ #_ #_ #_ #_ #p #H destruct
+| #a #G #L #V #W0 #T #U0 #l #_ #_ #_ #_ #p #H destruct
+| #G #L #U #T #U0 #_ #_ #_ #_ #p #H destruct
]
qed-.
fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
#h #g #G #L #X * -G -L -X
-[ #G #L #k #a #I #V #T #H destruct
-| #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
-| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1 by conj/
-| #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_#_ #_ #a #I #V #T #H destruct
-| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct
+[ #G #L #k #b #Z #X1 #X2 #H destruct
+| #I #G #L #K #V #i #_ #_ #b #Z #X1 #X2 #H destruct
+| #a #I #G #L #V #T #HV #HT #b #Z #X1 #X2 #H destruct /2 width=1 by conj/
+| #a #G #L #V #W0 #T #U0 #l #_ #_ #_ #_ #b #Z #X1 #X2 #H destruct
+| #G #L #U #T #U0 #_ #_ #_ #_ #b #Z #X1 #X2 #H destruct
]
qed-.
/2 width=4 by snv_inv_bind_aux/ qed-.
fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T →
- ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
- ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h] W & ⦃G, L⦄ ⊢ W ➡* W0 &
- ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
+ ∃∃a,W0,U0,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
+ ⦃G, L⦄ ⊢ V •*➡*[h, g, 1] W0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, l] ⓛ{a}W0.U0.
#h #g #G #L #X * -L -X
-[ #G #L #k #V #T #H destruct
-| #I #G #L #K #V0 #i #_ #_ #V #T #H destruct
-| #a #I #G #L #V0 #T0 #_ #_ #V #T #H destruct
-| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #Hl #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8 by ex6_5_intro/
-| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #V #T #H destruct
+[ #G #L #k #X1 #X2 #H destruct
+| #I #G #L #K #V #i #_ #_ #X1 #X2 #H destruct
+| #a #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
+| #a #G #L #V #W0 #T #U0 #l #HV #HT #HVW0 #HTU0 #X1 #X2 #H destruct /2 width=6 by ex4_4_intro/
+| #G #L #U #T #U0 #_ #_ #_ #_ #X1 #X2 #H destruct
]
qed-.
lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] →
- ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
- ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h] W & ⦃G, L⦄ ⊢ W ➡* W0 &
- ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
+ ∃∃a,W0,U0,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
+ ⦃G, L⦄ ⊢ V •*➡*[h, g, 1] W0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, l] ⓛ{a}W0.U0.
/2 width=3 by snv_inv_appl_aux/ qed-.
-fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T →
- ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
- ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h] U & ⦃G, L⦄ ⊢ U ⬌* W.
+fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀U,T. X = ⓝU.T →
+ ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
+ ⦃G, L⦄ ⊢ U ➡* U0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0.
#h #g #G #L #X * -G -L -X
-[ #G #L #k #W #T #H destruct
-| #I #G #L #K #V #i #_ #_ #W #T #H destruct
-| #a #I #G #L #V #T0 #_ #_ #W #T #H destruct
-| #a #G #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #_ #W #T #H destruct
-| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #Hl #HTU0 #HUW0 #W #T #H destruct /2 width=4 by ex5_2_intro/
+[ #G #L #k #X1 #X2 #H destruct
+| #I #G #L #K #V #i #_ #_ #X1 #X2 #H destruct
+| #a #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
+| #a #G #L #V #W0 #T #U0 #l #_ #_ #_ #_ #X1 #X2 #H destruct
+| #G #L #U #T #U0 #HV #HT #HU0 #HTU0 #X1 #X2 #H destruct /2 width=3 by ex4_intro/
]
qed-.
-lemma snv_inv_cast: ∀h,g,G,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] →
- ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
- ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h] U & ⦃G, L⦄ ⊢ U ⬌* W.
+lemma snv_inv_cast: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g] →
+ ∃∃U0. ⦃G, L⦄ ⊢ U ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
+ ⦃G, L⦄ ⊢ U ➡* U0 & ⦃G, L⦄ ⊢ T •*➡*[h, g, 1] U0.
/2 width=3 by snv_inv_cast_aux/ qed-.
include "basic_2/unfold/lstas_lift.ma".
include "basic_2/computation/csx_aaa.ma".
include "basic_2/computation/cpds_aaa.ma".
-include "basic_2/equivalence/cpcs_aaa.ma".
include "basic_2/dynamic/snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
[ /2 width=2 by aaa_sort, ex_intro/
| #I #G #L #K #V #i #HLK #_ * /3 width=6 by aaa_lref, ex_intro/
| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2 by aaa_abbr, aaa_abst, ex_intro/
-| #a #G #L #V #W #W0 #T #U #l #_ #_ #Hl #HVW #HW0 #HTU * #B #HV * #X #HT
- lapply (cpds_aaa_conf h g … HV W0 ?) [ -HTU /3 width=4 by cpds_strap1, sta_cprs_cpds/ ] -W #HW0 (**) (* auto fail without -HTU *)
- lapply (cpds_aaa_conf … HT … HTU) -HTU #H
+| #a #G #L #V #W0 #T #U0 #l #_ #_ #HVW0 #HTU0 * #B #HV * #X #HT
+ lapply (cpds_aaa_conf … HV … HVW0) -HVW0 #HW0
+ lapply (cpds_aaa_conf … HT … HTU0) -HTU0 #H
elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4 by aaa_appl, ex_intro/
-| #G #L #W #T #U #l #_ #_ #_ #HTU #HUW * #B #HW * #A #HT
- lapply (sta_aaa_conf … HT … HTU) -HTU #H
- lapply (cpcs_aaa_mono … HUW … H … HW) -HUW -H #H destruct /3 width=3 by aaa_cast, ex_intro/
+| #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT
+ lapply (cprs_aaa_conf … HU … HU0) -HU0 #HU0
+ lapply (cpds_aaa_conf … HT … HTU0) -HTU0 #H
+ lapply (aaa_mono … H … HU0) -U0 #H destruct /3 width=3 by aaa_cast, ex_intro/
]
qed-.
#h #g #G #L #T1 #T2 #l #HT1 #HT12
elim (snv_fwd_sta … HT1) -HT1 /2 width=5 by lstas_fwd_correct/
qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma snv_scast: ∀h,g,G,L,V,W,l. ⦃G, L⦄ ⊢ V ¡[h, g] → ⦃G, L⦄ ⊢ W ¡[h, g] →
- scast h g l G L V W → ⦃G, L⦄ ⊢V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ ⓝW.V ¡[h, g].
-#h #g #G #L #V #W #l #HV #HW #H #Hl
-elim (snv_fwd_sta … HV) /4 width=6 by snv_cast, sta_lstas/
-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/unfold/lstas_lstas.ma".
-include "basic_2/computation/fpbs_lift.ma".
-include "basic_2/computation/fpbg_fleq.ma".
-include "basic_2/equivalence/cpes_cpds.ma".
-include "basic_2/dynamic/snv.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Inductive premises for the preservation results **************************)
-
-definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
-
-definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-
-definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-
-definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
- ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
- ∀U. ⦃G, L⦄ ⊢ T •*[h, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g].
-
-(* Properties for the preservation results **********************************)
-
-fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
-#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
-qed-.
-
-fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
-qed-.
-
-fact da_cpcs_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
- ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
- ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2.
-#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H
-elim (cpcs_inv_cprs … H) -H /4 width=18 by da_cprs_lpr_aux, da_mono/
-qed-.
-
-fact sta_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •[h] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #H01 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12
-elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) -H01 -Hl -HT12 -HL12
-/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/
-qed-.
-
-fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
-[2: /3 width=12 by da_cprs_lpr_aux/
-|3: /3 width=10 by snv_cprs_lpr_aux/
-|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
-] -G0 -L0 -T0 -T1 -T -l1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-fact lstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
- ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
- ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
- ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (lstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1
-elim (lstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0
-lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
-qed-.
-
-fact snv_sta_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
- ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
- ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
- ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g].
-/3 width=8 by lstas_inv_SO, sta_lstas/ qed-.
-
-fact lstas_cpds_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
- ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
- ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 →
- ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2.
-#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2
-lapply (da_mono … H … Hl1) -H #H destruct
-lapply (lstas_da_conf … HTU1 … Hl1) #Hl12
-elim (le_or_ge l2 l) #Hl2
-[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T
- /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/
-| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l
- lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1
- elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) -IH3 -IH2 -IH1 -Hl1l -HTU1 -HTT2
- /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l, ex3_2_intro/
-]
-qed-.
-
-fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
-#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
-elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
-lapply (IH2 … H01 … Hl1 … HT12 … HL12) -L0 -T0 // -T1
-lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
-lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
-elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpbs_lift.ma".
+include "basic_2/computation/fpbg_fleq.ma".
+include "basic_2/equivalence/cpes_cpcs.ma".
+include "basic_2/equivalence/cpes_cpes.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+
+definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+
+definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+
+definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝
+ λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
+ ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
+ ∀U. ⦃G, L⦄ ⊢ T •*[h, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g].
+
+(* Properties for the preservation results **********************************)
+
+fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
+qed-.
+
+fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
+@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
+qed-.
+
+fact da_cpds_lpr_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l1. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+ ∀T2,l2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ l2 ≤ l1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l1-l2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l1 #Hl1 #T2 #l2 * #T #l0 #Hl20 #H #HT1 #HT2 #L2 #HL12
+lapply (da_mono … H … Hl1) -H #H destruct
+lapply (lstas_da_conf … HT1 … Hl1) #Hl12
+lapply (da_cprs_lpr_aux … IH2 IH1 … Hl12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12
+/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/
+qed-.
+
+fact da_cpes_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+ ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 →
+ ∀l21,l22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 →
+ ∧∧ l21 ≤ l11 & l22 ≤ l12 & l11 - l21 = l12 - l22.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l11 #Hl11 #l12 #Hl12 #l21 #l22 * #T #HT1 #HT2
+elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl11 … HT1 … L) -Hl11 -HT1 //
+elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl12 … HT2 … L) -Hl12 -HT2 //
+/3 width=7 by da_mono, and3_intro/
+qed-.
+
+fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
+[2: /3 width=12 by da_cprs_lpr_aux/
+|3: /3 width=10 by snv_cprs_lpr_aux/
+|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
+] -G0 -L0 -T0 -T1 -T -l1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
+lapply (IH2 … H01 … HTl1 … HT12 … HL12) -L0 -T0 // -T1
+lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
+qed-.
+
+fact cpes_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+ ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
+elim (cpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
+elim (cpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
+elim (cprs_conf … H1 … H2) -T0
+/3 width=5 by cpds_div, cpds_cprs_trans/
+qed-.
+
+fact lstas_cpds_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
+ ∀l,l1. l1 ≤ l → ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀T1. ⦃G, L⦄ ⊢ T •*[h, l1] T1 →
+ ∀T2,l2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l2-l1, l1-l2] T2.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #l #l1 #Hl1 #HTl #T1 #HT1 #T2 #l2 * #X #l0 #Hl20 #H #HTX #HXT2
+lapply (da_mono … H … HTl) -H #H destruct
+lapply (lstas_da_conf … HT1 … HTl) #HTl1
+lapply (lstas_da_conf … HTX … HTl) #HXl
+lapply (da_cprs_lpr_aux … IH3 IH2 … HXl … HXT2 L ?)
+[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTl2
+elim (le_or_ge l1 l2) #Hl12 >(eq_minus_O … Hl12)
+[ /5 width=3 by cpds_refl, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro, ex2_intro/
+| lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1
+ elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXl … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXl -HXT1 -HXT2
+ /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l/
+]
+qed-.
+
+fact cpes_le_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+ ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 →
+ ∀l21,l22,l. l21 + l ≤ l11 → l22 + l ≤ l12 →
+ ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21+l, l22+l] T2.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #l11 #Hl11 #Hl12 #Hl12 #l21 #l22 #l #H1 #H2 * #T0 #HT10 #HT20
+elim (da_inv_sta … Hl11) #X1 #HTX1
+elim (lstas_total … HTX1 (l21+l)) -X1 #X1 #HTX1
+elim (da_inv_sta … Hl12) #X2 #HTX2
+elim (lstas_total … HTX2 (l22+l)) -X2 #X2 #HTX2
+lapply (lstas_cpds_aux … IH4 IH3 IH2 IH1 … Hl11 … HTX1 … HT10) -HT10
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX1 ]
+lapply (lstas_cpds_aux … IH4 IH3 IH2 IH1 … Hl12 … HTX2 … HT20) -HT20
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX2 ]
+lapply (lstas_cpes_trans … Hl11 … HTX1 … HX1) [ // ] -Hl11 -HTX1 -HX1 -H1 #H1
+lapply (lstas_cpes_trans … Hl12 … HTX2 … HX2) [ // ] -Hl12 -HTX2 -HX2 -H2 #H2
+lapply (cpes_canc_dx … H1 … H2) // (**) (* full auto raises NTypeChecker failure *)
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma snv_cast_cpes: ∀h,g,G,L,U,T. ⦃G, L⦄ ⊢ U ¡[h, g] → ⦃G, L⦄ ⊢ T ¡[h, g] →
+ ⦃G, L⦄ ⊢ U •*⬌*[h, g, 0, 1] T → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, g].
+#h #g #G #L #U #T #HU #HT * /3 width=3 by snv_cast, cpds_fwd_cprs/
+qed.
(**************************************************************************)
include "basic_2/static/lsubd_da.ma".
-include "basic_2/computation/cpds_cpds.ma".
include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/snv_cpes.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
/4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, drop_drop/
]
| #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
+ elim (snv_inv_appl … H1) -H1 #b1 #W1 #U1 #l1 #HV1 #HT1 #HVW1 #HTU1
lapply (da_inv_flat … H2) -H2 #Hl
elim (cpr_inv_appl1 … H3) -H3 *
[ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/
- | #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct
- elim (snv_inv_bind … HT1) -HT1 #HW #HU1
+ | #b #V2 #W #W2 #U #U2 #HV12 #HW2 #HU2 #H1 #H2 destruct
+ elim (snv_inv_bind … HT1) -HT1 #HW #HU
lapply (da_inv_bind … Hl) -Hl #Hl
- elim (cpds_inv_abst1 … HT10) -HT10 #W3 #U3 #HW3 #_ #H destruct -U3
- lapply (cprs_div … HW3 … HW10) -W3 #HWW1
- lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #H
- elim (snv_fwd_da … HW) #l1 #Hl1
- lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbg, sta_lstas/ #HW1
- lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_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
+ elim (cpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -l1
+ elim (snv_fwd_da … HV1) #l1 #Hl1
+ elim (snv_fwd_da … HW) #l0 #Hl0
+ lapply (cpds_div … W … 0 … HVW1) /2 width=2 by cprs_cpds/ -W3 #H
+ elim (da_cpes_aux … IH3 IH2 IH1 … Hl0 … Hl1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
+ <minus_n_O #H destruct >(plus_minus_m_m l1 1) in Hl1; // -H1 #Hl1
+ lapply (IH1 … HV1 … Hl1 … HV12 … HL12) -HV1 -Hl1 -HV12 [ /2 by fqup_fpbg/ ]
+ lapply (IH1 … Hl0 … HW2 … HL12) -Hl0 /2 width=1 by fqup_fpbg/ -HW
+ lapply (IH1 … HU … Hl … HU2 (L2.ⓛW2) ?) -IH1 -HU -Hl -HU2 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
/4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/
- | #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH3 -IH2 -V -W0 -T0 -l0 -HV1 -HVW1
+ | #b #V0 #V2 #W #W2 #U #U2 #HV10 #HV02 #HW2 #HU2 #H1 #H2 destruct -IH3 -IH2 -b1 -V0 -W1 -U1 -l1 -HV1
elim (snv_inv_bind … HT1) -HT1 #_
lapply (da_inv_bind … Hl) -Hl
/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
+ elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
lapply (da_inv_flat … H2) -H2 #Hl
elim (cpr_inv_cast1 … H3) -H3
[ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
(* *)
(**************************************************************************)
+include "basic_2/multiple/fqus_alt.ma".
include "basic_2/computation/cpds_lift.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
include "basic_2/dynamic/snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #s #d #e #HLK #X #H
elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct
/4 width=5 by snv_bind, drop_skip/
-| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #s #d #e #HLK #X #H
+| #a #G #K #V #W0 #T #U0 #l #_ #_ #HVW0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H
elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
- elim (lift_total V0 d e) #W0 #HVW0
- elim (lift_total V1 d e) #W1 #HVW1
- elim (lift_total T1 (d+1) e) #U1 #HTU1
- @(snv_appl … a … W0 … W1 … U1 l)
- [1,2,3,4,5: /2 width=10 by cprs_lift, sta_lift, da_lift/ ]
- @(cpds_lift … HT1 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typecjhecker failure *)
-| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #s #d #e #HLK #X #H
- elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct
- elim (lift_total V d e)
- /3 width=12 by snv_cast, cpcs_lift, sta_lift, da_lift/
+ elim (lift_total W0 d e) #W1 #HW01
+ elim (lift_total U0 (d+1) e) #U1 #HU01
+ @(snv_appl … a … W1 … U1 l) [1,2,3: /2 width=10 by cpds_lift/ ] -IHV -IHT
+ @(cpds_lift … HTU0 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typechecker failure *)
+| #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
+ elim (lift_total U0 d e)
+ /3 width=12 by snv_cast, cprs_lift, cpds_lift/
]
qed.
| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #s #d #e #HLK #X #H
elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct
/4 width=5 by snv_bind, drop_skip/
-| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
+| #a #G #L #W #W1 #U #U1 #l #_ #_ #HW1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
+ elim (cpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0
+ elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0
+ elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct
+ lapply (lift_inj … HY … HW01) -HY #H destruct
+ /3 width=6 by snv_appl/
+| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
- lapply (da_inv_lift … Hl … HLK … HVW) -Hl #Hl
- elim (sta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0
- elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01
- elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU
- elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct
- lapply (lift_inj … HY … HVW1) -HY #H destruct
- /3 width=8 by snv_appl/
-| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #s #d #e #HLK #X #H
- elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct
- lapply (da_inv_lift … Hl … HLK … HTU) -Hl #Hl
- elim (sta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HVW #HTV
- lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W
- /3 width=8 by snv_cast/
+ elim (cprs_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0
+ elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0
+ lapply (lift_inj … HX … HU01) -HX #H destruct
+ /3 width=5 by snv_cast/
]
qed-.
-(* Advanced properties ******************************************************)
+(* Properties on subclosure *************************************************)
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].
]
]
qed-.
+
+lemma snv_fquq_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 (fquq_inv_gen … H) -H [|*]
+/2 width=5 by snv_fqu_conf/
+qed-.
+
+lemma snv_fqup_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 @(fqup_ind … H) -G2 -L2 -T2
+/3 width=5 by fqup_strap1, snv_fqu_conf/
+qed-.
+
+lemma snv_fqus_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 (fqus_inv_gen … H) -H [|*]
+/2 width=5 by snv_fqup_conf/
+qed-.
(**************************************************************************)
include "basic_2/dynamic/snv_lift.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/snv_cpes.ma".
include "basic_2/dynamic/lsubsv_snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
/4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, drop_drop/
]
| #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 (snv_inv_appl … H1) -H1 #a #W1 #U1 #l0 #HV1 #HT1 #HVW1 #HTU1
elim (cpr_inv_appl1 … H2) -H2 *
[ #V2 #T2 #HV12 #HT12 #H destruct -IH4
lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0
- elim (sta_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
- lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
- elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
- lapply (cpds_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?)
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H
+ elim (cprs_inv_abst1 … H) -H #XW #U2 #HXW #_ #H destruct -IH1 -IH3 -IH2 -L1
+ elim (cprs_conf … HXV … HXW) -W1 #W2 #HXV #HXW
+ lapply (cpds_cprs_trans … HVW2 … HXV) -XV
+ lapply (cpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?)
/2 width=7 by snv_appl, cprs_bind/
- | #b #V2 #W20 #W2 #T20 #T2 #HV12 #HW202 #HT202 #H1 #H2 destruct
- 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_sta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10
- lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #HlW10
- elim (snv_fwd_da … HW20) #l #Hl
- lapply (da_cpcs_aux … IH1 IH2 … HlW10 … Hl … HW120) // -HlW10
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_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 (sta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #W3 #HV2W3 #HW103
- lapply (da_sta_conf … HV2W3 … HlV2) <minus_plus_m_m #HlW3
- lapply (cpcs_cpr_strap1 … HW120 … HW202) -HW120 #HW102
- lapply (lpr_cpcs_conf … HL12 … HW102) -HW102 #HW102
- lapply (cpcs_canc_sn … HW103 … HW102) -W10 #HW32
- lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 #HV2
- lapply (IH1 … HW202 … HL12) /2 width=1 by fqup_fpbg/ -HW20 #HW2
- lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT20 #HT2
- lapply (snv_sta_aux … IH4 … HlV2 … HV2W3)
- /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_beta … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
- lapply (lstas_sta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
- @(lstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
- [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/
- | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
- ]
+ | #b #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
+ elim (snv_inv_bind … HT1) -HT1 #HW10 #HT10
+ elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -l0
+ elim (snv_fwd_da … HV1) #l #HV1l
+ elim (snv_fwd_da … HW10) #l0 #HW10l
+ lapply (cpds_div … W10 … 0 … HVW1) /2 width=2 by cprs_cpds/ -W30 #HVW10
+ elim (da_cpes_aux … IH4 IH1 IH2 … HW10l … HV1l … HVW10) /2 width=1 by fqup_fpbg/
+ #_ #Hl <minus_n_O #H destruct >(plus_minus_m_m l 1) in HV1l; // -Hl #HV1l
+ lapply (cpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20
+ lapply (IH2 … HV1l … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1l #HV2l
+ lapply (IH2 … HW10l … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10l #HW20l
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10 #HW20
+ lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 #HT20
+ @snv_bind /2 width=1 by snv_cast_cpes/
+ @(lsubsv_snv_trans … HT20) -HT20
+ @(lsubsv_beta … (l-1)) //
+ @hsnv_cast [1,2: // ] #l0 #Hl0
+ lapply (cpes_le_aux … IH4 IH1 IH2 IH3 … HW20l … HV2l … l0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20l -HV2l -HVW20
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
| #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
- lapply (lpr_cprs_conf … HL12 … HW10) -HW10 #HW10
- elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H
- elim (cprs_inv_abst1 … H) -H #W #U2 #HW1 #_ #H destruct -U3
- elim (sta_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 (sta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=2 by drop_drop/ -H1 #HVW20
- lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=2 by drop_drop/ -HW13 -H3 -H2 #HW320
- lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
- elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
- lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
- lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
- lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=2 by drop_drop/ -Hl0 #Hl0
- lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
- lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H
+ elim (cprs_inv_abst1 … H) -H #W #U2 #HW3 #_ #H destruct -U3
+ lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
+ lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #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, drop_drop/
+ lapply (snv_lift … HV0 (L2.ⓓW2) (Ⓕ) … HV02) /2 width=1 by drop_drop/ -HV0 #HV2
+ elim (lift_total XV 0 1) #XW #HXVW
+ lapply (cpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2
+ lapply (cprs_lift … HXVW1 (L2.ⓓW2) (Ⓕ) … HW13 … HXVW) /2 width=1 by drop_drop/ -W1 -XV #HXW3
+ elim (cprs_conf … HXW3 … HW3) -W3 #W3 #HXW3 #HW3
+ lapply (cpds_cprs_trans … HXWV2 … HXW3) -XW
+ lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W
+ /3 width=6 by snv_appl, snv_bind/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
- elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1
+ elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
elim (cpr_inv_cast1 … H2) -H2
[ * #W2 #T2 #HW12 #HT12 #H destruct
- lapply (cpcs_cprs_strap1 … HUW1 W2 ?) /2 width=1 by cpr_cprs/ -HUW1 #H1
- lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ -HW1 -HW12 #HW2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH1 #HT2
- elim (sta_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
+ elim (snv_fwd_da … HW1) #l #HW1l
+ lapply (cpds_div … W1 … 0 … HTU1) /2 width=2 by cprs_cpds/ -U1 -l #HWT1
+ lapply (cpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/
+ lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -L1
+ /2 width=1 by snv_cast_cpes/
+ | #H -IH3 -IH2 -HW1 -U1
lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/
]
]
(**************************************************************************)
include "basic_2/dynamic/snv_lift.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/snv_cpes.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
elim (lstas_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
+ elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #l0 #HV1 #HT1 #HVW1 #HTU1
lapply (da_inv_flat … Hl1) -Hl1 #Hl1
- elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
- lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1
- elim (lstas_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 (lstas_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 #_
- /3 width=7 by snv_appl, cprs_trans/
-| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2
+ elim (lstas_inv_appl1 … H2) -H2 #T0 #HT10 #H destruct
+ lapply (IH1 … HT1 … Hl1 … HT10) /2 width=1 by fqup_fpbg/ #HT0
+ lapply (lstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #H
+ elim (cpes_inv_abst2 … H) -H /3 width=6 by snv_appl, cpds_cprs_trans/
+| #U1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2
[ lapply (lstas_inv_O … H2) -H2 #H destruct // ]
- elim (snv_inv_cast … H1) -H1
+ elim (snv_inv_cast … H1) -H1
lapply (da_inv_flat … Hl1) -Hl1
lapply (lstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/
]
(* *)
(**************************************************************************)
-include "basic_2/computation/cpds_cpds.ma".
include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/snv_cpes.ma".
include "basic_2/dynamic/lsubsv_lstas.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
/5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, drop_drop, ex2_intro/
]
| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct
- elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10
+ elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #l0 #HV1 #HT1 #HVW1 #HTU1
lapply (da_inv_flat … Hl1) -Hl1 #Hl1
- elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
+ elim (lstas_inv_appl1 … H2) -H2 #X #HT1U #H destruct
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
+ [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -U1 -HV1 -IH4 -IH3 -IH2
+ elim (IH1 … Hl1 … HT1U … HT12 … HL12) -IH1 -Hl1 -HT1U
/4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lstas_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
- elim (lstas_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
- elim (cpds_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW20 #_ #H destruct
- lapply (cprs_div … HW10 … HW20) -W0 #HW12
- lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #H
- elim (snv_fwd_da … HW2) #l #Hl
- lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbg, sta_lstas/ #HW1
- lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_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, sta_lstas/ -HVW1 #W4 #H #HW14
- lapply (lstas_inv_SO … H) #HV2W4
- lapply (da_sta_conf … HV2W4 … HV2l) <minus_plus_m_m #HW4l
- lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW4
+ elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
+ elim (cpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0
+ elim (snv_fwd_da … HW2) #l0 #HW2l
+ lapply (cpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_cpds/ -W0 #H21
+ elim (snv_fwd_da … HV1) #l #HV1l
+ elim (da_cpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H
+ <minus_n_O #H0 destruct >(plus_minus_m_m l 1) in HV1l; // -H #HV1l
+ lapply (cpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32
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
+ lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH2 … HW2l … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2l #HW3l
+ lapply (IH2 … HV1l … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV1l #HV2l
+ elim (IH1 … Hl1 … HT2U … HT23 (L2.ⓛW3)) -HT2U /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23
elim (lsubsv_lstas_trans … g … HTU3 … Hl21 … (L2.ⓓⓝW3.V2)) -HTU3
- [ #U4 #HT3U4 #HU43 -HW12 -HW3 -HW3l -W4 -IH2 -IH3 -IH4
+ [ #U4 #HT3U4 #HU43 -IH1 -IH2 -IH3 -IH4 -l -l1 -HW3 -HV2 -HT2
@(ex2_intro … (ⓓ{b}ⓝW3.V2.U4)) /2 width=1 by lstas_bind/ -HT3U4
@(cpcs_canc_dx … (ⓓ{b}ⓝW3.V2.U3)) /2 width=1 by cpcs_bind_dx/ -HU43
@(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_beta … l) /3 width=7 by fqup_fpbg/
- #W #W0 #l0 #Hl0 #HV2W #HW30
- lapply (lstas_sta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W
- @(lstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) //
- [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/
- | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
- ]
+ @(lsubsv_beta … (l-1)) /3 width=7 by fqup_fpbg/
+ @hsnv_cast [1,2: // ] #l0 #Hl0
+ lapply (cpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
| -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
+ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -HV1 -IH4 -IH3 -IH2
elim (snv_inv_bind … HT1) -HT1 #_ #HT0
lapply (da_inv_bind … Hl1) -Hl1 #Hl1
- elim (lstas_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
+ elim (lstas_inv_bind1 … HT1U) -HT1U #U0 #HTU0 #H destruct
elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2
[ lapply (lstas_inv_O … H2) -H2 #H destruct -IH1 -H1 -l1 /4 width=5 by lpr_cpcs_conf, cpr_cpcs_dx, ex2_intro/ ]
- elim (snv_inv_cast … H1) -H1 #U1 #l #_ #HT1 #_ #_ #_ -U1 -l
+ elim (snv_inv_cast … H1) -H1 #U1 #_ #HT1 #_ #_ -U1
lapply (da_inv_flat … Hl1) -Hl1 #Hl1
lapply (lstas_inv_cast1 … H2) -H2 #HTU1
elim (cpr_inv_cast1 … H3) -H3
[ * #U2 #T2 #_ #HT12 #H destruct
elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 -HL12
/3 width=3 by fqup_fpbg, lstas_cast, ex2_intro/
- | #HT1X3
- elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12
+ | #HT1X3 elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12
/2 width=3 by fqup_fpbg, ex2_intro/
]
]
qed-.
(* Advanced preservation properties *****************************************)
-
-lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
-#h #g #G #L1 #T1 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
-qed-.
-
-lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
-qed-.
-
-lemma da_cpcs: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G, L⦄ ⊢ T2 ¡[h, g] →
- ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
- ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2.
-#h #g #G #L #T1 #HT1 #T2 #HT2 #l1 #Hl1 #l2 #Hl2 #H
-elim (cpcs_inv_cprs … H) -H /3 width=12 by da_cprs_lpr, da_mono/
-qed-.
-
-lemma sta_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •[h] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L1 #T1 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12
-elim (lstas_cpr_lpr … 1 … Hl U1 … HT12 … HL12) -Hl -HT12 -HL12
-/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/
-qed-.
-
-lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2
-[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
- ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
- ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
-elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
-lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
-qed-.
-
-lemma snv_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
- ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
- ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g].
-/3 width=7 by lstas_inv_SO, sta_lstas, snv_lstas/ qed-.
-
-lemma lstas_cpds: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] →
- ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
- ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 →
- ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2.
-#h #g #G #L #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2
-lapply (da_mono … H … Hl1) -H #H destruct
-lapply (lstas_da_conf … HTU1 … Hl1) #Hl12
-elim (le_or_ge l2 l) #Hl2
-[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T //
- /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/
-| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l
- lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1
- elim (lstas_cprs_lpr … Hl1l … HTU1 … HTT2 L) -Hl1l -HTU1 -HTT2
- /3 width=7 by snv_lstas, cpcs_cpes, monotonic_le_minus_l, ex3_2_intro/
-]
-qed-.
-
-lemma cpds_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
-#h #g #G #L1 #T1 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
-elim (lstas_cpr_lpr … Hl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12
-lapply (da_cpr_lpr … Hl1 … HT12 … HL12) // -T1
-lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
-lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
-elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/
-qed-.
(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-(* Main properties about atomic arity assignment on terms *******************)
+(* Main inversion lemmas about atomic arity assignment on terms *************)
theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/dpconvstar_6.ma".
-include "basic_2/static/da.ma".
-include "basic_2/unfold/lstas.ma".
-include "basic_2/equivalence/cpcs.ma".
+include "basic_2/notation/relations/dpconvstar_8.ma".
+include "basic_2/computation/cpds.ma".
(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-definition cpes: ∀h. sd h → relation4 genv lenv term term ≝
- λh,g,G,L,T1,T2.
- ∃∃T,l1,l2. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ⬌* T2.
+definition cpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
+ λh,g,l1,l2,G,L,T1,T2.
+ ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T.
interpretation "decomposed extended parallel equivalence (term)"
- 'DPConvStar h g G L T1 T2 = (cpes h g G L T1 T2).
+ 'DPConvStar h g l1 l2 G L T1 T2 = (cpes h g l1 l2 G L T1 T2).
(* Basic properties *********************************************************)
-lemma sta_cpcs_cpes: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T →
- ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2.
-/3 width=7 by sta_lstas, ex4_3_intro/ qed.
+lemma cpds_div: ∀h,g,G,L,T1,T2,T,l1,l2.
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T →
+ ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+/2 width=3 by ex2_intro/ qed.
-lemma lstas_cpes: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2.
-/2 width=7 by ex4_3_intro/ qed.
+lemma cpes_refl_O_O: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
+ ⦃G, L⦄ ⊢ T •*⬌*[h, g, 0, 0] T.
+/3 width=3 by cpds_refl, cpds_div/ qed.
-lemma cpcs_cpes: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2.
-/2 width=7 by lstar_O, ex4_3_intro/ qed.
-
-lemma cpes_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*⬌*[h, g] T.
-/2 width=2 by cpcs_cpes/ qed.
-
-lemma cpes_strap1: ∀h,g,G,L,T1,T,T2.
- ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2.
-#h #g #G #L #T1 #T #T2 * /3 width=9 by cpcs_strap1, ex4_3_intro/
-qed.
+lemma cpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+ ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1.
+#h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by cpds_div/
+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/cpds_aaa.ma".
+include "basic_2/equivalence/cpes.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
+
+(* Main inversion lemmas about atomic arity assignment on terms *************)
+
+theorem cpes_aaa_mono: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+ ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
+ A1 = A2.
+#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
+lapply (cpds_aaa_conf … HA1 … HT1) -T1 #HA1
+lapply (cpds_aaa_conf … HA2 … HT2) -T2 #HA2
+lapply (aaa_mono … HA1 … HA2) -L -T //
+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/cpds_cpds.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/equivalence/cpes.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
+
+(* Inversion lemmas on parallel equivalence for terms ***********************)
+
+lemma cpes_inv_lstas_eq: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+ ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l1] U1 →
+ ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, l2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2
+/3 width=8 by cpds_inv_lstas_eq, cprs_div/
+qed-.
+
+(* Properties on parallel equivalence for terms ***********************)
+
+lemma cpcs_cpes: ∀h,g,G,L,T1,l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 →
+ ∀U1,l12. l12 ≤ l11 → ⦃G, L⦄ ⊢ T1 •*[h, l12] U1 →
+ ∀T2,l21. ⦃G, L⦄ ⊢ T2 ▪[h, g] l21 →
+ ∀U2,l22. l22 ≤ l21 → ⦃G, L⦄ ⊢ T2 •*[h, l22] U2 →
+ ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l12, l22] T2.
+#h #g #G #L #T1 #l11 #HT1 #U1 #l12 #Hl121 #HTU1 #T2 #l21 #HT2 #U2 #l22 #Hl221 #HTU2 #HU12
+elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by cpds_div, ex4_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/computation/cpds.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/equivalence/cpes.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-
-(* Advanced properties ******************************************************)
-
-lemma cpds_cpes_dx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2.
-#h #g #G #L #T1 #T2 * /3 width=7 by cpcs_cprs_dx, ex4_3_intro/
-qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cpes_inv_abst2: ∀h,g,a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T •*⬌*[h, g] ⓛ{a}W1.T1 →
- ∃∃W2,T2. ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2.
-#h #g #a #G #L #W1 #T1 #T * #T0 #l #l0 #Hl0 #Hl #HT0 #H
-elim (cpcs_inv_abst2 … H) -H /3 width=7 by ex4_3_intro, ex2_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/computation/cpds_cpds.ma".
+include "basic_2/equivalence/cpes.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpes_inv_abst2: ∀h,g,a,G,L,T1,T2,W2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] ⓛ{a}W2.T2 →
+ ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W &
+ ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, g, l2] T.
+#h #g #a #G #L #T1 #T2 #W2 #l1 #l2 * #T0 #HT10 #H
+elim (cpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpes_refl: ∀h,g,G,L,T,l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
+ ⦃G, L⦄ ⊢ T •*⬌*[h, g, l2, l2] T.
+#h #g #G #L #T #l1 #l2 #Hl21 #Hl1
+elim (da_inv_sta … Hl1) #U #HTU
+elim (lstas_total … HTU l2) -U /3 width=3 by cpds_div, lstas_cpds/
+qed.
+
+lemma lstas_cpes_trans: ∀h,g,G,L,T1,l0,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l0 → l1 ≤ l0 →
+ ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T →
+ ∀T2,l,l2. ⦃G, L⦄ ⊢ T •*⬌*[h,g,l,l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,g,l1+l,l2] T2.
+#h #g #G #L #T1 #l0 #l1 #Hl0 #Hl10 #T #HT1 #T2 #l #l2 *
+/3 width=3 by cpds_div, lstas_cpds_trans/ qed-.
+
+(* Main properties **********************************************************)
+
+theorem cpes_trans: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
+ ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+#h #g #G #L #T1 #T #l1 #l * #X1 #HT1X1 #HTX1 #T2 #l2 * #X2 #HTX2 #HT2X2
+elim (cpds_conf_eq … HTX1 … HTX2) -T -l /3 width=5 by cpds_cprs_trans, cpds_div/
+qed-.
+
+theorem cpes_canc_sn: ∀h,g,G,L,T,T1,l,l1. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l1] T1 →
+ ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+#h #g #G #L #T #T1 #l #l1 #HT1
+@cpes_trans /2 width=1 by cpes_sym/ (**) (* full auto raises NTypeChecker failure *)
+qed-.
+
+theorem cpes_canc_dx: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
+ ∀T2,l2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
+#h #g #G #L #T1 #T #l1 #l #HT1 #T2 #l2 #HT2
+@(cpes_trans … HT1) -T1 -l1 /2 width=1 by cpes_sym/ (**) (* full auto raises NTypeChecker failure *)
+qed-.
--- /dev/null
+(* Advanced properties ******************************************************)
+
+lemma cpds_cpes_dx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T2.
+#h #g #G #L #T1 #T2 #l * /3 width=6 by cpcs_cprs_dx, ex4_2_intro/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpes_inv_abst2: ∀h,g,a,G,L,W1,T1,T,l. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l] ⓛ{a}W1.T1 →
+ ∃∃W2,T2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l] ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2.
+#h #g #a #G #L #W1 #T1 #T #l2 * #T0 #l1 #Hl21 #HT #HT0 #H
+elim (cpcs_inv_abst2 … H) -H /3 width=6 by ex4_2_intro, ex2_2_intro/
+qed-.
+
+(****************************************************************************)
+
+lemma sta_cpcs_cpes: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T →
+ ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, 1] T2.
+/3 width=6 by sta_lstas, ex4_2_intro/ qed.
+
+lemma lstas_cpes: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T2.
+/2 width=6 by ex4_2_intro/ qed.
+
+lemma cpes_strap1: ∀h,g,G,L,T1,T,T2,l.
+ ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T2.
+#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cpcs_strap1, ex4_2_intro/
+qed.
--- /dev/null
+lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G #L1 #T1 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
+qed-.
+
+lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H
+@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
+qed-.
+
+lemma da_cpcs: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+ ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
+ ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2.
+#h #g #G #L #T1 #HT1 #T2 #HT2 #l1 #Hl1 #l2 #Hl2 #H
+elim (cpcs_inv_cprs … H) -H /3 width=12 by da_cprs_lpr, da_mono/
+qed-.
+
+lemma sta_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •[h] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L1 #T1 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12
+elim (lstas_cpr_lpr … 1 … Hl U1 … HT12 … HL12) -Hl -HT12 -HL12
+/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/
+qed-.
+
+lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2
+[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+ ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
+ ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
+elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
+lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
+qed-.
+
+lemma snv_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
+ ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
+ ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g].
+/3 width=7 by lstas_inv_SO, sta_lstas, snv_lstas/ qed-.
+
+lemma lstas_cpds: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+ ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
+ ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 →
+ ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2.
+#h #g #G #L #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2
+lapply (da_mono … H … Hl1) -H #H destruct
+lapply (lstas_da_conf … HTU1 … Hl1) #Hl12
+elim (le_or_ge l2 l) #Hl2
+[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T //
+ /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/
+| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l
+ lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1
+ elim (lstas_cprs_lpr … Hl1l … HTU1 … HTT2 L) -Hl1l -HTU1 -HTT2
+ /3 width=7 by snv_lstas, cpcs_cpes, monotonic_le_minus_l, ex3_2_intro/
+]
+qed-.
+
+lemma cpds_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #g #G #L1 #T1 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (lstas_cpr_lpr … Hl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12
+lapply (da_cpr_lpr … Hl1 … HT12 … HL12) // -T1
+lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * break [ term 46 h , break term 46 g ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DPConvStar $h $g $G $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * break [ term 46 h , break term 46 g , break term 46 l1 , break term 46 l2 ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'DPConvStar $h $g $l1 $l2 $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 h , break term 46 g ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DPRedStar $h $g $G $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 h , break term 46 g , break term 46 l ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'DPRedStar $h $g $l $G $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h , break term 46 g , break term 46 l ] )"
+ non associative with precedence 45
+ for @{ 'NativeValid $h $g $l $G $L $T }.
(* Main properties on irreducibility ****************************************)
-theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
+theorem cix_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
/2 width=6 by cpx_fwd_cix/ qed.
(* Main inversion lemmas on irreducibility **********************************)
-theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
+theorem cnx_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
/2 width=7 by cnx_inv_crx/ qed-.
(* *)
(**************************************************************************)
-include "ground_2/lib/bool.ma".
include "ground_2/lib/lstar.ma".
include "basic_2/notation/relations/rdrop_5.ma".
include "basic_2/notation/relations/rdrop_4.ma".
}
]
[ { "stratified native validity" * } {
- [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpcs" + "snv_preserve" * ]
+ [ "hsnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" "hsnv_aaa" *
+ [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpes" + "snv_preserve" * ]
}
]
}
class "blue"
[ { "equivalence" * } {
[ { "decomposed extended equivalence" * } {
- [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )" "cpes_cpds" * ]
+ [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "cpes_aaa" + "cpes_cpcs" + "cpes_cpes" * ]
}
]
[ { "context-sensitive equivalence" * } {
}
]
[ { "decomposed extended computation" * } {
- [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ]
+ [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ]
}
]
[ { "context-sensitive extended computation" * } {
(* Equations ****************************************************************)
+lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
+// qed-.
+
(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }.
+(* multiple existental quantifier (7, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) }.
+
(* multiple existental quantifier (7, 4) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }.
-(* multiple existental quantifier (8, 5) *)
-
-notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }.
-
-notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }.
-
-(* multiple existental quantifier (9, 3) *)
+(* multiple existental quantifier (8, 4) *)
-notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)"
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P8) }.
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P7) }.
-notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)"
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P8) }.
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) }.
-(* multiple existental quantifier (10, 4) *)
+(* multiple existental quantifier (8, 5) *)
-notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)"
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P8) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P9) }.
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }.
-notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)"
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P8) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P9) }.
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }.
(* multiple disjunction connective (3) *)
<key name="ex">6 5</key>
<key name="ex">6 6</key>
<key name="ex">6 7</key>
+ <key name="ex">7 3</key>
<key name="ex">7 4</key>
<key name="ex">7 7</key>
+ <key name="ex">8 4</key>
<key name="ex">8 5</key>
- <key name="ex">9 3</key>
- <key name="ex">10 4</key>
<key name="or">3</key>
<key name="or">4</key>
<key name="or">5</key>
interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
+(* multiple existental quantifier (7, 3) *)
+
+inductive ex7_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→Prop) : Prop ≝
+ | ex7_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → ex7_3 ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_3 ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
(* multiple existental quantifier (7, 4) *)
inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝
interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
-(* multiple existental quantifier (8, 5) *)
-
-inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝
- | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7).
-
-(* multiple existental quantifier (9, 3) *)
+(* multiple existental quantifier (8, 4) *)
-inductive ex9_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8:A0→A1→A2→Prop) : Prop ≝
- | ex9_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → P7 x0 x1 x2 → P8 x0 x1 x2 → ex9_3 ? ? ? ? ? ? ? ? ? ? ? ?
+inductive ex8_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex8_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → P7 x0 x1 x2 x3 → ex8_4 ? ? ? ? ? ? ? ? ? ? ? ?
.
-interpretation "multiple existental quantifier (9, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 = (ex9_3 ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8).
+interpretation "multiple existental quantifier (8, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7).
-(* multiple existental quantifier (10, 4) *)
+(* multiple existental quantifier (8, 5) *)
-inductive ex10_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8,P9:A0→A1→A2→A3→Prop) : Prop ≝
- | ex10_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → P7 x0 x1 x2 x3 → P8 x0 x1 x2 x3 → P9 x0 x1 x2 x3 → ex10_4 ? ? ? ? ? ? ? ? ? ? ? ? ? ?
+inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝
+ | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ?
.
-interpretation "multiple existental quantifier (10, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 P9 = (ex10_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8 P9).
+interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7).
(* multiple disjunction connective (3) *)
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="xoa">
+ <key name="output_dir">contribs/lambdadelta/</key>
+ <key name="objects">ground_2/xoa/xoa2</key>
+ <key name="notations">ground_2/notation/xoa2_notation</key>
+ <key name="include">basics/pts.ma</key>
+ </section>
+</helm_registry>
projects / helm.git / commitdiff