---

Step * 1 of Lemma gammaFIM_equi_length


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. L :  List@i
 ||L|| = ||list_ind_reverse(L;[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi )||
BY
{ (InstLemma `list_ind_reverse_wf_dependent` [; List;[];r,f,l. if (g (r @ [l]) = 0)
                                                                        then r @ [l]
                                                                        else r @ [h r]
                                                                        fi ;l,b. (||l|| = ||b||)]
   THEN Auto
   THEN All Reduce
   THEN Auto
   THEN AutoSplit
   THEN MaAuto) }



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


By

(InstLemma  `list\_ind\_reverse\_wf\_dependent`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}  List\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}\mlambda{}r,f,l.  if  (g  (r  @  [l])  =\msubz{}  0)
                                                                                                                                            then  r  @  [l]
                                                                                                                                            else  r  @  [h  r]
                                                                                                                                            fi  \mkleeneclose{};\mkleeneopen{}\mlambda{}l,b.  (||l||  =  ||b||)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  Reduce\mcdot{}
  THEN  Auto
  THEN  AutoSplit
  THEN  MaAuto)



Home Index