Definition: hiddenfix
hiddenfix(F) ==  fix(F)

Definition: hdataflow
"halting dataflow", P, is either halted (inr ⋅ or it is function
that given an input a ∈ computes pair <Q, out>where is new 
"halting dataflow" and out is bag of type B.⋅

hdataflow(A;B) ==  corec(P.A ─→ (P × bag(B))?)

Lemma: hdataflow_wf
[A,B:Type].  (hdataflow(A;B) ∈ Type)

Lemma: hdataflow-ext
[A,B:Type].  hdataflow(A;B) ≡ A ─→ (hdataflow(A;B) × bag(B))?

Lemma: hdataflow-valueall-type
[A,B:Type].  valueall-type(hdataflow(A;B)) supposing ↓A

Lemma: hdataflow-value-type
[A,B:Type].  value-type(hdataflow(A;B)) supposing ↓A

Lemma: hdataflow_subtype
[A1,B1,A2,B2:Type].  (hdataflow(A1;B1) ⊆hdataflow(A2;B2)) supposing ((B1 ⊆B2) and (A2 ⊆A1))

Definition: hdf-ap
X(a) ==  case of inl(P) => inr(z) => <inr ⋅ {}>

Lemma: hdf-ap_wf
[A,B:Type]. ∀[X:hdataflow(A;B)]. ∀[a:A].  (X(a) ∈ hdataflow(A;B) × bag(B))

Definition: hdf-running
hdf-running(P) ==  isl(P)

Lemma: hdf-running_wf
[A,B:Type]. ∀[P:hdataflow(A;B)].  (hdf-running(P) ∈ 𝔹)

Definition: hdf-halted
hdf-halted(P) ==  isr(P)

Lemma: hdf-halted_wf
[A,B:Type]. ∀[P:hdataflow(A;B)].  (hdf-halted(P) ∈ 𝔹)

Lemma: hdf-halted-is-inr
[A,B:Type]. ∀[X:hdataflow(A;B)].  inr ⋅  supposing ↑hdf-halted(X)

Definition: hdf-halt
hdf-halt() ==  inr ⋅ 

Lemma: hdf-halt_wf
[A,B:Type].  (hdf-halt() ∈ hdataflow(A;B))

Lemma: hdf-halted-is-halt
[A,B:Type]. ∀[X:hdataflow(A;B)].  hdf-halt() supposing ↑hdf-halted(X)

Lemma: hdf_ap_halt_lemma
x:Top. (hdf-halt()(x) ~ <hdf-halt(), {}>)

Definition: hdf-run
hdf-run(P) ==  inl P

Lemma: hdf-run_wf
[A,B:Type]. ∀[P:A ─→ (hdataflow(A;B) × bag(B))].  (hdf-run(P) ∈ hdataflow(A;B))

Lemma: hdf-ap-run
[P,a:Top].  (hdf-run(P)(a) a)

Lemma: hdf-ap-inl
[P,a:Top].  (inl P(a) a)

Lemma: hdf-halted-halt
hdf-halted(hdf-halt()) tt

Lemma: hdf-halted-run
[P:Top]. (hdf-halted(hdf-run(P)) ff)

Lemma: hdf-halted-inl
[P:Top]. (hdf-halted(inl P) ff)

Lemma: hdf_halted_halt_red_lemma
hdf-halted(hdf-halt()) tt

Lemma: hdf_halted_run_red_lemma
P:Top. (hdf-halted(hdf-run(P)) ff)

Lemma: hdf_halted_inl_red_lemma
P:Top. (hdf-halted(inl P) ff)

Definition: hdf-out
hdf-out(P;x) ==  snd(P(x))

Lemma: hdf-out_wf
[A,B:Type]. ∀[P:hdataflow(A;B)]. ∀[x:A].  (hdf-out(P;x) ∈ bag(B))

Lemma: hdf-out-run
[P,x:Top].  (hdf-out(hdf-run(P);x) snd((P x)))

Lemma: hdf-out-inl
[P,x:Top].  (hdf-out(inl P;x) snd((P x)))

Lemma: hdf-out-halt
[x:Top]. (hdf-out(hdf-halt();x) {})

Lemma: hdf_out_halt_red_lemma
x:Top. (hdf-out(hdf-halt();x) {})

Definition: iterate-hdataflow
P*(inputs) ==  accumulate (with value and list item input): fst(p(input))over list:  inputswith starting value: P)

Lemma: iterate-hdataflow_wf
[A,B:Type]. ∀[P:hdataflow(A;B)]. ∀[inputs:A List].  (P*(inputs) ∈ hdataflow(A;B))

Lemma: iter_hdf_nil_lemma
P:Top. (P*([]) P)

Lemma: iter_hdf_cons_lemma
bs,a,P:Top.  (P*([a bs]) fst(P(a))*(bs))

Lemma: iterate-hdf-halt
[L:Top List]. (hdf-halt()*(L) hdf-halt())

Lemma: iterate-hdf-append
[L1:Top List]. ∀[F,L2:Top].  (F*(L1 L2) F*(L1)*(L2))

Lemma: hdataflow-equal
[A,B:Type]. ∀[P,Q:hdataflow(A;B)].
  uiff(P Q ∈ hdataflow(A;B);∀[inputs:A List]
                                (hdf-halted(P*(inputs)) hdf-halted(Q*(inputs))
                                ∧ (∀[a:A]. (hdf-out(P*(inputs);a) hdf-out(Q*(inputs);a) ∈ bag(B)))))

Definition: hdf-invariant
hdf-invariant(A;b.Q[b];X) ==  ∀L:A List. case X*(L) of inl(P) => ∀m:A. let X',b in Q[b] inr(z) => True

Lemma: hdf-invariant_wf
[A,B:Type]. ∀[Q:bag(B) ─→ ℙ]. ∀[X:hdataflow(A;B)].  (hdf-invariant(A;b.Q[b];X) ∈ ℙ)

Lemma: hdf-ap-invariant
[A,B:Type]. ∀[Q:bag(B) ─→ ℙ]. ∀[X:{X:hdataflow(A;B)| hdf-invariant(A;b.Q[b];X)} ]. ∀[a:A].
  (fst(X(a)) ∈ {X:hdataflow(A;B)| hdf-invariant(A;b.Q[b];X)} )

Lemma: hdf-ap-invariant2
[A,B:Type]. ∀[Q:bag(B) ─→ ℙ].
  (Q[{}]  (∀b:bag(B). SqStable(Q[b]))  (∀X:{X:hdataflow(A;B)| hdf-invariant(A;b.Q[b];X)} . ∀a:A.  Q[snd(X(a))]))

Definition: mk-hdf
mk-hdf(s,m.G[s; m];st.H[st];s0) ==
  fix((λmk-hdf,s0. if H[s0] then hdf-halt() else hdf-run(λm.let s1,b G[s0; m] in <mk-hdf s1, b>fi )) s0

Lemma: mk-hdf_wf
[A,B,S:Type]. ∀[s0:S]. ∀[H:S ─→ 𝔹]. ∀[G:S ─→ A ─→ (S × bag(B))].  (mk-hdf(s,m.G[s;m];s.H[s];s0) ∈ hdataflow(A;B))

Definition: hdf-base
hdf-base(m.F[m]) ==  mk-hdf(s,m.<s, F[m]>;s.ff;⋅)

Lemma: hdf-base_wf
[A,B:Type]. ∀[F:A ─→ bag(B)].  (hdf-base(m.F[m]) ∈ hdataflow(A;B))

Lemma: hdf-base-ap
[A,B:Type]. ∀[F:A ─→ bag(B)]. ∀[a:A].  (hdf-base(m.F[m])(a) = <hdf-base(m.F[m]), F[a]> ∈ (hdataflow(A;B) × bag(B)))

Lemma: hdf-base-ap-fst
[A,B:Type]. ∀[F:A ─→ bag(B)]. ∀[a:A].  ((fst(hdf-base(m.F[m])(a))) hdf-base(m.F[m]) ∈ hdataflow(A;B))

Definition: hdf-return
hdf-return(x) ==  hdf-run(λm.<hdf-halt(), x>)

Lemma: hdf-return_wf
[A,B:Type]. ∀[x:bag(B)].  (hdf-return(x) ∈ hdataflow(A;B))

Definition: hdf-at-locs
hdf-at-locs(pr;i;locs) ==  if bag-deq-member(IdDeq;i;locs) then pr else hdf-halt() fi 

Lemma: hdf-at-locs_wf
[A,B:Type]. ∀[pr:Id ─→ hdataflow(A;B)]. ∀[i:Id]. ∀[locs:bag(Id)].  (hdf-at-locs(pr;i;locs) ∈ hdataflow(A;B))

Definition: hdf-compose0
hdf-compose0(f;X) ==  mk-hdf(X,a.let X',bs X(a) in let out ←─ ∪b∈bs.f in <X', out>;X.hdf-halted(X);X)

Lemma: hdf-compose0_wf
[A,B,C:Type]. ∀[f:B ─→ bag(C)]. ∀[X:hdataflow(A;B)].  hdf-compose0(f;X) ∈ hdataflow(A;C) supposing valueall-type(C)

Definition: hdf-compose1
==  mk-hdf(X,a.let X',bs X(a) in let out ←─ bag-map(f;bs) in <X', out>;X.hdf-halted(X);X)

Lemma: hdf-compose1_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[f:B ─→ C].  X ∈ hdataflow(A;C) supposing valueall-type(C)

Lemma: hdf-compose1-ap
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[f:B ─→ C]. ∀[a:A].
  X(a) ~ <(fst(X(a))), bag-map(f;snd(X(a)))> supposing valueall-type(C)

Definition: hdf-compose2
==
  mk-hdf(XY,a.let X,Y XY 
              in let X',fs X(a) 
                 in let Y',bs Y(a) 
                    in let out ←─ ∪f∈fs.∪b∈bs.f b
                       in <<X', Y'>out>;XY.let X,Y XY 
                                          in hdf-halted(X) ∨bhdf-halted(Y);<X, Y>)

Lemma: hdf-compose2_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B ─→ bag(C))]. ∀[Y:hdataflow(A;B)].  Y ∈ hdataflow(A;C) supposing valueall-type(C)

Lemma: hdf-compose2-ap
[A,B,C:Type]. ∀[X:hdataflow(A;B ─→ bag(C))]. ∀[Y:hdataflow(A;B)].
  ∀[a:A]. (X Y(a) = <(fst(X(a))) (fst(Y(a))), ∪f∈snd(X(a)).∪b∈snd(Y(a)).f b> ∈ (hdataflow(A;C) × bag(C))) 
  supposing valueall-type(C)

Definition: hdf-compose2'
o' ==
  mk-hdf(XY,a.let X,Y XY 
              in let X',fs X(a) 
                 in let Y',bs Y(a) 
                    in let out ←─ ∪f∈fs.∪b∈bs.f b
                       in <<X', Y'>out>;XY.let X,Y XY 
                                          in hdf-halted(Y) ∨bhdf-halted(X);<X, Y>)

Definition: hdf-compose3
==
  mk-hdf(XY,a.let X,Y XY 
              in let X',fs X(a) 
                 in let Y',bs Y(a) 
                    in let out ←─ ∪f∈fs.bag-map(f;bs)
                       in <<X', Y'>out>;XY.let X,Y XY 
                                          in hdf-halted(X) ∨bhdf-halted(Y);<X, Y>)

Lemma: hdf-compose3_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B ─→ C)]. ∀[Y:hdataflow(A;B)].  Y ∈ hdataflow(A;C) supposing valueall-type(C)

Definition: hdf-compose0-bag
hdf-compose0-bag(f;X) ==  mk-hdf(X,a.let X',bs X(a) in let out ←─ bs in <X', out>;X.hdf-halted(X);X)

Lemma: hdf-compose0-bag_wf
[A,B,C:Type]. ∀[f:bag(B) ─→ bag(C)]. ∀[X:hdataflow(A;B)].
  hdf-compose0-bag(f;X) ∈ hdataflow(A;C) supposing valueall-type(C)

Lemma: hdf-halted-compose2
[A,B,C:Type]. ∀[X1:hdataflow(A;B ─→ bag(C))]. ∀[X2:hdataflow(A;B)].
  uiff(↑hdf-halted(X1 X2);↑(hdf-halted(X1) ∨bhdf-halted(X2))) supposing valueall-type(C)

Lemma: hdf-halted-compose2-iterate
[A,B,C:Type]. ∀[inputs:A List]. ∀[X1:hdataflow(A;B ─→ bag(C))]. ∀[X2:hdataflow(A;B)].
  hdf-halted(X1 X2*(inputs)) hdf-halted(X1*(inputs)) ∨bhdf-halted(X2*(inputs)) supposing valueall-type(C)

Lemma: hdf-halt-compose2
[X:Top]. (hdf-halt() hdf-halt())

Definition: simple-hdf-buffer
simple-hdf-buffer(X;bs) ==
  mk-hdf(Xbs,a.let X,bs Xbs 
               in let X',fs X(a) 
                  in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                     in <<X', if bag-null(bs') then bs else bs' fi >bs'>;s.ff;<X, bs>)

Lemma: simple-hdf-buffer_wf
[A,B:Type]. ∀[X:hdataflow(A;B ─→ bag(B))]. ∀[bs:bag(B)].
  simple-hdf-buffer(X;bs) ∈ hdataflow(A;B) supposing valueall-type(B)

Definition: hdf-buffer
hdf-buffer(X;bs) ==
  mk-hdf(Xbs,a.let X,bs Xbs 
               in let X',fs X(a) 
                  in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                     in <<X', if bag-null(bs') then bs else bs' fi >bs'>;s.let X,bs 
                                                                          in hdf-halted(X);<X, bs>)

Lemma: hdf-buffer_wf
[A,B:Type]. ∀[X:hdataflow(A;B ─→ bag(B))]. ∀[bs:bag(B)].  hdf-buffer(X;bs) ∈ hdataflow(A;B) supposing valueall-type(B)

Definition: simple-hdf-buffer2
simple-hdf-buffer2(X;bs) ==
  mk-hdf(Xbs,a.let X,bs Xbs 
               in let X',fs X(a) 
                  in let bs' ←─ ∪f∈fs.bag-map(f;bs)
                     in <<X', if bag-null(bs') then bs else bs' fi >bs'>;s.ff;<X, bs>)

Lemma: simple-hdf-buffer2_wf
[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[bs:bag(B)].
  simple-hdf-buffer2(X;bs) ∈ hdataflow(A;B) supposing valueall-type(B)

Definition: hdf-buffer2
hdf-buffer2(X;bs) ==
  mk-hdf(Xbs,a.let X,bs Xbs 
               in let X',fs X(a) 
                  in let bs' ←─ ∪f∈fs.bag-map(f;bs)
                     in <<X', if bag-null(bs') then bs else bs' fi >bs'>;s.let X,bs 
                                                                          in hdf-halted(X);<X, bs>)

Lemma: hdf-buffer2_wf
[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[bs:bag(B)].  hdf-buffer2(X;bs) ∈ hdataflow(A;B) supposing valueall-type(B)

Definition: hdf-state
hdf-state(X;bs) ==
  mk-hdf(Xbs,a.let X,s Xbs 
               in let X',fs X(a) 
                  in let b ←─ ∪f∈fs.bag-map(f;s)
                     in let s' ←─ if bag-null(b) then else fi 
                        in <<X', s'>s'>;s.ff;<X, bs>)

Lemma: hdf-state_wf
[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[bs:bag(B)].  hdf-state(X;bs) ∈ hdataflow(A;B) supposing valueall-type(B)

Definition: hdf-single-val-step
hdf-single-val-step(P;X;A;B) ==  case of inl(p) => ∀a:A. let X',b in single-valued-bag(b;B) ∧ inr(z) => True

Lemma: hdf-single-val-step_wf
[A,B:Type]. ∀[X:hdataflow(A;B)]. ∀[P:ℙ].  (hdf-single-val-step(P;X;A;B) ∈ ℙ)

Definition: hdf-single-valued
hdf-single-valued(X;A;B) ==
  ∀L:A List. case X*(L) of inl(P) => ∀a:A. let X',b in single-valued-bag(b;B) inr(z) => True

Lemma: hdf-single-valued_wf
[A,B:Type]. ∀[X:hdataflow(A;B)].  (hdf-single-valued(X;A;B) ∈ ℙ)

Definition: hdf-state-single-val
hdf-state-single-val(X;b) ==
  mk-hdf(Xb,a.let X,b Xb 
              in let X',fs X(a) 
                 in let b' ←─ if bag-null(fs) then else sv-bag-only(fs) fi 
                    in <<X', b'>{b'}>;s.ff;<X, b>)

Lemma: hdf-state-single-val_wf
[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[b:B].
  (hdf-state-single-val(X;b) ∈ hdataflow(A;B)) supposing (hdf-single-valued(X;A;B ─→ B) and valueall-type(B))

Definition: hdf-state1-single-val
hdf-state1-single-val(f;X;b) ==
  mk-hdf(Xb,a.let X,b Xb 
              in let X',xs X(a) 
                 in let b' ←─ if bag-null(xs) then else sv-bag-only(xs) fi 
                    in <<X', b'>{b'}>;s.ff;<X, b>)

Lemma: hdf-state1-single-val_wf
[A,B,C:Type]. ∀[f:B ─→ C ─→ C]. ∀[X:hdataflow(A;B)]. ∀[b:C].
  (hdf-state1-single-val(f;X;b) ∈ hdataflow(A;C)) supposing (hdf-single-valued(X;A;B) and valueall-type(C))

Definition: hdf-memory
hdf-memory(X;bs) ==
  mk-hdf(Xbs,a.let X,s Xbs 
               in let X',fs X(a) 
                  in let b ←─ ∪f∈fs.bag-map(f;s)
                     in let s' ←─ if bag-null(b) then else fi 
                        in <<X', s'>s>;s.ff;<X, bs>)

Lemma: hdf-memory_wf
[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[bs:bag(B)].  hdf-memory(X;bs) ∈ hdataflow(A;B) supposing valueall-type(B)

Definition: hdf-comb2
hdf-comb2(f;X;Y) ==  (f X) Y

Lemma: hdf-comb2_wf
[A,B,C,D:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[f:B ─→ C ─→ bag(D)].
  hdf-comb2(f;X;Y) ∈ hdataflow(A;D) supposing (↓C) ∧ valueall-type(D)

Definition: hdf-comb3
hdf-comb3(f;X;Y;Z) ==  Z

Lemma: hdf-comb3_wf
[A,C,B1,B2,B3:Type]. ∀[f:B1 ─→ B2 ─→ B3 ─→ bag(C)]. ∀[X:hdataflow(A;B1)]. ∀[Y:hdataflow(A;B2)]. ∀[Z:hdataflow(A;B3)].
  hdf-comb3(f;X;Y;Z) ∈ hdataflow(A;C) supposing ((↓B2) ∧ (↓B3)) ∧ valueall-type(C)

Definition: hdf-once
hdf-once(X) ==  mk-hdf(X,a.let X',b X(a) in <if bag-null(b) then X' else hdf-halt() fi b>;X.hdf-halted(X);X)

Lemma: hdf-once_wf
[A,B:Type]. ∀[X:hdataflow(A;B)].  (hdf-once(X) ∈ hdataflow(A;B))

Definition: hdf-until
hdf-until(X;Y) ==
  mk-hdf(p,a.let X,Y 
             in let X',b X(a) 
                in let Y',c Y(a) 
                   in <<if bag-null(c) then X' else hdf-halt() fi Y'>b>;p.hdf-halted(fst(p));<X, Y>)

Lemma: hdf-until_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)].  (hdf-until(X;Y) ∈ hdataflow(A;B))

Lemma: hdf-until-ap
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].
  (hdf-until(X;Y)(a)
  = <if bag-null(snd(Y(a))) then hdf-until(fst(X(a));fst(Y(a))) else hdf-halt() fi snd(X(a))>
  ∈ (hdataflow(A;B) × bag(B)))

Lemma: hdf-until-ap-fst
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].
  ((fst(hdf-until(X;Y)(a)))
  if bag-null(snd(Y(a))) then hdf-until(fst(X(a));fst(Y(a))) else hdf-halt() fi 
  ∈ hdataflow(A;B))

Lemma: hdf-until-ap-snd
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].  ((snd(hdf-until(X;Y)(a))) (snd(X(a))) ∈ bag(B))

Lemma: hdf-until-halt-left
[Y:Top]. (hdf-until(hdf-halt();Y) hdf-halt())

Lemma: hdf-until-halt-right
[A,B:Type]. ∀[X:hdataflow(A;B)].  (hdf-until(X;hdf-halt()) X ∈ hdataflow(A;B))

Definition: hdf-prior
hdf-prior(X;b) ==  hdf-buffer((λx,y. {x}) X;b)

Lemma: hdf-prior_wf
[A,B:Type]. ∀[X:hdataflow(A;B)]. ∀[b:bag(B)].  hdf-prior(X;b) ∈ hdataflow(A;B) supposing (↓B) ∧ valueall-type(B)

Definition: hdf-parallel
|| ==
  mk-hdf(XY,a.let X,Y XY 
              in let X',xs X(a) 
                 in let Y',ys Y(a) 
                    in let out ←─ xs ys
                       in <<X', Y'>out>;XY.let X,Y XY 
                                          in hdf-halted(X) ∧b hdf-halted(Y);<X, Y>)

Lemma: hdf-parallel_wf
[A,B:Type]. ∀[X,Y:hdataflow(A;B)].  || Y ∈ hdataflow(A;B) supposing valueall-type(B)

Lemma: hdf-parallel-halt-left
[A,B:Type]. ∀[X:hdataflow(A;B)].  hdf-halt() || X ∈ hdataflow(A;B) supposing valueall-type(B)

Lemma: hdf-parallel-halt-right
[A,B:Type]. ∀[X:hdataflow(A;B)].  || hdf-halt() X ∈ hdataflow(A;B) supposing valueall-type(B)

Lemma: hdf-parallel-halt
hdf-halt() || hdf-halt() hdf-halt()

Lemma: hdf-parallel-ap
[A,B:Type]. ∀[X,Y:hdataflow(A;B)]. ∀[a:A].
  || Y(a) = <fst(X(a)) || fst(Y(a)), (snd(X(a))) (snd(Y(a)))> ∈ (hdataflow(A;B) × bag(B)) supposing valueall-type(B)

Lemma: hdf-parallel-halted
[A,B:Type].
  ∀[inputs:A List]. ∀[X,Y:hdataflow(A;B)].
    hdf-halted(X || Y*(inputs)) hdf-halted(X*(inputs)) ∧b hdf-halted(Y*(inputs)) 
  supposing valueall-type(B)

Definition: hdf-parallel-bag
hdf-parallel-bag(Xs) ==
  mk-hdf(Xs,a.eval bag-map(λX.X(a);Xs) in
              let out ←─ ∪p∈x.snd(p)
              in <bag-map(λp.(fst(p));x), out>;Xs.bag_all(Xs;λx.hdf-halted(x));Xs)

Lemma: hdf-parallel-bag_wf
[A,B:Type]. ∀[Xs:bag(hdataflow(A;B))].  hdf-parallel-bag(Xs) ∈ hdataflow(A;B) supposing valueall-type(B)

Lemma: hdf-parallel-bag-iterate
[A,B:Type]. ∀[Xs:bag(hdataflow(A;B))]. ∀[inputs:A List].
  hdf-parallel-bag(Xs)*(inputs) hdf-parallel-bag(bag-map(λx.x*(inputs);Xs)) ∈ hdataflow(A;B) 
  supposing valueall-type(B)

Definition: hdf-union
==
  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 );ys)
                       in <<X', Y'>out>;XY.let X,Y XY 
                                          in hdf-halted(X) ∧b hdf-halted(Y);<X, Y>)

Lemma: hdf-union_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)].
  (X Y ∈ hdataflow(A;B C)) supposing (valueall-type(B) and valueall-type(C))

Lemma: hdf-union-halt
hdf-halt() hdf-halt() hdf-halt()

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 );snd(Y(a)))>
     ∈ (hdataflow(A;B C) × bag(B C))) supposing 
     (valueall-type(B) and 
     valueall-type(C))

Lemma: hdf-union-eq-disju
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)].
  (X x.(inl x)) || x.(inr )) Y ∈ hdataflow(A;B C)) supposing 
     (valueall-type(B) and 
     valueall-type(C))

Definition: hdf-sequence
hdf-sequence(X;Y;Z) ==
  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 Z(a) in <inr Z' bz> else <inl <X', Y'>bx> fi 
   inr(Z) =>
   let Z',b Z(a) 
   in <inr Z' b>;S.case of inl(XY) => ff inr(Z) => hdf-halted(Z);inl <X, Y>)

Lemma: hdf-sequence_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[Z:hdataflow(A;B)].
  hdf-sequence(X;Y;Z) ∈ hdataflow(A;B) supposing valueall-type(B)

Definition: bind-nxt
bind-nxt(Y;p;a) ==
  let X,ys 
  in let X',b X(a) 
     in let ybs ←─ bag-map(λP.P(a);ys bag-map(Y;b))
        in let ys' ←─ [y∈bag-map(λyb.(fst(yb));ybs)|¬bhdf-halted(y)]
           in let out ←─ ∪yb∈ybs.snd(yb)
              in <<X', ys'>out>

Lemma: bind-nxt_wf
[A,B,C:Type]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[p:hdataflow(A;B) × bag(hdataflow(A;C))]. ∀[a:A].
  bind-nxt(Y;p;a) ∈ hdataflow(A;B) × bag(hdataflow(A;C)) × bag(C) supposing valueall-type(C)

Definition: simple-bind-nxt
simple-bind-nxt(Y; p; a) ==
  let X,ys 
  in let X',b X(a) 
     in let ybs ←─ bag-map(λP.P(a);ys bag-map(Y;b))
        in let ys' ←─ bag-map(λyb.(fst(yb));ybs)
           in let out ←─ ∪yb∈ybs.snd(yb)
              in <<X', ys'>out>

Lemma: simple-bind-nxt_wf
[A,B,C:Type]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[p:hdataflow(A;B) × bag(hdataflow(A;C))]. ∀[a:A].
  simple-bind-nxt(Y; p; a) ∈ hdataflow(A;B) × bag(hdataflow(A;C)) × bag(C) supposing valueall-type(C)

Definition: hdf-bind
X >>==  mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys in hdf-halted(X) ∧b bag-null(ys);<X, {}>)

Lemma: hdf-bind_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)].  X >>Y ∈ hdataflow(A;C) supposing valueall-type(C)

Definition: hdf-bind-gen
(hdfs) >>==  mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys in hdf-halted(X) ∧b bag-null(ys);<X, hdfs>)

Lemma: hdf-bind-gen_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))].
  (hdfs) >>Y ∈ hdataflow(A;C) supposing valueall-type(C)

Lemma: hdf-bind-gen-halted
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))].
  hdf-halted(X (hdfs) >>Y) hdf-halted(X) ∧b bag-null(hdfs) supposing valueall-type(C)

Lemma: hdf-bind-gen-halt-left
[Y:Top]. (hdf-halt() ({}) >>hdf-halt())

Lemma: hdf-bind-as-gen
[X,Y:Top].  (X >>({}) >>Y)

Lemma: hdf-bind-gen-ap
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))]. ∀[a:A].
  (hdfs) >>Y(a) ~ <fst(X(a)) ([y∈bag-map(λP.(fst(P(a)));hdfs bag-map(Y;snd(X(a))))|¬bhdf-halted(y)]) >>Y
                      , ∪p∈bag-map(λP.P(a);hdfs bag-map(Y;snd(X(a)))).snd(p)
                      > 
  supposing valueall-type(C)

Lemma: hdf-bind-gen-ap-eq
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))]. ∀[a:A].
  (hdfs) >>Y(a)
  = <fst(X(a)) ([y∈bag-map(λP.(fst(P(a)));hdfs bag-map(Y;snd(X(a))))|¬bhdf-halted(y)]) >>Y
    , ∪p∈bag-map(λP.P(a);hdfs bag-map(Y;snd(X(a)))).snd(p)
    >
  ∈ (hdataflow(A;C) × bag(C)) 
  supposing valueall-type(C)

Lemma: hdf-bind-ap
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[a:A].
  X >>Y(a)
  = <fst(X(a)) ([y∈bag-map(λx.(fst(Y x(a)));snd(X(a)))|¬bhdf-halted(y)]) >>Y, ∪p∈bag-map(λx.Y x(a);snd(X(a))).snd(p)>
  ∈ (hdataflow(A;C) × bag(C)) 
  supposing valueall-type(C)

Lemma: hdf-bind-gen-left-halt
[A,B,C:Type]. ∀[Y:B ─→ hdataflow(A;C)]. ∀[hdfs:bag(hdataflow(A;C))].
  hdf-halt() (hdfs) >>hdf-halt() (hdfs) >>= λx.hdf-return({x}) ∈ hdataflow(A;C) supposing valueall-type(C)

Lemma: hdf-bind-gen-compose1-left
[A,B,C,U:Type]. ∀[f:B ─→ C]. ∀[X:hdataflow(A;B)]. ∀[Y:C ─→ hdataflow(A;U)]. ∀[hdfs:bag(hdataflow(A;U))].
  (f (hdfs) >>(hdfs) >>f ∈ hdataflow(A;U)) supposing (valueall-type(C) and valueall-type(U))

Lemma: hdf-bind-compose1-left
[A,B,C,U:Type]. ∀[f:B ─→ C]. ∀[X:hdataflow(A;B)]. ∀[Y:C ─→ hdataflow(A;U)].
  (f X >>X >>f ∈ hdataflow(A;U)) supposing (valueall-type(C) and valueall-type(U))

Definition: simple-hdf-bind
simple-hdf-bind(X;Y) ==  mk-hdf(p,a.simple-bind-nxt(Y; p; a);p.let X,ys in ff;<X, {}>)

Lemma: simple-hdf-bind_wf
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)].
  simple-hdf-bind(X;Y) ∈ hdataflow(A;C) supposing valueall-type(C)

Lemma: iterate-hdf-bind-simple
[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)].
  ∀[L:A List]. ∀[a:A].  ((snd(X >>Y*(L)(a))) (snd(simple-hdf-bind(X;Y)*(L)(a))) ∈ bag(C)) supposing valueall-type(C)

Lemma: iterate-hdf-buffer-simple
[A,B:Type]. ∀[X:hdataflow(A;B ─→ bag(B))]. ∀[bs:bag(B)].
  ∀[L:A List]. ∀[a:A].  ((snd(hdf-buffer(X;bs)*(L)(a))) (snd(simple-hdf-buffer(X;bs)*(L)(a))) ∈ bag(B)) 
  supposing valueall-type(B)

Lemma: iterate-hdf-buffer2-simple
[A,B:Type]. ∀[X:hdataflow(A;B ─→ B)]. ∀[bs:bag(B)].
  ∀[L:A List]. ∀[a:A].  ((snd(hdf-buffer2(X;bs)*(L)(a))) (snd(simple-hdf-buffer2(X;bs)*(L)(a))) ∈ bag(B)) 
  supposing valueall-type(B)

Definition: rec-bind-nxt
rec-bind-nxt(X;Y;p;a) ==
  let sx,sy 
  in let Ys ←─ bag-map(λp.p(a);sy)
     in let sy' bag-mapfilter(λx.(fst(x));λx.isl(fst(x));Ys) in
         let Youts = ∪x∈Ys.snd(x) in
         let newXs bag-map(X;Youts) in
         let Xs ←─ bag-map(λp.p(a);sx newXs)
         in let sx' bag-mapfilter(λx.(fst(x));λx.isl(fst(x));Xs) in
             let Xouts = ∪x∈Xs.snd(x) in
             let Ys' ←─ bag-map(λx.(fst(Y x(a)));Youts)
             in let sy'' [p∈Ys'|isl(p)] in
                    <<sx', sy' sy''>Xouts>

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))

Definition: hdf-rec-bind
hdf-rec-bind(X;Y) ==  λv.mk-hdf(p,a.rec-bind-nxt(X;Y;p;a);p.let xs,ys in bag-null(xs) ∧b bag-null(ys);<{X v}, {Y v}>\000C)

Lemma: hdf-rec-bind_wf
[A,B,C:Type]. ∀[X:C ─→ hdataflow(A;B)]. ∀[Y:C ─→ hdataflow(A;C)].
  (hdf-rec-bind(X;Y) ∈ C ─→ hdataflow(A;B)) supposing (valueall-type(B) and valueall-type(C))

Definition: hdf-cbva-simple
hdf-cbva-simple(L;m) ==  fix((λmk-hdf.(inl a.simple-cbva-seq(L[a];λout.<mk-hdf, out>;m)))))

Lemma: hdf-cbva-simple_wf
[U,T:Type]. ∀[m:ℕ+]. ∀[A:ℕm ─→ ValueAllType]. ∀[L:U ─→ i:ℕm ─→ funtype(i;λk.bag(A k);bag(A i))].
  (hdf-cbva-simple(L;m) ∈ hdataflow(U;A (m 1)))

Lemma: vr_test_55
(∀p:ℙ((¬¬p)  p))  (∀p:ℙ(p ∨ p)))

Lemma: hdf-sqequal1
[F:Top]. (hdf-base(m.F[m]) fix((λmk-hdf.(inl m.<mk-hdf, F[m]>)))))

Lemma: hdf-sqequal2
[F,G,H:Top].
  (fix((λmk-hdf,s0. case s0 of inl(y) => inl a.let X',bs in let out ←─ G[bs] in <mk-hdf X', out>inr(z) => H[\000Cz])) 
   fix((λmk-hdf.(inl m.<mk-hdf, F[m]>)))) fix((λmk-hdf.(inl a.let out ←─ G[F[a]]
                                                                    in <mk-hdf, out>)))))

Lemma: hdf-sqequal2-cbva
[F,G,H:Top].
  (fix((λmk-hdf,s0. case s0 of inl(y) => inl a.let X',bs in let out ←─ G[bs] in <mk-hdf X', out>inr(z) => H[\000Cz])) 
   fix((λmk-hdf.(inl m.let out ←─ F[m]
                         in <mk-hdf, out>)))) fix((λmk-hdf.(inl a.let out1 ←─ F[a]
                                                                   in let out2 ←─ G[out1]
                                                                      in <mk-hdf, out2>)))))

Lemma: hdf-sqequal8
[mk-hdf,a,s,X:Top].
  (let b ←─ a
   in case null(b) of inl(x1) => let s' ←─ in <mk-hdf <X, s'>s'> inr(y1) => <mk-hdf <X, b>b> let b ←─ a
                                                                          in let s' ←─ case null(b)
                                                                              of inl(x1) =>
                                                                              s
                                                                              inr(y1) =>
                                                                              b
                                                                             in <mk-hdf <X, s'>s'>)

Lemma: hdf-sqequal8-2
[mk-hdf,a,s,X:Top].
  (let b ←─ a
   in case null(b) of inl(x1) => let s' ←─ in <mk-hdf <X, s'>s'> inr(y1) => <mk-hdf <X, b>b> let b ←─ a
                                                                          in let s' ←─ if null(b) then else fi 
                                                                             in <mk-hdf <X, s'>s'>)

Lemma: hdf-sqequal8-3
[mk-hdf,a,s,X,x:Top].
  (let b ←─ a
   in case null(b) of inl(x1) => let s' ←─ in <mk-hdf <X, s'>x> inr(y1) => <mk-hdf <X, b>x> let b ←─ a
                                                                         in let s' ←─ if null(b) then else fi 
                                                                            in <mk-hdf <X, s'>x>)

Lemma: hdf-sqequal8-4
[C,a,b,F:Top].
  (case of inl(x1) => let x ←─ in F[x] inr(y1) => let x ←─ in F[x] let x ←─ case C
                                                                              of inl(x1) =>
                                                                              a
                                                                              inr(y1) =>
                                                                              b
                                                                             in F[x])

Lemma: hdf-base-transformation1
[F:Top]. (hdf-base(m.F[m]) fix((λmk-hdf.(inl a.cbva_seq(λx.⊥; λg.<mk-hdf, F[a]>0))))))

Lemma: hdf-base-transformation2
[F:Top]. (hdf-base(m.F[m]) fix((λmk-hdf,s. (inl a.cbva_seq(λx.⊥; λg.<mk-hdf Ax, F[a]>0))))) Ax)

Lemma: hdf-base-transformation1-base
[F:Base]. (hdf-base(m.F[m]) fix((λmk-hdf.(inl a.cbva_seq(λx.⊥; λg.<mk-hdf, F[a]>0))))))

Lemma: hdf-return-transformation1
[x:Top]. (hdf-return(x) fix((λmk-hdf.(inl a.cbva_seq(λx.⊥; λg.<inr ⋅ x>0))))))

Lemma: hdf-return-transformation2
[x:Top]. (hdf-return(x) inl m.<inr Ax x>))

Lemma: hdf-compose1-transformation0
[f,F:Top].
  (f fix((λmk-hdf.(inl a.<mk-hdf, F[a]>)))) 
  fix((λmk-hdf.(inl a.simple-cbva-seq(λn.bag-map(f;F[a]);λout.<mk-hdf, out>;1))))))

Lemma: hdf-compose1-transformation0-2
[f,F:Top].
  (f fix((λmk-hdf.(inl a.<mk-hdf, F[a]>)))) fix((λmk-hdf.(inl a.cbva_seq(λn.bag-map(f;F[a]); λg.<mk-hdf
                                                                                                        x.x)
                                                                                                        >1))))))

Lemma: hdf-compose1-transformation1
[f,L:Base]. ∀[m:ℕ+].
  (f fix((λmk-hdf.(inl a.simple-cbva-seq(L[a];λout.<mk-hdf, out>;m))))) 
  fix((λmk-hdf.(inl a.simple-cbva-seq(λn.if (n =z m)
                                             then mk_lambdas(λout.bag-map(f;out);m 1)
                                             else L[a] n
                                             fi out.<mk-hdf, out>;m 1))))))

Lemma: hdf-compose1-transformation1-2
[f,L,G:Base]. ∀[m:ℕ].
  (f fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[a;g]>m))))) 
  fix((λmk-hdf.(inl a.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.bag-map(f;G[a;g]);m) else L[a] fi ;
                                   λg.<mk-hdf, select_fun_ap(g;m 1;m)>1))))))

Lemma: hdf-compose1-transformation2
[f,L,G:Top]. ∀[m:ℕ].
  (f fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[a;g]>m))))) 
  fix((λmk-hdf.(inl a.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.bag-map(f;G[a;g]);m) else L[a] fi ;
                                   λg.<mk-hdf, select_fun_ap(g;m 1;m)>1))))))

Lemma: hdf-compose1-transformation3
[f,L,S,G,init:Top]. ∀[m:ℕ].
  (f (fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]>m))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.bag-map(f;G[s;a;g]);m) else L[s;a] fi ;
                                      λg.<mk-hdf S[s;a;partial_ap(g;m 1;m)], select_fun_ap(g;m 1;m)>1))))) 
    init)

Lemma: hdf-compose0-transformation2
[f,L,G:Top]. ∀[m:ℕ].
  (hdf-compose0(f;fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[a;g]>m)))))) 
  fix((λmk-hdf.(inl a.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.∪b∈G[a;g].f b;m) else L[a] fi ;
                                   λg.<mk-hdf, select_fun_ap(g;m 1;m)>1))))))

Lemma: hdf-compose0-transformation1
[f,L,S,G,s:Top]. ∀[m:ℕ].
  (hdf-compose0(f;fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]>m))))) s) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.∪b∈G[s;a;g].f b;m) else L[s;a] fi ;
                                      λg.<mk-hdf S[s;a;partial_ap(g;m 1;m)], select_fun_last(g;m)>1))))) 
    s)

Lemma: hdf-buffer-transformation2
[init,L,G:Top]. ∀[m:ℕ].
  (hdf-buffer(fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[g]>m)))));init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.∪f∈G[g].∪b∈s.f b;m) else L[a] fi ;
                                      λg.<mk-hdf if bag-null(select_fun_last(g;m)) then else select_fun_last(g;m) fi 
                                         select_fun_last(g;m)
                                         >1))))) 
    init)

Lemma: hdf-buffer-transformation3
[init,s,L,S,G:Top]. ∀[m:ℕ].
  (hdf-buffer(fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]>m))))) s;init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z m)
                                         then mk_lambdas_fun(λg.∪f∈G[fst(s);a;g].∪b∈snd(s).f b;m)
                                         else L[fst(s);a] n
                                         fi ; λg.<mk-hdf 
                                                  <S[fst(s);a;partial_ap(g;m 1;m)]
                                                  if bag-null(select_fun_last(g;m))
                                                    then snd(s)
                                                    else select_fun_last(g;m)
                                                    fi 
                                                  >
                                                 select_fun_last(g;m)
                                                 >1))))) 
    <s, init>)

Lemma: hdf-state-transformation2
[init,L,G:Top]. ∀[m:ℕ].
  (hdf-state(fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[g]>m)))));init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z 1)
                                           then mk_lambdas_fun(λg.if bag-null(select_fun_last(g;m))
                                                                  then s
                                                                  else select_fun_last(g;m)
                                                                  fi ;m 1)
                                         if (n =z m) then mk_lambdas_fun(λg.∪f∈G[g].bag-map(f;s);m)
                                         else L[a] n
                                         fi ; λg.<mk-hdf select_fun_last(g;m 1), select_fun_last(g;m 1)>2)))))\000C 
    init)

Lemma: hdf-memory-transformation2
[init,L,G:Top]. ∀[m:ℕ].
  (hdf-memory(fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[g]>m)))));init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z 1)
                                           then mk_lambdas_fun(λg.if bag-null(select_fun_last(g;m))
                                                                  then s
                                                                  else select_fun_last(g;m)
                                                                  fi ;m 1)
                                         if (n =z m) then mk_lambdas_fun(λg.∪f∈G[g].bag-map(f;s);m)
                                         else L[a] n
                                         fi ; λg.<mk-hdf select_fun_last(g;m 1), s>2))))) 
    init)

Lemma: hdf-parallel-transformation1
[L1,L2:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.simple-cbva-seq(L1[a];λout.<mk-hdf, out>;m1)))))
   || fix((λmk-hdf.(inl a.simple-cbva-seq(L2[a];λout.<mk-hdf, out>;m2))))) 
  fix((λmk-hdf.(inl a.simple-cbva-seq(λn.if n <m1 then L1[a] n
                                             if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                             else mk_lambdas(λout1.mk_lambdas(λout2.(out1 out2);m2 1);m1 1)
                                             fi out.<mk-hdf, out>;(m1 m2) 1))))))

Lemma: hdf-parallel-transformation1-2-0
[L1,L2,G1,G2:Base]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1))))) || fix((λmk-hdf.(inl a.cbva_seq(L2[a]; λg.<mk-hdf
                                                                                                                 G2[g]
                                                                                                                 >;
                                                                                                       m2))))) 
  fix((λmk-hdf.(inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                      if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                      else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] G2[g2]);m2);m1)
                                      fi ; λg.<mk-hdf, select_fun_last(g;m1 m2)>(m1 m2) 1))))))

Lemma: hdf-parallel-transformation1-2-1
[L1,L2,G1,G2,S1,S2,init1,init2:Base]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf,s. (inl a.cbva_seq(L1[s;a]; λg.<mk-hdf S1[g;s], G1[g]>m1))))) init1
   || fix((λmk-hdf,s. (inl a.cbva_seq(L2[s;a]; λg.<mk-hdf S2[g;s], G2[g]>m2))))) init2 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[fst(s);a] n
                                         if n <m1 m2 then mk_lambdas(L2[snd(s);a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] G2[g2]);m2);m1)
                                         fi ; λg.<mk-hdf 
                                                  <S1[partial_ap_gen(g;(m1 m2) 1;0;m1);fst(s)]
                                                  S2[partial_ap_gen(g;(m1 m2) 1;m1;m2);snd(s)]
                                                  >
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    <init1, init2>)

Lemma: hdf-parallel-transformation2
[L,G,H,S,init,out:Base]. ∀[m:ℕ].
  (inl a.<inr Ax out>|| fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<case H[g;s]
                                                                             of inl() =>
                                                                             mk-hdf S[g;s]
                                                                             inr() =>
                                                                             inr Ax 
                                                                           G[g]
                                                                           >m))))) 
                              init fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z m)
                                                                          then case fst(s)
                                                                                of inl(x) =>
                                                                                mk_lambdas_fun(λg.(out G[g]);m)
                                                                                inr(x) =>
                                                                                mk_lambdas_fun(λg.G[g];m)
                                                                          else L[snd(s);a] n
                                                                          fi ; λg.<case H[partial_ap(g;m 1;m);snd(s)]
                                                                                    of inl() =>
                                                                                    mk-hdf 
                                                                                    <inr Ax 
                                                                                    S[partial_ap(g;m 1;m);snd(s)]
                                                                                    >
                                                                                    inr() =>
                                                                                    inr Ax 
                                                                                  select_fun_last(g;m)
                                                                                  >1))))) 
                                     <inl Ax, init>)

Lemma: hdf-parallel-transformation2-0
[L1,L2,G1,G2:Top]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[a;g]>m1)))))
   || fix((λmk-hdf.(inl a.cbva_seq(L2[a]; λg.<mk-hdf, G2[a;g]>m2))))) 
  fix((λmk-hdf.(inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                      if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                      else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[a;g1] G2[a;g2]);m2);m1)
                                      fi ; λg.<mk-hdf, select_fun_last(g;m1 m2)>(m1 m2) 1))))))

Lemma: hdf-parallel-transformation2-1
[L1,L2,G1,G2:Top]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1))))) || fix((λmk-hdf.(inl a.cbva_seq(L2[a]; λg.<mk-hdf
                                                                                                                 G2[g]
                                                                                                                 >;
                                                                                                       m2))))) 
  fix((λmk-hdf.(inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                      if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                      else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] G2[g2]);m2);m1)
                                      fi ; λg.<mk-hdf, select_fun_last(g;m1 m2)>(m1 m2) 1))))))

Lemma: hdf-parallel-transformation2-2
[L1,L2,G1,G2,S1,S2,init1,init2:Top]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf,s. (inl a.cbva_seq(L1[s;a]; λg.<mk-hdf S1[g;s], G1[g]>m1))))) init1
   || fix((λmk-hdf,s. (inl a.cbva_seq(L2[s;a]; λg.<mk-hdf S2[g;s], G2[g]>m2))))) init2 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[fst(s);a] n
                                         if n <m1 m2 then mk_lambdas(L2[snd(s);a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] G2[g2]);m2);m1)
                                         fi ; λg.<mk-hdf 
                                                  <S1[partial_ap_gen(g;(m1 m2) 1;0;m1);fst(s)]
                                                  S2[partial_ap_gen(g;(m1 m2) 1;m1;m2);snd(s)]
                                                  >
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    <init1, init2>)

Lemma: hdf-parallel-transformation2-3
[L,G,H,S,init,out:Top]. ∀[m:ℕ].
  (inl a.<inr Ax out>|| fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<case H[g;s]
                                                                             of inl() =>
                                                                             mk-hdf S[g;s]
                                                                             inr() =>
                                                                             inr Ax 
                                                                           G[g]
                                                                           >m))))) 
                              init fix((λmk-hdf,s. (inl a.cbva_seq(λn.if (n =z m)
                                                                          then case fst(s)
                                                                                of inl(x) =>
                                                                                mk_lambdas_fun(λg.(out G[g]);m)
                                                                                inr(x) =>
                                                                                mk_lambdas_fun(λg.G[g];m)
                                                                          else L[snd(s);a] n
                                                                          fi ; λg.<case H[partial_ap(g;m 1;m);snd(s)]
                                                                                    of inl() =>
                                                                                    mk-hdf 
                                                                                    <inr Ax 
                                                                                    S[partial_ap(g;m 1;m);snd(s)]
                                                                                    >
                                                                                    inr() =>
                                                                                    inr Ax 
                                                                                  select_fun_last(g;m)
                                                                                  >1))))) 
                                     <inl Ax, init>)

Lemma: hdf-compose2-transformation1
[L1,L2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.simple-cbva-seq(L1[a];λout.<mk-hdf, out>;m1)))))
   (fix((λmk-hdf,s. (inl a.simple-cbva-seq(L2[a];λout.<mk-hdf S[s], out>;m2))))) init) 
  fix((λmk-hdf,s. (inl a.simple-cbva-seq(λn.if n <m1 then L1[a] n
                                                if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                                else mk_lambdas(λfs.mk_lambdas(λbs.∪f∈fs.∪b∈bs.f b;m2 1);m1 1)
                                                fi out.<mk-hdf S[s], out>;(m1 m2) 1))))) 
    init)

Lemma: hdf-compose2-transformation1-2-0
[L1,L2,G1,G2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1)))))
   (fix((λmk-hdf,s. (inl a.cbva_seq(L2[a]; λg.<mk-hdf S[s], G2[g]>m2))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                         if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.∪f∈G1[g1].∪b∈G2[g2].f b;m2);m1)
                                         fi ; λg.<mk-hdf S[s], select_fun_last(g;m1 m2)>(m1 m2) 1))))) 
    init)

Lemma: hdf-compose2-transformation1-2-1
[L1,L2,G1,G2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1)))))
   (fix((λmk-hdf,s. (inl a.cbva_seq(L2[a]; λg.<mk-hdf S[g;s], G2[g]>m2))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                         if n <m1 m2 then mk_lambdas(L2[a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.∪f∈G1[g1].∪b∈G2[g2].f b;m2);m1)
                                         fi ; λg.<mk-hdf S[partial_ap_gen(g;(m1 m2) 1;m1;m2);s]
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    init)

Lemma: hdf-compose2-transformation1-2-2
[L1,L2,G1,G2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1)))))
   (fix((λmk-hdf,s. (inl a.cbva_seq(L2[s;a]; λg.<mk-hdf S[g;s], G2[g]>m2))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                         if n <m1 m2 then mk_lambdas(L2[s;a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.∪f∈G1[g1].∪b∈G2[g2].f b;m2);m1)
                                         fi ; λg.<mk-hdf S[partial_ap_gen(g;(m1 m2) 1;m1;m2);s]
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    init)

Lemma: hdf-compose2-transformation1-2-3
[L1,L2,G1,G2,init,S:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1)))))
   (fix((λmk-hdf,s. (inl a.cbva_seq(L2[s;a]; λg.<mk-hdf S[g;s], G2[g;s]>m2))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                         if n <m1 m2 then mk_lambdas(L2[s;a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.∪f∈G1[g1].∪b∈G2[g2;s].f b;m2);m1)
                                         fi ; λg.<mk-hdf S[partial_ap_gen(g;(m1 m2) 1;m1;m2);s]
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    init)

Lemma: hdf-compose2-transformation2
[L1,L2,G1,G2,init,S:Top]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf.(inl a.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>m1)))))
   (fix((λmk-hdf,s. (inl a.cbva_seq(L2[s;a]; λg.<mk-hdf S[g;s], G2[g;s]>m2))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if n <m1 then L1[a] n
                                         if n <m1 m2 then mk_lambdas(L2[s;a] (n m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.∪f∈G1[g1].∪b∈G2[g2;s].f b;m2);m1)
                                         fi ; λg.<mk-hdf S[partial_ap_gen(g;(m1 m2) 1;m1;m2);s]
                                                 select_fun_last(g;m1 m2)
                                                 >(m1 m2) 1))))) 
    init)

Lemma: hdf-once-transformation1
[L,G,S,init:Base]. ∀[m:ℕ].
  (hdf-once(fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<mk-hdf S[g;s], G[g]>m))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<case null(G[g]) of inl() => mk-hdf S[g;s] inr() => inr Ax G[g]>;
                                      m))))) 
    init)

Lemma: hdf-once-transformation2
[L,G,S,init:Top]. ∀[m:ℕ].
  (hdf-once(fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<mk-hdf S[g;s], G[g]>m))))) init) 
  fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<case null(G[g]) of inl() => mk-hdf S[g;s] inr() => inr Ax G[g]>;
                                      m))))) 
    init)

Lemma: hdf-once-transformation3
[L,G:Top]. ∀[m:ℕ].
  (hdf-once(fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<mk-hdf, G[a;g]>m)))))) 
  fix((λmk-hdf.(inl a.cbva_seq(L[a]; λg.<case null(G[a;g]) of inl() => mk-hdf inr() => inr Ax G[a;g]>m))))))

Lemma: hdf-state-base
[f,C,F,s:Top].
  (hdf-state((λx,s. f[x;s]) hdf-base(a.if C[a] then [F[a]] else [] fi );[s]) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if C[a] then f[F[a];s] else fi ; λg.<mk-hdf (g x.x)), x.[x])>1))))) s\000C)

Lemma: hdf-state-base2-2
[C1,C2,F1,F2,f1,f2,s:Top]. ∀[hdr1,hdr2:Name].
  hdf-state((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi || x,s. f2[x;s])
             hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi );[s]) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
                                         if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
                                         else s
                                         fi ; λg.<mk-hdf (g x.x)), x.[x])>1))))) 
    
  supposing ¬(hdr1 hdr2 ∈ Name)

Lemma: hdf-state-base3-2
[C1,C2,C3,F1,F2,F3,f1,f2,f3,s:Top]. ∀[hdr1,hdr2,hdr3:Name].
  (hdf-state((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
             || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi || x,s. f3[x;s\000C])
                 hdf-base(a.if name_eq(fst(a);hdr3) ∧b C3[a] then [F3[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) ∧b C3[a] then f3[F3[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), x.[x])>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)))

Lemma: hdf-state-base4-2
[C1,C2,C3,C4,F1,F2,F3,F4,f1,f2,f3,f4,s:Top]. ∀[hdr1,hdr2,hdr3,hdr4:Name].
  (hdf-state((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
             || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi )
                || x,s. f3[x;s]) hdf-base(a.if name_eq(fst(a);hdr3) ∧b C3[a] then [F3[a]] else [] fi || x,s. f4[\000Cx;s])
                    hdf-base(a.if name_eq(fst(a);hdr4) ∧b C4[a] then [F4[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) ∧b C3[a] then f3[F3[a];s]
                                            if name_eq(fst(a);hdr4) ∧b C4[a] then f4[F4[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), x.[x])>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr1 hdr4 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)) and 
     (hdr2 hdr4 ∈ Name)) and 
     (hdr3 hdr4 ∈ Name)))

Lemma: hdf-state-base2-3
[F1,F2,f1,f2,s:Top]. ∀[hdr1,hdr2:Name].
  hdf-state((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi || x,s. f2[x;s])
             hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi );[s]) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) then f1[F1[a];s]
                                         if name_eq(fst(a);hdr2) then f2[F2[a];s]
                                         else s
                                         fi ; λg.<mk-hdf (g x.x)), x.[x])>1))))) 
    
  supposing ¬(hdr1 hdr2 ∈ Name)

Lemma: hdf-state-base3-3
[F1,F2,F3,f1,f2,f3,s:Top]. ∀[hdr1,hdr2,hdr3:Name].
  (hdf-state((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
             || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi || x,s. f3[x;s])
                 hdf-base(a.if name_eq(fst(a);hdr3) then [F3[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) then f3[F3[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), x.[x])>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)))

Lemma: hdf-state-base4-3
[F1,F2,F3,F4,f1,f2,f3,f4,s:Top]. ∀[hdr1,hdr2,hdr3,hdr4:Name].
  (hdf-state((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
             || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi )
                || x,s. f3[x;s]) hdf-base(a.if name_eq(fst(a);hdr3) then [F3[a]] else [] fi || x,s. f4[x;s])
                    hdf-base(a.if name_eq(fst(a);hdr4) then [F4[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) then f3[F3[a];s]
                                            if name_eq(fst(a);hdr4) then f4[F4[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), x.[x])>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr1 hdr4 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)) and 
     (hdr2 hdr4 ∈ Name)) and 
     (hdr3 hdr4 ∈ Name)))

Lemma: hdf-memory-base
[f,C,F,s:Top].
  (hdf-memory((λx,s. f[x;s]) hdf-base(a.if C[a] then [F[a]] else [] fi );[s]) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if C[a] then f[F[a];s] else fi ; λg.<mk-hdf (g x.x)), [s]>1))))) s)

Lemma: hdf-memory-base2-2
[C1,C2,F1,F2,f1,f2,s:Top]. ∀[hdr1,hdr2:Name].
  hdf-memory((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi || x,s. f2[x;s])
              hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi );[s]) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
                                         if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
                                         else s
                                         fi ; λg.<mk-hdf (g x.x)), [s]>1))))) 
    
  supposing ¬(hdr1 hdr2 ∈ Name)

Lemma: hdf-memory-base3-2
[C1,C2,C3,F1,F2,F3,f1,f2,f3,s:Top]. ∀[hdr1,hdr2,hdr3:Name].
  (hdf-memory((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
              || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi || x,s. f3[x;\000Cs])
                  hdf-base(a.if name_eq(fst(a);hdr3) ∧b C3[a] then [F3[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) ∧b C3[a] then f3[F3[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), [s]>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)))

Lemma: hdf-memory-base4-2
[C1,C2,C3,C4,F1,F2,F3,F4,f1,f2,f3,f4,s:Top]. ∀[hdr1,hdr2,hdr3,hdr4:Name].
  (hdf-memory((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
              || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi )
                 || x,s. f3[x;s]) hdf-base(a.if name_eq(fst(a);hdr3) ∧b C3[a] then [F3[a]] else [] fi )
                    || x,s. f4[x;s]) hdf-base(a.if name_eq(fst(a);hdr4) ∧b C4[a] then [F4[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) ∧b C3[a] then f3[F3[a];s]
                                            if name_eq(fst(a);hdr4) ∧b C4[a] then f4[F4[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), [s]>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr1 hdr4 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)) and 
     (hdr2 hdr4 ∈ Name)) and 
     (hdr3 hdr4 ∈ Name)))

Lemma: hdf-memory-base2-3
[F1,F2,f1,f2,s:Top]. ∀[hdr1,hdr2:Name].
  hdf-memory((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi || x,s. f2[x;s])
              hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi );[s]) 
  fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) then f1[F1[a];s]
                                         if name_eq(fst(a);hdr2) then f2[F2[a];s]
                                         else s
                                         fi ; λg.<mk-hdf (g x.x)), [s]>1))))) 
    
  supposing ¬(hdr1 hdr2 ∈ Name)

Lemma: hdf-memory-base3-3
[F1,F2,F3,f1,f2,f3,s:Top]. ∀[hdr1,hdr2,hdr3:Name].
  (hdf-memory((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
              || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi || x,s. f3[x;s])
                  hdf-base(a.if name_eq(fst(a);hdr3) then [F3[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) then f3[F3[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), [s]>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)))

Lemma: hdf-memory-base4-3
[F1,F2,F3,F4,f1,f2,f3,f4,s:Top]. ∀[hdr1,hdr2,hdr3,hdr4:Name].
  (hdf-memory((λx,s. f1[x;s]) hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
              || x,s. f2[x;s]) hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi )
                 || x,s. f3[x;s]) hdf-base(a.if name_eq(fst(a);hdr3) then [F3[a]] else [] fi || x,s. f4[x;s])
                     hdf-base(a.if name_eq(fst(a);hdr4) then [F4[a]] else [] fi );[s]) 
     fix((λmk-hdf,s. (inl a.cbva_seq(λn.if name_eq(fst(a);hdr1) then f1[F1[a];s]
                                            if name_eq(fst(a);hdr2) then f2[F2[a];s]
                                            if name_eq(fst(a);hdr3) then f3[F3[a];s]
                                            if name_eq(fst(a);hdr4) then f4[F4[a];s]
                                            else s
                                            fi ; λg.<mk-hdf (g x.x)), [s]>1))))) 
       s) supposing 
     ((¬(hdr1 hdr2 ∈ Name)) and 
     (hdr1 hdr3 ∈ Name)) and 
     (hdr1 hdr4 ∈ Name)) and 
     (hdr2 hdr3 ∈ Name)) and 
     (hdr2 hdr4 ∈ Name)) and 
     (hdr3 hdr4 ∈ Name)))

Lemma: hdf-with-state-pair-left-axiom
[L,S,G,init:Top]. ∀[m:ℕ].
  (fix((λmk-hdf,s. (inl a.cbva_seq(L[s;a]; λg.<mk-hdf <Ax, S[s;a;g]>G[s;a;g]>m))))) <Ax, init> fix((λmk-hdf,s. (\000Cinl a.cbva_seq(L[<Ax, s>;a]; λg.<mk-hdf S[<Ax, s>;a;g], G[<Ax, s>;a;g]>m))))) init)

Lemma: sqequal-fix-lemma1
[F,G,H:Base].  fix(F) fix(G) fix((λx.(inl H[x]))) supposing ∀a,b:Base.  (F (G b) inl H[a b])

Lemma: hdf-sqequal2-weak
[F,G,H:Base].
  (fix((λmk-hdf,s0. case s0 of inl(y) => inl a.let X',bs in let out ←─ G[bs] in <mk-hdf X', out>inr(z) => H[\000Cz])) 
   fix((λmk-hdf.(inl m.<mk-hdf, F[m]>)))) fix((λmk-hdf.(inl a.let out ←─ G[F[a]]
                                                                    in <mk-hdf, out>)))))

Lemma: hdf-sqequal3
[F,G,H,K,L,s:Top].
  (fix((λmk-hdf,s0. let X,bs s0 
                    in case X
                        of inl(y) =>
                        inl a.let X',fs 
                                in let bs' ←─ G[fs;bs]
                                   in <mk-hdf <X', K[bs;bs']>L[bs;bs']>)
                        inr(z) =>
                        H[z])) 
   <fix((λmk-hdf.(inl a.<mk-hdf, F[a]>)))), s> fix((λmk-hdf,s0. (inl a.let bs' ←─ G[F[a];s0]
                                                                             in <mk-hdf K[s0;bs'], L[s0;bs']>)))) 
                                                   s)

Lemma: hdf-sqequal3-cbva
[F,G,H,K,L,s:Top].
  (fix((λmk-hdf,s0. let X,bs s0 
                    in case X
                        of inl(y) =>
                        inl a.let X',fs 
                                in let bs' ←─ G[fs;bs]
                                   in <mk-hdf <X', K[bs;bs']>L[bs;bs']>)
                        inr(z) =>
                        H[z])) 
   <fix((λmk-hdf.(inl a.let out ←─ F[a] in <mk-hdf, out>)))), s> fix((λmk-hdf,s0. (inl a.let out ←─ F[a]
                                                                            in let bs' ←─ G[out;s0]
                                                                               in <mk-hdf K[s0;bs'], L[s0;bs']>)))) 
                                                  s)

Lemma: hdf-sqequal4
[F1,F2:Top].
  (fix((λmk-hdf.(inl a.let out ←─ F1[a]
                         in <mk-hdf, out>)))) || fix((λmk-hdf.(inl a.let out ←─ F2[a]
                                                                    in <mk-hdf, out>)))) 
  fix((λmk-hdf.(inl a.let out1 ←─ F1[a]
                          in let out2 ←─ F2[a]
                             in let out ←─ out1 out2
                                in <mk-hdf, out>)))))

Lemma: sqequal-spread-cbva-weak
[a:Top × Top]. ∀[b,F:Top].  (let x ←─ in let u,v in F[u;v] let u,v in let x ←─ in let y ←─ in F[x;y])

Lemma: sqequal-append-cbva-weak2
[a:Top List]. ∀[b,F:Top].  (let x ←─ in F[x] let u ←─ in let v ←─ in let x ←─ in F[x])

Lemma: sqequal-append-cbva-weak3
[a:Top List]. ∀[b,F:Top].  (let u ←─ in let v ←─ in let x ←─ in F[x] let x ←─ in F[x])

Lemma: hdf-sqequal6
[s,F,G:Top].
  (fix((λmk-hdf,s0. (inl a.let bs' ←─ reduce(λl,l'. (l l');[];map(λb.[G[a;b]];s0))
                             in <mk-hdf case null(bs') of inl() => s0 inr() => bs', F[s0;bs']>)))) 
   [s] fix((λmk-hdf,s0. (inl a.let bs' ←─ G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)

Lemma: hdf-sqequal6-1
[s,F,G:Top].
  (fix((λmk-hdf,s0. (inl a.let bs' ←─ ∪b∈s0.[G[a;b]]
                             in <mk-hdf case null(bs') of inl() => s0 inr() => bs', F[s0;bs']>)))) 
   [s] fix((λmk-hdf,s0. (inl a.let bs' ←─ G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)

Lemma: hdf-sqequal6-2
[s,F,G:Top].
  (fix((λmk-hdf,s0. (inl a.let bs' ←─ ∪f∈b.[G[a;b]]].∪b∈s0.f b
                             in <mk-hdf case null(bs') of inl() => s0 inr() => bs', F[s0;bs']>)))) 
   [s] fix((λmk-hdf,s0. (inl a.let bs' ←─ G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)

Lemma: hdf-sqequal7
[F,G,H,K,L,J,init:Top].
  (fix((λmk-hdf,s0. (inl a.let X,s s0 
                             in case X
                                 of inl(P) =>
                                 let X',fs 
                                 in let b ←─ G[fs;s]
                                    in let s' ←─ J[b;s]
                                       in <mk-hdf <X', K[s;s']>L[s;s']>
                                 inr(z) =>
                                 H[mk-hdf;s;z])))) 
   <fix((λmk-hdf.(inl a.let out ←─ F[a] in <mk-hdf, out>)))), init> fix((λmk-hdf,s. (inl a.let out ←─ F[a]
                                                                              in let b ←─ G[out;s]
                                                                                 in let s' ←─ J[b;s]
                                                                                    in <mk-hdf K[s;s'], L[s;s']>)))) 
                                                     init)

Lemma: hdf-sqequal9
[mk-hdf,a,s:Top].
  (let b ←─ a
   in case null(b) of inl(x1) => let s' ←─ in <mk-hdf s', s'> inr(y1) => <mk-hdf b, b> let b ←─ a
                                                                              in let s' ←─ case null(b)
                                                                                  of inl(x1) =>
                                                                                  s
                                                                                  inr(y1) =>
                                                                                  b
                                                                                 in <mk-hdf s', s'>)

Lemma: sqequal-induction-test1
hdf-buffer((λn,m. {n m}) hdf-base(m.{m});{0}) fix((λR,z. (inl a.let x ←─ in <x, {x}>)))) 0

Lemma: hdf-transformation-test1
hdf-buffer((λn,m. {n m}) hdf-base(m.{m});{0}) fix((λR,z. (inl a.let x ←─ in <x, {x}>)))) 0



Home Index