---

Step * 1 1 of Lemma aa_pc_3n_new


1. m:. n:.  ((m ~ snd(aa_3n_plus_1_depth_pi(n)))  (m  0 ))@i
2. d : @i
3. d1:
     n:
       (((n > 0)  (d1 ~ snd(aa_3n_plus_1_depth_pi(n))))  (m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m)))) 
     supposing d1 < d
4. n : @i
5. (n > 0)  (d ~ snd(aa_3n_plus_1_depth_pi(n)))@i
 m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m))
BY
{ (D (-1) THEN D (-1) THENA Auto' THEN Unfold `aa_3n_plus_1_depth_pi` (-1)
   THEN RW (AddrC[2;1] UnrollRecursionC ) (-1) 
   THEN Reduce (-1)
   THEN Fold `aa_3n_plus_1_depth_pi` (-1)
   THEN (SplitOnHypITE (-1) THENA Auto')) }

1
.....truecase..... 
1. m:. n:.  ((m ~ snd(aa_3n_plus_1_depth_pi(n)))  (m  0 ))@i
2. d : @i
3. d1:
     n:
       (((n > 0)  (d1 ~ snd(aa_3n_plus_1_depth_pi(n))))  (m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m)))) 
     supposing d1 < d
4. n : @i
5. n > 0@i
6. d ~ snd(<0, 0>)
7. n = 1
 m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m))

2
.....falsecase..... 
1. m:. n:.  ((m ~ snd(aa_3n_plus_1_depth_pi(n)))  (m  0 ))@i
2. d : @i
3. d1:
     n:
       (((n > 0)  (d1 ~ snd(aa_3n_plus_1_depth_pi(n))))  (m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m)))) 
     supposing d1 < d
4. n : @i
5. n > 0@i
6. d ~ snd(if (n rem 2 = 0)
then <1 + (fst(aa_3n_plus_1_depth_pi(n  2))), 1 + (snd(aa_3n_plus_1_depth_pi(n  2)))>
else <fst(aa_3n_plus_1_depth_pi(1 + (3 * n))), 1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))>
fi )
7. (n = 1)
 m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m))



1.  \mforall{}m:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    ((m  \msim{}  snd(aa\_3n\_plus\_1\_depth\_pi(n)))  {}\mRightarrow{}  (m  \mgeq{}  0  ))@i
2.  d  :  \mBbbN{}@i
3.  \mforall{}d1:\mBbbN{}
          \mforall{}n:\mBbbZ{}
              (((n  >  0)  \mwedge{}  (d1  \msim{}  snd(aa\_3n\_plus\_1\_depth\_pi(n))))
              {}\mRightarrow{}  (\mexists{}m:\mBbbN{}.  ((fst(aa\_3n\_plus\_1\_depth\_pi(n))  \msim{}  m)  \mwedge{}  (n  \mleq{}  2\^{}m)))) 
          supposing  d1  <  d
4.  n  :  \mBbbZ{}@i
5.  (n  >  0)  \mwedge{}  (d  \msim{}  snd(aa\_3n\_plus\_1\_depth\_pi(n)))@i
\mvdash{}  \mexists{}m:\mBbbN{}.  ((fst(aa\_3n\_plus\_1\_depth\_pi(n))  \msim{}  m)  \mwedge{}  (n  \mleq{}  2\^{}m))


By

(D  (-1)  THEN  D  (-1)  THENA  Auto'  THEN  Unfold  `aa\_3n\_plus\_1\_depth\_pi`  (-1)\mcdot{}
  THEN  RW  (AddrC[2;1]  UnrollRecursionC  )  (-1) 
  THEN  Reduce  (-1)
  THEN  Fold  `aa\_3n\_plus\_1\_depth\_pi`  (-1)
  THEN  (SplitOnHypITE  (-1)  THENA  Auto'))\mcdot{}



Home Index