---

Step * of Lemma rec-bind-nxt_wf

∀[A,B,C:Type]. ∀[X:C ⟶ hdataflow(A;B)]. ∀[Y:C ⟶ hdataflow(A;C)]. ∀[p:bag(hdataflow(A;B)) × bag(hdataflow(A;C))].
∀[a:A].
  (rec-bind-nxt(X;Y;p;a) ∈ bag(hdataflow(A;B)) × bag(hdataflow(A;C)) × bag(B)) supposing 
     (valueall-type(B) and 
     valueall-type(C))
BY
{ (ProveWfLemmaAux (Try (Complete Auto))
   THEN HDataflowHDAll
   THEN RepUR ``hdf-run hdf-halt`` 0
   THEN DVar `p'
   THEN Reduce 0
   THEN (GenConcl ⌜bag-map(λp.p(a);p2) = Z ∈ bag(hdataflow(A;C) × bag(C))⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN ((GenConcl ⌜bag-map(λp.p(a);p1 + bag-map(X;⋃x∈Z.snd(x))) = V ∈ bag(hdataflow(A;B) × bag(B))⌝⋅ THENA Auto)
         THEN (CallByValueReduce 0 THENA Auto)
         THEN ((GenConcl ⌜bag-map(λx.(fst(Y x(a)));⋃x∈Z.snd(x)) = W ∈ bag(hdataflow(A;C))⌝⋅ THENA Auto)
               THEN (CallByValueReduce 0 THENA Auto)
               )⋅)⋅) }

1
1. A : Type
2. B : Type
3. C : Type
4. X : C ⟶ hdataflow(A;B)
5. Y : C ⟶ hdataflow(A;C)
6. p1 : bag(hdataflow(A;B))
7. p2 : bag(hdataflow(A;C))
8. a : A
9. valueall-type(C)
10. valueall-type(B)
11. Z : bag(hdataflow(A;C) × bag(C))@i
12. bag-map(λp.p(a);p2) = Z ∈ bag(hdataflow(A;C) × bag(C))@i
13. V : bag(hdataflow(A;B) × bag(B))@i
14. bag-map(λp.p(a);p1 + bag-map(X;⋃x∈Z.snd(x))) = V ∈ bag(hdataflow(A;B) × bag(B))@i
15. W : bag(hdataflow(A;C))@i
16. bag-map(λx.(fst(Y x(a)));⋃x∈Z.snd(x)) = W ∈ bag(hdataflow(A;C))@i
⊢ <<bag-mapfilter(λx.(fst(x));λx.isl(fst(x));V), bag-mapfilter(λx.(fst(x));λx.isl(fst(x));Z) + [p∈W|isl(p)]>
  , ⋃x∈V.snd(x)
  > ∈ bag(hdataflow(A;B)) × bag(hdataflow(A;C)) × bag(B)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X:C  {}\mrightarrow{}  hdataflow(A;B)].  \mforall{}[Y:C  {}\mrightarrow{}  hdataflow(A;C)].
\mforall{}[p:bag(hdataflow(A;B))  \mtimes{}  bag(hdataflow(A;C))].  \mforall{}[a:A].
    (rec-bind-nxt(X;Y;p;a)  \mmember{}  bag(hdataflow(A;B))  \mtimes{}  bag(hdataflow(A;C))  \mtimes{}  bag(B))  supposing 
          (valueall-type(B)  and 
          valueall-type(C))


By

---

Latex:
(ProveWfLemmaAux  (Try  (Complete  Auto))
  THEN  HDataflowHDAll
  THEN  RepUR  ``hdf-run  hdf-halt``  0
  THEN  DVar  `p'
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}bag-map(\mlambda{}p.p(a);p2)  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  ((GenConcl  \mkleeneopen{}bag-map(\mlambda{}p.p(a);p1  +  bag-map(X;\mcup{}x\mmember{}Z.snd(x)))  =  V\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (CallByValueReduce  0  THENA  Auto)
              THEN  ((GenConcl  \mkleeneopen{}bag-map(\mlambda{}x.(fst(Y  x(a)));\mcup{}x\mmember{}Z.snd(x))  =  W\mkleeneclose{}\mcdot{}  THENA  Auto)
                          THEN  (CallByValueReduce  0  THENA  Auto)
                          )\mcdot{})\mcdot{})

---

Home Index