---

Step * 1 2 2 of Lemma aa_3n_plus_1_depth_pi_wf

.....falsecase..... 
1. n : @i
2. (n = 1)
3. ((n rem 2) = 0)
 <fst(aa_3n_plus_1_depth_pi(1 + (3 * n))), 1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))>  Top  Top
BY
{ MaAuto }


.....falsecase..... 
1.  n  :  \mBbbN{}@i
2.  \mneg{}(n  =  1)
3.  \mneg{}((n  rem  2)  =  0)
\mvdash{}  <fst(aa\_3n\_plus\_1\_depth\_pi(1  +  (3  *  n))),  1  +  (snd(aa\_3n\_plus\_1\_depth\_pi(1  +  (3  *  n))))>  \mmember{}  Top
    \mtimes{}  Top


By

MaAuto



Home Index