Definition: eclass0-program
eclass0-program(f;pr) == λi.hdf-compose0(f i;pr i)
Lemma: eclass0-program_wf
∀[Info,B,C:Type].
∀[X:EClass(B)]. ∀[F:Id ⟶ B ⟶ bag(C)]. ∀[Xpr:LocalClass(X)]. (eclass0-program(F;Xpr) ∈ LocalClass((F o X)))
supposing valueall-type(C)
Lemma: eclass0_local
∀[Info,B,C:Type]. ∀[X:EClass(B)].
∀f:Id ⟶ B ⟶ bag(C). (LocalClass(X) ⇒ LocalClass((f o X))) supposing valueall-type(C)
Definition: eclass1-program
eclass1-program(f;pr) == λi.((f i) o (pr i))
Lemma: eclass1-program_wf
∀[Info,B,C:Type].
∀[X:EClass(B)]. ∀[f:Id ⟶ B ⟶ C]. ∀[pr:LocalClass(X)]. (eclass1-program(f;pr) ∈ LocalClass((f o X)))
supposing valueall-type(C)
Lemma: eclass1-program-wf-hdf
∀[Info,B,C:Type].
∀[f:Id ⟶ B ⟶ C]. ∀[pr:Id ⟶ hdataflow(Info;B)]. (eclass1-program(f;pr) ∈ Id ⟶ hdataflow(Info;C))
supposing valueall-type(C)
Lemma: eclass1_local
∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀f:Id ⟶ B ⟶ C. (LocalClass(X) ⇒ LocalClass((f o X))) supposing valueall-type(C)
Definition: eclass2-program
Xpr o Ypr == λi.((Xpr i) o (Ypr i))
Lemma: eclass2-program_wf
∀[Info,B,C:Type].
∀[X:EClass(B ⟶ bag(C))]. ∀[Y:EClass(B)]. ∀[Xpr:LocalClass(X)]. ∀[Ypr:LocalClass(Y)].
(Xpr o Ypr ∈ LocalClass((X o Y)))
supposing valueall-type(C)
Lemma: eclass2-program-wf-hdf
∀[Info,B,C:Type].
∀[Xpr:Id ⟶ hdataflow(Info;B ⟶ bag(C))]. ∀[Ypr:Id ⟶ hdataflow(Info;B)]. (Xpr o Ypr ∈ Id ⟶ hdataflow(Info;C))
supposing valueall-type(C)
Lemma: eclass2-program-eq-hdf
∀[Info,B,C:Type].
∀[Xpr1,Xpr2:Id ⟶ hdataflow(Info;B ⟶ bag(C))]. ∀[Ypr1,Ypr2:Id ⟶ hdataflow(Info;B)].
(Xpr1 o Ypr1 = Xpr2 o Ypr2 ∈ (Id ⟶ hdataflow(Info;C))) supposing
((Xpr1 = Xpr2 ∈ (Id ⟶ hdataflow(Info;B ⟶ bag(C)))) and
(Ypr1 = Ypr2 ∈ (Id ⟶ hdataflow(Info;B))))
supposing valueall-type(C)
Lemma: eclass2_local
∀[Info,B,C:Type]. ∀[X:EClass(B ⟶ bag(C))]. ∀[Y:EClass(B)].
LocalClass(X) ⇒ LocalClass(Y) ⇒ LocalClass((X o Y)) supposing valueall-type(C)
Definition: eclass3-program
eclass3-program(Xpr;Ypr) == λi.Xpr i o Ypr i
Lemma: eclass3-program_wf
∀[Info,B,C:Type].
∀[X:EClass(B ⟶ C)]. ∀[Y:EClass(B)]. ∀[Xpr:LocalClass(X)]. ∀[Ypr:LocalClass(Y)].
(eclass3-program(Xpr;Ypr) ∈ LocalClass(eclass3(X;Y)))
supposing valueall-type(C)
Lemma: eclass3_local
∀[Info,B,C:Type]. ∀[X:EClass(B ⟶ C)]. ∀[Y:EClass(B)].
LocalClass(X) ⇒ LocalClass(Y) ⇒ LocalClass(eclass3(X;Y)) supposing valueall-type(C)
Definition: eclass0-bag-program
eclass0-bag-program(f;pr) == λi.hdf-compose0-bag(f i;pr i)
Lemma: eclass0-bag-program_wf
∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[F:Id ⟶ bag(B) ⟶ bag(C)]. ∀[Xpr:LocalClass(X)].
(eclass0-bag-program(F;Xpr) ∈ LocalClass(eclass0-bag(F;X))) supposing
((∀i:Id. ((F i {}) = {} ∈ bag(C))) and
valueall-type(C))
Definition: once-class-program
once-class-program(pr) == λi.hdf-once(pr i)
Lemma: once-class-program_wf
∀[Info,B:Type]. ∀[X:EClass(B)]. ∀[pr:LocalClass(X)]. (once-class-program(pr) ∈ LocalClass((X once)))
Lemma: once-class-program-wf-hdf
∀[Info,B:Type]. ∀[pr:Id ⟶ hdataflow(Info;B)]. (once-class-program(pr) ∈ Id ⟶ hdataflow(Info;B))
Lemma: once-class-program-eq-hdf
∀[Info,B:Type]. ∀[pr1,pr2:Id ⟶ hdataflow(Info;B)].
once-class-program(pr1) = once-class-program(pr2) ∈ (Id ⟶ hdataflow(Info;B))
supposing pr1 = pr2 ∈ (Id ⟶ hdataflow(Info;B))
Lemma: once-class_local
∀[Info,B:Type]. ∀[X:EClass(B)]. (LocalClass(X) ⇒ LocalClass((X once)))
Definition: until-class-program
until-class-program(xpr;ypr) == λi.hdf-until(xpr i;ypr i)
Lemma: until-class-program_wf
∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[Y:EClass(C)]. ∀[xpr:LocalClass(X)]. ∀[ypr:LocalClass(Y)].
(until-class-program(xpr;ypr) ∈ LocalClass((X until Y)))
Lemma: until-class_local
∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[Y:EClass(C)]. (LocalClass(X) ⇒ LocalClass(Y) ⇒ LocalClass((X until Y)))
Definition: loop-class-program
loop-class-program(init;pr) == λi.hdf-buffer(pr i;init i)
Lemma: loop-class-program_wf
∀[Info,B:Type].
∀[X:EClass(B ⟶ bag(B))]. ∀[init:Id ⟶ bag(B)]. ∀[pr:LocalClass(X)].
(loop-class-program(init;pr) ∈ LocalClass(loop-class(X;init)))
supposing valueall-type(B)
Lemma: loop-class_local
∀[Info,B:Type]. ∀[X:EClass(B ⟶ bag(B))].
∀init:Id ⟶ bag(B). LocalClass(X) ⇒ LocalClass(loop-class(X;init)) supposing valueall-type(B)
Definition: loop-class2-program
loop-class2-program(init;pr) == λi.hdf-buffer2(pr i;init i)
Lemma: loop-class2-program_wf
∀[Info,B:Type].
∀[X:EClass(B ⟶ B)]. ∀[init:Id ⟶ bag(B)]. ∀[pr:LocalClass(X)].
(loop-class2-program(init;pr) ∈ LocalClass(loop-class2(X;init)))
supposing valueall-type(B)
Lemma: loop-class2_local
∀[Info,B:Type]. ∀[X:EClass(B ⟶ B)].
∀init:Id ⟶ bag(B). LocalClass(X) ⇒ LocalClass(loop-class2(X;init)) supposing valueall-type(B)
Definition: bind-class-program
xpr >>= ypr == λi.xpr i >>= λx.(ypr x i)
Lemma: bind-class-program_wf
∀[Info,A,B:Type].
∀[X:EClass(A)]. ∀[Y:A ⟶ EClass(B)]. ∀[xpr:LocalClass(X)]. ∀[ypr:a:A ⟶ LocalClass(Y[a])].
(xpr >>= ypr ∈ LocalClass(X >a> Y[a]))
supposing valueall-type(B)
Lemma: bind-class-program-wf-hdf
∀[Info,A,B:Type].
∀[xpr:Id ⟶ hdataflow(Info;A)]. ∀[ypr:A ⟶ Id ⟶ hdataflow(Info;B)]. (xpr >>= ypr ∈ Id ⟶ hdataflow(Info;B))
supposing valueall-type(B)
Lemma: bind-class_local
∀[Info,A,B:Type].
∀[X:EClass(A)]. ∀[Y:A ⟶ EClass(B)]. (LocalClass(X) ⇒ (∀a:A. LocalClass(Y[a])) ⇒ LocalClass(X >a> Y[a]))
supposing valueall-type(B)
Lemma: bind-class-program-eq-hdf
∀[Info,A,B:Type].
∀[xpr1,xpr2:Id ⟶ hdataflow(Info;A)]. ∀[ypr1,ypr2:A ⟶ Id ⟶ hdataflow(Info;B)].
(xpr1 >>= ypr1 = xpr2 >>= ypr2 ∈ (Id ⟶ hdataflow(Info;B))) supposing
((xpr1 = xpr2 ∈ (Id ⟶ hdataflow(Info;A))) and
(ypr1 = ypr2 ∈ (A ⟶ Id ⟶ hdataflow(Info;B))))
supposing valueall-type(B)
Definition: eclass-state-program
eclass-state-program(init;f;pr) == loop-class-program(λl.{init l};eclass1-program(λi,a,b. {f i a b};pr))
Lemma: eclass-state-program_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[pr:LocalClass(X)].
eclass-state-program(init;f;pr) ∈ LocalClass(eclass-state(init;f;X)) supposing valueall-type(B) ∧ (↓B)
Definition: loop-class-state-program
loop-class-state-program(pr;init) == λi.hdf-state(pr i;init i)
Lemma: loop-class-state-program_wf
∀[Info,B:Type].
∀[X:EClass(B ⟶ B)]. ∀[init:Id ⟶ bag(B)]. ∀[pr:LocalClass(X)].
(loop-class-state-program(pr;init) ∈ LocalClass(loop-class-state(X;init)))
supposing valueall-type(B)
Lemma: loop-class-state-program-wf-hdf
∀[Info,B:Type].
∀[init:Id ⟶ bag(B)]. ∀[pr:Id ⟶ hdataflow(Info;B ⟶ B)].
(loop-class-state-program(pr;init) ∈ Id ⟶ hdataflow(Info;B))
supposing valueall-type(B)
Definition: loop-class-memory-program
loop-class-memory-program(pr;init) == λi.hdf-memory(pr i;init i)
Lemma: loop-class-memory-program_wf
∀[Info,B:Type].
∀[X:EClass(B ⟶ B)]. ∀[init:Id ⟶ bag(B)]. ∀[pr:LocalClass(X)].
(loop-class-memory-program(pr;init) ∈ LocalClass(loop-class-memory(X;init)))
supposing valueall-type(B)
Definition: base-class-program
base-class-program(hdr) == λi.hdf-base(v.cond-msg-body(hdr;v))
Lemma: base-class-program_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type]. base-class-program(hdr) ∈ LocalClass(Base(hdr)) supposing hdr encodes T
Lemma: base-class-program-wf-sub
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type]. base-class-program(hdr) ∈ LocalClass(Base(hdr)) supposing hdr encodes T
Lemma: base-class-program-wf-hdf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type].
base-class-program(hdr) ∈ Id ⟶ hdataflow(Message(f);T) supposing hdr encodes T
Definition: verify-class-program
verify-class-program(hdr) == λi.hdf-base(v.cond-verify-msg-body(hdr;v))
Lemma: verify-class-program_wf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type]. verify-class-program(hdr) ∈ LocalClass(Verify(hdr)) supposing hdr encodes T
Lemma: verify-class-program-wf-sub
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type]. verify-class-program(hdr) ∈ LocalClass(Verify(hdr)) supposing hdr encodes T
Lemma: verify-class-program-wf-hdf
∀[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type].
verify-class-program(hdr) ∈ Id ⟶ hdataflow(Message(f);T) supposing hdr encodes T
Definition: base-process-class-program
base-process-class-program(X;loc;hdr) ==
λi.mk-hdf(P,m.if test-msg-header-and-loc(m;hdr;loc) then P(snd(msg-body(m))) else <P, {}> fi ;s.hdf-halted(s);X loc)
Lemma: base-process-class-program_wf1
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
∀[P:LocalClass(X)]. (base-process-class-program(P;loc;hdr) ∈ Id ⟶ hdataflow(Message(f);T))
supposing hdr encodes Id × Info
Lemma: base-process-class-program-ap
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[loc:Id]. ∀[hdr:Name].
∀[P:Id ⟶ hdataflow(Info;T)]. ∀[a:Message(f)]. ∀[i:Top].
(base-process-class-program(P;loc;hdr) i(a) ~ if hdf-halted(P loc) then <hdf-halt(), {}>
if test-msg-header-and-loc(a;hdr;loc)
then let P',b = P loc(snd(msg-body(a)))
in <base-process-class-program(λi.P';loc;hdr) i, b>
else <base-process-class-program(P;loc;hdr) i, {}>
fi )
supposing hdr encodes Id × Top
Lemma: iterate-base-process-class-program
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[loc:Id]. ∀[hdr:Name].
∀[P:Id ⟶ hdataflow(Info;T)]. ∀[L:Message(f) List]. ∀[m:Message(f)]. ∀[i:Top].
(snd(base-process-class-program(P;loc;hdr) i*(L)(m)) ~ if test-msg-header-and-loc(m;hdr;loc)
then snd(P loc*(mapfilter(λmsg.(snd(msg-body(msg)));λmsg.test-msg-header-and-loc(msg;hdr;loc);L))(snd(msg-body(m))))
else {}
fi )
supposing hdr encodes Id × Info
Lemma: base-process-class-program_wf
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[loc:Id]. ∀[hdr:Name].
∀[X:EClass(T)]. ∀[P:LocalClass(X)].
(base-process-class-program(P;loc;hdr) ∈ LocalClass(base-process-class(X;loc;hdr)))
supposing hdr encodes Id × Info
Definition: parallel-class-program
X || Y == λi.X i || Y i
Lemma: parallel-class-program_wf
∀[Info,B:Type].
∀[X,Y:EClass(B)]. ∀[Xpr:LocalClass(X)]. ∀[Ypr:LocalClass(Y)]. (Xpr || Ypr ∈ LocalClass(X || Y))
supposing valueall-type(B)
Lemma: parallel-class-program-wf-hdf
∀[A,B:Type]. ∀[Xpr,Ypr:Id ⟶ hdataflow(A;B)]. (Xpr || Ypr ∈ Id ⟶ hdataflow(A;B)) supposing valueall-type(B)
Lemma: parallel-compose2-program-eq
∀[Info,B,C:Type]. ∀[X1,X2:Id ⟶ hdataflow(Info;B ⟶ bag(C))]. ∀[X:Id ⟶ hdataflow(Info;B)].
(X1 o X || X2 o X = X1 || X2 o X ∈ (Id ⟶ hdataflow(Info;C))) supposing
(valueall-type(C) and
valueall-type(B) and
(↓B))
Lemma: parallel-class-program-compose2-eq
∀[A,B,C:Type]. ∀[X1,X2:Id ⟶ hdataflow(A;B ⟶ bag(C))]. ∀[X:Id ⟶ hdataflow(A;B)].
(X1 o X || X2 o X = X1 || X2 o X ∈ (Id ⟶ hdataflow(A;C))) supposing (valueall-type(C) and valueall-type(B) and (↓B))
Lemma: parallel-class-program-eq
∀[Info,B:Type].
∀[X,Y:EClass(B)]. ∀[Xpr1,Xpr2:LocalClass(X)]. ∀[Ypr1,Ypr2:LocalClass(Y)].
(Xpr1 || Ypr1 = Xpr2 || Ypr2 ∈ (Id ⟶ hdataflow(Info;B))) supposing
((Xpr1 = Xpr2 ∈ (Id ⟶ hdataflow(Info;B))) and
(Ypr1 = Ypr2 ∈ (Id ⟶ hdataflow(Info;B))))
supposing valueall-type(B)
Lemma: parallel-class-program-eq-hdf
∀[Info,B:Type].
∀[Xpr1,Xpr2,Ypr1,Ypr2:Id ⟶ hdataflow(Info;B)].
(Xpr1 || Ypr1 = Xpr2 || Ypr2 ∈ (Id ⟶ hdataflow(Info;B))) supposing
((Xpr1 = Xpr2 ∈ (Id ⟶ hdataflow(Info;B))) and
(Ypr1 = Ypr2 ∈ (Id ⟶ hdataflow(Info;B))))
supposing valueall-type(B)
Definition: class-at-program
(pr)@locs == λi.if bag-deq-member(IdDeq;i;locs) then pr i else hdf-halt() fi
Lemma: class-at-program_wf
∀[Info,B:Type]. ∀[X:EClass(B)]. ∀[pr:LocalClass(X)]. ∀[locs:bag(Id)].
(pr)@locs ∈ LocalClass(X@locs) supposing valueall-type(B)
Lemma: class-at-program-wf-hdf
∀[A,B:Type]. ∀[pr:Id ⟶ hdataflow(A;B)]. ∀[locs:bag(Id)]. (pr)@locs ∈ Id ⟶ hdataflow(A;B) supposing valueall-type(B)
Lemma: class-at-program-eq-hdf
∀[A,B:Type]. ∀[pr1,pr2:Id ⟶ hdataflow(A;B)]. ∀[locs:bag(Id)].
((pr1)@locs = (pr2)@locs ∈ (Id ⟶ hdataflow(A;B))) supposing
((pr1 = pr2 ∈ (Id ⟶ hdataflow(A;B))) and
valueall-type(B))
Definition: on-loc-class-program
on-loc-class-program(pr) == λi.(pr i i)
Lemma: on-loc-class-program_wf
∀[Info,B:Type]. ∀[X:Id ⟶ EClass(B)]. ∀[pr:∀i:Id. LocalClass(X i)].
on-loc-class-program(pr) ∈ LocalClass(on-loc-class(X)) supposing valueall-type(B)
Lemma: on-loc-class-program-wf-hdf
∀[Info,B:Type]. ∀[pr:Id ⟶ Id ⟶ hdataflow(Info;B)].
on-loc-class-program(pr) ∈ Id ⟶ hdataflow(Info;B) supposing valueall-type(B)
Lemma: on-loc-class-program-eq-hdf
∀[Info,B:Type]. ∀[pr1,pr2:Id ⟶ Id ⟶ hdataflow(Info;B)].
(on-loc-class-program(pr1) = on-loc-class-program(pr2) ∈ (Id ⟶ hdataflow(Info;B))) supposing
((pr1 = pr2 ∈ (Id ⟶ Id ⟶ hdataflow(Info;B))) and
valueall-type(B))
Definition: return-loc-bag-class-program
return-loc-bag-class-program(x) == λi.hdf-return(x i)
Lemma: return-loc-bag-class-program_wf
∀[Info,B:Type]. ∀[x:Id ⟶ bag(B)].
return-loc-bag-class-program(x) ∈ LocalClass(return-loc-bag-class(x)) supposing valueall-type(B)
Lemma: return-loc-bag-class-program-wf-hdf
∀[Info,B:Type]. ∀[x:Id ⟶ bag(B)]. return-loc-bag-class-program(x) ∈ Id ⟶ hdataflow(Info;B) supposing valueall-type(B)
Definition: null-class-program
null-class-program() == λi.hdf-return({})
Lemma: null-class-program_wf
∀[Info,B:Type]. (null-class-program() ∈ LocalClass(Null))
Definition: eclass-disju-program
xpr + ypr == eclass1-program(λl,x. (inl x);xpr) || eclass1-program(λl,x. (inr x );ypr)
Lemma: eclass-disju-program_wf
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[xpr:LocalClass(X)]. ∀[ypr:LocalClass(Y)].
(xpr + ypr ∈ LocalClass(X + Y)) supposing (valueall-type(A) and valueall-type(B))
Definition: sequence-class-program
sequence-class-program(xpr;ypr;zpr) == λi.hdf-sequence(xpr i;ypr i;zpr i)
Lemma: sequence-class-program_wf
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(A)]. ∀[xpr:LocalClass(X)]. ∀[ypr:LocalClass(Y)].
∀[zpr:LocalClass(Z)].
sequence-class-program(xpr;ypr;zpr) ∈ LocalClass(sequence-class(X;Y;Z)) supposing valueall-type(A)
Definition: state-class1-program
state-class1-program(init;tr;pr) == loop-class-state-program(eclass1-program(tr;pr);λloc.{init loc})
Lemma: state-class1-program_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[pr:LocalClass(X)].
(state-class1-program(init;f;pr) ∈ LocalClass(state-class1(init;f;X))) supposing (valueall-type(B) and (↓B))
Lemma: state-class1-program-wf-hdf
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[pr:Id ⟶ hdataflow(Info;A)].
(state-class1-program(init;f;pr) ∈ Id ⟶ hdataflow(Info;B)) supposing (valueall-type(B) and (↓B))
Definition: state-class2-program
state-class2-program(init;tr1;pr1;tr2;pr2) ==
loop-class-state-program(eclass1-program(tr1;pr1) || eclass1-program(tr2;pr2);λloc.{init loc})
Lemma: state-class2-program_wf
∀[Info,A1,A2,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[pr1:LocalClass(X1)]. ∀[tr2:Id
⟶ A2
⟶ B
⟶ B].
∀[X2:EClass(A2)]. ∀[pr2:LocalClass(X2)].
(state-class2-program(init;tr1;pr1;tr2;pr2) ∈ LocalClass(state-class2(init;tr1;X1;tr2;X2))) supposing
(valueall-type(A1) and
valueall-type(A2) and
valueall-type(B) and
(↓B))
Definition: state-class3-program
state-class3-program(init;tr1;pr1;tr2;pr2;tr3;pr3) ==
loop-class-state-program(eclass1-program(tr1;pr1) || eclass1-program(tr2;pr2) || eclass1-program(tr3;pr3);λloc.{init
loc})
Lemma: state-class3-program_wf
∀[Info,A1,A2,A3,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[pr1:LocalClass(X1)].
∀[tr2:Id ⟶ A2 ⟶ B ⟶ B]. ∀[X2:EClass(A2)]. ∀[pr2:LocalClass(X2)]. ∀[tr3:Id ⟶ A3 ⟶ B ⟶ B]. ∀[X3:EClass(A3)].
∀[pr3:LocalClass(X3)].
(state-class3-program(init;tr1;pr1;tr2;pr2;tr3;pr3) ∈ LocalClass(state-class3(init;tr1;X1;tr2;X2;tr3;X3))) supposing
(valueall-type(A1) and
valueall-type(A2) and
valueall-type(A3) and
valueall-type(B) and
(↓B))
Definition: state-class4-program
state-class4-program(init;tr1;pr1;tr2;pr2;tr3;pr3;tr4;pr4) ==
loop-class-state-program(eclass1-program(tr1;pr1) || eclass1-program(tr2;pr2) || eclass1-program(tr3;pr3)
|| eclass1-program(tr4;pr4);
λloc.{init loc})
Lemma: state-class4-program_wf
∀[Info,A1,A2,A3,A4,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[pr1:LocalClass(X1)].
∀[tr2:Id ⟶ A2 ⟶ B ⟶ B]. ∀[X2:EClass(A2)]. ∀[pr2:LocalClass(X2)]. ∀[tr3:Id ⟶ A3 ⟶ B ⟶ B]. ∀[X3:EClass(A3)].
∀[pr3:LocalClass(X3)]. ∀[tr4:Id ⟶ A4 ⟶ B ⟶ B]. ∀[X4:EClass(A4)]. ∀[pr4:LocalClass(X4)].
(state-class4-program(init;tr1;pr1;tr2;pr2;tr3;pr3;tr4;pr4)
∈ LocalClass(state-class4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4))) supposing
(valueall-type(A1) and
valueall-type(A2) and
valueall-type(A3) and
valueall-type(A4) and
valueall-type(B) and
(↓B))
Definition: state-class5-program
state-class5-program(init;tr1;pr1;tr2;pr2;tr3;pr3;tr4;pr4;tr5;pr5) ==
loop-class-state-program(eclass1-program(tr1;pr1) || eclass1-program(tr2;pr2) || eclass1-program(tr3;pr3)
|| eclass1-program(tr4;pr4)
|| eclass1-program(tr5;pr5);
λloc.{init loc})
Lemma: state-class5-program_wf
∀[Info,A1,A2,A3,A4,A5,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[pr1:LocalClass(X1)].
∀[tr2:Id ⟶ A2 ⟶ B ⟶ B]. ∀[X2:EClass(A2)]. ∀[pr2:LocalClass(X2)]. ∀[tr3:Id ⟶ A3 ⟶ B ⟶ B]. ∀[X3:EClass(A3)].
∀[pr3:LocalClass(X3)]. ∀[tr4:Id ⟶ A4 ⟶ B ⟶ B]. ∀[X4:EClass(A4)]. ∀[pr4:LocalClass(X4)]. ∀[tr5:Id ⟶ A5 ⟶ B ⟶ B].
∀[X5:EClass(A5)]. ∀[pr5:LocalClass(X5)].
(state-class5-program(init;tr1;pr1;tr2;pr2;tr3;pr3;tr4;pr4;tr5;pr5)
∈ LocalClass(state-class5(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4;tr5;X5))) supposing
(valueall-type(A1) and
valueall-type(A2) and
valueall-type(A3) and
valueall-type(A4) and
valueall-type(A5) and
valueall-type(B) and
(↓B))
Definition: memory-class1-program
memory-class1-program(init;tr;pr) == loop-class-memory-program(eclass1-program(tr;pr);λloc.{init loc})
Lemma: memory-class1-program_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[pr:LocalClass(X)].
(memory-class1-program(init;f;pr) ∈ LocalClass(memory-class1(initially init
applying f
on X))) supposing
(valueall-type(B) and
(↓B))
Definition: memory-class2-program
memory-class2-program(init;tr1;pr1;tr2;pr2) ==
loop-class-memory-program(eclass1-program(tr1;pr1) || eclass1-program(tr2;pr2);λloc.{init loc})
Lemma: memory-class2-program_wf
∀[Info,A1,A2,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[pr1:LocalClass(X1)]. ∀[tr2:Id
⟶ A2
⟶ B
⟶ B].
∀[X2:EClass(A2)]. ∀[pr2:LocalClass(X2)].
(memory-class2-program(init;tr1;pr1;tr2;pr2) ∈ LocalClass(memory-class2(init;tr1;X1;tr2;X2))) supposing
(valueall-type(A1) and
valueall-type(A2) and
valueall-type(B) and
(↓B))
Definition: memory-class3-program
memory-class3-program(init;tr1;pr1;tr2;pr2;tr3;pr3) ==
loop-class-memory-program(eclass1-program(tr1;pr1) || eclass1-program(tr2;pr2) || eclass1-program(tr3;pr3);λloc.{init
loc})
Lemma: memory-class3-program_wf
∀[Info,A1,A2,A3,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[pr1:LocalClass(X1)].
∀[tr2:Id ⟶ A2 ⟶ B ⟶ B]. ∀[X2:EClass(A2)]. ∀[pr2:LocalClass(X2)]. ∀[tr3:Id ⟶ A3 ⟶ B ⟶ B]. ∀[X3:EClass(A3)].
∀[pr3:LocalClass(X3)].
(memory-class3-program(init;tr1;pr1;tr2;pr2;tr3;pr3)
∈ LocalClass(memory-class3(init;tr1;X1;tr2;X2;tr3;X3))) supposing
(valueall-type(A1) and
valueall-type(A2) and
valueall-type(A3) and
valueall-type(B) and
(↓B))
Definition: memory-class4-program
memory-class4-program(init;tr1;pr1;tr2;pr2;tr3;pr3;tr4;pr4) ==
loop-class-memory-program(eclass1-program(tr1;pr1) || eclass1-program(tr2;pr2) || eclass1-program(tr3;pr3)
|| eclass1-program(tr4;pr4);
λloc.{init loc})
Lemma: memory-class4-program_wf
∀[Info,A1,A2,A3,A4,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[pr1:LocalClass(X1)].
∀[tr2:Id ⟶ A2 ⟶ B ⟶ B]. ∀[X2:EClass(A2)]. ∀[pr2:LocalClass(X2)]. ∀[tr3:Id ⟶ A3 ⟶ B ⟶ B]. ∀[X3:EClass(A3)].
∀[pr3:LocalClass(X3)]. ∀[tr4:Id ⟶ A4 ⟶ B ⟶ B]. ∀[X4:EClass(A4)]. ∀[pr4:LocalClass(X4)].
(memory-class4-program(init;tr1;pr1;tr2;pr2;tr3;pr3;tr4;pr4)
∈ LocalClass(memory-class4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4))) supposing
(valueall-type(A1) and
valueall-type(A2) and
valueall-type(A3) and
valueall-type(A4) and
valueall-type(B) and
(↓B))
Lemma: hdf-parallel-bind-halt-eq
∀[A,B,C:Type]. ∀[X1,X2:hdataflow(A;B)]. ∀[X:B ⟶ hdataflow(A;C)].
(∀inputs:A List. hdf-halted(X1 >>= X || X2 >>= X*(inputs)) = hdf-halted(X1 || X2 >>= X*(inputs))) supposing
(valueall-type(C) and
valueall-type(B))
Lemma: hdf-parallel-bind-halt-eq-gen
∀[A,B1,B2,C:Type]. ∀[X1:hdataflow(A;B1)]. ∀[X2:hdataflow(A;B2)]. ∀[Y1:B1 ⟶ hdataflow(A;C)]. ∀[Y2:B2 ⟶ hdataflow(A;C)].
(∀inputs:A List
hdf-halted(X1 >>= Y1 || X2 >>= Y2*(inputs))
= hdf-halted(X1 + X2 >>= λx.case x of inl(b1) => Y1[b1] | inr(b2) => Y2[b2]*(inputs))) supposing
(valueall-type(C) and
valueall-type(B1) and
valueall-type(B2))
Lemma: parallel-bind-program-eq
∀[Info,B,C:Type]. ∀[X1,X2:Id ⟶ hdataflow(Info;B)]. ∀[X:B ⟶ Id ⟶ hdataflow(Info;C)].
(X1 >>= X || X2 >>= X = X1 || X2 >>= X ∈ (Id ⟶ hdataflow(Info;C))) supposing (valueall-type(C) and valueall-type(B))
Lemma: parallel-bind-program-eq-gen
∀[Info,B1,B2,C:Type]. ∀[X1:Id ⟶ hdataflow(Info;B1)]. ∀[X2:Id ⟶ hdataflow(Info;B2)].
∀[Y1:B1 ⟶ Id ⟶ hdataflow(Info;C)]. ∀[Y2:B2 ⟶ Id ⟶ hdataflow(Info;C)].
(X1 >>= Y1 || X2 >>= Y2
= X1 + X2 >>= λb.case b of inl(b1) => Y1 b1 | inr(b2) => Y2 b2
∈ (Id ⟶ hdataflow(Info;C))) supposing
(valueall-type(C) and
valueall-type(B1) and
valueall-type(B2))
Lemma: hdf-parallel-bind-eq
∀[A,B,C:Type]. ∀[X1,X2:hdataflow(A;B)]. ∀[X:B ⟶ hdataflow(A;C)].
(X1 >>= X || X2 >>= X = X1 || X2 >>= X ∈ hdataflow(A;C)) supposing (valueall-type(C) and valueall-type(B))
Lemma: hdf-parallel-compose-eq
∀[A,B,C:Type]. ∀[X1,X2:hdataflow(A;B ⟶ bag(C))]. ∀[X:hdataflow(A;B)].
(X1 o X || X2 o X = (X1 || X2 o X) ∈ hdataflow(A;C)) supposing (valueall-type(C) and valueall-type(B) and (↓B))
Lemma: hdf-parallel-bind-eq-gen
∀[A,B1,B2,C:Type]. ∀[X1:hdataflow(A;B1)]. ∀[X2:hdataflow(A;B2)]. ∀[Y1:B1 ⟶ hdataflow(A;C)]. ∀[Y2:B2 ⟶ hdataflow(A;C)].
(X1 >>= Y1 || X2 >>= Y2 = X1 + X2 >>= λb.case b of inl(b1) => Y1 b1 | inr(b2) => Y2 b2 ∈ hdataflow(A;C)) supposing
(valueall-type(C) and
valueall-type(B2) and
valueall-type(B1))
Home
Index