Step
*
1
2
1
1
1
1
1
1
of Lemma
bind-class-program_wf
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(B)
5. es : EO+(Info)@i'
6. X : hdataflow(Info;A)@i
7. Y : A ⟶ hdataflow(Info;B)@i
8. e : E@i
9. ∀e1:E
((e1 < e)
⇒ (simple-hdf-bind(X;λx.(Y x))*(map(λx.info(x);before(e1)))
= mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a);p.let X,ys = p
in ff;<X*(map(λx.info(x);before(e1)))
, ⋃e'∈before(e1).
bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
before(e1))));
snd(X*(map(λx.info(x);before(e')))(info(e'))))
>)
∈ hdataflow(Info;B)))
10. ¬↑first(e)
11. v : hdataflow(Info;A)@i
12. X*(map(λx.info(x);before(pred(e)))) = v ∈ hdataflow(Info;A)@i
13. v2 : hdataflow(Info;A)@i
14. v3 : bag(A)@i
15. v(info(pred(e))) = <v2, v3> ∈ (hdataflow(Info;A) × bag(A))@i
⊢ (fst(let s1,b = let ybs ⟵ bag-map(λP.P(info(pred(e)));
⋃e'∈before(pred(e)).bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;before(pred(e)))));
snd(X*(map(λx.info(x);before(e')))(info(e'))))
+ bag-map(λx.(Y x);v3))
in let ys' ⟵ bag-map(λyb.(fst(yb));ybs)
in let out ⟵ ⋃yb∈ybs.snd(yb)
in <<v2, ys'>, out>
in <mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a);p.let X,ys = p in ff;s1), b>))
= mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a
);p.let X,ys = p
in ff;<v2
, ⋃e'∈before(pred(e)) + {pred(e)}.
bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
before(pred(e)) + {pred(e)})));
snd(X*(map(λx.info(x);before(e')))(info(e'))))
>)
∈ hdataflow(Info;B)
BY
{ ((Assert ↓Info BY
(D 0 THEN UseWitness ⌜info(e)⌝⋅ THEN Auto))
THEN (GenConcl ⌜before(pred(e)) = L ∈ ({e':E| (e' <loc pred(e))} List)⌝⋅ THENA Auto)
THEN RepeatFor 3 ((CallByValueReduce 0 THENA MaAuto))
THEN Reduce 0
THEN RepeatFor 2 ((EqCD THEN Auto))
THEN (RWO "bag-combine-append-left bag-map-map" 0 THENA (Auto THEN Unfolds ``bag-append single-bag`` 0 THEN Auto))
THEN RepUR ``compose`` 0
THEN (RWO "bag-map-append" 0 THENA Auto)
THEN EqCD
THEN Auto)⋅ }
1
.....subterm..... T:t
1:n
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(B)
5. es : EO+(Info)@i'
6. X : hdataflow(Info;A)@i
7. Y : A ⟶ hdataflow(Info;B)@i
8. e : E@i
9. ∀e1:E
((e1 < e)
⇒ (simple-hdf-bind(X;λx.(Y x))*(map(λx.info(x);before(e1)))
= mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a);p.let X,ys = p
in ff;<X*(map(λx.info(x);before(e1)))
, ⋃e'∈before(e1).
bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
before(e1))));
snd(X*(map(λx.info(x);before(e')))(info(e'))))
>)
∈ hdataflow(Info;B)))
10. ¬↑first(e)
11. v : hdataflow(Info;A)@i
12. X*(map(λx.info(x);before(pred(e)))) = v ∈ hdataflow(Info;A)@i
13. v2 : hdataflow(Info;A)@i
14. v3 : bag(A)@i
15. v(info(pred(e))) = <v2, v3> ∈ (hdataflow(Info;A) × bag(A))@i
16. Info
17. L : {e':E| (e' <loc pred(e))} List@i
18. before(pred(e)) = L ∈ ({e':E| (e' <loc pred(e))} List)@i
⊢ bag-map(λx.(fst(x(info(pred(e)))));⋃e'∈L.bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;L)));
snd(X*(map(λx.info(x);before(e')))(info(e')))))
= ⋃e'∈L.bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;L + {pred(e)})));
snd(X*(map(λx.info(x);before(e')))(info(e'))))
∈ bag(hdataflow(Info;B))
2
.....subterm..... T:t
2:n
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(B)
5. es : EO+(Info)@i'
6. X : hdataflow(Info;A)@i
7. Y : A ⟶ hdataflow(Info;B)@i
8. e : E@i
9. ∀e1:E
((e1 < e)
⇒ (simple-hdf-bind(X;λx.(Y x))*(map(λx.info(x);before(e1)))
= mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a);p.let X,ys = p
in ff;<X*(map(λx.info(x);before(e1)))
, ⋃e'∈before(e1).
bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
before(e1))));
snd(X*(map(λx.info(x);before(e')))(info(e'))))
>)
∈ hdataflow(Info;B)))
10. ¬↑first(e)
11. v : hdataflow(Info;A)@i
12. X*(map(λx.info(x);before(pred(e)))) = v ∈ hdataflow(Info;A)@i
13. v2 : hdataflow(Info;A)@i
14. v3 : bag(A)@i
15. v(info(pred(e))) = <v2, v3> ∈ (hdataflow(Info;A) × bag(A))@i
16. Info
17. L : {e':E| (e' <loc pred(e))} List@i
18. before(pred(e)) = L ∈ ({e':E| (e' <loc pred(e))} List)@i
⊢ bag-map(λx.(fst(x(info(pred(e)))));bag-map(λx.(Y x);v3))
= ⋃e'∈{pred(e)}.bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;L + {pred(e)})));
snd(X*(map(λx.info(x);before(e')))(info(e'))))
∈ bag(hdataflow(Info;B))
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(B)
5. es : EO+(Info)@i'
6. X : hdataflow(Info;A)@i
7. Y : A {}\mrightarrow{} hdataflow(Info;B)@i
8. e : E@i
9. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} (simple-hdf-bind(X;\mlambda{}x.(Y x))*(map(\mlambda{}x.info(x);before(e1)))
= mk-hdf(p,a.simple-bind-nxt
(\mlambda{}x.(Y x); p; a);p.let X,ys = p
in ff;<X*(map(\mlambda{}x.info(x);before(e1)))
, \mcup{}e'\mmember{}before(e1).
bag-map(\mlambda{}a.Y a*(map(\mlambda{}x.info(x);
filter(\mlambda{}a.e' \mleq{}loc a;
before(e1))));
snd(X*(map(\mlambda{}x.info(x);before(e')))(info(e'))))
>)))
10. \mneg{}\muparrow{}first(e)
11. v : hdataflow(Info;A)@i
12. X*(map(\mlambda{}x.info(x);before(pred(e)))) = v@i
13. v2 : hdataflow(Info;A)@i
14. v3 : bag(A)@i
15. v(info(pred(e))) = <v2, v3>@i
\mvdash{} (fst(let s1,b = let ybs \mleftarrow{}{} bag-map(\mlambda{}P.P(info(pred(e)));
\mcup{}e'\mmember{}before(pred(e)).
bag-map(\mlambda{}a.Y a*(map(\mlambda{}x.info(x);filter(\mlambda{}a.e' \mleq{}loc a;before(pred(e)))));
snd(X*(map(\mlambda{}x.info(x);before(e')))(info(e'))))
+ bag-map(\mlambda{}x.(Y x);v3))
in let ys' \mleftarrow{}{} bag-map(\mlambda{}yb.(fst(yb));ybs)
in let out \mleftarrow{}{} \mcup{}yb\mmember{}ybs.snd(yb)
in <<v2, ys'>, out>
in <mk-hdf(p,a.simple-bind-nxt(\mlambda{}x.(Y x); p; a);p.let X,ys = p in ff;s1), b>))
= mk-hdf(p,a.simple-bind-nxt(\mlambda{}x.(Y x); p; a);p.let X,ys = p
in ff;<v2
, \mcup{}e'\mmember{}before(pred(e)) + \{pred(e)\}.
bag-map(\mlambda{}a.Y a*(map(\mlambda{}x.info(x);
filter(\mlambda{}a.e' \mleq{}loc a;
before(pred(e))
+ \{pred(e)\})));
snd(X*(map(\mlambda{}x.info(x);
before(e')))(info(e'))))
>)
By
Latex:
((Assert \mdownarrow{}Info BY
(D 0 THEN UseWitness \mkleeneopen{}info(e)\mkleeneclose{}\mcdot{} THEN Auto))
THEN (GenConcl \mkleeneopen{}before(pred(e)) = L\mkleeneclose{}\mcdot{} THENA Auto)
THEN RepeatFor 3 ((CallByValueReduce 0 THENA MaAuto))
THEN Reduce 0
THEN RepeatFor 2 ((EqCD THEN Auto))
THEN (RWO "bag-combine-append-left bag-map-map" 0
THENA (Auto THEN Unfolds ``bag-append single-bag`` 0 THEN Auto)
)
THEN RepUR ``compose`` 0
THEN (RWO "bag-map-append" 0 THENA Auto)
THEN EqCD
THEN Auto)\mcdot{}
Home
Index