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. 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
+ โจโจ โโn. #n โ t & ๐ฑโจnโฉโ๐ = 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
.
#t #p #H elim H -H
[ #n * /3 width=3 by or5_intro0, ex2_intro/
qed-.
lemma bdd_inv_in_comp_d:
- โt,q,n. t ฯต ๐๐ โ ๐ฑโจnโฉ;q ฯต t โ
+ โt,q,n. t ฯต ๐๐ โ ๐ฑโจnโฉโq ฯต t โ
โจโจ โงโง #n โ t & ๐ = q
| โโu. u ฯต ๐๐ & q ฯต u & ๐n.u โ t
.
qed-.
lemma bdd_inv_in_root_d:
- โt,q,n. t ฯต ๐๐ โ ๐ฑโจnโฉ;q ฯต โตt โ
+ โt,q,n. t ฯต ๐๐ โ ๐ฑโจnโฉโq ฯต โตt โ
โจโจ โงโง #n โ t & ๐ = q
| โโu. u ฯต ๐๐ & q ฯต โตu & ๐n.u โ t
.
qed-.
lemma bdd_inv_in_comp_L:
- โt,q. t ฯต ๐๐ โ ๐;q ฯต t โ
+ โt,q. t ฯต ๐๐ โ ๐โq ฯต t โ
โโu. u ฯต ๐๐ & q ฯต u & ๐.u โ t
.
#t #q #Ht #Hq
qed-.
lemma bdd_inv_in_root_L:
- โt,q. t ฯต ๐๐ โ ๐;q ฯต โตt โ
+ โt,q. t ฯต ๐๐ โ ๐โq ฯต โตt โ
โโu. u ฯต ๐๐ & q ฯต โตu & ๐.u โ t.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_L โฆ Ht Hq) -Ht -Hq
qed-.
lemma bdd_inv_in_comp_A:
- โt,q. t ฯต ๐๐ โ ๐;q ฯต t โ
+ โt,q. t ฯต ๐๐ โ ๐โq ฯต t โ
โโv,u. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต u & @v.u โ t
.
#t #q #Ht #Hq
qed-.
lemma bdd_inv_in_root_A:
- โt,q. t ฯต ๐๐ โ ๐;q ฯต โตt โ
+ โt,q. t ฯต ๐๐ โ ๐โq ฯต โตt โ
โโv,u. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต โตu & @v.u โ t
.
#t #q #Ht * #r #Hq
qed-.
lemma bdd_inv_in_comp_S:
- โt,q. t ฯต ๐๐ โ ๐ฆ;q ฯต t โ
+ โt,q. t ฯต ๐๐ โ ๐ฆโq ฯต t โ
โโv,u. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต v & @v.u โ t
.
#t #q #Ht #Hq
qed-.
lemma bdd_inv_in_root_S:
- โt,q. t ฯต ๐๐ โ ๐ฆ;q ฯต โตt โ
+ โt,q. t ฯต ๐๐ โ ๐ฆโq ฯต โตt โ
โโv,u. v ฯต ๐๐ & u ฯต ๐๐ & q ฯต โตv & @v.u โ t
.
#t #q #Ht * #r #Hq
(* Advanced inversions ******************************************************)
lemma bbd_mono_in_root_d:
- โl,n,p,t. t ฯต ๐๐ โ p,๐ฑโจnโฉ ฯต โตt โ p,l ฯต โตt โ ๐ฑโจnโฉ = l.
+ โl,n,p,t. t ฯต ๐๐ โ pโ๐ฑโจnโฉ ฯต โตt โ pโl ฯต โตt โ ๐ฑโจnโฉ = l.
#l #n #p elim p -p
[ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
elim (bdd_inv_in_root_d โฆ Ht Hn) -Ht -Hn *