# summary ####################################################################
define SUMMARY_TEMPLATE
- TBL_$(1) := $(1)/$(1)_sum.tbl
+ TBL_$(1) := $(1)/web/$(1)_sum.tbl
TBLS += $$(TBL_$(1))
$$(TBL_$(1)): S1 := $$(shell ls $$(MAS_$(1)) | wc -l)
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "applications of lambdadelta version 2"
+ title = "applications of lambdadelta version 2"
+ head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
+>
+ <section>Contents of the Specification</section>
+ <body>This specification comprises a collection of checked
+ applications of λδ version 2.
+ In particular it contains the components below.
+ </body>
+ <news date="MLTT1.">
+ Martin-Löf's Type Theory with one universe
+ using λδ as theory of expressions.
+ </news>
+ <news date="Functional.">
+ The validation algorithm for λδ as implemented in
+ <rlink to="implementation.html#helena">Helena 0.8</rlink>.
+ </news>
+
+ <section>Summary of the Specification</section>
+ <body>Here is a numerical acount of the specification's contents
+ and its timeline.
+ </body>
+ <table name="apps_2_sum"/>
+ <news date="2012 February 24.">
+ The Applications directory is started.
+ </news>
+ <news date="2011 December 20.">
+ The Functional component is started
+ inside the specification of λδ version 2.
+ </news>
+ <news date="2011 December 12.">
+ The MLTT1 component is started.
+ </news>
+
+ <section>Logical Structure of the Specification</section>
+ <body>The source files are grouped in planes and components
+ according to the following table.
+ Each component contains its own notation file.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses (? are placeholders).
+ </body>
+ <table name="apps_2_src"/>
+
+ <section>Physical Structure of the Specification</section>
+ <body>The source files are grouped in directories,
+ one for each component.
+ </body>
+ <footer/>
+</page>
--- /dev/null
+name "apps_2_src"
+
+table {
+ class "grey"
+ [ { "component" * } {
+ [ { "plane" * } {
+ [ "files" * ]
+ }
+ ]
+ }
+ ]
+ class "orange"
+ [ { "MLTT1" * } {
+ [ { "" * } {
+ [ "genv_primitive" "judgement" * ]
+ }
+ ]
+ }
+ ]
+ class "red"
+ [ { "functional" * } {
+ [ { "reduction and type machine" * } {
+ [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+ }
+ ]
+ [ { "unfold" * } {
+ [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
+ }
+ ]
+ }
+ ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
--- /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.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Note: this is not transitive *)
+inductive lsubsv (h:sh) (g:sd h): relation lenv ≝
+| lsubsv_atom: lsubsv h g (⋆) (⋆)
+| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 →
+ lsubsv h g (L1. ⓑ{I} V) (L2. ⓑ{I} V)
+| lsubsv_abbr: ∀L1,L2,V1,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g, l+1] W1 →
+ L1 ⊢ W2 ⬌* W1 → ⦃h, L2⦄ ⊩ W2 :[g] →
+ lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2)
+.
+
+interpretation
+ "local environment refinement (stratified native validity)"
+ 'CrSubEqV h g L1 L2 = (lsubsv h g L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
+#h #g #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V1 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊩:⊑[g] L2 → L2 = ⋆.
+/2 width=5 by lsubsv_inv_atom1_aux/ qed-.
+
+fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+ ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
+ ∃∃K2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] &
+ h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
+#h #g #L1 #L2 * -L1 -L2
+[ #J #K1 #U1 #H destruct
+| #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/
+| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #HL12 #J #K1 #U1 #H destruct /3 width=9/
+]
+qed-.
+
+lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊩:⊑[g] L2 →
+ (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
+ ∃∃K2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] &
+ h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
+/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
+
+fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
+#h #g #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V1 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊩:⊑[g] ⋆ → L1 = ⋆.
+/2 width=5 by lsubsv_inv_atom2_aux/ qed-.
+
+fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+ ∀I,K2,W2. L2 = K2. ⓑ{I} W2 →
+ (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
+ ∃∃K1,W1,V1,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] &
+ h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
+#h #g #L1 #L2 * -L1 -L2
+[ #J #K2 #U2 #H destruct
+| #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/
+| #L1 #L2 #V1 #W1 #W2 #l #HV #HVW1 #HW21 #HW2 #HL12 #J #K2 #U2 #H destruct /3 width=9/
+]
+qed-.
+
+lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊩:⊑[g] K2. ⓑ{I} W2 →
+ (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
+ ∃∃K1,W1,V1,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] &
+ h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
+/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
+
+(* Basic_forward lemmas *****************************************************)
+
+lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L1|] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubsv_refl: ∀h,g,L. h ⊢ L ⊩:⊑[g] L.
+#h #g #L elim L -L // /2 width=1/
+qed.
+
+lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+/3 width=5 by lsubsv_fwd_lsubs2, cprs_lsubs_trans/
+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/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+ ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=4/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+]
+qed.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+ ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=4/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+]
+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/lsubsv_ldrop.ma".
+(*
+include "basic_2/dynamic/lsubsv_ssta.ma".
+include "basic_2/dynamic/lsubsv_cpcs.ma".
+*)
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties concerning stratified native validity *************************)
+(*
+axiom lsubsv_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
+ ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2.
+
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_xprs_trans/ qed-.
+*)
+axiom lsubsv_snv_trans: ∀h,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] →
+ ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g].
+(*
+#h #g #L2 #T #H elim H -L2 -T //
+[ #I2 #L2 #K2 #V2 #i #HLK2 #_ #IHV2 #L1 #HL12
+ elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -IHV2 ]
+ [ #HK12 #H destruct /3 width=5/
+ | #V1 #l #HV1 #_ #_ #_ #H destruct /2 width=5/
+ ]
+| #a #I #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 /4 width=1/
+| #a #L2 #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU #IHV #IHT #L1 #HL12
+ lapply (IHV … HL12) -IHV #HV
+ lapply (IHT … HL12) -IHT #HT
+ lapply (lsubsv_ssta_trans … HVW … HL12) -HVW #HVW
+ lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0
+ lapply (lsubsv_xprs_trans … HL12 … HTU) -HL12 -HTU /2 width=8/
+| #L2 #W #T #U #l #_ #_ #HTU #HWU #IHW #IHT #L1 #HL12
+ lapply (IHW … HL12) -IHW #HW
+ lapply (IHT … HL12) -IHT #HT
+ lapply (lsubsv_ssta_trans … HTU … HL12) -HTU #HTU
+ lapply (lsubsv_cpcs_trans … HL12 … HWU) -HL12 -HWU /2 width=4/
+]
+qed-.
+*)
include "basic_2/computation/dxprs_dxprs.ma".
include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/lsubsv_snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 /2 width=8/
+ | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
+ elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
+ elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
+ lapply (cprs_div … HW230 … HW10) -W30 #HW210
+ lapply (ltpr_cpcs_conf … HL12 … HW210) -HW210 #HW210
+ lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
+ lapply (IH1 … HW20 … HL12 W20 ?) // [ /2 width=1/ ] -HW20 #HW20
+ lapply (IH1 … HT20 … (L2.ⓛW20) … HT202) [1,2: /2 width=1/ ] -IH1 -HT20 -HT202 #HT2
+ elim (IH3 … HVW1 … HL12 … HV12) // [2: /2 width=1/ ] -HV1 -HVW1 -HV12 #W200 #HVW200 #H
+ lapply (cpcs_trans … HW210 … H) -W10 #HW200
+ lapply (lsubsv_snv_trans … HT2 (L2.ⓓV2) ?) -L1 -HT2 /2 width=1/ /2 width=4/
+ |
\ No newline at end of file
+++ /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.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Note: this is not transitive *)
-inductive lsubsv (h:sh) (g:sd h): relation lenv ≝
-| lsubsv_atom: lsubsv h g (⋆) (⋆)
-| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 →
- lsubsv h g (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsubsv_abbr: ∀L1,L2,V1,V2,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → L1 ⊢ W2 ⬌* W1 →
- ⦃h, L1⦄ ⊢ V1 •[g, l + 1] W1 → ⦃h, L2⦄ ⊢ W2 •[g, l] V2 →
- lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2)
-.
-
-interpretation
- "local environment refinement (stratified native validity)"
- 'CrSubEqV h g L1 L2 = (lsubsv h g L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊩:⊑[g] L2 → L2 = ⋆.
-/2 width=5 by lsubsv_inv_atom1_aux/ qed-.
-
-fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
- ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
- ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
-#h #g #L1 #L2 * -L1 -L2
-[ #J #K1 #U1 #H destruct
-| #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HW21 #HVW1 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=10/
-]
-qed-.
-
-lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊩:⊑[g] L2 →
- (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
- ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
-/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
-
-fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊩:⊑[g] ⋆ → L1 = ⋆.
-/2 width=5 by lsubsv_inv_atom2_aux/ qed-.
-
-fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
- ∀I,K2,W2. L2 = K2. ⓑ{I} W2 →
- (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
- ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
-#h #g #L1 #L2 * -L1 -L2
-[ #J #K2 #U2 #H destruct
-| #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV #HW21 #HVW1 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=11/
-]
-qed-.
-
-lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊩:⊑[g] K2. ⓑ{I} W2 →
- (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
- ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
-/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
-
-(* Basic_forward lemmas *****************************************************)
-
-lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L1|] L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
-qed-.
-
-lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsubsv_refl: ∀h,g,L. h ⊢ L ⊩:⊑[g] L.
-#h #g #L elim L -L // /2 width=1/
-qed.
-
-lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
- ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-/3 width=5 by lsubsv_fwd_lsubs2, cprs_lsubs_trans/
-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/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties concerning basic local environment slicing ********************)
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
- ∀K1,e. ⇩[0, e] L1 ≡ K1 →
- ∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
- elim (ldrop_inv_O1 … H) -H * #He #HLK1
- [ destruct
- elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
- <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
- ]
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HW21 #HVW1 #HWV2 #_ #IHL12 #K1 #e #H
- elim (ldrop_inv_O1 … H) -H * #He #HLK1
- [ destruct
- elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
- <(ldrop_inv_refl … H) in HL12; -H /3 width=6/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
- ]
-]
-qed.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
- ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
- elim (ldrop_inv_O1 … H) -H * #He #HLK2
- [ destruct
- elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
- <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
- ]
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV #HW21 #HVW1 #HWV2 #_ #IHL12 #K2 #e #H
- elim (ldrop_inv_O1 … H) -H * #He #HLK2
- [ destruct
- elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
- <(ldrop_inv_refl … H) in HL12; -H /3 width=6/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
- ]
-]
-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/lsubsv_ldrop.ma".
-include "basic_2/dynamic/lsubsv_ssta.ma".
-include "basic_2/dynamic/lsubsv_cpcs.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties concerning stratified native validity *************************)
-
-axiom lsubsv_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
- ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2.
-(*
-/3 width=3 by lsubsv_fwd_lsubss, lsubss_xprs_trans/ qed-.
-*)
-axiom lsubsv_snv_trans: ∀h,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] →
- ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g].
-(*
-#h #g #L2 #T #H elim H -L2 -T //
-[ #I2 #L2 #K2 #V2 #i #HLK2 #_ #IHV2 #L1 #HL12
- elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -IHV2 ]
- [ #HK12 #H destruct /3 width=5/
- | #V1 #l #HV1 #_ #_ #_ #H destruct /2 width=5/
- ]
-| #a #I #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 /4 width=1/
-| #a #L2 #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU #IHV #IHT #L1 #HL12
- lapply (IHV … HL12) -IHV #HV
- lapply (IHT … HL12) -IHT #HT
- lapply (lsubsv_ssta_trans … HVW … HL12) -HVW #HVW
- lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0
- lapply (lsubsv_xprs_trans … HL12 … HTU) -HL12 -HTU /2 width=8/
-| #L2 #W #T #U #l #_ #_ #HTU #HWU #IHW #IHT #L1 #HL12
- lapply (IHW … HL12) -IHW #HW
- lapply (IHT … HL12) -IHT #HT
- lapply (lsubsv_ssta_trans … HTU … HL12) -HTU #HTU
- lapply (lsubsv_cpcs_trans … HL12 … HWU) -HL12 -HWU /2 width=4/
-]
-qed-.
-*)
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "lambdadelta version 2"
+ title = "lambdadelta version 2"
+ head = "cic:/matita/lambdadelta/basic_2/ (λδ version 2)"
+>
+ <section>System's Syntax and Behavior</section>
+ <body>This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </body>
+ <table name="basic_2_blk"/>
+ <body>* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </body>
+
+ <section>Summary of the Specification</section>
+ <body>Here is a numerical acount of the specification's contents
+ and its timeline.
+ </body>
+ <table name="basic_2_sum"/>
+ <news date="In progress.">
+ Context-sensitive subject equivalence
+ for native type assignment.
+ </news>
+ <news date="In progress.">
+ Closure of extended context-sensitive computation
+ for native validity.
+ </news>
+ <news date="In progress.">
+ Extended context-sensitive strong normalization
+ for simply typed terms.
+ </news>
+ <news date="2012 October 16.">
+ Confluence for context-free parallel reduction on closures.
+ </news>
+ <news date="2012 July 26.">
+ Term binders polarized to control ζ reduction.
+ </news>
+ <news date="2012 April 16.">
+ Context-sensitive subject equivalence
+ for atomic arity assignment
+ (anniversary milestone).
+ </news>
+ <news date="2012 March 15.">
+ Context-sensitive strong normalization
+ for simply typed terms.
+ </news>
+ <news date="2012 January 27.">
+ Support for abstract candidates of reducibility.
+ </news>
+ <news date="2011 September 21.">
+ Confluence for context-sensitive parallel reduction on terms.
+ </news>
+ <news date="2011 September 6.">
+ Confluence for context-free parallel reduction on terms.
+ </news>
+ <news date="2011 April 17.">
+ Specification starts.
+ </news>
+
+ <section>Logical Structure of the Specification</section>
+ <body>The source files are grouped in planes and components
+ according to the following table.
+ A notation file covering the whole specification is provided.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses (? are placeholders).
+ </body>
+ <table name="basic_2_src"/>
+
+ <section>Physical Structure of the Specification</section>
+ <body>The source files are grouped in directories,
+ one for each component.
+ </body>
+ <footer/>
+</page>
--- /dev/null
+name "basic_2_blk"
+
+table {
+ class "grey" [ { "domain" * } {
+ [
+ [ "block" ] [ "leader" ]
+ [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ]
+ ]
+ } ]
+ [ { "{X | Γ ⊢ X : W}" * } {
+ class "wine" [
+ [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ]
+ [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
+ ]
+ class "magenta" [
+ [ "local typed declaration **" ] [ "Γ ⊢ -λW" ]
+ [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
+ ]
+ class "prune" [
+ [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+ ]
+ class "blue" [
+ [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ]
+ [ "no" ] [ "no" ] [ "yes" ] [ "no" ]
+ ]
+ } ]
+ [ { "{X | Γ ⊢ X = V}" * } {
+ class "sky" [
+ [ "local abbreviation *" ] [ "Γ ⊢ +δV" ]
+ [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
+ ]
+ class "cyan" [
+ [ "local definition **" ] [ "Γ ⊢ -δV" ]
+ [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ]
+ ]
+ class "water" [
+ [ "global definition ***" ] [ "Γ ⊢ pδV" ]
+ [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
+ ]
+ } ]
+ [ { "no" * } {
+ class "green" [
+ [ "sort ****" ] [ "Γ ⊢ ⋆k" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "no" ]
+ ]
+ } ]
+}
+
+class "text" { 0 } { 2 * }
+
+class "plane" { 1 }
--- /dev/null
+name "basic_2_src"
+
+table {
+ class "grey"
+ [ { "component" * } {
+ [ { "plane" * } {
+ [ "files" * ]
+ }
+ ]
+ }
+ ]
+(*
+ class "wine"
+ [ { "examples" * } {
+ [ { "" * } {
+ [ "" * ]
+ }
+ ]
+ }
+ ]
+ class "magenta"
+ [ { "higher order dynamic typing" * } {
+ [ { "higher order native type assignment" * } {
+ [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
+ }
+ ]
+ }
+ ]
+*)
+ class "prune"
+ [ { "dynamic typing" * } {
+(*
+ [ { "local env. ref. for native type assignment" * } {
+ [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ]
+ }
+ ]
+ [ { "native type assignment" * } {
+ [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
+ }
+ ]
+*)
+ [ { "local env. ref. for stratified native validity" * } {
+ [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" "lsubsv_snv" * ]
+ }
+ ]
+ [ { "stratified native validity" * } {
+ [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ]
+ }
+ ]
+ }
+ ]
+ class "blue"
+ [ { "equivalence" * } {
+ [ { "focalized equivalence" * } {
+ [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_fpcs" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
+ [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ]
+ }
+ ]
+ [ { "local env. ref. for context-sensitive equivalence" * } {
+ [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ]
+ }
+ ]
+ [ { "context-sensitive equivalence" * } {
+ [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss_dx" + "cpcs_ltpss_sn" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ]
+ }
+ ]
+ }
+ ]
+ class "sky"
+ [ { "conversion" * } {
+ [ { "focalized conversion" * } {
+ [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
+ [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ]
+ }
+ ]
+ [ { "context-sensitive conversion" * } {
+ [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
+ }
+ ]
+ }
+ ]
+ class "cyan"
+ [ { "computation" * } {
+ [ { "focalized computation" * } {
+ [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ]
+ [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
+ }
+ ]
+ [ { "\"big tree\" order" * } {
+ [ "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
+ }
+ ]
+ [ { "decomposed extended computation" * } {
+ [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ]
+ }
+ ]
+ [ { "weakly normalizing computation" * } {
+ [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ]
+ }
+ ]
+ [ { "strongly normalizing computation" * } {
+ [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" + "csn_tstc_vector" + "csn_aaa" * ]
+ [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ]
+ }
+ ]
+ [ { "context-sensitive computation" * } {
+ [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
+ }
+ ]
+ [ { "context-free computation" * } {
+ [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" + "ltprs_ltprs" * ]
+ [ "tprs ( ? ➡* ?)" "tprs_lift" + "tprs_tprs" * ]
+ }
+ ]
+ [ { "local env. ref. for abstract candidates of reducibility" * } {
+ [ "lsubc ( ? ⊑[?] ? )" "lsubc_ldrop" + "lsubc_ldrops" + "lsubc_lsuba" * ]
+ }
+ ]
+ [ { "support for abstract computation properties" * } {
+ [ "acp" "acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )" "acp_aaa" * ]
+ }
+ ]
+ }
+ ]
+ class "water"
+ [ { "reducibility" * } {
+ [ { "context-sensitive focalized reduction" * } {
+ [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
+ }
+ ]
+ [ { "context-free focalized reduction" * } {
+ [ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" "lfpr_aaa" + "lfpr_cpr" + "lfpr_fpr" + "lfpr_lfpr" * ]
+ [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ]
+ }
+ ]
+ [ { "\"big tree\" successor" * } {
+ [ "ysucc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
+ }
+ ]
+ [ { "context-sensitive normal forms" * } {
+ [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
+ }
+ ]
+ [ { "context-sensitive reduction" * } {
+ [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss_dx" + "cpr_ltpss_sn" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ]
+ }
+ ]
+ [ { "context-sensitive reducible forms" * } {
+ [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ]
+ }
+ ]
+ [ { "context-free normal forms" * } {
+ [ "thnf ( 𝐇𝐍⦃?⦄ )" * ]
+ }
+ ]
+ [ { "context-free reduction" * } {
+ [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
+ [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
+ }
+ ]
+ }
+ ]
+ class "green"
+ [ { "unwind" * } {
+ [ { "iterated stratified static type assignment" * } {
+ [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_lsubss" + "sstas_sstas" * ]
+ }
+ ]
+ }
+ ]
+ class "grass"
+ [ { "static typing" * } {
+ [ { "local env. ref. for stratified static type assignment" * } {
+ [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
+ }
+ ]
+ [ { "stratified static type assignment" * } {
+ [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ]
+ }
+ ]
+ [ { "local env. ref. for atomic arity assignment" * } {
+ [ "lsuba ( ? ⁝⊑ ? )" "lsuba_ldrop" + "lsuba_aaa" + "lsuba_lsuba" * ]
+ }
+ ]
+ [ { "atomic arity assignment" * } {
+ [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_ltpss_dx" + "aaa_ltpss_sn" + "aaa_aaa" * ]
+ }
+ ]
+ [ { "parameters" * } {
+ [ "sh" "sd" * ]
+ }
+ ]
+ }
+ ]
+ class "yellow"
+ [ { "unfold" * } {
+ [ { "basic local env. thinning" * } {
+ [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ]
+ }
+ ]
+ [ { "inverse basic term relocation" * } {
+ [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ]
+ }
+ ]
+ [ { "partial unfold" * } {
+ [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ]
+ [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ]
+ [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
+ }
+ ]
+ [ { "generic local env. slicing" * } {
+ [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
+ }
+ ]
+ [ { "iterated restricted structural predecessor for closures" * } {
+ [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ]
+ [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ]
+ }
+ ]
+ [ { "generic term relocation" * } {
+ [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
+ [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ]
+ }
+ ]
+ [ { "support for generic relocation" * } {
+ [ "gr2 ( @⦃?,?⦄ ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ]
+ }
+ ]
+ }
+ ]
+ class "orange"
+ [ { "substitution" * } {
+ [ { "parallel substitution" * } {
+ [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ]
+ }
+ ]
+ [ { "global env. slicing" * } {
+ [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
+ }
+ ]
+ [ { "basic local env. slicing" * } {
+ [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_sfr" + "ldrop_ldrop" * ]
+ }
+ ]
+ [ { "local env. ref. for substitution" * } {
+ [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
+ }
+ ]
+ [ { "restricted structural predecessor for closures" * } {
+ [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ]
+ }
+ ]
+ [ { "basic term relocation" * } {
+ [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
+ [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
+ }
+ ]
+ }
+ ]
+ class "red"
+ [ { "grammar" * } {
+ [ { "same head term form" * } {
+ [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
+ }
+ ]
+ [ { "same top term constructor" * } {
+ [ "tstc ( ? ≃ ? )" "tstc_tstc" + "tstc_vector" * ]
+ }
+ ]
+ [ { "closures" * } {
+ [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?} )" * ]
+ }
+ ]
+ [ { "internal syntax" * } {
+ [ "genv" * ]
+ [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_bi" * ]
+ [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
+ [ "item" * ]
+ }
+ ]
+ [ { "external syntax" * } {
+ [ "aarity" * ]
+ }
+ ]
+ }
+ ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
<key name="ex">6 5</key>
<key name="ex">6 6</key>
<key name="ex">6 7</key>
+ <key name="ex">7 4</key>
<key name="ex">7 7</key>
<key name="or">3</key>
<key name="or">4</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, 4) *)
+
+inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex7_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 → ex7_4 ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
(* multiple existental quantifier (7, 7) *)
inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
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, 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}.λ${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) }.
+
+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.$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) }.
+
(* multiple existental quantifier (7, 7) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 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)"
projects / helm.git / commitdiff