---

Step * 1 2 1 of Lemma aa_3n_plus_1_depth_pi_wf

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


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


By

MaAuto



Home Index