---

Step * 1 1 2 of Lemma aa_fib_count_wf

.....falsecase..... 
1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
3. ((n = 0)  (n = 1))
 <(fst((fix((f,n. if (n = 0) (n = 1)
                   then <1, 0>
                   else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                   fi )) 
         (n - 1))))
   + (fst((fix((f,n. if (n = 0) (n = 1)
                     then <1, 0>
                     else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                     fi )) 
           (n - 2))))
  , (snd((fix((f,n. if (n = 0) (n = 1)
                    then <1, 0>
                    else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                    fi )) 
          (n - 1))))
    + (snd((fix((f,n. if (n = 0) (n = 1)
                      then <1, 0>
                      else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                      fi )) 
            (n - 2))))
  >    
BY
{ (Assert ((n = 0))  ((n = 1)) THENA Auto) }

1
1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
3. ((n = 0)  (n = 1))
 (n = 0)

2
1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
3. ((n = 0)  (n = 1))
 (n = 1)

3
1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
3. ((n = 0)  (n = 1))
4. ((n = 0))  ((n = 1))
 <(fst((fix((f,n. if (n = 0) (n = 1)
                   then <1, 0>
                   else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                   fi )) 
         (n - 1))))
   + (fst((fix((f,n. if (n = 0) (n = 1)
                     then <1, 0>
                     else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                     fi )) 
           (n - 2))))
  , (snd((fix((f,n. if (n = 0) (n = 1)
                    then <1, 0>
                    else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                    fi )) 
          (n - 1))))
    + (snd((fix((f,n. if (n = 0) (n = 1)
                      then <1, 0>
                      else <(fst((f (n - 1)))) + (fst((f (n - 2)))), (snd((f (n - 1)))) + (snd((f (n - 2))))>
                      fi )) 
            (n - 2))))
  >    


.....falsecase..... 
1.  n  :  \mBbbN{}@i
2.  \mforall{}n1:\mBbbN{}.  aa\_fib\_count(n1)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}  supposing  n1  <  n
3.  \mneg{}((n  =  0)  \mvee{}  (n  =  1))
\mvdash{}  <(fst((fix((\mlambda{}f,n.  if  (n  =\msubz{}  0)  \mvee{}\msubb{}(n  =\msubz{}  1)
                                      then  ə,  0>
                                      else  <(fst((f  (n  -  1))))  +  (fst((f  (n  -  2))))
                                                ,  (snd((f  (n  -  1))))  +  (snd((f  (n  -  2))))
                                                >
                                      fi  )) 
                  (n  -  1))))
      +  (fst((fix((\mlambda{}f,n.  if  (n  =\msubz{}  0)  \mvee{}\msubb{}(n  =\msubz{}  1)
                                          then  ə,  0>
                                          else  <(fst((f  (n  -  1))))  +  (fst((f  (n  -  2))))
                                                    ,  (snd((f  (n  -  1))))  +  (snd((f  (n  -  2))))
                                                    >
                                          fi  )) 
                      (n  -  2))))
    ,  (snd((fix((\mlambda{}f,n.  if  (n  =\msubz{}  0)  \mvee{}\msubb{}(n  =\msubz{}  1)
                                        then  ə,  0>
                                        else  <(fst((f  (n  -  1))))  +  (fst((f  (n  -  2))))
                                                  ,  (snd((f  (n  -  1))))  +  (snd((f  (n  -  2))))
                                                  >
                                        fi  )) 
                    (n  -  1))))
        +  (snd((fix((\mlambda{}f,n.  if  (n  =\msubz{}  0)  \mvee{}\msubb{}(n  =\msubz{}  1)
                                            then  ə,  0>
                                            else  <(fst((f  (n  -  1))))  +  (fst((f  (n  -  2))))
                                                      ,  (snd((f  (n  -  1))))  +  (snd((f  (n  -  2))))
                                                      >
                                            fi  )) 
                        (n  -  2))))
    >  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}


By

(Assert  \mkleeneopen{}(\mneg{}(n  =  0))  \mwedge{}  (\mneg{}(n  =  1))\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}



Home Index