---

Step * of Lemma aa_pc_3n_new

(m:. n:.  ((m ~ snd(aa_3n_plus_1_depth_pi(n)))  (m  0 )))
 (d:. n:.
      (((n > 0)  (d ~ snd(aa_3n_plus_1_depth_pi(n))))  (m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m)))))
BY
{ ((D 0 THENA Auto) THEN (D 0 THENA Auto') THEN CompNatInd 2) }

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
 n:. (((n > 0)  (d ~ snd(aa_3n_plus_1_depth_pi(n))))  (m:. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m)  (n  2^m))))


(\mforall{}m:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    ((m  \msim{}  snd(aa\_3n\_plus\_1\_depth\_pi(n)))  {}\mRightarrow{}  (m  \mgeq{}  0  )))
{}\mRightarrow{}  (\mforall{}d:\mBbbN{}.  \mforall{}n:\mBbbZ{}.
            (((n  >  0)  \mwedge{}  (d  \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)))))


By

((D  0  THENA  Auto)  THEN  (D  0  THENA  Auto')  THEN  CompNatInd  2)



Home Index