---

Step * 1 1 1 of Lemma bar_bwd_implies_fwd


1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
3. (a: List. ((R a)  (c:  . x:. (R (a @ mklist(x;c))))))
 (a: List. ((s:. c:  .  x:. (R ((a @ [s]) @ mklist(x;c))))  (c:  . x:. (R (a @ mklist(x;c))))))
 (c:  . x:. (R mklist(x;c)))
 f:  . x:. (R mklist(x;f))
BY
{ (D 3 THEN Auto) }

1
1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
3. a :  List@i
4. R a@i
5. c :   @i
 x:. (R (a @ mklist(x;c)))

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



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


By

(D  3  THEN  Auto)



Home Index