--- /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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝐁 )"
+ non associative with precedence 70
+ for @{ 'ClassB }.
--- /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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝐏 )"
+ non associative with precedence 70
+ for @{ 'ClassP }.
--- /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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( ɱ. break term 70 t )"
+ non associative with precedence 70
+ for @{ 'MHook $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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝗺 )"
+ non associative with precedence 70
+ for @{ 'NodeLabelM }.
+++ /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 DELAYED UPDATING ********************************************)
-
-notation "hvbox( Ꝕ term 70 x )"
- non associative with precedence 45
- for @{ 'PredicatePTail $x }.
+++ /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 DELAYED UPDATING ********************************************)
-
-notation "hvbox( ⊓ term 70 p )"
- non associative with precedence 45
- for @{ 'PredicateSquareCap $p }.
definition dfr (p) (q): relation2 prototerm prototerm ≝
λt1,t2. ∃b.
let r ≝ p●𝗔◗b●𝗟◗q in
- â\88§â\88§ â\8a\93(â\8a\97b) & râ\97\96ð\9d\97±(â\86\91â\9d\98qâ\9d\98) ϵ t1 &
- t2 ⇔ t1[⋔r←𝛗(↑❘q❘).t1⋔(p◖𝗦)]
+ â\88§â\88§ â\8a\97b ϵ ð\9d\90\81 & râ\97\96ð\9d\97±â\9d\98qâ\9d\98 ϵ t1 &
+ t1[⋔r←𝛗❘q❘.(t1⋔(p◖𝗦))] ⇔ t2
.
interpretation
include "delayed_updating/reduction/dfr.ma".
include "delayed_updating/reduction/ifr.ma".
include "delayed_updating/substitution/fsubst_lift.ma".
+include "delayed_updating/syntax/prototerm_proper_constructors.ma".
(* DELAYED FOCUSED REDUCTION ************************************************)
* #b * #Hb #Ht1 #Ht2
@(ex_intro … (⊗b)) @and3_intro
[ //
-| lapply (in_comp_lift_bi f … Ht1) -Ht1 #Ht1
-
-
-
-
+| lapply (in_comp_lift_bi f … Ht1) -Ht1 #Ht1
+| lapply (eq_lift_bi f … Ht2) -Ht2 #Ht2
+ @(subset_eq_trans … Ht2) -t2
+ @(subset_eq_trans … (lift_fsubst …))
+ [ <structure_append <structure_A_sn <structure_append <structure_L_sn
+ | //
+ | /2 width=2 by ex_intro/
+ | //
+ ]
+]
+
definition ifr (p) (q): relation2 prototerm prototerm ≝
λt1,t2. ∃b.
let r ≝ p●𝗔◗b●𝗟◗q in
- â\88§â\88§ â\8a\93(â\8a\97b) & râ\97\96ð\9d\97±(â\86\91â\9d\98qâ\9d\98) ϵ t1 &
- t2 ⇔ t1[⋔r←↑[𝐮❨↑❘q❘❩]t1⋔(p◖𝗦)]
+ â\88§â\88§ â\8a\97b ϵ ð\9d\90\81 & râ\97\96ð\9d\97±â\9d\98qâ\9d\98 ϵ t1 &
+ t1[⋔r←↑[𝐮❨❘q❘❩](t1⋔(p◖𝗦))] ⇔ t2
.
interpretation
(* FOCALIZED SUBSTITUTION ***************************************************)
-lemma lift_fsubst_sn (f) (t) (u) (p): Ꝕu →
+lemma lift_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 →
(↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]).
#f #t #u #p #Hu #ql * *
[ #rl * #r #Hr #H1 #H2 destruct
>lift_append_proper_dx
- /4 width=1 by subset_in_ext_f1_dx, or_introl/
+ /4 width=5 by in_comp_lift_bi, in_ppc_comp_trans, or_introl, ex2_intro/
| * #q #Hq #H1 #H0
@(ex2_intro … H1) @or_intror @conj // *
[ <list_append_empty_dx #H2 destruct
]
qed-.
-lemma lift_fsubst_dx (f) (t) (u) (p): Ꝕu → p ϵ ▵t → t ϵ 𝐓 →
+lemma lift_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u].
#f #t #u #p #Hu #H1p #H2p #ql * #q * *
[ #r #Hu #H1 #H2 destruct
@or_introl @ex2_intro
- [|| <lift_append_proper_dx /2 width=1 by/ ]
+ [|| <lift_append_proper_dx /2 width=5 by in_ppc_comp_trans/ ]
/2 width=3 by ex2_intro/
| #Hq #H0 #H1 destruct
- @or_intror @conj [ /2 width=1 by subset_in_ext_f1_dx/ ] *
+ @or_intror @conj [ /2 width=1 by in_comp_lift_bi/ ] *
[ <list_append_empty_dx #Hr @(H0 … (𝐞)) -H0
<list_append_empty_dx @H2p -H2p /2 width=1 by prototerm_in_comp_root/
| #l #r #Hr
]
qed-.
-lemma lift_fsubst (f) (t) (u) (p): Ꝕu → p ϵ ▵t → t ϵ 𝐓 →
+lemma lift_fsubst (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
(↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⇔ ↑[f](t[⋔p←u]).
/4 width=3 by lift_fsubst_sn, conj, lift_fsubst_dx/ qed.
[ list_empty ⇒ k f (𝐞)
| list_lcons l q ⇒
match l with
- [ label_node_d n ⇒
+ [ label_d n ⇒
match q with
[ list_empty ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (f∘𝐮❨n❩) q
| list_lcons _ _ ⇒ lift_gen (A) k (f∘𝐮❨n❩) q
]
- | label_edge_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
- | label_edge_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
- | label_edge_S ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q
+ | label_m ⇒ lift_gen (A) k f q
+ | label_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
+ | label_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
+ | label_S ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q
]
].
↑❨k, f∘𝐮❨ninj n❩, l◗p❩ = ↑{A}❨k, f, 𝗱n◗l◗p❩.
// qed.
+lemma lift_m_sn (A) (k) (p) (f):
+ ↑❨k, f, p❩ = ↑{A}❨k, f, 𝗺◗p❩.
+// qed.
+
lemma lift_L_sn (A) (k) (p) (f):
↑❨(λg,p. k g (𝗟◗p)), ⫯f, p❩ = ↑{A}❨k, f, 𝗟◗p❩.
// qed.
↑[f∘𝐮❨ninj n❩](l◗p) = ↑[f](𝗱n◗l◗p).
// qed.
+lemma lift_path_m_sn (f) (p):
+ ↑[f]p = ↑[f](𝗺◗p).
+// qed.
+
(* Basic constructions with proj_rmap ***************************************)
lemma lift_rmap_d_sn (f) (p) (n):
↑[p](f∘𝐮❨ninj n❩) = ↑[𝗱n◗p]f.
#f * // qed.
+lemma lift_rmap_m_sn (f) (p):
+ ↑[p]f = ↑[𝗺◗p]f.
+// qed.
+
lemma lift_rmap_L_sn (f) (p):
↑[p](⫯f) = ↑[𝗟◗p]f.
// qed.
lemma lift_rmap_append (p2) (p1) (f):
↑[p2]↑[p1]f = ↑[p1●p2]f.
#p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f //
-[ <lift_rmap_A_sn <lift_rmap_A_sn //
+[ <lift_rmap_m_sn <lift_rmap_m_sn //
+| <lift_rmap_A_sn <lift_rmap_A_sn //
| <lift_rmap_S_sn <lift_rmap_S_sn //
]
qed.
Q (𝐞) →
(∀n. Q (𝐞) → Q (𝗱n◗𝐞)) →
(∀n,l,p. Q (l◗p) → Q (𝗱n◗l◗p)) →
+ (∀p. Q p → Q (𝗺◗p)) →
(∀p. Q p → Q (𝗟◗p)) →
(∀p. Q p → Q (𝗔◗p)) →
(∀p. Q p → Q (𝗦◗p)) →
∀p. Q p.
-#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #p
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
elim p -p [| * [ #n * ] ]
/2 width=1 by/
qed-.
q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
#p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
[ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+| <lift_m_sn <lift_m_sn //
| <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
<IH <IH -IH <list_append_rcons_sn //
| <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
lemma in_comp_lift_bi (f) (p) (t):
p ϵ t → ↑[f]p ϵ ↑[f]t.
-/2 width=1 by subset_in_ext_f1_dx/ qed.
+/2 width=1 by subset_in_ext_f1_dx/
+qed.
+
+lemma eq_lift_bi (f) (t1) (t2):
+ t1 ⇔ t2 → ↑[f]t1 ⇔ ↑[f]t2.
+/2 width=1 by subset_equivalence_ext_f1_bi/
+qed.
(* Constructions with proper condition for path *****************************)
-lemma lift_append_proper_dx (p2) (p1) (f): Ꝕp2 →
+lemma lift_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
(⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
#p2 #p1 @(path_ind_lift … p1) -p1 //
[ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
[ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
| <lift_path_d_lcons_sn <IH //
+| <lift_path_m_sn <IH //
| <lift_path_L_sn <IH //
| <lift_path_A_sn <IH //
| <lift_path_S_sn <IH //
#n #p #f <lift_append_proper_dx //
qed.
+lemma lift_m_dx (p) (f):
+ ⊗p = ↑[f](p◖𝗺).
+#p #f <lift_append_proper_dx //
+qed.
+
lemma lift_L_dx (p) (f):
(⊗p)◖𝗟 = ↑[f](p◖𝗟).
#p #f <lift_append_proper_dx //
| <lift_path_d_lcons_sn #H
elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
/2 width=5 by ex4_2_intro/
+| <lift_path_m_sn #H
+ elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+ /2 width=5 by ex4_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_m_sn (q) (p) (f):
+ (𝗺◗q) = ↑[f]p → ⊥.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H /2 width=2 by/
+| <lift_path_m_sn #H /2 width=2 by/
| <lift_path_L_sn #H destruct
| <lift_path_A_sn #H destruct
| <lift_path_S_sn #H destruct
| <lift_path_d_lcons_sn #H
elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
/2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+ elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/
| <lift_path_L_sn #H destruct -IH
/2 width=5 by ex3_2_intro/
| <lift_path_A_sn #H destruct
| <lift_path_d_lcons_sn #H
elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
/2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+ elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/
| <lift_path_L_sn #H destruct
| <lift_path_A_sn #H destruct -IH
/2 width=5 by ex3_2_intro/
| <lift_path_d_lcons_sn #H
elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
/2 width=5 by ex3_2_intro/
-| <lift_path_L_sn #H destruct
+| <lift_path_m_sn #H
+ elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/| <lift_path_L_sn #H destruct
| <lift_path_A_sn #H destruct
| <lift_path_S_sn #H destruct -IH
/2 width=5 by ex3_2_intro/
(* Inversions with proper condition for path ********************************)
-lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): Ꝕq2 →
- q1●q2 = ↑[f]p →
+lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
+ q2 ϵ 𝐏 → q1●q2 = ↑[f]p →
∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
#q2 #q1 elim q1 -q1
[ #p #f #Hq2 <list_append_empty_sn #H destruct
[ elim (lift_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
elim Hq2 -Hq2 //
+ | elim (lift_path_inv_m_sn … H)
| elim (lift_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
@(ex3_2_intro … (r1●𝗟◗p1)) //
"by-depth delayed (prototerm)"
'ClassDPhi = (bdd).
+(*
+
(* Basic inversions *********************************************************)
lemma bdd_inv_in_comp_gen:
∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
- | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱n◗q = p
+ | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱n◗𝗺◗q = p
| ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
| ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
| ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
lemma bdd_inv_in_comp_d:
∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ t →
∨∨ ∧∧ #n ⇔ t & 𝐞 = q
- | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t
+ | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ɱ.u & 𝛗n.u ⇔ t
.
#t #q #n #Ht #Hq
elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
[ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
-| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
+| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct
+ /4 width=4 by ex3_intro, ex2_intro, or_intror/
| #u0 #q0 #_ #_ #_ #H0 destruct
| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
lemma bdd_inv_in_root_d:
∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ ▵t →
∨∨ ∧∧ #n ⇔ t & 𝐞 = q
- | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t
+ | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵ɱ.u & 𝛗n.u ⇔ t
.
#t #q #n #Ht * #r #Hq
elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
]
]
qed-.
+*)
\ No newline at end of file
include "ground/arith/pnat.ma".
include "delayed_updating/notation/functions/nodelabel_d_1.ma".
+include "delayed_updating/notation/functions/nodelabel_m_0.ma".
include "delayed_updating/notation/functions/edgelabel_l_0.ma".
include "delayed_updating/notation/functions/edgelabel_a_0.ma".
include "delayed_updating/notation/functions/edgelabel_s_0.ma".
(* LABEL ********************************************************************)
inductive label: Type[0] ≝
-| label_node_d: pnat → label
-| label_edge_L: label
-| label_edge_A: label
-| label_edge_S: label
+| label_d: pnat → label
+| label_m: label
+| label_L: label
+| label_A: label
+| label_S: label
.
interpretation
"variable reference by depth (label)"
- 'NodeLabelD p = (label_node_d p).
+ 'NodeLabelD p = (label_d p).
+
+interpretation
+ "mark (label)"
+ 'NodeLabelM = (label_m).
interpretation
"name-free functional abstruction (label)"
- 'EdgeLabelL = (label_edge_L).
+ 'EdgeLabelL = (label_L).
interpretation
"application (label)"
- 'EdgeLabelA = (label_edge_A).
+ 'EdgeLabelA = (label_A).
interpretation
"side branch (label)"
- 'EdgeLabelS = (label_edge_S).
+ 'EdgeLabelS = (label_S).
(**************************************************************************)
include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/relations/predicate_squarecap_1.ma".
+include "delayed_updating/notation/functions/class_b_0.ma".
(* BALANCE CONDITION FOR PATH ***********************************************)
(* This condition applies to a structural path *)
inductive pbc: predicate path ≝
-| pbc_empty: pbc (𝐞)
+| pbc_empty: pbc (𝐞)
| pbc_redex: ∀b. pbc b → pbc (𝗔◗b◖𝗟)
| pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1●b2)
.
interpretation
"balance condition (path)"
- 'PredicateSquareCap p = (pbc p).
+ 'ClassB = (pbc).
(**************************************************************************)
include "delayed_updating/syntax/path.ma".
-include "ground/arith/nat_succ.ma".
include "ground/notation/functions/verticalbars_1.ma".
(* DEPTH FOR PATH ***********************************************************)
-rec definition depth (p) on p: nat ≝
+rec definition depth (p) on p: pnat ≝
match p with
-[ list_empty â\87\92 ð\9d\9f\8e
+[ list_empty â\87\92 ð\9d\9f\8f
| list_lcons l q ⇒
match l with
- [ label_node_d _ ⇒ depth q
- | label_edge_L ⇒ ↑(depth q)
- | label_edge_A ⇒ depth q
- | label_edge_S ⇒ depth q
+ [ label_d _ ⇒ depth q
+ | label_m ⇒ depth q
+ | label_L ⇒ ↑(depth q)
+ | label_A ⇒ depth q
+ | label_S ⇒ depth q
]
].
(* Basic constructions ******************************************************)
-lemma depth_empty: ð\9d\9f\8e = ❘𝐞❘.
+lemma depth_empty: ð\9d\9f\8f = ❘𝐞❘.
// qed.
lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
// qed.
+lemma depth_m (q): ❘q❘ = ❘𝗺◗q❘.
+// qed.
+
lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.
// qed.
(**************************************************************************)
include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/relations/predicate_p_tail_1.ma".
+include "delayed_updating/notation/functions/class_p_0.ma".
+include "ground/lib/subset.ma".
include "ground/xoa/ex_1_2.ma".
(* PROPER CONDITION FOR PATH ************************************************)
interpretation
"proper condition (path)"
- 'PredicatePTail p = (ppc p).
+ 'ClassP = (ppc).
(* Basic constructions ******************************************************)
-lemma ppc_lcons (l) (q): Ꝕ(l◗q).
+lemma ppc_lcons (l) (q): l◗q ϵ 𝐏.
#l #p #H destruct
qed.
(* Basic inversions ********************************************************)
lemma ppc_inv_lcons (p):
- Ꝕp → ∃∃l,q. l◗q = p.
+ p ϵ 𝐏 → ∃∃l,q. l◗q = p.
*
[ #H elim H -H //
| #l #q #_ /2 width=3 by ex1_2_intro/
[ list_empty ⇒ 𝐞
| list_lcons l q ⇒
match l with
- [ label_node_d n ⇒ structure q
- | label_edge_L ⇒ 𝗟◗structure q
- | label_edge_A ⇒ 𝗔◗structure q
- | label_edge_S ⇒ 𝗦◗structure q
+ [ label_d n ⇒ structure q
+ | label_m ⇒ structure q
+ | label_L ⇒ 𝗟◗structure q
+ | label_A ⇒ 𝗔◗structure q
+ | label_S ⇒ 𝗦◗structure q
]
].
⊗p = ⊗(𝗱n◗p).
// qed.
+lemma structure_m_sn (p):
+ ⊗p = ⊗(𝗺◗p).
+// qed.
+
lemma structure_L_sn (p):
- 𝗟◗⊗p = ⊗(𝗟◗p).
+ (𝗟◗⊗p) = ⊗(𝗟◗p).
// qed.
lemma structure_A_sn (p):
- 𝗔◗⊗p = ⊗(𝗔◗p).
+ (𝗔◗⊗p) = ⊗(𝗔◗p).
// qed.
lemma structure_S_sn (p):
- 𝗦◗⊗p = ⊗(𝗦◗p).
+ (𝗦◗⊗p) = ⊗(𝗦◗p).
// qed.
(* Main constructions *******************************************************)
#p #n <structure_append //
qed.
+lemma structure_m_dx (p):
+ ⊗p = ⊗(p◖𝗺).
+#p <structure_append //
+qed.
+
lemma structure_L_dx (p):
(⊗p)◖𝗟 = ⊗(p◖𝗟).
#p <structure_append //
(**************************************************************************)
include "delayed_updating/syntax/prototerm.ma".
+include "delayed_updating/notation/functions/m_hook_1.ma".
include "delayed_updating/notation/functions/hash_1.ma".
include "delayed_updating/notation/functions/phi_2.ma".
include "delayed_updating/notation/functions/lamda_1.ma".
definition prototerm_node_1 (l): prototerm → prototerm ≝
λt,p. ∃∃q. q ϵ t & l◗q = p.
+definition prototerm_node_1_2 (l1) (l2): prototerm → prototerm ≝
+ λt,p. ∃∃q. q ϵ t & l1◗l2◗q = p.
+
definition prototerm_node_2 (l1) (l2): prototerm → prototerm → prototerm ≝
λt1,t2,p.
∨∨ ∃∃q. q ϵ t1 & l1◗q = p
| ∃∃q. q ϵ t2 & l2◗q = p.
+interpretation
+ "mark (prototerm)"
+ 'MHook t = (prototerm_node_1 label_m t).
+
interpretation
"outer variable reference by depth (prototerm)"
- 'Hash n = (prototerm_node_0 (label_node_d n)).
+ 'Hash n = (prototerm_node_0 (label_d n)).
interpretation
"inner variable reference by depth (prototerm)"
- 'Phi n t = (prototerm_node_1 (label_node_d n) t).
+ 'Phi n t = (prototerm_node_1_2 (label_d n) label_m t).
interpretation
"name-free functional abstraction (prototerm)"
- 'Lamda t = (prototerm_node_1 label_edge_L t).
+ 'Lamda t = (prototerm_node_1 label_L t).
interpretation
"application (prototerm)"
- 'At u t = (prototerm_node_2 label_edge_S label_edge_A u t).
+ 'At u t = (prototerm_node_2 label_S label_A u t).
(* Basic Inversions *********************************************************)
lemma prototerm_in_root_inv_lcons_iref:
∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
- ∧∧ 𝗱n = l & p ϵ ▵t.
-#t #p #l #n * #q
-<list_append_lcons_sn * #r #Hr #H0 destruct
+ ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
+#t #p #l #n * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct -H0
+/4 width=4 by ex2_intro, ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_mark:
+ ∀t,p,l. l◗p ϵ ▵ɱ.t →
+ ∧∧ 𝗺 = l & p ϵ ▵t.
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
/3 width=2 by ex_intro, conj/
qed-.
lemma prototerm_in_root_inv_lcons_abst:
∀t,p,l. l◗p ϵ ▵𝛌.t →
∧∧ 𝗟 = l & p ϵ ▵t.
-#t #p #l * #q
-<list_append_lcons_sn * #r #Hr #H0 destruct
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
/3 width=2 by ex_intro, conj/
qed-.
∀u,t,p,l. l◗p ϵ ▵@u.t →
∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
| ∧∧ 𝗔 = l & p ϵ ▵t.
-#u #t #p #l * #q
-<list_append_lcons_sn * * #r #Hr #H0 destruct
+#u #t #p #l * #q * * #r #Hr
+<list_append_lcons_sn #H0 destruct
/4 width=2 by ex_intro, or_introl, or_intror, conj/
qed-.
(* *)
(**************************************************************************)
+include "delayed_updating/syntax/prototerm.ma".
include "delayed_updating/syntax/path_proper.ma".
include "ground/lib/subset_ext_equivalence.ma".
interpretation
"proper condition (prototerm)"
- 'PredicatePTail t = (subset_ext_p1 path ppc t).
+ 'ClassP = (subset_ext_p1 path ppc).
(* Basic constructions ******************************************************)
lemma tpc_i (t):
- (𝐞 ⧸ϵ t) → Ꝕt.
+ (𝐞 ⧸ϵ t) → t ϵ 𝐏.
#t #Ht * //
#H elim (Ht H)
qed.
(* Basic inversions *********************************************************)
-lemma tpc_e (t): Ꝕt → 𝐞 ϵ t → ⊥.
-/2 width=5 by subset_in_inv_ext_p1_dx/ qed-.
+lemma in_ppc_comp_trans (t) (p):
+ p ϵ t → t ϵ 𝐏 → p ϵ 𝐏.
+#t #p #Hp #Ht
+@(Ht … Hp)
+qed-.
+
+lemma tpc_e (t): 𝐞 ϵ t → t ϵ 𝐏 → ⊥.
+/2 width=5 by in_ppc_comp_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 "delayed_updating/syntax/prototerm_proper.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
+
+(* PROPER CONDITION FOR PROTOTERM *******************************************)
+
+(* Constructions with prototerm constructors ********************************)
+
+lemma ppc_iref (t) (n):
+ (𝛗n.t) ϵ 𝐏.
+#t #n #p * #q #Hq #H0 destruct //
+qed.
["K"; "𝕂"; "𝐊"; "Ⓚ"; ] ;
["l"; "λ"; "𝕝"; "𝐥"; "𝛌"; "ⓛ"; ] ;
["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; "𝗟"; ] ;
- ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; ] ;
+ ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; "𝗺"; "ɱ"; ] ;
["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;
projects / helm.git / commitdiff