Step
*
1
of Lemma
loop-class-memory-program_wf
.....assertion.....
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
⊢ 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)
BY
{ (MoveToConcl (-1)
THEN CausalInd'
THEN (RWO "loop-class-memory-eq" 0 THENA Auto)
THEN RepeatFor 2 (Try (OldAutoSplit))
THEN RecUnfold `es-before` 0
THEN OldAutoSplit
THEN (InstHyp [⌈pred(e)⌉] (-4)⋅ THENA MaAuto)
THEN (RWW "map_append_sq iterate-hdf-append" 0 THENA MaAuto)
THEN Reduce 0
THEN (RWO "es-loc-pred" (-1) THENA Auto)
THEN (HypSubst' (-1) 0 THENA Auto)
THEN RepUR ``eclass3 class-ap`` 0
THEN Fold `class-ap` 0
THEN GenConclAtAddr [2;1;1;1]
THEN GenConclAtAddr [2;1;1;2]
THEN RW (AddrC [2] (UnfoldC `hdf-memory`)) 0
THEN RecUnfold `mk-hdf` 0
THEN RepUR ``hdf-ap hdf-run`` 0
THEN (Subst' loc(e) ~ loc(pred(e)) -3 THENA MaAuto)
THEN MoveToConcl (-3)
THEN (HDataflowHD (-3) THENA Auto)
THEN Reduce 0) }
1
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. ∀e1:E
((e1 < e)
⇒ (hdf-memory(pr loc(e1);init loc(e1))*(map(λx.info(x);before(e1)))
= hdf-memory(pr loc(e1)*(map(λx.info(x);before(e1)));loop-class-memory(X;init)(e1))
∈ hdataflow(Info;B)))
11. ¬↑first(e)
12. ↑pred(e) ∈b X
13. ¬↑first(e)
14. hdf-memory(pr loc(e);init loc(e))*(map(λx.info(x);before(pred(e))))
= hdf-memory(pr loc(e)*(map(λx.info(x);before(pred(e))));loop-class-memory(X;init)(pred(e)))
∈ hdataflow(Info;B)
15. v1 : bag(B)@i
16. loop-class-memory(X;init)(pred(e)) = v1 ∈ bag(B)@i
17. x : Info ─→ (hdataflow(Info;B ─→ B) × bag(B ─→ B))@i
⊢ (pr loc(pred(e))*(map(λx.info(x);before(pred(e)))) = (inl x) ∈ hdataflow(Info;B ─→ B))
⇒ ((fst(let s1,b = let X',fs = x info(pred(e))
in let b ←─ ∪f∈fs.bag-map(f;v1)
in let s' ←─ if bag-null(b) then v1 else b fi
in <<X', s'>, v1>
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
>))
= hdf-memory(fst((x info(pred(e))));∪f∈X(pred(e)).bag-map(f;v1))
∈ hdataflow(Info;B))
2
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. ∀e1:E
((e1 < e)
⇒ (hdf-memory(pr loc(e1);init loc(e1))*(map(λx.info(x);before(e1)))
= hdf-memory(pr loc(e1)*(map(λx.info(x);before(e1)));loop-class-memory(X;init)(e1))
∈ hdataflow(Info;B)))
11. ¬↑first(e)
12. ↑pred(e) ∈b X
13. ¬↑first(e)
14. hdf-memory(pr loc(e);init loc(e))*(map(λx.info(x);before(pred(e))))
= hdf-memory(pr loc(e)*(map(λx.info(x);before(pred(e))));loop-class-memory(X;init)(pred(e)))
∈ hdataflow(Info;B)
15. v1 : bag(B)@i
16. loop-class-memory(X;init)(pred(e)) = v1 ∈ bag(B)@i
17. y : Unit@i
⊢ (pr loc(pred(e))*(map(λx.info(x);before(pred(e)))) = (inr y ) ∈ hdataflow(Info;B ─→ B))
⇒ ((fst(let s1,b = let s' ←─ v1
in <<inr ⋅ , s'>, v1>
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
>))
= hdf-memory(inr ⋅ ;∪f∈X(pred(e)).bag-map(f;v1))
∈ hdataflow(Info;B))
3
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. ∀e1:E
((e1 < e)
⇒ (hdf-memory(pr loc(e1);init loc(e1))*(map(λx.info(x);before(e1)))
= hdf-memory(pr loc(e1)*(map(λx.info(x);before(e1)));loop-class-memory(X;init)(e1))
∈ hdataflow(Info;B)))
11. ¬↑first(e)
12. ¬↑pred(e) ∈b X
13. ¬↑first(e)
14. hdf-memory(pr loc(e);init loc(e))*(map(λx.info(x);before(pred(e))))
= hdf-memory(pr loc(e)*(map(λx.info(x);before(pred(e))));loop-class-memory(X;init)(pred(e)))
∈ hdataflow(Info;B)
15. v1 : bag(B)@i
16. loop-class-memory(X;init)(pred(e)) = v1 ∈ bag(B)@i
17. x : Info ─→ (hdataflow(Info;B ─→ B) × bag(B ─→ B))@i
⊢ (pr loc(pred(e))*(map(λx.info(x);before(pred(e)))) = (inl x) ∈ hdataflow(Info;B ─→ B))
⇒ ((fst(let s1,b = let X',fs = x info(pred(e))
in let b ←─ ∪f∈fs.bag-map(f;v1)
in let s' ←─ if bag-null(b) then v1 else b fi
in <<X', s'>, v1>
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
>))
= hdf-memory(fst((x info(pred(e))));v1)
∈ hdataflow(Info;B))
4
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. ∀e1:E
((e1 < e)
⇒ (hdf-memory(pr loc(e1);init loc(e1))*(map(λx.info(x);before(e1)))
= hdf-memory(pr loc(e1)*(map(λx.info(x);before(e1)));loop-class-memory(X;init)(e1))
∈ hdataflow(Info;B)))
11. ¬↑first(e)
12. ¬↑pred(e) ∈b X
13. ¬↑first(e)
14. hdf-memory(pr loc(e);init loc(e))*(map(λx.info(x);before(pred(e))))
= hdf-memory(pr loc(e)*(map(λx.info(x);before(pred(e))));loop-class-memory(X;init)(pred(e)))
∈ hdataflow(Info;B)
15. v1 : bag(B)@i
16. loop-class-memory(X;init)(pred(e)) = v1 ∈ bag(B)@i
17. y : Unit@i
⊢ (pr loc(pred(e))*(map(λx.info(x);before(pred(e)))) = (inr y ) ∈ hdataflow(Info;B ─→ B))
⇒ ((fst(let s1,b = let s' ←─ v1
in <<inr ⋅ , s'>, v1>
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
>))
= hdf-memory(inr ⋅ ;v1)
∈ hdataflow(Info;B))
Latex:
Latex:
.....assertion.....
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
\mvdash{} 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))
By
Latex:
(MoveToConcl (-1)
THEN CausalInd'
THEN (RWO "loop-class-memory-eq" 0 THENA Auto)
THEN RepeatFor 2 (Try (OldAutoSplit))
THEN RecUnfold `es-before` 0
THEN OldAutoSplit
THEN (InstHyp [\mkleeneopen{}pred(e)\mkleeneclose{}] (-4)\mcdot{} THENA MaAuto)
THEN (RWW "map\_append\_sq iterate-hdf-append" 0 THENA MaAuto)
THEN Reduce 0
THEN (RWO "es-loc-pred" (-1) THENA Auto)
THEN (HypSubst' (-1) 0 THENA Auto)
THEN RepUR ``eclass3 class-ap`` 0
THEN Fold `class-ap` 0
THEN GenConclAtAddr [2;1;1;1]
THEN GenConclAtAddr [2;1;1;2]
THEN RW (AddrC [2] (UnfoldC `hdf-memory`)) 0
THEN RecUnfold `mk-hdf` 0
THEN RepUR ``hdf-ap hdf-run`` 0
THEN (Subst' loc(e) \msim{} loc(pred(e)) -3 THENA MaAuto)
THEN MoveToConcl (-3)
THEN (HDataflowHD (-3) THENA Auto)
THEN Reduce 0)
Home
Index