Step
*
of Lemma
gammaFIM_id
g,h:
 List ![](../FONT/dash.png)
 
.
  (spr(g) ![](../FONT/eq.png)
 (
a:
 List. (((g a) = 0) ![](../FONT/eq.png)
 ((g (a @ [h a])) = 0))) ![](../FONT/eq.png)
 (
l:
 List. (((g l) = 0) ![](../FONT/eq.png)
 (l = gammaFIM(l;g;h)))))
BY
{ (Auto THEN RepeatFor 2 (MoveToConcl (-1)) THEN Unfold `gammaFIM` 0) }
1
1. g : 
 List ![](../FONT/dash.png)
 
@i
2. h : 
 List ![](../FONT/dash.png)
 
@i
3. spr(g)@i
4. 
a:
 List. (((g a) = 0) ![](../FONT/eq.png)
 ((g (a @ [h a])) = 0))@i
 
l:
 List. (((g l) = 0) ![](../FONT/eq.png)
 (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{}  (\mforall{}l:\mBbbN{}  List.  (((g  l)  =  0)  {}\mRightarrow{}  (l  =  gammaFIM(l;g;h)))))
By
(Auto  THEN  RepeatFor  2  (MoveToConcl  (-1))  THEN  Unfold  `gammaFIM`  0)
Home
Index