Proof of Nuprl Lemma : iterate-hdf-bind-simple

Step * 2 1 2 1 2 1 2 of Lemma iterate-hdf-bind-simple

1. A : Type
2. B : Type
3. C : Type
4. Y : B ⟶ hdataflow(A;C)
5. valueall-type(C)
6. u : A@i
7. v : A List@i
8. ∀X:hdataflow(A;B). ∀ys1,ys2:bag(hdataflow(A;C)). ∀a:A.
((ys1 = [y∈ys2|¬_bhdf-halted(y)] ∈ bag(hdataflow(A;C)))
⇒

 ((snd(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧_b hdf-halted(X);<X, ys1>)*(v)(a))) = (snd(mk-hd\000Cf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(v)(a))) ∈ bag(C)))@i

9. X : hdataflow(A;B)@i
10. ys1 : bag(hdataflow(A;C))@i
11. ys2 : bag(hdataflow(A;C))@i
12. a : A@i
13. ys1 = [y∈ys2|¬_bhdf-halted(y)] ∈ bag(hdataflow(A;C))@i
14. ys1 = {} ∈ bag(hdataflow(A;C))
15. ↑hdf-halted(X)
16. ys1 = {} ∈ bag(hdataflow(A;C))
17. ↑hdf-halted(X)
18. ([x∈ys2|hdf-halted(x)] + [x∈ys2|¬_bhdf-halted(x)]) = ys2 ∈ bag(hdataflow(A;C))
19. v1 : bag({x:hdataflow(A;C)| ↑hdf-halted(x)} )@i
20. [x∈ys2|hdf-halted(x)] = v1 ∈ bag({x:hdataflow(A;C)| ↑hdf-halted(x)} )@i

⊢ {} = (snd(fst(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), v1>)(u))*(v)(a))) ∈ bag(C)

BY
{ Assert ⌜∀L:A List. ∀a:A. ∀ys:bag({x:hdataflow(A;C)| ↑hdf-halted(x)} ).

            ({} = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), ys>)*(L)(a))) ∈ bag(C))⌝⋅ }

1
.....assertion.....
1. A : Type
2. B : Type
3. C : Type
4. Y : B ⟶ hdataflow(A;C)
5. valueall-type(C)
6. u : A@i
7. v : A List@i
8. ∀X:hdataflow(A;B). ∀ys1,ys2:bag(hdataflow(A;C)). ∀a:A.
((ys1 = [y∈ys2|¬_bhdf-halted(y)] ∈ bag(hdataflow(A;C)))
⇒

 ((snd(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧_b hdf-halted(X);<X, ys1>)*(v)(a))) = (snd(mk-hd\000Cf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(v)(a))) ∈ bag(C)))@i

    ({} = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), ys>)*(L)(a))) ∈ bag(C))

2
1. A : Type
2. B : Type
3. C : Type
4. Y : B ⟶ hdataflow(A;C)
5. valueall-type(C)
6. u : A@i
7. v : A List@i
8. ∀X:hdataflow(A;B). ∀ys1,ys2:bag(hdataflow(A;C)). ∀a:A.
((ys1 = [y∈ys2|¬_bhdf-halted(y)] ∈ bag(hdataflow(A;C)))
⇒

 ((snd(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧_b hdf-halted(X);<X, ys1>)*(v)(a))) = (snd(mk-hd\000Cf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(v)(a))) ∈ bag(C)))@i

      ({} = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), ys>)*(L)(a))) ∈ bag(C))

⊢ {} = (snd(fst(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), v1>)(u))*(v)(a))) ∈ bag(C)

Latex:

Latex:
1. A : Type 2. B : Type 3. C : Type 4. Y : B {}\mrightarrow{} hdataflow(A;C) 5. valueall-type(C) 6. u : A@i 7. v : A List@i 8. \mforall{}X:hdataflow(A;B). \mforall{}ys1,ys2:bag(hdataflow(A;C)). \mforall{}a:A. ((ys1 = [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]) {}\mRightarrow{} ((snd(mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) \mwedge{}\msubb{} hdf-halted(X);<X, ys1>)*(\000Cv)(a))) = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<X, ys2>)*(v)(a)))))@i 9. X : hdataflow(A;B)@i 10. ys1 : bag(hdataflow(A;C))@i 11. ys2 : bag(hdataflow(A;C))@i 12. a : A@i 13. ys1 = [y\mmember{}ys2|\mneg{}\msubb{}hdf-halted(y)]@i 14. ys1 = \{\} 15. \muparrow{}hdf-halted(X) 16. ys1 = \{\} 17. \muparrow{}hdf-halted(X) 18. ([x\mmember{}ys2|hdf-halted(x)] + [x\mmember{}ys2|\mneg{}\msubb{}hdf-halted(x)]) = ys2 19. v1 : bag(\{x:hdataflow(A;C)| \muparrow{}hdf-halted(x)\} )@i 20. [x\mmember{}ys2|hdf-halted(x)] = v1@i \mvdash{} \{\} = (snd(fst(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), v1>)(u))*(v)(a\000C))) By Latex: Assert \mkleeneopen{}\mforall{}L:A List. \mforall{}a:A. \mforall{}ys:bag(\{x:hdataflow(A;C)| \muparrow{}hdf-halted(x)\} ). (\{\} = (snd(mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;<hdf-halt(), ys>)*(L)(\000Ca))))\mkleeneclose{}\mcdot{} Home Index