(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
inductive bdd: π«β¨prototermβ© β
-| bdd_oref: βn. bdd (⧣n)
-| bdd_iref: βt,n. bdd t β bdd (πn.t)
+| bdd_oref: βk. bdd (⧣k)
+| bdd_iref: βt,k. bdd t β bdd (πk.t)
| bdd_abst: βt. bdd t β bdd (π.t)
| bdd_appl: βu,t. bdd u β bdd t β bdd (οΌ u.t)
| bdd_conv: βt1,t2. t1 β t2 β bdd t1 β bdd t2
interpretation
"variable reference by depth (label)"
- 'NodeLabelD p = (label_d p).
+ 'NodeLabelD k = (label_d k).
interpretation
"mark (label)"
(* PATH *********************************************************************)
-(* Note: a path is a list of labels *)
+(* Note: a path is a list of labels *)
+(* Note: constructed from the leaf (right end) to the root (left end) *)
definition path β list label.
interpretation
'ElementE = (list_empty label).
interpretation
- "left cons (paths)"
- 'BlackHalfCircleRight l p = (list_lcons label l p).
+ "right cons (paths)"
+ 'BlackHalfCircleLeft p l = (list_lcons label l p).
interpretation
"append (paths)"
- 'BlackCircle l1 l2 = (list_append label l1 l2).
+ 'BlackCircle p q = (list_append label q p).
interpretation
- "right cons (paths)"
- 'BlackHalfCircleLeft p l = (list_append label p (list_lcons label l (list_empty label))).
+ "left cons (paths)"
+ 'BlackHalfCircleRight l p = (list_append label p (list_lcons label l (list_empty label))).
lemma depth_empty: π = βπ.
// qed.
-lemma depth_d_sn (q) (n): βq = β(π±nβq).
+lemma depth_d_dx (p) (k):
+ βp = β(pβπ±k).
// qed.
-lemma depth_m_sn (q): βq = β(πΊβq).
+lemma depth_m_dx (p):
+ βp = β(pβπΊ).
// qed.
-lemma depth_L_sn (q): ββq = β(πβq).
+lemma depth_L_dx (p):
+ ββp = β(pβπ).
// qed.
-lemma depth_A_sn (q): βq = β(πβq).
+lemma depth_A_dx (p):
+ βp = β(pβπ).
// qed.
-lemma depth_S_sn (q): βq = β(π¦βq).
+lemma depth_S_dx (p):
+ βp = β(pβπ¦).
// qed.
(* Main constructions *******************************************************)
-theorem depth_append (p1) (p2):
- (βp2)+(βp1) = β(p1βp2).
-#p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
-[ <depth_d_sn <depth_d_sn //
-| <depth_m_sn <depth_m_sn //
-| <depth_L_sn <depth_L_sn //
-| <depth_A_sn <depth_A_sn //
-| <depth_S_sn <depth_S_sn //
+theorem depth_append (p) (q):
+ (βp)+(βq) = β(pβq).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <depth_d_dx <depth_d_dx //
+| <depth_m_dx <depth_m_dx //
+| <depth_L_dx <depth_L_dx //
+| <depth_A_dx <depth_A_dx //
+| <depth_S_dx <depth_S_dx //
]
qed.
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma depth_d_dx (p) (n):
- βp = β(pβπ±n).
+lemma depth_d_sn (p) (k):
+ βp = β(π±kβp).
// qed.
-lemma depth_m_dx (p):
- βp = β(pβπΊ).
+lemma depth_m_sn (p):
+ βp = β(πΊβp).
// qed.
-lemma depth_L_dx (p):
- ββp = β(pβπ).
+lemma depth_L_sn (p):
+ ββp = β(πβp).
// qed.
-lemma depth_A_dx (p):
- βp = β(pβπ).
+lemma depth_A_sn (p):
+ βp = β(πβp).
// qed.
-lemma depth_S_dx (p):
- βp = β(pβπ¦).
+lemma depth_S_sn (p):
+ βp = β(π¦βp).
// qed.
lemma depth_labels_L (n):
n = β(πββn).
#n @(nat_ind_succ β¦ n) -n //
-#n #IH <labels_succ <depth_L_sn //
+#n #IH <labels_succ <depth_L_dx //
qed.
(* HEAD FOR PATH ************************************************************)
-rec definition path_head (m) (p) on p: path β
-match m with
+rec definition path_head (n) (p) on p: path β
+match n with
[ nzero β π
-| ninj o β
+| ninj m β
match p with
- [ list_empty β πββm
+ [ list_empty β πββn
| list_lcons l q β
match l with
- [ label_d n β lβ(path_head (m+n) q)
- | label_m β lβ(path_head m q)
- | label_L β lβ(path_head (βo) q)
- | label_A β lβ(path_head m q)
- | label_S β lβ(path_head m q)
+ [ label_d k β (path_head (n+k) q)βl
+ | label_m β (path_head n q)βl
+ | label_L β (path_head (βm) q)βl
+ | label_A β (path_head n q)βl
+ | label_S β (path_head n q)βl
]
]
].
interpretation
- "head (reversed path)"
+ "head (path)"
'DownArrowRight n p = (path_head n p).
(* basic constructions ****************************************************)
(πββn) = β³[n]π.
* // qed.
-lemma path_head_d_sn (p) (n) (m:pnat):
- (π±mββ³[βn+m]p) = β³[βn](π±mβp).
+lemma path_head_d_dx (p) (n) (k:pnat):
+ (β³[βn+k]p)βπ±k = β³[βn](pβπ±k).
// qed.
-lemma path_head_m_sn (p) (n):
- (πΊββ³[βn]p) = β³[βn](πΊβp).
+lemma path_head_m_dx (p) (n):
+ (β³[βn]p)βπΊ = β³[βn](pβπΊ).
// qed.
-lemma path_head_L_sn (p) (n):
- (πββ³[n]p) = β³[βn](πβp).
+lemma path_head_L_dx (p) (n):
+ (β³[n]p)βπ = β³[βn](pβπ).
#p #n
whd in β’ (???%); //
qed.
-lemma path_head_A_sn (p) (n):
- (πββ³[βn]p) = β³[βn](πβp).
+lemma path_head_A_dx (p) (n):
+ (β³[βn]p)βπ = β³[βn](pβπ).
// qed.
-lemma path_head_S_sn (p) (n):
- (π¦ββ³[βn]p) = β³[βn](π¦βp).
+lemma path_head_S_dx (p) (n):
+ (β³[βn]p)βπ¦ = β³[βn](pβπ¦).
// qed.
(* Basic inversions *********************************************************)
lemma eq_inv_path_empty_head (p) (n):
(π) = β³[n]p β π = n.
*
-[ #
m <path_head_empty #H0
- <(eq_inv_empty_labels β¦ H0) -m //
-| * [ #n ] #p #n @(nat_ind_succ β¦ n) -n // #m #_
- [ <path_head_d_sn
- | <path_head_m_sn
- | <path_head_L_sn
- | <path_head_A_sn
- | <path_head_S_sn
+[ #
n <path_head_empty #H0
+ <(eq_inv_empty_labels β¦ H0) -n //
+| * [ #k ] #p #n @(nat_ind_succ β¦ n) -n // #n #_
+ [ <path_head_d_dx
+ | <path_head_m_dx
+ | <path_head_L_dx
+ | <path_head_A_dx
+ | <path_head_S_dx
] #H0 destruct
]
qed-.
-(* Constructions with list_append *******************************************)
+(* Constructions with path_append *******************************************)
lemma path_head_refl_append (p) (q) (n):
- q = β³[n]q β q = β³[n](qβp).
+ q = β³[n]q β q = β³[n](pβq).
#p #q elim q -q
[ #n #Hn <(eq_inv_path_empty_head β¦ Hn) -Hn //
| #l #q #IH #n @(nat_ind_succ β¦ n) -n
- [ #Hq | #n #_ cases l [ #m ] ]
+ [ #Hq | #n #_ cases l [ #k ] ]
[ lapply (eq_inv_path_head_zero_dx β¦ Hq) -Hq #Hq destruct
- | <path_head_d_sn <path_head_d_sn
- | <path_head_m_sn <path_head_m_sn
- | <path_head_L_sn <path_head_L_sn
- | <path_head_A_sn <path_head_A_sn
- | <path_head_S_sn <path_head_S_sn
+ | <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx
] #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
/3 width=1 by eq_f/
]
qed-.
-(* Inversions with list_append **********************************************)
+(* Inversions with path_append **********************************************)
lemma eq_inv_path_head_refl_append (p) (q) (n):
- q = β³[n](qβp) β q = β³[n]q.
+ q = β³[n](pβq) β q = β³[n]q.
#p #q elim q -q
[ #n #Hn <(eq_inv_path_empty_head β¦ Hn) -p //
| #l #q #IH #n @(nat_ind_succ β¦ n) -n //
- #n #_ cases l [ #m ]
- [ <path_head_d_sn <path_head_d_sn
- | <path_head_m_sn <path_head_m_sn
- | <path_head_L_sn <path_head_L_sn
- | <path_head_A_sn <path_head_A_sn
- | <path_head_S_sn <path_head_S_sn
+ #n #_ cases l [ #k ]
+ [ <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx
] #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
/3 width=1 by eq_f/
n + β―(β³[n]p) = ββ³[n]p.
#p elim p -p // #l #p #IH
#n @(nat_ind_succ β¦ n) -n // #n #_
-cases l [ #m ]
-[ <path_head_d_sn <height_d_sn <depth_d_sn //
-| <path_head_m_sn <height_m_sn <depth_m_sn //
-| <path_head_L_sn <height_L_sn <depth_L_sn
+cases l [ #k ]
+[ <path_head_d_dx <height_d_dx <depth_d_dx <IH //
+| <path_head_m_dx <height_m_dx <depth_m_dx //
+| <path_head_L_dx <height_L_dx <depth_L_dx
<nplus_succ_sn //
-| <path_head_A_sn <height_A_sn <depth_A_sn //
-| <path_head_S_sn <height_S_sn <depth_S_sn //
+| <path_head_A_dx <height_A_dx <depth_A_dx //
+| <path_head_S_dx <height_S_dx <depth_S_dx //
]
qed-. (**) (* gets in the way with auto *)
(* Constructions with structure *********************************************)
-lemma path_head_structure_height (p) (m):
- ββ³[m]p = β³[m+β―β³[m]p]βp.
+lemma path_head_structure_height (p) (n):
+ ββ³[n]p = β³[n+β―β³[n]p]βp.
#p elim p -p //
-#l #p #IH #m @(nat_ind_succ β¦ m) -m //
-#m #_ cases l [ #n ]
-[ <height_d_sn <structure_d_sn //
-| <structure_m_sn //
-| <structure_L_sn //
-| <height_A_sn <structure_A_sn <nplus_succ_sn <path_head_A_sn //
-| <height_S_sn <structure_S_sn <nplus_succ_sn <path_head_S_sn //
+#l #p #IH #n @(nat_ind_succ β¦ n) -n //
+#n #_ cases l [ #k ]
+[ <height_d_dx <structure_d_dx //
+| <structure_m_dx //
+| <structure_L_dx //
+| <height_A_dx <structure_A_dx <nplus_succ_sn <path_head_A_dx //
+| <height_S_dx <structure_S_dx <nplus_succ_sn <path_head_S_dx //
]
qed.
-lemma path_head_structure_depth (p) (m):
- ββ³[m]p = β³[ββ³[m]p]βp.
-#p #m
+lemma path_head_structure_depth (p) (n):
+ ββ³[n]p = β³[ββ³[n]p]βp.
+#p #n
<path_head_depth //
qed.
[ list_empty β π
| list_lcons l q β
match l with
- [ label_d n β n + height q
+ [ label_d k β height q + k
| label_m β height q
| label_L β height q
| label_A β height q
lemma height_empty: π = β―π.
// qed.
-lemma height_d_sn (q) (n): ninj n+β―q = β―(π±nβq).
+lemma height_d_dx (p) (k:pnat):
+ (β―p)+k = β―(pβπ±k).
// qed.
-lemma height_m_sn (q): β―q = β―(πΊβq).
+lemma height_m_dx (p):
+ (β―p) = β―(pβπΊ).
// qed.
-lemma height_L_sn (q): β―q = β―(πβq).
+lemma height_L_dx (p):
+ (β―p) = β―(pβπ).
// qed.
-lemma height_A_sn (q): β―q = β―(πβq).
+lemma height_A_dx (p):
+ (β―p) = β―(pβπ).
// qed.
-lemma height_S_sn (q): β―q = β―(π¦βq).
+lemma height_S_dx (p):
+ (β―p) = β―(pβπ¦).
// qed.
(* Main constructions *******************************************************)
-theorem height_append (p1) (p2):
- (β―p2+β―p1) = β―(p1βp2).
-#p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
-[ <height_d_sn <height_d_sn //
-| <height_m_sn <height_m_sn //
-| <height_L_sn <height_L_sn //
-| <height_A_sn <height_A_sn //
-| <height_S_sn <height_S_sn //
+theorem height_append (p) (q):
+ (β―p+β―q) = β―(pβq).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <height_d_dx <height_d_dx //
+| <height_m_dx <height_m_dx //
+| <height_L_dx <height_L_dx //
+| <height_A_dx <height_A_dx //
+| <height_S_dx <height_S_dx //
]
qed.
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma height_d_dx (p) (n):
- (β―p)+(ninj n) = β―(pβπ±n).
+lemma height_d_sn (p) (k:pnat):
+ k+β―p = β―(π±kβp).
// qed.
-lemma height_m_dx (p):
- (β―p) = β―(pβπΊ).
+lemma height_m_sn (p):
+ β―p = β―(πΊβp).
// qed.
-lemma height_L_dx (p):
- (β―p) = β―(pβπ).
+lemma height_L_sn (p):
+ β―p = β―(πβp).
// qed.
-lemma height_A_dx (p):
- (β―p) = β―(pβπ).
+lemma height_A_sn (p):
+ β―p = β―(πβp).
// qed.
-lemma height_S_dx (p):
- (β―p) = β―(pβπ¦).
+lemma height_S_sn (p):
+ β―p = β―(π¦βp).
// qed.
lemma height_labels_L (n):
(π) = β―(πββn).
#n @(nat_ind_succ β¦ n) -n //
-#n #IH <labels_succ <height_L_sn //
+#n #IH <labels_succ <height_L_dx //
qed.
(* INNER CONDITION FOR PATH *************************************************)
definition pic: predicate path β
- Ξ»p. βq,n. qβπ±n = p β β₯
+ Ξ»p. βq,k. qβπ±k = p β β₯
.
interpretation
(* Basic constructions ******************************************************)
-lemma pic_empty: π Ο΅ π.
-#q #n #H0
-elim (eq_inv_list_empty_rcons ??? (sym_eq β¦ H0))
+lemma pic_empty:
+ (π) Ο΅ π.
+#q #k #H0 destruct
qed.
-lemma pic_m_dx (p): pβπΊ Ο΅ π.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_m_dx (p):
+ pβπΊ Ο΅ π.
+#p #q #k #H0 destruct
qed.
-lemma pic_L_dx (p): pβπ Ο΅ π.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_L_dx (p):
+ pβπ Ο΅ π.
+#p #q #k #H0 destruct
qed.
-lemma pic_A_dx (p): pβπ Ο΅ π.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_A_dx (p):
+ pβπ Ο΅ π.
+#p #q #k #H0 destruct
qed.
-lemma pic_S_dx (p): pβπ¦ Ο΅ π.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_S_dx (p):
+ pβπ¦ Ο΅ π.
+#p #q #k #H0 destruct
qed.
(* Basic inversions ********************************************************)
-lemma pic_inv_d_dx (p) (n):
- pβπ±n Ο΅ π β β₯.
-#p #n #H0 @H0 -H0 //
+lemma pic_inv_d_dx (p) (k):
+ pβπ±k Ο΅ π β β₯.
+#p #k #H0 @H0 -H0 //
qed-.
// qed.
lemma labels_succ (l) (n):
- lβ(lββn) = lββ(βn).
+ (lββn)βl = lββ(βn).
#l #n
<labels_unfold <labels_unfold <niter_succ //
qed.
(* Basic constructions ******************************************************)
-lemma ppc_lcons (l) (q): lβq Ο΅ π.
-#l #q #H0 destruct
+lemma ppc_rcons (p) (l):
+ pβl Ο΅ π.
+#p #l #H0 destruct
qed.
-lemma ppc_rcons (l) (q): qβl Ο΅ π.
-#l #q #H
-elim (eq_inv_list_empty_rcons ??? H)
+lemma ppc_lcons (p) (l):
+ lβp Ο΅ π.
+#p #l #H0
+elim (eq_inv_list_empty_rcons ??? H0)
qed.
(* Basic inversions ********************************************************)
#H0 @H0 -H0 //
qed-.
-lemma ppc_inv_lcons (p):
- p Ο΅ π β ββl,q. lβq = p.
+lemma ppc_inv_rcons (p):
+ p Ο΅ π β ββq,l. qβl = p.
*
[ #H0 elim (ppc_inv_empty β¦ H0)
| #l #q #_ /2 width=3 by ex1_2_intro/
]
qed-.
-lemma ppc_inv_rcons (p):
- p Ο΅ π β ββq,l. qβl = p.
+lemma ppc_inv_lcons (p):
+ p Ο΅ π β ββq,l. lβq = p.
#p @(list_ind_rcons β¦ p) -p
[ #H0 elim (ppc_inv_empty β¦ H0)
| #q #l #_ #_ /2 width=3 by ex1_2_intro/
[ list_empty β π
| list_lcons l q β
match l with
- [ label_d n β structure q
+ [ label_d k β structure q
| label_m β structure q
- | label_L β πβstructure q
- | label_A β πβstructure q
- | label_S β π¦βstructure q
+ | label_L β (structure q)βπ
+ | label_A β (structure q)βπ
+ | label_S β (structure q)βπ¦
]
].
π = βπ.
// qed.
-lemma structure_d_sn (p) (n):
- βp = β(π±nβp).
+lemma structure_d_dx (p) (k):
+ βp = β(pβπ±k).
// qed.
-lemma structure_m_sn (p):
- βp = β(πΊβp).
+lemma structure_m_dx (p):
+ βp = β(pβπΊ).
// qed.
-lemma structure_L_sn (p):
- (πββp) = β(πβp).
+lemma structure_L_dx (p):
+ (βp)βπ = β(pβπ).
// qed.
-lemma structure_A_sn (p):
- (πββp) = β(πβp).
+lemma structure_A_dx (p):
+ (βp)βπ = β(pβπ).
// qed.
-lemma structure_S_sn (p):
- (π¦ββp) = β(π¦βp).
+lemma structure_S_dx (p):
+ (βp)βπ¦ = β(pβπ¦).
// qed.
(* Main constructions *******************************************************)
theorem structure_idem (p):
βp = ββp.
-#p elim p -p [| * [ #n ] #p #IH ] //
+#p elim p -p [| * [ #k ] #p #IH ] //
qed.
-theorem structure_append (p1) (p2):
- βp1ββp2 = β(p1βp2).
-#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+theorem structure_append (p) (q):
+ βpββq = β(pβq).
+#p #q elim q -q [| * [ #k ] #q #IH ]
[||*: <list_append_lcons_sn ] //
qed.
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma structure_d_dx (p) (n):
- βp = β(pβπ±n).
+lemma structure_d_sn (p) (k):
+ βp = β(π±kβp).
#p #n <structure_append //
qed.
-lemma structure_m_dx (p):
- βp = β(pβπΊ).
+lemma structure_m_sn (p):
+ βp = β(πΊβp).
#p <structure_append //
qed.
-lemma structure_L_dx (p):
- (βp)βπ = β(pβπ).
+lemma structure_L_sn (p):
+ (πββp) = β(πβp).
#p <structure_append //
qed.
-lemma structure_A_dx (p):
- (βp)βπ = β(pβπ).
+lemma structure_A_sn (p):
+ (πββp) = β(πβp).
#p <structure_append //
qed.
-lemma structure_S_dx (p):
- (βp)βπ¦ = β(pβπ¦).
+lemma structure_S_sn (p):
+ (π¦ββp) = β(π¦βp).
#p <structure_append //
qed.
lemma depth_structure (p):
βp = ββp.
#p elim p -p //
-* [ #n ] #p #IH //
-[ <structure_L_sn <depth_L_sn <depth_L_sn //
-| <structure_A_sn <depth_A_sn <depth_A_sn //
-| <structure_S_sn <depth_S_sn <depth_S_sn //
+* [ #k ] #p #IH //
+[ <structure_L_dx <depth_L_dx <depth_L_dx //
+| <structure_A_dx <depth_A_dx <depth_A_dx //
+| <structure_S_dx <depth_S_dx <depth_S_dx //
]
qed.
lemma structure_pic (p):
βp Ο΅ π.
-#p @(list_ind_rcons β¦ p) -p
+#p elim p -p
[ <structure_empty //
-| #p * [ #n ] #IH
+| * [ #k ] #p #IH
[ <structure_d_dx //
| <structure_m_dx //
| <structure_L_dx //
(* Basic inversions *********************************************************)
-lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (r):
- pβr Ο΅ β΅t β t Ο΅ π β π = βr β π = r.
-#t #p #r #Hpr #Ht #Hr
-lapply (Ht p ?? Hpr ?)
+lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (q):
+ pβq Ο΅ β΅t β t Ο΅ π β π = βq β π = q.
+#t #p #q #Hpq #Ht #Hq
+lapply (Ht p ?? Hpq ?)
[ <structure_append //
| /2 width=2 by prototerm_in_root_append_des_sn/
-| /2 width=3 by eq_inv_list_append_dx_sn_refl/
+| /2 width=3 by eq_inv_list_append_dx_dx_refl/
]
qed-.
interpretation
"outer variable reference by depth (prototerm)"
- 'Hash n = (prototerm_node_0 (label_d n)).
+ 'Hash k = (prototerm_node_0 (label_d k)).
interpretation
"inner variable reference by depth (prototerm)"
- 'Tau n t = (prototerm_node_1_2 (label_d n) label_m t).
+ 'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
interpretation
"name-free functional abstraction (prototerm)"
(* Basic constructions *******************************************************)
-lemma in_comp_iref (t) (q) (n):
- q Ο΅ t β π±nβπΊβq Ο΅ πn.t.
+lemma in_comp_iref (t) (q) (k):
+ q Ο΅ t β π±kβπΊβq Ο΅ πk.t.
/2 width=3 by ex2_intro/ qed.
(* Basic inversions *********************************************************)
-lemma in_comp_inv_iref (t) (p) (n):
- p Ο΅ πn.t β
- ββq. π±nβπΊβq = p & q Ο΅ t.
-#t #p #n * #q #Hq #Hp
+lemma in_comp_inv_iref (t) (p) (k):
+ p Ο΅ πk.t β
+ ββq. π±kβπΊβq = p & q Ο΅ t.
+#t #p #k * #q #Hq #Hp
/2 width=3 by ex2_intro/
qed-.
+
(* COMMENT
lemma prototerm_in_root_inv_lcons_oref:
βp,l,n. lβp Ο΅ β΅#n β
(* Constructions with equivalence for prototerm *****************************)
-lemma iref_eq_repl (t1) (t2) (n):
- t1 β t2 β πn.t1 β πn.t2.
+lemma iref_eq_repl (t1) (t2) (k):
+ t1 β t2 β πk.t1 β πk.t2.
/2 width=1 by subset_equivalence_ext_f1_bi/
qed.
(* Constructions with prototerm constructors ********************************)
-lemma ppc_iref (t) (n):
- (πn.t) Ο΅ π.
-#t #n #p * #q #Hq #H0 destruct //
+lemma ppc_iref (t) (k):
+ (πk.t) Ο΅ π.
+#t #k #p * #q #Hq #H0 destruct //
qed.
projects / helm.git / commitdiff