(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
inductive bdd: π«β¨prototermβ© β
-| bdd_oref: βn. bdd (#n)
+| bdd_oref: βn. bdd (⧣n)
| bdd_iref: βt,n. bdd t β bdd (πn.t)
| bdd_abst: βt. bdd t β bdd (π.t)
| bdd_appl: βu,t. bdd u β bdd t β bdd (@u.t)
"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