---

Step * 1 1 1 of Lemma gammaFIM_fun_id


1. g :  List  @i
2. h :  List  @i
3. spr(g)@i
4. a: List. (((g a) = 0)  ((g (a @ [h a])) = 0))@i
5. (g []) = 0@i
6. f :   @i
7. x:. ((g mklist(x;f)) = 0)@i
8. x : 
 (f x) = gammaFIM(mklist(x + 1;f);g;h)[x]
BY
{ (RWO "gammaFIM_id<" 0 THEN Auto) }

1
1. g :  List  @i
2. h :  List  @i
3. spr(g)@i
4. a: List. (((g a) = 0)  ((g (a @ [h a])) = 0))@i
5. (g []) = 0@i
6. f :   @i
7. x:. ((g mklist(x;f)) = 0)@i
8. x : 
9. 0  x
 x < ||gammaFIM(mklist(x + 1;f);g;h)||

2
1. g :  List  @i
2. h :  List  @i
3. spr(g)@i
4. a: List. (((g a) = 0)  ((g (a @ [h a])) = 0))@i
5. (g []) = 0@i
6. f :   @i
7. x:. ((g mklist(x;f)) = 0)@i
8. x : 
 (f x) = mklist(x + 1;f)[x]



1.  g  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  h  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
3.  spr(g)@i
4.  \mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  ((g  (a  @  [h  a]))  =  0))@i
5.  (g  [])  =  0@i
6.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
7.  \mforall{}x:\mBbbN{}.  ((g  mklist(x;f))  =  0)@i
8.  x  :  \mBbbN{}
\mvdash{}  (f  x)  =  gammaFIM(mklist(x  +  1;f);g;h)[x]


By

(RWO  "gammaFIM\_id<"  0  THEN  Auto)



Home Index