---

Step * 1 1 of Lemma aa_fib_count_wf


1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
 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    
BY
{ ((RW (AddrC[2] UnrollRecursionC ) (0)  THEN Reduce 0) THEN (SplitOnHypITE (0) THENA Auto')) }

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

2
.....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))))
  >    



1.  n  :  \mBbbN{}@i
2.  \mforall{}n1:\mBbbN{}.  aa\_fib\_count(n1)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}  supposing  n1  <  n
\mvdash{}  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  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}


By

((RW  (AddrC[2]  UnrollRecursionC  )  (0)  \mcdot{}  THEN  Reduce  0)  THEN  (SplitOnHypITE  (0)  THENA  Auto'))



Home Index