---

Step * 1 2 of Lemma aa_3n_plus_1_depth_pi_wf

.....falsecase..... 
1. n : @i
2. (n = 1)
 if (n rem 2 = 0)
  then <1 + (fst(aa_3n_plus_1_depth_pi(n  2))), 1 + (snd(aa_3n_plus_1_depth_pi(n  2)))>
  else <fst(aa_3n_plus_1_depth_pi(1 + (3 * n))), 1 + (snd(aa_3n_plus_1_depth_pi(1 + (3 * n))))>
  fi   Top  Top
BY
{ (SplitOnHypITE (0) THENA Auto') }

1
.....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

2
.....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


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


By

(SplitOnHypITE  (0)  THENA  Auto')\mcdot{}



Home Index