---

Step * 2 1 1 1 1 1 1 1 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. x  0
9. 0 < x
10. gammaFIM(mklist(x - 1;f);g;h) = mklist(x - 1;n.gammaFIM(mklist(n + 1;f);g;h)[n])
11. l: List. (((g l) = 0)  (l = gammaFIM(l;g;h)))
12. L: List. ((g gammaFIM(L;g;h)) = 0)
13. L: List. (||L|| = ||gammaFIM(L;g;h)||)
14. f:  . x:.  (x ~ ||gammaFIM(mklist(x;f);g;h)||)
15. x:. (x ~ ||gammaFIM(mklist(x;f);g;h)||)
16. n.gammaFIM(mklist(n + 1;f);g;h)[n]    
17. RHS : Base
18. RHS ~ h,g,f,x. mklist(x;n.gammaFIM(mklist(n + 1;f);g;h)[n])
19. RHS h g f x   List
20. last(mklist(x;f))  
 if (g (gammaFIM(mklist(x - 1;f);g;h) @ [last(mklist(x;f))]) = 0)
then gammaFIM(mklist(x - 1;f);g;h) @ [last(mklist(x;f))]
else gammaFIM(mklist(x - 1;f);g;h) @ [h gammaFIM(mklist(x - 1;f);g;h)]
fi 
= (RHS h g f x)
BY
{ (((InstLemma `mklist-add1` [x - 1;n.gammaFIM(mklist(n + 1;f);g;h)[n]] THENA Auto)
    THEN (Subst (x - 1) + 1 ~ x (-1) THENA Auto)
    )
   THEN (HypSubst 18 0 THEN Reduce 0)
   THEN (HypSubst' (-1) 0 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. x  0
9. 0 < x
10. gammaFIM(mklist(x - 1;f);g;h) = mklist(x - 1;n.gammaFIM(mklist(n + 1;f);g;h)[n])
11. l: List. (((g l) = 0)  (l = gammaFIM(l;g;h)))
12. L: List. ((g gammaFIM(L;g;h)) = 0)
13. L: List. (||L|| = ||gammaFIM(L;g;h)||)
14. f:  . x:.  (x ~ ||gammaFIM(mklist(x;f);g;h)||)
15. x:. (x ~ ||gammaFIM(mklist(x;f);g;h)||)
16. n.gammaFIM(mklist(n + 1;f);g;h)[n]    
17. RHS : Base
18. RHS ~ h,g,f,x. mklist(x;n.gammaFIM(mklist(n + 1;f);g;h)[n])
19. RHS h g f x   List
20. last(mklist(x;f))  
21. mklist(x;n.gammaFIM(mklist(n + 1;f);g;h)[n]) ~ mklist(x - 1;n.gammaFIM(mklist(n + 1;f);g;h)[n])
@ [(n.gammaFIM(mklist(n + 1;f);g;h)[n]) (x - 1)]
 if (g (gammaFIM(mklist(x - 1;f);g;h) @ [last(mklist(x;f))]) = 0)
then gammaFIM(mklist(x - 1;f);g;h) @ [last(mklist(x;f))]
else gammaFIM(mklist(x - 1;f);g;h) @ [h gammaFIM(mklist(x - 1;f);g;h)]
fi 
= (mklist(x - 1;n.gammaFIM(mklist(n + 1;f);g;h)[n]) @ [(n.gammaFIM(mklist(n + 1;f);g;h)[n]) (x - 1)])



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.  x  \mneq{}  0
9.  0  <  x
10.  gammaFIM(mklist(x  -  1;f);g;h)  =  mklist(x  -  1;\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n])
11.  \mforall{}l:\mBbbN{}  List.  (((g  l)  =  0)  {}\mRightarrow{}  (l  =  gammaFIM(l;g;h)))
12.  \mforall{}L:\mBbbN{}  List.  ((g  gammaFIM(L;g;h))  =  0)
13.  \mforall{}L:\mBbbN{}  List.  (||L||  =  ||gammaFIM(L;g;h)||)
14.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x:\mBbbN{}.    (x  \msim{}  ||gammaFIM(mklist(x;f);g;h)||)
15.  \mforall{}x:\mBbbN{}.  (x  \msim{}  ||gammaFIM(mklist(x;f);g;h)||)
16.  \mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n]  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
17.  RHS  :  Base
18.  RHS  \msim{}  \mlambda{}h,g,f,x.  mklist(x;\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n])
19.  RHS  h  g  f  x  \mmember{}  \mBbbN{}  List
20.  last(mklist(x;f))  \mmember{}  \mBbbN{}
\mvdash{}  if  (g  (gammaFIM(mklist(x  -  1;f);g;h)  @  [last(mklist(x;f))])  =\msubz{}  0)
then  gammaFIM(mklist(x  -  1;f);g;h)  @  [last(mklist(x;f))]
else  gammaFIM(mklist(x  -  1;f);g;h)  @  [h  gammaFIM(mklist(x  -  1;f);g;h)]
fi 
=  (RHS  h  g  f  x)


By

(((InstLemma  `mklist-add1`  [\mkleeneopen{}x  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n]\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (Subst  \mkleeneopen{}(x  -  1)  +  1  \msim{}  x\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
    )
  THEN  (HypSubst  18  0  THEN  Reduce  0)
  THEN  (HypSubst'  (-1)  0  THENA  Auto))



Home Index