---

Step * 2 2 2 of Lemma not_funcNbarB_decidable_eq_fullExt


1. t1,t2:  bar().  Dec(t1 = t2)@i
2. eqd :   bar()    bar()  
3. t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
4. isBot :   bar()  
5. t:  bar(). ((isBot t)  t = (x.bottom()))
6. isBot fix((t,x. if isBot t then tt else bottom() fi ))  
 False
BY
{ (skip{(RW (AddrC [2;2] UnrollRecursionC) (-1) THEN Reduce (-1))}
   THEN (Assert isBot fix((t,x. if isBot t then tt else bottom() fi )) 
               = isBot (x.if isBot fix((t,x. if isBot t then tt else bottom() fi )) then tt else bottom() fi ) BY
               (RW (AddrC [2;2] UnrollRecursionC) 0 THEN Reduce 0 THEN MaAuto))
   ) }

1
1. t1,t2:  bar().  Dec(t1 = t2)@i
2. eqd :   bar()    bar()  
3. t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
4. isBot :   bar()  
5. t:  bar(). ((isBot t)  t = (x.bottom()))
6. isBot fix((t,x. if isBot t then tt else bottom() fi ))  
7. isBot fix((t,x. if isBot t then tt else bottom() fi )) 
= isBot (x.if isBot fix((t,x. if isBot t then tt else bottom() fi )) then tt else bottom() fi )
 False



1.  \mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    Dec(t1  =  t2)@i
2.  eqd  :  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbB{}
3.  \mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    (\muparrow{}(eqd  t1  t2)  \mLeftarrow{}{}\mRightarrow{}  t1  =  t2)
4.  isBot  :  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}t:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).  (\muparrow{}(isBot  t)  \mLeftarrow{}{}\mRightarrow{}  t  =  (\mlambda{}x.bottom()))
6.  isBot  fix((\mlambda{}t,x.  if  isBot  t  then  tt  else  bottom()  fi  ))  \mmember{}  \mBbbB{}
\mvdash{}  False


By

(skip\{(RW  (AddrC  [2;2]  UnrollRecursionC)  (-1)  THEN  Reduce  (-1))\}
  THEN  (Assert  isBot  fix((\mlambda{}t,x.  if  isBot  t  then  tt  else  bottom()  fi  )) 
                          =  isBot 
                              (\mlambda{}x.if  isBot  fix((\mlambda{}t,x.  if  isBot  t  then  tt  else  bottom()  fi  ))
                                      then  tt
                                      else  bottom()
                                      fi  )  BY
                          (RW  (AddrC  [2;2]  UnrollRecursionC)  0  THEN  Reduce  0  THEN  MaAuto))
  )



Home Index