---

Step * 2 of Lemma gammaFIM_fun


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])
BY
{ ((InstLemma `gammaFIM_id` [g;h] THENA Auto)
   THEN (InstLemma `gammaFIM_true` [g;h] THENA Auto)
   THEN (InstLemma `gammaFIM_equi_length` [g;h] THENA Auto)
   THEN (InstLemma `gammaFIM_equi_length_mklist` [g;h] THENA Auto)
   THEN (InstHyp [f] (-1) THENA 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. (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])
10. l: List. (((g l) = 0)  (l = gammaFIM(l;g;h)))
11. L: List. ((g gammaFIM(L;g;h)) = 0)
12. L: List. (||L|| = ||gammaFIM(L;g;h)||)
13. f:  . x:.  (x ~ ||gammaFIM(mklist(x;f);g;h)||)
14. x:. (x ~ ||gammaFIM(mklist(x;f);g;h)||)
 gammaFIM(mklist(x;f);g;h) = mklist(x;n.gammaFIM(mklist(n + 1;f);g;h)[n])



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.  (g  [])  =  0@i
6.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
7.  x  :  \mBbbZ{}
8.  0  <  x
9.  gammaFIM(mklist(x  -  1;f);g;h)  =  mklist(x  -  1;\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n])
\mvdash{}  gammaFIM(mklist(x;f);g;h)  =  mklist(x;\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n])


By

((InstLemma  `gammaFIM\_id`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `gammaFIM\_true`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `gammaFIM\_equi\_length`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `gammaFIM\_equi\_length\_mklist`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))



Home Index