---

Step * of Lemma not_funcNbarB_decidable_eq_fullExt

(t1,t2:  bar().  Dec(t1 = t2))
BY
{ ((D 0 THEN Auto)
   THEN Assert eqd:  bar()    bar()  . t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
   ) }

1
.....assertion..... 
1. t1,t2:  bar().  Dec(t1 = t2)@i
 eqd:  bar()    bar()  . t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)

2
1. t1,t2:  bar().  Dec(t1 = t2)@i
2. eqd:  bar()    bar()  . t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
 False


\mneg{}(\mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    Dec(t1  =  t2))


By

((D  0  THEN  Auto)
  THEN  Assert  \mkleeneopen{}\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)\mkleeneclose{}
            \mcdot{}
  )



Home Index