Step
*
2
1
2
of Lemma
loop-class-memory-program_wf
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B ─→ B)
5. init : Id ─→ bag(B)
6. pr : Id ─→ hdataflow(Info;B ─→ B)
7. ∀es:EO+(Info). ∀e:E. (X(e) = (snd(pr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B ─→ B))
8. es : EO+(Info)@i'
9. e : E@i
10. hdf-memory(pr loc(e);init loc(e))*(map(λx.info(x);before(e)))
= hdf-memory(pr loc(e)*(map(λx.info(x);before(e)));loop-class-memory(X;init)(e))
∈ hdataflow(Info;B)
11. v : bag(B)@i
12. loop-class-memory(X;init)(e) = v ∈ bag(B)@i
13. y : Unit@i
⊢ v
= (snd(let s1,b = let s' ←─ v
in <<inr ⋅ , s'>, v>
in <mk-hdf(Xbs,a.let X,s = Xbs
in let X',fs = case X of inl(P) => P a | inr(z) => <inr ⋅ , {}>
in let b ←─ ∪f∈fs.bag-map(f;s)
in let s' ←─ if bag-null(b) then s else b fi
in <<X', s'>, s>;s.ff;s1)
, b
>))
∈ bag(B)
BY
{ (Reduce 0 THEN (CallByValueReduceOn ⌈v⌉ 0⋅ THENA MaAuto) THEN Reduce 0 THEN Auto) }
Latex:
Latex:
1. Info : Type
2. B : Type
3. valueall-type(B)
4. X : EClass(B {}\mrightarrow{} B)
5. init : Id {}\mrightarrow{} bag(B)
6. pr : Id {}\mrightarrow{} hdataflow(Info;B {}\mrightarrow{} B)
7. \mforall{}es:EO+(Info). \mforall{}e:E. (X(e) = (snd(pr loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))
8. es : EO+(Info)@i'
9. e : E@i
10. hdf-memory(pr loc(e);init loc(e))*(map(\mlambda{}x.info(x);before(e)))
= hdf-memory(pr loc(e)*(map(\mlambda{}x.info(x);before(e)));loop-class-memory(X;init)(e))
11. v : bag(B)@i
12. loop-class-memory(X;init)(e) = v@i
13. y : Unit@i
\mvdash{} v
= (snd(let s1,b = let s' \mleftarrow{}{} v
in <<inr \mcdot{} , s'>, v>
in <mk-hdf(Xbs,a.let X,s = Xbs
in let X',fs = case X of inl(P) => P a | inr(z) => <inr \mcdot{} , \{\}>
in let b \mleftarrow{}{} \mcup{}f\mmember{}fs.bag-map(f;s)
in let s' \mleftarrow{}{} if bag-null(b) then s else b fi
in <<X', s'>, s>s.ff;s1)
, b
>))
By
Latex:
(Reduce 0 THEN (CallByValueReduceOn \mkleeneopen{}v\mkleeneclose{} 0\mcdot{} THENA MaAuto) THEN Reduce 0 THEN Auto)
Home
Index