---

Step * 1 1 1 2 1 of Lemma bar_bwd_implies_fwd


1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
3. f :   @i
4. a :  List@i
5. s:. c:  .  x:. (R ((a @ [s]) @ mklist(x;c)))@i
6. c :   @i
 x:. (R (a @ mklist(x;c)))
BY
{ (InstHyp [c 0;x.(c (1 + x))] (-2) THEN Auto) }

1
1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
3. f :   @i
4. a :  List@i
5. s:. c:  .  x:. (R ((a @ [s]) @ mklist(x;c)))@i
6. c :   @i
7. x:. (R ((a @ [c 0]) @ mklist(x;x.(c (1 + x)))))
 x:. (R (a @ mklist(x;c)))



1.  R  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_bwd\_fim(R;A)@i'
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
4.  a  :  \mBbbN{}  List@i
5.  \mforall{}s:\mBbbN{}.  \mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    \mexists{}x:\mBbbN{}.  (R  ((a  @  [s])  @  mklist(x;c)))@i
6.  c  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
\mvdash{}  \mexists{}x:\mBbbN{}.  (R  (a  @  mklist(x;c)))


By

(InstHyp  [\mkleeneopen{}c  0\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(c  (1  +  x))\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)\mcdot{}



Home Index