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

Step * 2 2 2 1 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

                   in <mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧_b hdf-halted(X);s1), b>)(u))*(v)(a)))

= (snd(fst(let s1,b = simple-bind-nxt(Y; <X, ys2>; u)
           in <mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;s1), b>)*(v)(a)))
∈ bag(C)
BY
{ ((RW (AddrC [3;1;1;1;1;1] (UnfoldC `simple-bind-nxt`)) 0⋅ THEN Reduce 0)⋅
   THEN ((RW (AddrC [2;1;1;1;1;1;1;1;1] (UnfoldC `bind-nxt`)) 0⋅ THEN Reduce 0)
         THEN RepUR ``hdf-ap`` 0
         THEN Fold `hdf-ap` 0
         THEN (GenConclAtAddr [2;1;1;1;1;1;1]⋅
               THEN D -2
               THEN Reduce 0
               THEN (Assert λP.P(u) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C)) BY
                           Auto)
               THEN skip{(RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
                          THEN Reduce 0
                          THEN BackThruSomeHyp
                          THEN Try ((DoSubsume THEN Auto)))})⋅)⋅
   ) }

1
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)))) ∨ (¬↑hdf-halted(X))
15. v2 : hdataflow(A;B)@i
16. v3 : bag(B)@i
17. X(u) = <v2, v3> ∈ (hdataflow(A;B) × bag(B))@i
18. λP.P(u) ∈ hdataflow(A;C) ⟶ (hdataflow(A;C) × bag(C))
⊢ (snd(fst(let s1,b = let ybs ⟵ bag-map(λP.P(u);ys1 + bag-map(Y;v3))
                      in let ys' ⟵ [y∈bag-map(λyb.(fst(yb));ybs)|¬_bhdf-halted(y)]
                         in let out ⟵ ⋃yb∈ybs.snd(yb)
                            in <<v2, ys'>, out>

           in <mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) ∧_b hdf-halted(X);s1), b>)*(v)(a)))

= (snd(fst(let s1,b = let ybs ⟵ bag-map(λP.P(u);ys2 + bag-map(Y;v3))
                      in let ys' ⟵ bag-map(λyb.(fst(yb));ybs)
                         in let out ⟵ ⋃yb∈ybs.snd(yb)
                            in <<v2, ys'>, out>
           in <mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;s1), b>)*(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. (\mneg{}(ys1 = \{\})) \mvee{} (\mneg{}\muparrow{}hdf-halted(X)) \mvdash{} (snd(fst(inl (\mlambda{}a.let s1,b = bind-nxt(Y;<X, ys1>a) in <mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in bag-null(ys) \mwedge{}\msubb{} hdf-halted(X);s1) , b >)(u))*(v)(a))) = (snd(fst(let s1,b = simple-bind-nxt(Y; <X, ys2> u) in <mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys = p in ff;s1), b>)*(v)(a))) By Latex: ((RW (AddrC [3;1;1;1;1;1] (UnfoldC `simple-bind-nxt`)) 0\mcdot{} THEN Reduce 0)\mcdot{} THEN ((RW (AddrC [2;1;1;1;1;1;1;1;1] (UnfoldC `bind-nxt`)) 0\mcdot{} THEN Reduce 0) THEN RepUR ``hdf-ap`` 0 THEN Fold `hdf-ap` 0 THEN (GenConclAtAddr [2;1;1;1;1;1;1]\mcdot{} THEN D -2 THEN Reduce 0 THEN (Assert \mlambda{}P.P(u) \mmember{} hdataflow(A;C) {}\mrightarrow{} (hdataflow(A;C) \mtimes{} bag(C)) BY Auto) THEN skip\{(RepeatFor 3 ((CallByValueReduce 0 THENA Auto)) THEN Reduce 0 THEN BackThruSomeHyp THEN Try ((DoSubsume THEN Auto)))\})\mcdot{})\mcdot{} ) Home Index