---

Step * of Lemma gammaFIM_fun

g,h: List  .
  (spr(g)
   (a: List. (((g a) = 0)  ((g (a @ [h a])) = 0)))
   ((g []) = 0)
   (f:  . x:.  (gammaFIM(mklist(x;f);g;h) = mklist(x;n.gammaFIM(mklist(n + 1;f);g;h)[n]))))
BY
{ (Auto THEN NatInd (-1) THEN All Reduce) }

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
 gammaFIM([];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 : 
8. 0 < x
9. gammaFIM(mklist(x - 1;f);g;h) = mklist(x - 1;n.gammaFIM(mklist(n + 1;f);g;h)[n])
 gammaFIM(mklist(x;f);g;h) = mklist(x;n.gammaFIM(mklist(n + 1;f);g;h)[n])


\mforall{}g,h:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.
    (spr(g)
    {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  ((g  (a  @  [h  a]))  =  0)))
    {}\mRightarrow{}  ((g  [])  =  0)
    {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x:\mBbbN{}.
                (gammaFIM(mklist(x;f);g;h)  =  mklist(x;\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n]))))


By

(Auto  THEN  NatInd  (-1)  THEN  All  Reduce)



Home Index