Definition: hiddenfix
hiddenfix(F) == fix(F)
Definition: hdataflow
A "halting dataflow", P, is either halted (inr ⋅ ) or it is a function
that given an input a ∈ A computes a pair <Q, out>, where Q is a new
"halting dataflow" and out is a 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) ⊆r hdataflow(A2;B2)) supposing ((B1 ⊆r B2) and (A2 ⊆r A1))
Definition: hdf-ap
X(a) == case X of inl(P) => P a | 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)]. X ~ 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)]. X ~ 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) ~ P a)
Lemma: hdf-ap-inl
∀[P,a:Top]. (inl P(a) ~ P 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 p 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 = P m 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 i 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 b 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
f o X == 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]. f o 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].
f o X(a) ~ <f o (fst(X(a))), bag-map(f;snd(X(a)))> supposing valueall-type(C)
Definition: hdf-compose2
X o Y ==
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)]. X o 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 o Y(a) = <(fst(X(a))) o (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'
X o' Y ==
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
X o Y ==
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)]. X o 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 ←─ f 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 o 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 o X2*(inputs)) = hdf-halted(X1*(inputs)) ∨bhdf-halted(X2*(inputs)) supposing valueall-type(C)
Lemma: hdf-halt-compose2
∀[X:Top]. (hdf-halt() o X ~ 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 = s
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 = s
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 s else b 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 X of inl(p) => ∀a:A. let X',b = p a in single-valued-bag(b;B) ∧ P | 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 = P a 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 b else sv-bag-only(fs) b 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 b else f sv-bag-only(xs) b 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 s else b 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 o X) o 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) == f o X o Y o 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 = p
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}) o 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
X || Y ==
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)]. X || Y ∈ hdataflow(A;B) supposing valueall-type(B)
Lemma: hdf-parallel-halt-left
∀[A,B:Type]. ∀[X:hdataflow(A;B)]. hdf-halt() || X = X ∈ hdataflow(A;B) supposing valueall-type(B)
Lemma: hdf-parallel-halt-right
∀[A,B:Type]. ∀[X:hdataflow(A;B)]. X || 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].
X || 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 x = 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
X + Y ==
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 x );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 x );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 + Y = (λx.(inl x)) o X || (λx.(inr x )) o 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 S 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 = p
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 = p
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 >>= Y == mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p 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
X (hdfs) >>= Y == mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p 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))].
X (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() ({}) >>= Y ~ hdf-halt())
Lemma: hdf-bind-as-gen
∀[X,Y:Top]. (X >>= Y ~ 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].
X (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].
X (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) >>= Y = 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 o X (hdfs) >>= Y = X (hdfs) >>= Y o 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 o X >>= Y = X >>= Y o 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 = p 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 = p
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 = p 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 = y a 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 = y a 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' ←─ 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' ←─ s in <mk-hdf <X, s'>, s'> | inr(y1) => <mk-hdf <X, b>, b> ~ let b ←─ a
in let s' ←─ if null(b) then s else b 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' ←─ s in <mk-hdf <X, s'>, x> | inr(y1) => <mk-hdf <X, b>, x> ~ let b ←─ a
in let s' ←─ if null(b) then s else b fi
in <mk-hdf <X, s'>, x>)
Lemma: hdf-sqequal8-4
∀[C,a,b,F:Top].
(case C of inl(x1) => let x ←─ a in F[x] | inr(y1) => let x ←─ b 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 o 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 o 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
, g (λx.x)
>; 1))))))
Lemma: hdf-compose1-transformation1
∀[f,L:Base]. ∀[m:ℕ+].
(f o 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 o 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] n fi ;
λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1))))))
Lemma: hdf-compose1-transformation2
∀[f,L,G:Top]. ∀[m:ℕ].
(f o 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] n fi ;
λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1))))))
Lemma: hdf-compose1-transformation3
∀[f,L,S,G,init:Top]. ∀[m:ℕ].
(f o (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] n fi ;
λg.<mk-hdf S[s;a;partial_ap(g;m + 1;m)], select_fun_ap(g;m + 1;m)>; 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] n fi ;
λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; 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] n fi ;
λg.<mk-hdf S[s;a;partial_ap(g;m + 1;m)], select_fun_last(g;m)>; 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] n fi ;
λg.<mk-hdf if bag-null(select_fun_last(g;m)) then s else select_fun_last(g;m) fi
, select_fun_last(g;m)
>; 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)
>; 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 m + 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)>; m + 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 m + 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>; m + 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 <z m1 then L1[a] n
if n <z 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 <z m1 then L1[a] n
if n <z 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 <z m1 then L1[fst(s);a] n
if n <z 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)
>; 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 <z m1 then L1[a] n
if n <z 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 <z m1 then L1[a] n
if n <z 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 <z m1 then L1[fst(s);a] n
if n <z 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)
>; 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)))))
o (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 <z m1 then L1[a] n
if n <z 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)))))
o (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 <z m1 then L1[a] n
if n <z 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)))))
o (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 <z m1 then L1[a] n
if n <z 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)))))
o (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 <z m1 then L1[a] n
if n <z 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)))))
o (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 <z m1 then L1[a] n
if n <z 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)))))
o (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 <z m1 then L1[a] n
if n <z 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]) o 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 s fi ; λg.<mk-hdf (g (λx.x)), g (λ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]) o hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi ) || (λx,s. f2[x;s])
o 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)), g (λx.[x])>; 1)))))
s
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]) o hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi ) || (λx,s. f3[x;s\000C])
o 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)), g (λ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]) o hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi )
|| (λx,s. f3[x;s]) o hdf-base(a.if name_eq(fst(a);hdr3) ∧b C3[a] then [F3[a]] else [] fi ) || (λx,s. f4[\000Cx;s])
o 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)), g (λ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]) o hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi ) || (λx,s. f2[x;s])
o 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)), g (λx.[x])>; 1)))))
s
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]) o hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi ) || (λx,s. f3[x;s])
o 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)), g (λ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]) o hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi )
|| (λx,s. f3[x;s]) o hdf-base(a.if name_eq(fst(a);hdr3) then [F3[a]] else [] fi ) || (λx,s. f4[x;s])
o 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)), g (λ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]) o 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 s 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]) o hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi ) || (λx,s. f2[x;s])
o 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)))))
s
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]) o hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi ) || (λx,s. f3[x;\000Cs])
o 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]) o hdf-base(a.if name_eq(fst(a);hdr1) ∧b C1[a] then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) ∧b C2[a] then [F2[a]] else [] fi )
|| (λx,s. f3[x;s]) o hdf-base(a.if name_eq(fst(a);hdr3) ∧b C3[a] then [F3[a]] else [] fi )
|| (λx,s. f4[x;s]) o 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]) o hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi ) || (λx,s. f2[x;s])
o 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)))))
s
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]) o hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi ) || (λx,s. f3[x;s])
o 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]) o hdf-base(a.if name_eq(fst(a);hdr1) then [F1[a]] else [] fi )
|| (λx,s. f2[x;s]) o hdf-base(a.if name_eq(fst(a);hdr2) then [F2[a]] else [] fi )
|| (λx,s. f3[x;s]) o hdf-base(a.if name_eq(fst(a);hdr3) then [F3[a]] else [] fi ) || (λx,s. f4[x;s])
o 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 a (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 = y a 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 = y a
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 = y a
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 ←─ a in let u,v = x in F[u;v] ~ let u,v = a in let x ←─ u in let y ←─ v in F[x;y])
Lemma: sqequal-append-cbva-weak2
∀[a:Top List]. ∀[b,F:Top]. (let x ←─ a @ b in F[x] ~ let u ←─ a in let v ←─ b in let x ←─ u @ v in F[x])
Lemma: sqequal-append-cbva-weak3
∀[a:Top List]. ∀[b,F:Top]. (let u ←─ a in let v ←─ b in let x ←─ u @ v in F[x] ~ let x ←─ a @ b 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 = P a
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' ←─ 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}) o hdf-base(m.{m});{0}) ~ fix((λR,z. (inl (λa.let x ←─ a + z in <R x, {x}>)))) 0
Lemma: hdf-transformation-test1
hdf-buffer((λn,m. {n + m}) o hdf-base(m.{m});{0}) ~ fix((λR,z. (inl (λa.let x ←─ a + z in <R x, {x}>)))) 0
Home
Index