Step
*
4
of Lemma
hdf-union-ap
1. A : Type
2. B : Type
3. C : Type
4. a : A
5. valueall-type(C)
6. valueall-type(B)
7. x : A ─→ (hdataflow(A;B) × bag(B))@i
8. z1 : hdataflow(A;B)@i
9. z2 : bag(B)@i
10. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
11. x1 : A ─→ (hdataflow(A;C) × bag(C))@i
12. z3 : hdataflow(A;C)@i
13. z4 : bag(C)@i
14. (x1 a) = <z3, z4> ∈ (hdataflow(A;C) × bag(C))@i
⊢ let s1,b = let out ←─ bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)
in <<z1, z3>, out>
in <mk-hdf(XY,a.let X,Y = XY
in let X',xs = X(a)
in let Y',ys = Y(a)
in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
in <<X', Y'>, out>;XY.let X,Y = XY
in hdf-halted(X) ∧b hdf-halted(Y);s1)
, b
>
= <if hdf-halted(z1) ∧b hdf-halted(z3)
then hdf-halt()
else hdf-run(λa1.let s1,b = let X',xs = z1(a1)
in let Y',ys = z3(a1)
in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
in <<X', Y'>, out>
in <mk-hdf(XY,a.let X,Y = XY
in let X',xs = X(a)
in let Y',ys = Y(a)
in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
in <<X', Y'>, out>;XY.let X,Y = XY
in hdf-halted(X) ∧b hdf-halted(Y);s1)
, b
>)
fi
, bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)
>
∈ (hdataflow(A;B + C) × bag(B + C))
BY
{ ((GenConcl ⌈(bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)) = b ∈ bag(B + C)⌉⋅ THENA Auto)
THEN (CallByValueReduceOn ⌈b⌉ 0⋅ THENA Auto)
THEN Reduce 0
THEN (EqCD THEN Auto)
THEN RW (AddrC [2] RecUnfoldTopAbC) 0
THEN Reduce 0
THEN Fold `member` 0
THEN Auto) }
1
1. A : Type
2. B : Type
3. C : Type
4. a : A
5. valueall-type(C)
6. valueall-type(B)
7. x : A ─→ (hdataflow(A;B) × bag(B))@i
8. z1 : hdataflow(A;B)@i
9. z2 : bag(B)@i
10. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
11. x1 : A ─→ (hdataflow(A;C) × bag(C))@i
12. z3 : hdataflow(A;C)@i
13. ¬((↑hdf-halted(z1)) ∧ (↑hdf-halted(z3)))
14. z4 : bag(C)@i
15. (x1 a) = <z3, z4> ∈ (hdataflow(A;C) × bag(C))@i
16. b : bag(B + C)@i
17. (bag-map(λx.(inl x);z2) + bag-map(λx.(inr x );z4)) = b ∈ bag(B + C)@i
18. ff ∈ 𝔹
19. a1 : A@i
⊢ let s1,b = let X',xs = z1(a1)
in let Y',ys = z3(a1)
in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
in <<X', Y'>, out>
in <mk-hdf(XY,a.let X,Y = XY
in let X',xs = X(a)
in let Y',ys = Y(a)
in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
in <<X', Y'>, out>;XY.let X,Y = XY
in hdf-halted(X) ∧b hdf-halted(Y);s1)
, b
> ∈ hdataflow(A;B + C) × bag(B + C)
Latex:
1. A : Type
2. B : Type
3. C : Type
4. a : A
5. valueall-type(C)
6. valueall-type(B)
7. x : A {}\mrightarrow{} (hdataflow(A;B) \mtimes{} bag(B))@i
8. z1 : hdataflow(A;B)@i
9. z2 : bag(B)@i
10. (x a) = <z1, z2>@i
11. x1 : A {}\mrightarrow{} (hdataflow(A;C) \mtimes{} bag(C))@i
12. z3 : hdataflow(A;C)@i
13. z4 : bag(C)@i
14. (x1 a) = <z3, z4>@i
\mvdash{} let s1,b = let out \mleftarrow{}{} bag-map(\mlambda{}x.(inl x);z2) + bag-map(\mlambda{}x.(inr x );z4)
in <<z1, z3>, out>
in <mk-hdf(XY,a.let X,Y = XY
in let X',xs = X(a)
in let Y',ys = Y(a)
in let out \mleftarrow{}{} bag-map(\mlambda{}x.(inl x);xs) + bag-map(\mlambda{}x.(inr x );ys)
in <<X', Y'>, out>XY.let X,Y = XY
in hdf-halted(X) \mwedge{}\msubb{} hdf-halted(Y);s1)
, b
>
= <if hdf-halted(z1) \mwedge{}\msubb{} hdf-halted(z3)
then hdf-halt()
else hdf-run(\mlambda{}a1.let s1,b = let X',xs = z1(a1)
in let Y',ys = z3(a1)
in let out \mleftarrow{}{} bag-map(\mlambda{}x.(inl x);xs) + bag-map(\mlambda{}x.(inr x );ys)
in <<X', Y'>, out>
in <mk-hdf(XY,a.let X,Y = XY
in let X',xs = X(a)
in let Y',ys = Y(a)
in let out \mleftarrow{}{} bag-map(\mlambda{}x.(inl x);xs)
+ bag-map(\mlambda{}x.(inr x );ys)
in <<X', Y'>
, out
>XY.let X,Y = XY
in hdf-halted(X) \mwedge{}\msubb{} hdf-halted(Y);s1)
, b
>)
fi
, bag-map(\mlambda{}x.(inl x);z2) + bag-map(\mlambda{}x.(inr x );z4)
>
By
((GenConcl \mkleeneopen{}(bag-map(\mlambda{}x.(inl x);z2) + bag-map(\mlambda{}x.(inr x );z4)) = b\mkleeneclose{}\mcdot{} THENA Auto)
THEN (CallByValueReduceOn \mkleeneopen{}b\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN Reduce 0
THEN (EqCD THEN Auto)
THEN RW (AddrC [2] RecUnfoldTopAbC) 0
THEN Reduce 0
THEN Fold `member` 0
THEN Auto)
Home
Index