---

Step * 1 1 2 3 of Lemma aa_fib_count_wf


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))))
  >    
BY
{ ((((Fold `aa_fib_count` 0 THEN (Assert n  2  THENA Auto')) THEN (InstHyp [n - 1] 2 THENA Auto'))
    THEN (InstHyp [n - 2] 2 THENA Auto')
    )
   THEN MemCD
   THEN BLemma `add_nat_wf`
   THEN Auto') }



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))
4.  (\mneg{}(n  =  0))  \mwedge{}  (\mneg{}(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

((((Fold  `aa\_fib\_count`  0  THEN  (Assert  \mkleeneopen{}n  \mgeq{}  2  \mkleeneclose{}\mcdot{}  THENA  Auto'))
      THEN  (InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  2\mcdot{}  THENA  Auto')
      )
    THEN  (InstHyp  [\mkleeneopen{}n  -  2\mkleeneclose{}]  2\mcdot{}  THENA  Auto')
    )
  THEN  MemCD
  THEN  BLemma  `add\_nat\_wf`
  THEN  Auto')



Home Index