--- /dev/null
+notation > "hvbox( L . break ②{ term 46 I } break term 47 T1 )"
+ non associative with precedence 46
+ for @{ 'DxBind2 $L $I $T1 }.
T: boolean true
a: application
-b: binder
+b: generic binder with one argument
d: abbreviation
-f: flat
-l: abstraction
+f: generic flat with one argument
+l: typed abstraction
n: native type annotation
+u: generic binder with zero argument
+x: exclusion
NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
notation "hvbox( L . break ⓓ T1 )"
- left associative with precedence 48
+ left associative with precedence 49
for @{ 'DxAbbr $L $T1 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
notation "hvbox( L . break ⓛ T1 )"
- left associative with precedence 49
+ left associative with precedence 50
for @{ 'DxAbst $L $T1 }.
--- /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( L . break ⓤ { term 46 I } )"
+ non associative with precedence 46
+ for @{ 'DxBind1 $L $I }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation > "hvbox( L . break ②{ term 46 I } break term 47 T1 )"
- non associative with precedence 46
- for @{ 'DxBind2 $L $I $T1 }.
-
notation "hvbox( L . break ⓑ { term 46 I } break term 48 T1 )"
non associative with precedence 47
for @{ 'DxBind2 $L $I $T1 }.
--- /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( L . ⓧ )"
+ non associative with precedence 48
+ for @{ 'DxVoid $L }.
--- /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 L )"
+ non associative with precedence 55
+ for @{ 'SnBind1 $I $L }.
--- /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 L )"
+ non associative with precedence 55
+ for @{ 'SnVoid $L }.
#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L
#L1 #_ #IHL1 @lfsx_intro
#L2 #H #HnL12 elim (lfpx_pair_sn_split … o I … T H) -H
-/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/
+/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/
qed-.
(* Basic_2A1: uses: lsx_fwd_flat_dx *)
#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L
#L1 #_ #IHL1 @lfsx_intro
#L2 #H #HnL12 elim (lfpx_flat_dx_split … o I … V … H) -H
-/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/
+/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/
qed-.
(* Advanced inversion lemmas ************************************************)
∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≡[h, o, T] L2.
/3 width=5 by lfpx_frees_conf, lfxs_flat_dx_split/ qed-.
+lemma lfpx_bind_dx_split: ∀h,o,p,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 →
+ ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≡[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V.
+/3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split/ qed-.
+
lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o).
#h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/
[ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02
/4 width=7 by sle_lexs_trans, ex2_intro/
qed-.
+lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+ lexs_frees_confluent … R1 cfull →
+ ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⦻*[R1, T] L2 → ∀p.
+ ∃∃L,V. L1 ⦻*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⦻*[R2, T] L2 & R1 L1 V1 V.
+#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p
+elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg
+elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy
+lapply(frees_mono … H … Hf) -H #H2
+lapply (tl_eq_repl … H2) -H2 #H2
+lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
+lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
+elim (lexs_sle_split … HR1 HR2 … HL12 … Hfg) -HL12 #Y #H #HL2
+lapply (sle_lexs_trans … H … Hfg) // #H0
+elim (lexs_inv_next1 … H) -H #L #V #HL1 #HV0 #H destruct
+elim (HR … Hf … H0) -HR -Hf -H0
+/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/
+qed-.
+
(* Main properties **********************************************************)
(* Basic_2A1: uses: llpx_sn_bind llpx_sn_bind_O *)
projects / helm.git / commitdiff