non associative with precedence 50
for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
-notation "hvbox( ↑ [ term 46 d , break term 46 e ] break term 46 T )"
+notation "hvbox( ↑* [ term 46 f ] break term 46 T )"
non associative with precedence 46
- for @{ 'Lift $d $e $T }.
+ for @{ 'LiftStar $f $T }.
notation "hvbox( T1 ⇨ break term 46 T2 )"
non associative with precedence 45
+++ /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 "ground_2/notation/functions/append_2.ma".
-include "ground_2/ynat/ynat_plus.ma".
-include "basic_2/notation/functions/snbind2_3.ma".
-include "basic_2/notation/functions/snabbr_2.ma".
-include "basic_2/notation/functions/snabst_2.ma".
-include "basic_2/grammar/lenv_length.ma".
-
-(* LOCAL ENVIRONMENTS *******************************************************)
-
-let rec append L K on K ≝ match K with
-[ LAtom ⇒ L
-| LPair K I V ⇒ (append L K). ⓑ{I} V
-].
-
-interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
-
-interpretation "local environment tail binding construction (binary)"
- 'SnBind2 I T L = (append (LPair LAtom I T) L).
-
-interpretation "tail abbreviation (local environment)"
- 'SnAbbr T L = (append (LPair LAtom Abbr T) L).
-
-interpretation "tail abstraction (local environment)"
- 'SnAbst L T = (append (LPair LAtom Abst T) L).
-
-definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
- ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
-
-(* Basic properties *********************************************************)
-
-lemma append_atom: ∀L. L @@ ⋆ = L.
-// qed.
-
-lemma append_pair: ∀I,L,K,V. L @@ (K.ⓑ{I}V) = (L @@ K).ⓑ{I}V.
-// qed.
-
-lemma append_atom_sn: ∀L. ⋆ @@ L = L.
-#L elim L -L //
-#L #I #V >append_pair //
-qed.
-
-lemma append_assoc: associative … append.
-#L1 #L2 #L3 elim L3 -L3 //
-qed.
-
-lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
-#L1 #L2 elim L2 -L2 //
-#L2 #I #V2 >append_pair >length_pair >length_pair //
-qed.
-
-lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|.
-#I #L #V >append_length //
-qed.
-
-(* Basic_1: was just: chead_ctail *)
-lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
-#L elim L -L /2 width=5 by ex2_3_intro/
-#L #Z #X #IHL #I #V elim (IHL Z X) -IHL
-#J #K #W #H #_ >H -H >ltail_length
-@(ex2_3_intro … J (K.ⓑ{I}V) W) //
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
- L1 = L2 ∧ K1 = K2.
-#K1 elim K1 -K1
-[ * /2 width=1 by conj/
- #K2 #I2 #V2 #L1 #L2 #_ >length_atom >length_pair
- #H elim (ysucc_inv_O_sn … H)
-| #K1 #I1 #V1 #IH *
- [ #L1 #L2 #_ >length_atom >length_pair
- #H elim (ysucc_inv_O_dx … H)
- | #K2 #I2 #V2 #L1 #L2 #H1 #H2
- elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1) -IH -H1 /3 width=1 by ysucc_inv_inj, conj/
- ]
-]
-qed-.
-
-(* Note: lemma 750 *)
-lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
- L1 = L2 ∧ K1 = K2.
-#K1 elim K1 -K1
-[ * /2 width=1 by conj/
- #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct
- >length_pair >append_length <yplus_succ2 #H
- elim (discr_yplus_xy_x … H) -H #H
- [ elim (ylt_yle_false (|L2|) (∞)) // | elim (ysucc_inv_O_dx … H) ]
-| #K1 #I1 #V1 #IH *
- [ #L1 #L2 >append_pair >append_atom #H destruct
- >length_pair >append_length <yplus_succ2 #H
- elim (discr_yplus_x_xy … H) -H #H
- [ elim (ylt_yle_false (|L1|) (∞)) // | elim (ysucc_inv_O_dx … H) ]
- | #K2 #I2 #V2 #L1 #L2 >append_pair >append_pair #H1 #H2
- elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1) -IH -H1 /2 width=1 by conj/
- ]
-]
-qed-.
-
-lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
-#L #K #H elim (append_inj_dx … (⋆) … H) //
-qed-.
-
-lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
-#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
-qed-.
-
-lemma length_inv_pos_dx_ltail: ∀L,l. |L| = ⫯l →
- ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K.
-#Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct
-elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
-qed-.
-
-lemma length_inv_pos_sn_ltail: ∀L,l. ⫯l = |L| →
- ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K.
-#Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct
-elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
-qed-.
-
-(* Basic eliminators ********************************************************)
-
-(* Basic_1: was: c_tail_ind *)
-lemma lenv_ind_alt: ∀R:predicate lenv.
- R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
- ∀L. R L.
-#R #IH1 #IH2 #L @(ynat_f_ind … length … L) -L #x #IHx * // -IH1
-#L #I #V #H destruct elim (lpair_ltail L I V)
-/4 width=1 by monotonic_ylt_plus_sn/
-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 "ground_2/notation/functions/append_2.ma".
+include "basic_2/notation/functions/snbind2_3.ma".
+include "basic_2/notation/functions/snabbr_2.ma".
+include "basic_2/notation/functions/snabst_2.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENTS *******************************************************)
+
+let rec append L K on K ≝ match K with
+[ LAtom ⇒ L
+| LPair K I V ⇒ (append L K). ⓑ{I} V
+].
+
+interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+
+interpretation "local environment tail binding construction (binary)"
+ 'SnBind2 I T L = (append (LPair LAtom I T) L).
+
+interpretation "tail abbreviation (local environment)"
+ 'SnAbbr T L = (append (LPair LAtom Abbr T) L).
+
+interpretation "tail abstraction (local environment)"
+ 'SnAbst L T = (append (LPair LAtom Abst T) L).
+
+definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
+ ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
+
+(* Basic properties *********************************************************)
+
+lemma append_atom: ∀L. L @@ ⋆ = L.
+// qed.
+
+lemma append_pair: ∀I,L,K,V. L @@ (K.ⓑ{I}V) = (L @@ K).ⓑ{I}V.
+// qed.
+
+lemma append_atom_sn: ∀L. ⋆ @@ L = L.
+#L elim L -L //
+#L #I #V >append_pair //
+qed.
+
+lemma append_assoc: associative … append.
+#L1 #L2 #L3 elim L3 -L3 //
+qed.
+
+lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
+#L1 #L2 elim L2 -L2 //
+#L2 #I #V2 >append_pair >length_pair >length_pair //
+qed.
+
+lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|.
+#I #L #V >append_length //
+qed.
+
+(* Basic_1: was just: chead_ctail *)
+lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
+#L elim L -L /2 width=5 by ex2_3_intro/
+#L #Z #X #IHL #I #V elim (IHL Z X) -IHL
+#J #K #W #H #_ >H -H >ltail_length
+@(ex2_3_intro … J (K.ⓑ{I}V) W) /2 width=1 by length_pair/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
+ L1 = L2 ∧ K1 = K2.
+#K1 elim K1 -K1
+[ * /2 width=1 by conj/
+ #K2 #I2 #V2 #L1 #L2 #_ >length_atom >length_pair
+ #H destruct
+| #K1 #I1 #V1 #IH *
+ [ #L1 #L2 #_ >length_atom >length_pair
+ #H destruct
+ | #K2 #I2 #V2 #L1 #L2 #H1 #H2
+ elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
+ elim (IH … H1) -IH -H1 /2 width=1 by conj/
+ ]
+]
+qed-.
+
+(* Note: lemma 750 *)
+lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
+ L1 = L2 ∧ K1 = K2.
+#K1 elim K1 -K1
+[ * /2 width=1 by conj/
+ #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct
+ >length_pair >append_length >plus_n_Sm
+ #H elim (plus_xSy_x_false … H)
+| #K1 #I1 #V1 #IH *
+ [ #L1 #L2 >append_pair >append_atom #H destruct
+ >length_pair >append_length >plus_n_Sm #H
+ lapply (discr_plus_x_xy … H) -H #H destruct
+ | #K2 #I2 #V2 #L1 #L2 >append_pair >append_pair #H1 #H2
+ elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
+ elim (IH … H1) -IH -H1 /2 width=1 by conj/
+ ]
+]
+qed-.
+
+lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
+#L #K #H elim (append_inj_dx … (⋆) … H) //
+qed-.
+
+lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
+#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
+qed-.
+
+lemma length_inv_pos_dx_ltail: ∀L,l. |L| = ⫯l →
+ ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K.
+#Y #l #H elim (length_inv_succ_dx … H) -H #I #L #V #Hl #HLK destruct
+elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
+qed-.
+
+lemma length_inv_pos_sn_ltail: ∀L,l. ⫯l = |L| →
+ ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K.
+#Y #l #H elim (length_inv_succ_sn … H) -H #I #L #V #Hl #HLK destruct
+elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
+qed-.
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_1: was: c_tail_ind *)
+lemma lenv_ind_alt: ∀R:predicate lenv.
+ R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
+ ∀L. R L.
+#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // -IH1
+#L #I #V #H destruct elim (lpair_ltail L I V) /4 width=1 by/
+qed-.
(* Basic properties *********************************************************)
-lemma applv_nil: ∀T. Ⓐ ◊.T = T.
+lemma applv_nil: ∀T. Ⓐ◊.T = T.
// qed.
-lemma applv_cons: ∀V,Vs,T. Ⓐ V@Vs.T = ⓐV.ⒶVs.T.
+lemma applv_cons: ∀V,Vs,T. ⒶV@Vs.T = ⓐV.ⒶVs.T.
// qed.
-(* properties concerning simple terms ***************************************)
+(* Properties with simple terms *********************************************)
-lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄.
+lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄.
#T * //
qed.
(* *)
(**************************************************************************)
+include "ground_2/relocation/rtmap_isfin.ma".
include "basic_2/notation/relations/rdropstar_4.ma".
include "basic_2/relocation/lreq.ma".
include "basic_2/relocation/lifts.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
(* Basic_1: includes: drop_skip_bind drop1_skip_bind *)
(* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip
lemma drops_isuni_fwd_drop2: ∀I,X,K,V,c,f. 𝐔⦃f⦄ → ⬇*[c, f] X ≡ K.ⓑ{I}V → ⬇*[c, ⫯f] X ≡ K.
/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
+(* forward lemmas with test for finite colength *****************************)
+
+lemma drops_fwd_isfin: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐅⦃f⦄.
+#L1 #L2 #f #H elim H -L1 -L2 -f
+/3 width=1 by isfin_next, isfin_push, isfin_isid/
+qed-.
+
(* Basic_2A1: removed theorems 14:
drops_inv_nil drops_inv_cons d1_liftable_liftables
drop_refl_atom_O2
include "basic_2/relocation/drops.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-(* Properties on context sensitive equivalence for terms ********************)
+(* Properties with context-sensitive equivalence for terms ******************)
lemma ceq_lift: d_liftable2 ceq.
/2 width=3 by ex2_intro/ qed-.
include "basic_2/relocation/lifts_lifts.ma".
include "basic_2/relocation/drops_weight.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
(* Main properties **********************************************************)
(* *)
(**************************************************************************)
-include "ground_2/relocation/rtmap_isfin.ma".
include "basic_2/grammar/lenv_length.ma".
include "basic_2/relocation/drops.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
(* Forward lemmas with length for local environments ************************)
include "basic_2/relocation/drops.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-(* Properties on general entrywise extension of context-sensitive relations *)
+(* Properties with entrywise extension of context-sensitive relations *******)
(* Basic_2A1: includes: lpx_sn_deliftable_dropable *)
lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →
include "basic_2/relocation/drops_ceq.ma".
include "basic_2/relocation/drops_lexs.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-(* Properties on ranged equivalence for local environments ******************)
+(* Properties with ranged equivalence for local environments ****************)
lemma lreq_dedropable: dedropable_sn lreq.
@lexs_liftable_dedropable
include "basic_2/relocation/lreq_lreq.ma".
include "basic_2/relocation/drops.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-(* Properties on reflexive and transitive closure ***************************)
+(* Properties with reflexive and transitive closure *************************)
(* Basic_2A1: was: d_liftable_LTC *)
lemma d2_liftable_LTC: ∀R. d_liftable2 R → d_liftable2 (LTC … R).
include "basic_2/relocation/lifts_vector.ma".
include "basic_2/relocation/drops.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
definition d_liftable1_all: relation2 lenv term → predicate bool ≝
λR,c. ∀L,K,f. ⬇*[c, f] L ≡ K →
∀Ts,Us. ⬆*[f] Ts ≡ Us →
all … (R K) Ts → all … (R L) Us.
-(* Properties on general relocation for term vectors ************************)
+(* Properties with generic relocation for term vectors **********************)
(* Basic_2A1: was: d1_liftables_liftables_all *)
lemma d1_liftable_liftable_all: ∀R,c. d_liftable1 R c → d_liftable1_all R c.
include "basic_2/relocation/lifts_weight.ma".
include "basic_2/relocation/drops.ma".
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-(* Forward lemmas on weight for local environments **************************)
+(* Forward lemmas with weight for local environments ************************)
(* Basic_2A1: includes: drop_fwd_lw *)
lemma drops_fwd_lw: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}.
]
qed-.
-(* Forward lemmas on restricted weight for closures *************************)
+(* Forward lemmas with restricted weight for closures ***********************)
(* Basic_2A1: includes: drop_fwd_rfw *)
lemma drops_pair2_fwd_rfw: ∀I,L,K,V,c,f. ⬇*[c, f] L ≡ K.ⓑ{I}V → ∀T. ♯{K, V} < ♯{L, T}.
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-(* Properties on ranged equivalence for local environments ******************)
+(* Properties with ranged equivalence for local environments ****************)
lemma frees_lreq_conf: ∀L1,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≡[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
#L1 #T #f #H elim H -L1 -T -f
include "basic_2/relocation/frees_weight.ma".
include "basic_2/relocation/frees_lreq.ma".
-(* LAZY EQUIVALENCE FOR CLOSURES ********************************************)
+(* RANGED EQUIVALENCE FOR CLOSURES ******************************************)
inductive freq (G) (L1) (T): relation3 genv lenv term ≝
| fleq_intro: ∀L2,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → freq G L1 T G L2 T
include "basic_2/relocation/frees_frees.ma".
include "basic_2/relocation/freq.ma".
-(* LAZY EQUIVALENCE FOR CLOSURES *******************************************)
+(* RANGED EQUIVALENCE FOR CLOSURES *****************************************)
(* Main properties **********************************************************)
include "basic_2/notation/relations/relationstar_5.ma".
include "basic_2/grammar/lenv.ma".
-(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
+(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
≝ λA,B,C,D,E.A→B→C→D→E→Prop.
include "basic_2/grammar/lenv_length.ma".
include "basic_2/relocation/lexs.ma".
-(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
+(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
-(* Forward lemmas on length for local environments **************************)
+(* Forward lemmas with length for local environments ************************)
(* Basic_2A1: includes: lpx_sn_fwd_length *)
lemma lexs_fwd_length: ∀RN,RP,L1,L2,f. L1 ⦻*[RN, RP, f] L2 → |L1| = |L2|.
include "basic_2/grammar/lenv_weight.ma".
include "basic_2/relocation/lexs.ma".
-(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
+(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
(* Main properties **********************************************************)
(* GENERIC RELOCATION FOR TERMS *********************************************)
-(* Forward lemmas on simple terms *******************************************)
+(* Forward lemmas with simple terms *****************************************)
(* Basic_2A1: includes: lift_simple_dx *)
lemma lifts_simple_dx: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
(* GENERIC RELOCATION FOR TERMS *********************************************)
-(* Forward lemmas on weight for terms ***************************************)
+(* Forward lemmas with weight for terms *************************************)
(* Basic_2A1: includes: lift_fwd_tw *)
lemma lifts_fwd_tw: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → ♯{T1} = ♯{T2}.
(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************)
-(* Forward lemmas on length for local environments **************************)
+(* Forward lemmas with length for local environments ************************)
(* Basic_2A1: includes: lreq_fwd_length *)
lemma lreq_fwd_length: ∀L1,L2,f. L1 ≡[f] L2 → |L1| = |L2|.
for native type assignment.
</news>
- <subsection name="A">Stage "A": "Extending the Applicability Condition"</subsection>
+ <subsection name="A2">Stage "A2": "Extending the Applicability Condition"</subsection>
<news class="alpha" date="2015 October 9.">
λδ version 2A2 is started.
</news>
+
+ <subsection name="A1">Stage "A1": "Extending the Applicability Condition"</subsection>
<news class="delta" date="2015 August 27.">
λδ version 2A1 appears too complex and is dismissed.
</news>
]
}
]
+(*
class "wine"
[ { "examples" * } {
[ { "terms with special features" * } {
]
}
]
- class "yellow"
- [ { "multiple substitution" * } {
- [ { "lazy equivalence" * } {
- [ "fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
- [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
- }
- ]
- [ { "lazy pointwise extension of a relation" * } {
- [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
- }
- ]
- [ { "pointwise union for local environments" * } {
- [ "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
- }
- ]
- [ { "context-sensitive exclusion from free variables" * } {
- [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_lreq" + "frees_lift" * ]
- }
- ]
+
[ { "context-sensitive multiple rt-substitution" * } {
[ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
}
[ "fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
}
]
- [ { "iterated local env. slicing" * } {
- [ "drops ( ⬇*[?,?] ? ≡ ? )" "drops_drop" + "drops_drops" * ]
- }
- ]
- [ { "generic term relocation" * } {
- [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lift_vector" * ]
- [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ]
+ [ { "pointwise union for local environments" * } {
+ [ "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
}
]
[ { "support for multiple relocation" * } {
[ "mr2 ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" "mr2_mr2" * ]
}
]
- }
- ]
- class "orange"
- [ { "substitution" * } {
+ [ { "lazy pointwise extension of a relation" * } {
+ [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
+ }
+ ]
[ { "structural successor for closures" * } {
[ "fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )" * ]
[ "fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" * ]
[ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
}
]
- [ { "basic local env. slicing" * } {
- [ "drop ( ⬇[?,?,?] ? ≡ ? )" "drop_append" + "drop_lreq" + "drop_drop" * ]
+ [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
+*)
+ class "yellow"
+ [ { "relocation" * } {
+ [ { "ranged equivalence for closures" * } {
+ [ "freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "freq_freq" * ]
+ }
+ ]
+ [ { "context-sensitive free variables" * } {
+ [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_frees" * ]
}
]
- [ { "basic term relocation" * } {
- [ "lift_vector ( ⬆[?,?] ? ≡ ? )" "lift_lift_vector" * ]
- [ "lift ( ⬆[?,?] ? ≡ ? )" "lift_neq" + "lift_lift" * ]
+ [ { "generic slicing for local environments" * } {
+ [ "drops_vector ( ⬇*[?,?] ? ≡ ? )" * ]
+ [ "drops ( ⬇*[?,?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ceq" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+ }
+ ]
+ [ { "generic relocation for terms" * } {
+ [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lift_vector" * ]
+ [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_lifts" * ]
+ }
+ ]
+ [ { "ranged equivalence for local environments" * } {
+ [ "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
+ }
+ ]
+ [ { "generic entrywise extension of context-sensitive relations for terma" * } {
+ [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_length" + "lexs_lexs" * ]
+ }
+ ]
+ }
+ ]
+ class "orange"
+ [ { "" * } {
+ [ { "" * } {
+ [ * ]
}
]
}
]
class "red"
[ { "grammar" * } {
- [ { "equivalence for local environments" * } {
- [ "lreq ( ? ⩬[?,?] ? )" "lreq_lreq" * ]
+ [ { "context-sensitive equivalences for terms" * } {
+ [ "ceq" "ceq_ceq" * ]
}
]
[ { "same top term structure" * } {
projects / helm.git / commitdiff