---

Step * 1 of Lemma gammaFIM_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
 l: List. (((g l) = 0)  (l = list_ind_reverse(l;[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi )))
BY
{ ((Assert l: List
             ((l,b. (((g l) = 0)  (l = b))) l 
              list_ind_reverse(l;[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi )) BY
          skip{[tactic]})
   THEN Reduce (-1)
   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. l :  List@i
 (l,b. (((g l) = 0)  (l = b))) l list_ind_reverse(l;[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi \000C)



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
\mvdash{}  \mforall{}l:\mBbbN{}  List
        (((g  l)  =  0)
        {}\mRightarrow{}  (l  =  list\_ind\_reverse(l;[];\mlambda{}r,f,l.  if  (g  (r  @  [l])  =\msubz{}  0)  then  r  @  [l]  else  r  @  [h  r]  fi  )))


By

((Assert  \mforall{}l:\mBbbN{}  List
                      ((\mlambda{}l,b.  (((g  l)  =  0)  {}\mRightarrow{}  (l  =  b)))  l 
                        list\_ind\_reverse(l;[];\mlambda{}r,f,l.  if  (g  (r  @  [l])  =\msubz{}  0)  then  r  @  [l]  else  r  @  [h  r]  fi  ))  BY
                skip\{[tactic]\})
  THEN  Reduce  (-1)
  THEN  Auto)\mcdot{}



Home Index