"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