Step
*
of Lemma
hdf-union-ap
∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].
(X + Y(a)
= <fst(X(a)) + fst(Y(a)), bag-map(λx.(inl x);snd(X(a))) + bag-map(λx.(inr x );snd(Y(a)))>
∈ (hdataflow(A;B + C) × bag(B + C))) supposing
(valueall-type(B) and
valueall-type(C))
BY
{ (Auto
THEN RepUR ``hdf-union hdf-ap`` 0
THEN RecUnfold `mk-hdf` 0
THEN Reduce 0
THEN Fold `hdf-ap` 0
THEN ((BoolCase ⌜hdf-halted(X)⌝⋅ THENA Auto)
THENL [((Subst' X ~ hdf-halt() 0 THENA (BLemma `hdf-halted-is-halt` THEN Auto)) THEN Reduce 0)
; HDataflowHDVar' `X']
)
THEN ((BoolCase ⌜hdf-halted(Y)⌝⋅ THENA Auto)
THENL [((Subst' Y ~ hdf-halt() 0 THENA (BLemma `hdf-halted-is-halt` THEN Auto)) THEN Reduce 0)
; HDataflowHDVar' `Y']
)) }
1
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. Y : hdataflow(A;C)
6. a : A
7. valueall-type(C)
8. valueall-type(B)
9. ↑hdf-halted(X)
10. ↑hdf-halted(Y)
⊢ <hdf-halt(), {}> = <hdf-halt(), {}> ∈ (hdataflow(A;B + C) × bag(B + C))
2
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. a : A
6. valueall-type(C)
7. valueall-type(B)
8. ↑hdf-halted(X)
9. x : A ⟶ (hdataflow(A;C) × bag(C))@i
10. z1 : hdataflow(A;C)@i
11. z2 : bag(C)@i
12. (x a) = <z1, z2> ∈ (hdataflow(A;C) × bag(C))@i
⊢ let s1,b = let out ⟵ bag-map(λx.(inr x );z2)
in <<hdf-halt(), z1>, 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)
then hdf-halt()
else hdf-run(λa1.let s1,b = let Y',ys = z1(a1)
in let out ⟵ bag-map(λx.(inr x );ys)
in <<hdf-halt(), 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.(inr x );z2)
>
∈ (hdataflow(A;B + C) × bag(B + C))
3
1. A : Type
2. B : Type
3. C : Type
4. Y : hdataflow(A;C)
5. a : A
6. valueall-type(C)
7. valueall-type(B)
8. x : A ⟶ (hdataflow(A;B) × bag(B))@i
9. z1 : hdataflow(A;B)@i
10. z2 : bag(B)@i
11. (x a) = <z1, z2> ∈ (hdataflow(A;B) × bag(B))@i
12. ↑hdf-halted(Y)
⊢ let s1,b = let out ⟵ bag-map(λx.(inl x);z2) + {}
in <<z1, inr ⋅ >, 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 tt
then hdf-halt()
else hdf-run(λa1.let s1,b = let X',xs = z1(a1)
in let out ⟵ bag-map(λx.(inl x);xs) + {}
in <<X', inr ⋅ >, 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) + {}
>
∈ (hdataflow(A;B + C) × bag(B + C))
4
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))
Latex:
Latex:
\mforall{}[A,B,C:Type]. \mforall{}[X:hdataflow(A;B)]. \mforall{}[Y:hdataflow(A;C)]. \mforall{}[a:A].
(X + Y(a)
= <fst(X(a)) + fst(Y(a))
, bag-map(\mlambda{}x.(inl x);snd(X(a))) + bag-map(\mlambda{}x.(inr x );snd(Y(a)))
>) supposing
(valueall-type(B) and
valueall-type(C))
By
Latex:
(Auto
THEN RepUR ``hdf-union hdf-ap`` 0
THEN RecUnfold `mk-hdf` 0
THEN Reduce 0
THEN Fold `hdf-ap` 0
THEN ((BoolCase \mkleeneopen{}hdf-halted(X)\mkleeneclose{}\mcdot{} THENA Auto)
THENL [((Subst' X \msim{} hdf-halt() 0 THENA (BLemma `hdf-halted-is-halt` THEN Auto))
THEN Reduce 0
)
; HDataflowHDVar' `X']
)
THEN ((BoolCase \mkleeneopen{}hdf-halted(Y)\mkleeneclose{}\mcdot{} THENA Auto)
THENL [((Subst' Y \msim{} hdf-halt() 0 THENA (BLemma `hdf-halted-is-halt` THEN Auto))
THEN Reduce 0
)
; HDataflowHDVar' `Y']
))
Home
Index