Step
*
1
1
1
1
1
1
1
1
of Lemma
sequence-class-program_wf
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
((∀u:E List. ∀y:E.
(u @ [y] ≤ v
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(y)))))))))
⇒ (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> f\000Ci
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);v))
, ypr*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)))
10. xpr : hdataflow(Info;A)@i
11. ypr : hdataflow(Info;B)@i
12. zpr : hdataflow(Info;A)@i
13. ∀u@0:E List. ∀y:E.
(u@0 @ [y] ≤ [u / v]
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u@0))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u@0))(info(y))))))))@i
⊢ fst(mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)(info(u)))*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <fst(xpr(info(u)))*(map(λx.info(x);v))
, fst(ypr(info(u)))*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)
BY
{ (RW (AddrC [2] (RecUnfoldC `mk-hdf`)) 0
THEN Reduce 0
THEN (RWO "hdf-ap-run" 0 THENA Auto)
THEN Reduce 0
THEN HDataflowHDVar' `xpr'
THEN HDataflowHDVar' `ypr'
THEN Try (RW (AddrC [1] (SweepUpC (FoldC `hdf-run`))) 0)
THEN (UnivCD THENA Auto)
THEN Try ((BackThruSomeHyp THEN (UnivCD THENA Auto)))
THEN Try (Complete (((RWO "iterate-hdf-halt" 0 THENA Auto) THEN Reduce 0 THEN Auto)))
THEN Try ((BoolCase ⌜bag-null(z2)⌝⋅ THENA Auto))) }
1
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
((∀u:E List. ∀y:E.
(u @ [y] ≤ v
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(y)))))))))
⇒ (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> f\000Ci
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);v))
, ypr*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)))
10. zpr : hdataflow(Info;A)@i
11. x : Info ⟶ (hdataflow(Info;A) × bag(A))@i
12. z1 : hdataflow(Info;A)@i
13. z2 : bag(A)@i
14. (x info(u)) = <z1, z2> ∈ (hdataflow(Info;A) × bag(A))@i
15. x1 : Info ⟶ (hdataflow(Info;B) × bag(B))@i
16. ∀u@0:E List. ∀y:E.
(u@0 @ [y] ≤ [u / v]
⇒ (¬↑(bag-null(snd(inl x*(map(λx.info(x);u@0))(info(y))))
∧b (¬bbag-null(snd(inl x1*(map(λx.info(x);u@0))(info(y))))))))@i
17. z3 : hdataflow(Info;B)@i
18. z4 : bag(B)@i
19. (x1 info(u)) = <z3, z4> ∈ (hdataflow(Info;B) × bag(B))@i
20. z2 = {} ∈ bag(A)
⊢ fst(let s1,b = if ¬bbag-null(z4) then let Z',bz = zpr(info(u)) in <inr Z' , bz> else <inl <z1, z3>, z2> fi
in <mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);s1)
, b
>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <z1*(map(λx.info(x);v))
, z3*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)
2
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
((∀u:E List. ∀y:E.
(u @ [y] ≤ v
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(y)))))))))
⇒ (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> f\000Ci
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);v))
, ypr*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)))
10. zpr : hdataflow(Info;A)@i
11. x : Info ⟶ (hdataflow(Info;A) × bag(A))@i
12. z1 : hdataflow(Info;A)@i
13. z2 : bag(A)@i
14. ¬(z2 = {} ∈ bag(A))
15. (x info(u)) = <z1, z2> ∈ (hdataflow(Info;A) × bag(A))@i
16. x1 : Info ⟶ (hdataflow(Info;B) × bag(B))@i
17. ∀u@0:E List. ∀y:E.
(u@0 @ [y] ≤ [u / v]
⇒ (¬↑(bag-null(snd(inl x*(map(λx.info(x);u@0))(info(y))))
∧b (¬bbag-null(snd(inl x1*(map(λx.info(x);u@0))(info(y))))))))@i
18. z3 : hdataflow(Info;B)@i
19. z4 : bag(B)@i
20. (x1 info(u)) = <z3, z4> ∈ (hdataflow(Info;B) × bag(B))@i
⊢ mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <z1, z3>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <z1*(map(λx.info(x);v))
, z3*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)
3
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
((∀u:E List. ∀y:E.
(u @ [y] ≤ v
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(y)))))))))
⇒ (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> f\000Ci
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);v))
, ypr*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)))
10. zpr : hdataflow(Info;A)@i
11. x : Info ⟶ (hdataflow(Info;A) × bag(A))@i
12. z1 : hdataflow(Info;A)@i
13. z2 : bag(A)@i
14. (x info(u)) = <z1, z2> ∈ (hdataflow(Info;A) × bag(A))@i
15. y : 0 = 0 ∈ ℤ
16. ∀u@0:E List. ∀y@0:E.
(u@0 @ [y@0] ≤ [u / v]
⇒ (¬↑(bag-null(snd(hdf-run(x)*(map(λx.info(x);u@0))(info(y@0))))
∧b (¬bbag-null(snd(hdf-halt()*(map(λx.info(x);u@0))(info(y@0))))))))@i
17. z2 = {} ∈ bag(A)
⊢ mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <z1, hdf-halt()>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <z1*(map(λx.info(x);v))
, hdf-halt()*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)
4
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
((∀u:E List. ∀y:E.
(u @ [y] ≤ v
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(y)))))))))
⇒ (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> f\000Ci
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);v))
, ypr*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)))
10. zpr : hdataflow(Info;A)@i
11. x : Info ⟶ (hdataflow(Info;A) × bag(A))@i
12. z1 : hdataflow(Info;A)@i
13. z2 : bag(A)@i
14. ¬(z2 = {} ∈ bag(A))
15. (x info(u)) = <z1, z2> ∈ (hdataflow(Info;A) × bag(A))@i
16. y : 0 = 0 ∈ ℤ
17. ∀u@0:E List. ∀y@0:E.
(u@0 @ [y@0] ≤ [u / v]
⇒ (¬↑(bag-null(snd(hdf-run(x)*(map(λx.info(x);u@0))(info(y@0))))
∧b (¬bbag-null(snd(hdf-halt()*(map(λx.info(x);u@0))(info(y@0))))))))@i
⊢ mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <z1, hdf-halt()>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <z1*(map(λx.info(x);v))
, hdf-halt()*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)
5
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
((∀u:E List. ∀y:E.
(u @ [y] ≤ v
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(y)))))))))
⇒ (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> f\000Ci
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);v))
, ypr*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)))
10. zpr : hdataflow(Info;A)@i
11. y : 0 = 0 ∈ ℤ
12. x : Info ⟶ (hdataflow(Info;B) × bag(B))@i
13. z1 : hdataflow(Info;B)@i
14. z2 : bag(B)@i
15. (x info(u)) = <z1, z2> ∈ (hdataflow(Info;B) × bag(B))@i
16. ∀u@0:E List. ∀y@0:E.
(u@0 @ [y@0] ≤ [u / v]
⇒ (¬↑(bag-null(snd(hdf-halt()*(map(λx.info(x);u@0))(info(y@0))))
∧b (¬bbag-null(snd(hdf-run(x)*(map(λx.info(x);u@0))(info(y@0))))))))@i
17. z2 = {} ∈ bag(B)
⊢ mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <hdf-halt(), z1>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <hdf-halt()*(map(λx.info(x);v))
, z1*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)
6
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
((∀u:E List. ∀y:E.
(u @ [y] ≤ v
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(y))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(y)))))))))
⇒ (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> f\000Ci
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);v))
, ypr*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)))
10. zpr : hdataflow(Info;A)@i
11. y : 0 = 0 ∈ ℤ
12. x : Info ⟶ (hdataflow(Info;B) × bag(B))@i
13. z1 : hdataflow(Info;B)@i
14. z2 : bag(B)@i
15. ¬(z2 = {} ∈ bag(B))
16. (x info(u)) = <z1, z2> ∈ (hdataflow(Info;B) × bag(B))@i
17. ∀u@0:E List. ∀y@0:E.
(u@0 @ [y@0] ≤ [u / v]
⇒ (¬↑(bag-null(snd(hdf-halt()*(map(λx.info(x);u@0))(info(y@0))))
∧b (¬bbag-null(snd(hdf-run(x)*(map(λx.info(x);u@0))(info(y@0))))))))@i
⊢ fst(let s1,b = let Z',bz = zpr(info(u))
in <inr Z' , bz>
in <mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);s1)
, b
>)*(map(λx.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <hdf-halt()*(map(λx.info(x);v))
, z1*(map(λx.info(x);v))
>)
∈ hdataflow(Info;A)
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. \mforall{}xpr:hdataflow(Info;A). \mforall{}ypr:hdataflow(Info;B). \mforall{}zpr:hdataflow(Info;A).
((\mforall{}u:E List. \mforall{}y:E.
(u @ [y] \mleq{} v
{}\mRightarrow{} (\mneg{}\muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);u))(info(y))))
\mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);u))(info(y)))))))))
{}\mRightarrow{} (mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(\mlambda{}x\000C.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>S.case S
of inl(XY) =>
ff
| inr(Z) =>
hdf-halted(Z);inl <xpr*(map(\mlambda{}x.info(x);v)), ypr*(map(\mlambda{}x.info(x);v))>)))
10. xpr : hdataflow(Info;A)@i
11. ypr : hdataflow(Info;B)@i
12. zpr : hdataflow(Info;A)@i
13. \mforall{}u@0:E List. \mforall{}y:E.
(u@0 @ [y] \mleq{} [u / v]
{}\mRightarrow{} (\mneg{}\muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);u@0))(info(y))))
\mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);u@0))(info(y))))))))@i
\mvdash{} fst(mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)(info(u)))*(map(\000C\mlambda{}x.info(x);v))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>S.case S
of inl(XY) =>
ff
| inr(Z) =>
hdf-halted(Z);inl <fst(xpr(info(u)))*(map(\mlambda{}x.info(x);v)), fst(ypr(info(u)))*(map(\mlambda{}x.info(x);v))>)
By
Latex:
(RW (AddrC [2] (RecUnfoldC `mk-hdf`)) 0
THEN Reduce 0
THEN (RWO "hdf-ap-run" 0 THENA Auto)
THEN Reduce 0
THEN HDataflowHDVar' `xpr'
THEN HDataflowHDVar' `ypr'
THEN Try (RW (AddrC [1] (SweepUpC (FoldC `hdf-run`))) 0)
THEN (UnivCD THENA Auto)
THEN Try ((BackThruSomeHyp THEN (UnivCD THENA Auto)))
THEN Try (Complete (((RWO "iterate-hdf-halt" 0 THENA Auto) THEN Reduce 0 THEN Auto)))
THEN Try ((BoolCase \mkleeneopen{}bag-null(z2)\mkleeneclose{}\mcdot{} THENA Auto)))
Home
Index