---

Step * of Lemma gammaFIM_equi_length

g,h: List  .
  (spr(g)
   (a: List. (((g a) = 0)  ((g (a @ [h a])) = 0)))
   ((g []) = 0)
   (L: List. (||L|| = ||gammaFIM(L;g;h)||)))
BY
{ (Auto THEN Unfold `gammaFIM` 0) }

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. L :  List@i
 ||L|| = ||list_ind_reverse(L;[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi )||


\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{}L:\mBbbN{}  List.  (||L||  =  ||gammaFIM(L;g;h)||)))


By

(Auto  THEN  Unfold  `gammaFIM`  0)



Home Index