Step
*
of Lemma
aa_3n_plus_1_depth_wf_comp_ind_pi_full
((
p:
. 
a,b:Base.  ((p ~ a + b) ![](../FONT/eq.png)
 ((
a1:
. (a1 ~ a)) 
 (
b1:
. (b1 ~ b)))))
 (
m:
. 
n:
.  ((m ~ snd(aa_3n_plus_1_depth_pi(n))) ![](../FONT/eq.png)
 (m 
 0 ))))
![](../FONT/eq.png)
 (
d:
. 
n:
.
      (((n > 0) 
 (d ~ snd(aa_3n_plus_1_depth_pi(n)))) ![](../FONT/eq.png)
 (
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. (
p:
. 
a,b:Base.  ((p ~ a + b) ![](../FONT/eq.png)
 ((
a1:
. (a1 ~ a)) 
 (
b1:
. (b1 ~ b)))))
 (
m:
. 
n:
.  ((m ~ snd(aa_3n_plus_1_depth_pi(n))) ![](../FONT/eq.png)
 (m 
 0 )))@i
2. d : 
@i
3. 
d1:![](../FONT/nat.png)
     
n:![](../FONT/int.png)
       (((n > 0) 
 (d1 ~ snd(aa_3n_plus_1_depth_pi(n)))) ![](../FONT/eq.png)
 (
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)))) ![](../FONT/eq.png)
 (
m:
. ((fst(aa_3n_plus_1_depth_pi(n)) ~ m) 
 (n 
 2^m))))
((\mforall{}p:\mBbbZ{}.  \mforall{}a,b:Base.    ((p  \msim{}  a  +  b)  {}\mRightarrow{}  ((\mexists{}a1:\mBbbZ{}.  (a1  \msim{}  a))  \mwedge{}  (\mexists{}b1:\mBbbZ{}.  (b1  \msim{}  b)))))
\mwedge{}  (\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