---

Step * 1 1 2 2 2 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@i
6. d ~ 1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))
7. (n = 1)
8. ((n rem 2) = 0)
9. (1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n)))))
10. 1  
11. snd(aa_3n_plus_1_depth_pi(1 + (3 * n)))  
12. (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))  0 
13. m:. ((fst(aa_3n_plus_1_depth_pi(1 + (3 * n))) ~ m)  ((1 + (3 * n))  2^m))
 m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m))
BY
{ (((D (-1) THEN D (-1)) THEN InstConcl [m]) THEN Auto) }

1
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 ~ 1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))
7. (n = 1)
8. ((n rem 2) = 0)
9. (1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n)))))
10. 1  
11. snd(aa_3n_plus_1_depth_pi(1 + (3 * n)))  
12. (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))  0 
13. m : 
14. fst(aa_3n_plus_1_depth_pi(1 + (3 * n))) ~ m
15. (1 + (3 * n))  2^m
 fst(aa_3n_plus_1_depth_pi(n)) ~ m

2
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 ~ 1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))
7. (n = 1)
8. ((n rem 2) = 0)
9. (1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n)))))
10. 1  
11. snd(aa_3n_plus_1_depth_pi(1 + (3 * n)))  
12. (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))  0 
13. m : 
14. fst(aa_3n_plus_1_depth_pi(1 + (3 * n))) ~ m
15. (1 + (3 * n))  2^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@i
6.  d  \msim{}  1  +  (snd(aa\_3n\_plus\_1\_depth\_pi(1  +  (3  *  n))))
7.  \mneg{}(n  =  1)
8.  \mneg{}((n  rem  2)  =  0)
9.  (1  +  (snd(aa\_3n\_plus\_1\_depth\_pi(1  +  (3  *  n)))))\mdownarrow{}
10.  1  \mmember{}  \mBbbZ{}
11.  snd(aa\_3n\_plus\_1\_depth\_pi(1  +  (3  *  n)))  \mmember{}  \mBbbZ{}
12.  (snd(aa\_3n\_plus\_1\_depth\_pi(1  +  (3  *  n))))  \mgeq{}  0 
13.  \mexists{}m:\mBbbN{}.  ((fst(aa\_3n\_plus\_1\_depth\_pi(1  +  (3  *  n)))  \msim{}  m)  \mwedge{}  ((1  +  (3  *  n))  \mleq{}  2\^{}m))
\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))  THEN  InstConcl  [\mkleeneopen{}m\mkleeneclose{}]\mcdot{})  THEN  Auto)



Home Index