---

Step * 2 of Lemma not_funcNbarB_decidable_eq_fullExt


1. t1,t2:  bar().  Dec(t1 = t2)@i
2. eqd:  bar()    bar()  . t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
 False
BY
{ (D (-1) THEN Assert isBot:  bar()  . t:  bar(). ((isBot t)  t = (x.bottom()))) }

1
.....assertion..... 
1. t1,t2:  bar().  Dec(t1 = t2)@i
2. eqd :   bar()    bar()  
3. t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
 isBot:  bar()  . t:  bar(). ((isBot t)  t = (x.bottom()))

2
1. t1,t2:  bar().  Dec(t1 = t2)@i
2. eqd :   bar()    bar()  
3. t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
4. isBot:  bar()  . t:  bar(). ((isBot t)  t = (x.bottom()))
 False



1.  \mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    Dec(t1  =  t2)@i
2.  \mexists{}eqd:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    (\muparrow{}(eqd  t1  t2)  \mLeftarrow{}{}\mRightarrow{}  t1  =  t2)
\mvdash{}  False


By

(D  (-1)  THEN  Assert  \mkleeneopen{}\mexists{}isBot:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).  (\muparrow{}(isBot  t)  \mLeftarrow{}{}\mRightarrow{}  t  =  (\mlambda{}x.bottom()))\mkleeneclose{}\mcdot{})\mcdot{}



Home Index