---

Step * 1 of Lemma aa_3n_plus_1_depth_pi_wf


1. n : @i
 aa_3n_plus_1_depth_pi(n)  Top  Top
BY
{ (((Unfold `aa_3n_plus_1_depth_pi` 0 THEN RW (AddrC[2] UnrollRecursionC ) (0) )
    THEN Reduce 0
    THEN Fold `aa_3n_plus_1_depth_pi` 0)
   THEN (SplitOnHypITE (0) THENA Auto')
   THEN skip{hello}) }

1
.....truecase..... 
1. n : @i
2. n = 1
 <0, 0>  Top  Top

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



1.  n  :  \mBbbN{}@i
\mvdash{}  aa\_3n\_plus\_1\_depth\_pi(n)  \mmember{}  Top  \mtimes{}  Top


By

(((Unfold  `aa\_3n\_plus\_1\_depth\_pi`  0  THEN  RW  (AddrC[2]  UnrollRecursionC  )  (0)  )
    THEN  Reduce  0
    THEN  Fold  `aa\_3n\_plus\_1\_depth\_pi`  0)
  THEN  (SplitOnHypITE  (0)  THENA  Auto')
  THEN  skip\{hello\})\mcdot{}



Home Index