Step
*
1
1
1
2
1
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
7. 
x:
. (R ((a @ [c 0]) @ mklist(x;
x.(c (1 + x)))))
 
x:
. (R (a @ mklist(x;c)))
BY
{ ((RWO "append_assoc" (-1) THEN Auto) THEN (RWO "mklist-single<" (-1) THEN Auto) THEN RWO "mklist-add<" (-1) 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 @ mklist(1 + x;c)))
 
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
7.  \mexists{}x:\mBbbN{}.  (R  ((a  @  [c  0])  @  mklist(x;\mlambda{}x.(c  (1  +  x)))))
\mvdash{}  \mexists{}x:\mBbbN{}.  (R  (a  @  mklist(x;c)))
By
((RWO  "append\_assoc"  (-1)  THEN  Auto)
  THEN  (RWO  "mklist-single<"  (-1)  THEN  Auto)
  THEN  RWO  "mklist-add<"  (-1)
  THEN  Auto)\mcdot{}
Home
Index