---

Step * 1 1 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
5. l :  List@i
6. L :  List@i
7. x : @i
8. b :  List@i
9. b = list_ind_reverse(L;[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi )@i
10. ((g L) = 0)  (L = b)@i
11. (g (L @ [x])) = 0@i
 (L @ [x]) = if (g (b @ [x]) = 0) then b @ [x] else b @ [h b] fi 
BY
{ (FLemma `spr_down_closed` [(-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
6. L :  List@i
7. x : @i
8. b :  List@i
9. b = list_ind_reverse(L;[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi )@i
10. ((g L) = 0)  (L = b)@i
11. (g (L @ [x])) = 0@i
12. (g L) = 0
 (L @ [x]) = if (g (b @ [x]) = 0) then b @ [x] else b @ [h b] fi 



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


By

(FLemma  `spr\_down\_closed`  [(-1)]  THEN  Auto)



Home Index