Definition: labeled-graph
LabeledGraph(T) == self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
Lemma: labeled-graph_wf
∀[T:Type]. (LabeledGraph(T) ∈ Type)
Definition: lg-size
lg-size(g) == ||g||
Lemma: lg-size_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. (lg-size(g) ∈ ℕ)
Definition: lg-nil
lg-nil() == []
Lemma: lg-nil_wf
∀[T:Type]. (lg-nil() ∈ LabeledGraph(T))
Lemma: continuous-labeled-graph
∀[F:Type ─→ Type]. Continuous+(T.LabeledGraph(F[T])) supposing Continuous+(T.F[T])
Lemma: monotone-labeled-graph
∀[F:Type ─→ Type]. Monotone(T.LabeledGraph(F[T])) supposing Monotone(T.F[T])
Lemma: subtype_rel-labeled-graph
∀[A,B:Type]. LabeledGraph(A) ⊆r LabeledGraph(B) supposing A ⊆r B
Definition: lg-append
lg-append(g1;g2) ==
g1 @ map(λtr.let lbl,in,out = tr in <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>;g2)
Lemma: lg-append_wf
∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. (lg-append(g1;g2) ∈ LabeledGraph(T))
Lemma: lg-append_assoc
∀[T:Type]. ∀[a,b,c:LabeledGraph(T)]. (lg-append(a;lg-append(b;c)) ~ lg-append(lg-append(a;b);c))
Lemma: lg-append-assoc
∀[T:Type]. Assoc(LabeledGraph(T);λa,b. lg-append(a;b))
Lemma: lg-append-nil
∀[T:Type]. ∀[g:LabeledGraph(T)]. (lg-append(g;lg-nil()) = g ∈ LabeledGraph(T))
Lemma: lg-nil-append
∀[T:Type]. ∀[g:LabeledGraph(T)]. (lg-append(lg-nil();g) ~ g)
Definition: lg-contains
g1 ⊆ g2 == ∃ga,gb:LabeledGraph(T). (g2 = lg-append(ga;lg-append(g1;gb)) ∈ LabeledGraph(T))
Lemma: lg-contains_wf
∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. (g1 ⊆ g2 ∈ ℙ)
Lemma: lg-append-contains
∀[T:Type]. ∀g1,g2:LabeledGraph(T). (g1 ⊆ lg-append(g1;g2) ∧ g2 ⊆ lg-append(g1;g2))
Lemma: lg-contains_transitivity
∀[T:Type]. ∀g1,g2,g3:LabeledGraph(T). (g1 ⊆ g2 ⇒ g2 ⊆ g3 ⇒ g1 ⊆ g3)
Lemma: lg-contains_weakening
∀[T:Type]. ∀g1,g2:LabeledGraph(T). g1 ⊆ g2 supposing g1 = g2 ∈ LabeledGraph(T)
Definition: lg-remove
lg-remove(g;n) ==
map(λtr.let lbl,in,out = tr in
<lbl
, map(λx.if x ≤z n then x else x - 1 fi ;filter(λx.(¬b(x =z n));in))
, map(λx.if x ≤z n then x else x - 1 fi ;filter(λx.(¬b(x =z n));out))>;firstn(n;g) @ nth_tl(n + 1;g))
Lemma: lg-remove_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕ]. (lg-remove(g;x) ∈ LabeledGraph(T))
Lemma: lg-remove-noop
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕ]. lg-remove(g;x) ~ g supposing lg-size(g) ≤ x
Lemma: lg-size-remove
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)]. (lg-size(lg-remove(g;x)) = (lg-size(g) - 1) ∈ ℤ)
Lemma: lg-size-append
∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. (lg-size(lg-append(g1;g2)) = (lg-size(g1) + lg-size(g2)) ∈ ℤ)
Lemma: lg-size-nil
∀[T:Type]. ∀[g:LabeledGraph(T)]. uiff(lg-size(g) = 0 ∈ ℤ;g = lg-nil() ∈ LabeledGraph(T))
Lemma: lg-contains_antisymmetry
∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. (g1 = g2 ∈ LabeledGraph(T)) supposing (g2 ⊆ g1 and g1 ⊆ g2)
Definition: lg-filter
lg-filter(P;G) == let rms = filter(λi.(¬b(P (fst(G[i]))));upto(lg-size(G))) in reduce(λx,g. lg-remove(g;x);G;rms)
Lemma: lg-filter_wf
∀[T:Type]. ∀[P:T ─→ 𝔹]. ∀[G:LabeledGraph(T)]. (lg-filter(P;G) ∈ LabeledGraph(T))
Definition: make-lg
make-lg(L) == map(λx.<x, [], []>;L)
Lemma: make-lg_wf
∀[T:Type]. ∀[L:T List]. (make-lg(L) ∈ LabeledGraph(T))
Definition: lg-add
lg-add(g;a;b) ==
mklist(||g||;λi.let lbl,L1,L2 = g[i] in
<lbl
, if (i =z a) then if (i =z b) then <[i / L1], [i / L2]> else <L1, [b / L2]> fi
if (i =z b) then <[a / L1], L2>
else <L1, L2>
fi
>)
Lemma: lg-add_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[a,b:ℕlg-size(g)]. (lg-add(g;a;b) ∈ LabeledGraph(T))
Lemma: lg-size-add
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x,y:ℤ]. (lg-size(lg-add(g;x;y)) = lg-size(g) ∈ ℤ)
Definition: lg-in-edges
lg-in-edges(g;x) == fst(snd(g[x]))
Lemma: lg-in-edges_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)]. (lg-in-edges(g;x) ∈ ℕlg-size(g) List)
Definition: lg-out-edges
lg-out-edges(g;x) == snd(snd(g[x]))
Lemma: lg-out-edges_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)]. (lg-out-edges(g;x) ∈ ℕlg-size(g) List)
Definition: lg-edge
lg-edge(g;a;b) == (a ∈ lg-in-edges(g;b))
Lemma: lg-edge_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[a,b:ℕlg-size(g)]. (lg-edge(g;a;b) ∈ ℙ)
Lemma: lg-edge-remove
∀[T:Type]
∀g:LabeledGraph(T). ∀i:ℕlg-size(g). ∀a,b:ℕlg-size(g) - 1.
(lg-edge(lg-remove(g;i);a;b) ⇐⇒ lg-edge(g;if a <z i then a else a + 1 fi ;if b <z i then b else b + 1 fi ))
Lemma: lg-edge-add
∀[T:Type]
∀g:LabeledGraph(T). ∀i,j,a,b:ℕlg-size(g).
(lg-edge(lg-add(g;i;j);a;b) ⇐⇒ lg-edge(g;a;b) ∨ ((a = i ∈ ℤ) ∧ (b = j ∈ ℤ)))
Lemma: lg-edge-append
∀[T:Type]
∀g1,g2:LabeledGraph(T). ∀a,b:ℕlg-size(g1) + lg-size(g2).
(lg-edge(lg-append(g1;g2);a;b)
⇐⇒ (a < lg-size(g1) ∧ b < lg-size(g1) ∧ lg-edge(g1;a;b))
∨ ((lg-size(g1) ≤ a) ∧ (lg-size(g1) ≤ b) ∧ lg-edge(g2;a - lg-size(g1);b - lg-size(g1))))
Lemma: decidable__lg-edge
∀[T:Type]. ∀g:LabeledGraph(T). ∀a,b:ℕlg-size(g). Dec(lg-edge(g;a;b))
Definition: lg-connected
lg-connected(g;a;b) == a λx,y. lg-edge(g;x;y)+ b
Lemma: lg-connected_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[a,b:ℕlg-size(g)]. (lg-connected(g;a;b) ∈ ℙ)
Lemma: lg-edge-lg-connected
∀[T:Type]. ∀g:LabeledGraph(T). ∀a,b:ℕlg-size(g). (lg-edge(g;a;b) ⇒ lg-connected(g;a;b))
Lemma: lg-connected-remove
∀[T:Type]
∀g:LabeledGraph(T). ∀i:ℕlg-size(g). ∀a,b:ℕlg-size(g) - 1.
(lg-connected(lg-remove(g;i);a;b)
⇒ lg-connected(g;if a <z i then a else a + 1 fi ;if b <z i then b else b + 1 fi ))
Lemma: lg-connected_transitivity
∀[T:Type]. ∀g:LabeledGraph(T). ∀a,b,c:ℕlg-size(g). (lg-connected(g;a;b) ⇒ lg-connected(g;b;c) ⇒ lg-connected(g;a;c))
Definition: lg-acyclic
lg-acyclic(g) == ∀a:ℕlg-size(g). (¬lg-connected(g;a;a))
Lemma: lg-acyclic_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. (lg-acyclic(g) ∈ ℙ)
Lemma: lg-acyclic-remove
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[i:ℕlg-size(g)]. lg-acyclic(lg-remove(g;i)) supposing lg-acyclic(g)
Definition: lg-label
lg-label(g;x) == fst(g[x])
Lemma: lg-label_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)]. (lg-label(g;x) ∈ T)
Definition: lg-label2
lg-label2(g;x) == lg-label(g;x)
Lemma: lg-label2_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)]. (lg-label2(g;x) ∈ T)
Definition: lg-is-source
lg-is-source(g;i) == if i <z lg-size(g) then null(lg-in-edges(g;i)) else ff fi
Lemma: lg-is-source_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[i:ℕ]. (lg-is-source(g;i) ∈ 𝔹)
Lemma: assert-lg-is-source
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[i:ℕlg-size(g)]. uiff(↑lg-is-source(g;i);∀[j:ℕlg-size(g)]. (¬lg-edge(g;j;i)))
Lemma: lg-acyclic-has-source
∀[T:Type]. ∀g:LabeledGraph(T). (∃i:ℕlg-size(g). (↑lg-is-source(g;i))) supposing (lg-acyclic(g) and 0 < lg-size(g))
Lemma: lg-acyclic-well-founded
∀[T:Type]. ∀g:LabeledGraph(T). (lg-acyclic(g) ⇐⇒ SWellFounded(lg-edge(g;a;b)))
Definition: is-dag
is-dag(g) == ∀a,b:ℕlg-size(g). (lg-edge(g;a;b) ⇒ a < b)
Lemma: is-dag_wf
∀[T:Type]. ∀[g:LabeledGraph(T)]. (is-dag(g) ∈ ℙ)
Lemma: is-dag-append
∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. (is-dag(lg-append(g1;g2))) supposing (is-dag(g2) and is-dag(g1))
Lemma: is-dag-remove
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)]. is-dag(lg-remove(g;x)) supposing is-dag(g)
Lemma: is-dag-add
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[y:ℕlg-size(g)]. ∀[x:ℕy]. is-dag(lg-add(g;x;y)) supposing is-dag(g)
Definition: ldag
LabeledDAG(T) == {g:LabeledGraph(T)| is-dag(g)}
Lemma: ldag_wf
∀[T:Type]. (LabeledDAG(T) ∈ Type)
Lemma: continuous-ldag
∀[F:Type ─→ Type]. Continuous+(T.LabeledDAG(F[T])) supposing Continuous+(T.F[T])
Lemma: monotone-ldag
∀[F:Type ─→ Type]. Monotone(T.LabeledDAG(F[T])) supposing Monotone(T.F[T])
Lemma: subtype_rel-ldag
∀[A,B:Type]. LabeledDAG(A) ⊆r LabeledDAG(B) supposing A ⊆r B
Lemma: lg-append_wf_dag
∀[T:Type]. ∀[g1,g2:LabeledDAG(T)]. (lg-append(g1;g2) ∈ LabeledDAG(T))
Lemma: lg-remove_wf_dag
∀[T:Type]. ∀[g:LabeledDAG(T)]. ∀[x:ℕ]. (lg-remove(g;x) ∈ LabeledDAG(T))
Lemma: lg-add_wf_dag
∀[T:Type]. ∀[g:LabeledDAG(T)]. ∀[y:ℕlg-size(g)]. ∀[x:ℕy]. (lg-add(g;x;y) ∈ LabeledDAG(T))
Lemma: make-lg_wf_dag
∀[T:Type]. ∀[L:T List]. (make-lg(L) ∈ LabeledDAG(T))
Lemma: lg-is-source-wf_dag
∀[T:Type]. ∀[g:LabeledDAG(T)]. ∀[i:ℕ]. (lg-is-source(g;i) ∈ 𝔹)
Lemma: lg-label-wf_dag
∀[T:Type]. ∀[g:LabeledDAG(T)]. ∀[i:ℕlg-size(g)]. (lg-label(g;i) ∈ T)
Lemma: lg-size-wf_dag
∀[T:Type]. ∀[g:LabeledDAG(T)]. (lg-size(g) ∈ ℕ)
Definition: lg-map
lg-map(f;g) == map(λtr.let lbl,in,out = tr in <f lbl, in, out>;g)
Lemma: lg-map_wf
∀[T,S:Type]. ∀[f:T ─→ S]. ∀[g:LabeledGraph(T)]. (lg-map(f;g) ∈ LabeledGraph(S))
Lemma: lg-size-map
∀[T,S:Type]. ∀[f:T ─→ S]. ∀[g:LabeledGraph(T)]. (lg-size(lg-map(f;g)) = lg-size(g) ∈ ℤ)
Lemma: lg-edge-map
∀[T,S:Type]. ∀f:T ─→ S. ∀g:LabeledGraph(T). ∀a,b:ℕlg-size(g). (lg-edge(lg-map(f;g);a;b) ⇐⇒ lg-edge(g;a;b))
Lemma: is-dag-map
∀[T,S:Type]. ∀[f:T ─→ S]. ∀[g:LabeledGraph(T)]. is-dag(lg-map(f;g)) supposing is-dag(g)
Lemma: lg-map-wf_dag
∀[T,S:Type]. ∀[f:T ─→ S]. ∀[g:LabeledDAG(T)]. (lg-map(f;g) ∈ LabeledDAG(S))
Lemma: lg-label-map
∀[f:Top]. ∀[g:LabeledGraph(Top)]. ∀[x:ℕlg-size(g)]. (lg-label(lg-map(f;g);x) ~ f lg-label(g;x))
Lemma: lg-label-append
∀[T:Type]. ∀[g1,g2:LabeledGraph(T)]. ∀[x:ℕlg-size(lg-append(g1;g2))].
(lg-label(lg-append(g1;g2);x) ~ if x <z lg-size(g1) then lg-label(g1;x) else lg-label(g2;x - lg-size(g1)) fi )
Lemma: lg-label-remove
∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[k:ℕlg-size(g)]. ∀[x:ℕlg-size(g) - 1].
(lg-label(lg-remove(g;k);x) ~ if x <z k then lg-label(g;x) else lg-label(g;x + 1) fi )
Definition: lg-all
∀x∈G.P[x] == ∀n:ℕlg-size(G). P[lg-label(G;n)]
Lemma: lg-all_wf
∀[T:Type]. ∀[P:T ─→ ℙ]. ∀[G:LabeledGraph(T)]. (∀x∈G.P[x] ∈ ℙ)
Lemma: lg-all_functionality
∀[T:Type]. ∀G:LabeledDAG(T). ∀[P1,P2:T ─→ ℙ]. ((∀x:T. (P1[x] ⇒ P2[x])) ⇒ {∀x∈G.P1[x] ⇒ ∀x∈G.P2[x]})
Lemma: lg-all-wf_dag
∀[T:Type]. ∀[P:T ─→ ℙ]. ∀[G:LabeledDAG(T)]. (∀x∈G.P[x] ∈ ℙ)
Lemma: lg-nil_wf_dag
∀[T:Type]. (lg-nil() ∈ LabeledDAG(T))
Definition: lg-exists
lg-exists(G;x.P[x]) == ∃n:ℕlg-size(G). P[lg-label(G;n)]
Lemma: lg-exists_wf
∀[T:Type]. ∀[P:T ─→ ℙ]. ∀[G:LabeledGraph(T)]. (lg-exists(G;x.P[x]) ∈ ℙ)
Lemma: lg-all-append
∀[T:Type]. ∀[P:T ─→ ℙ]. ∀g1,g2:LabeledGraph(T). (∀x∈lg-append(g1;g2).P[x] ⇐⇒ ∀x∈g1.P[x] ∧ ∀x∈g2.P[x])
Lemma: lg-all-remove
∀[T:Type]. ∀[P:T ─→ ℙ]. ∀g:LabeledGraph(T). ∀x:ℕlg-size(g). (∀x∈g.P[x] ⇐⇒ ∀x∈lg-remove(g;x).P[x] ∧ P[lg-label(g;x)])
Lemma: lg-all-map
∀[A,T:Type]. ∀f:A ─→ T. ∀[P:T ─→ ℙ]. ∀g:LabeledGraph(A). (∀x∈lg-map(f;g).P[x] ⇐⇒ ∀x∈g.P[f x])
Definition: lg-search
lg-search(G;x.P[x]) == let s = search(lg-size(G);λn.P[lg-label(G;n)]) in if (s =z 0) then inr ⋅ else inl (s - 1) fi
Lemma: lg-search_wf
∀[T:Type]. ∀[G:LabeledGraph(T)]. ∀[P:T ─→ 𝔹]. (lg-search(G;x.P[x]) ∈ ℕlg-size(G)?)
Lemma: lg-search-property
∀[T:Type]. ∀G:LabeledGraph(T). ∀P:T ─→ 𝔹. (↑isl(lg-search(G;x.P[x])) ⇐⇒ lg-exists(G;x.↑P[x]))
Lemma: lg-search-minimal
∀[T:Type]. ∀[G:LabeledGraph(T)]. ∀[P:T ─→ 𝔹].
∀[n:ℕlg-size(G)]. outl(lg-search(G;x.P[x])) ≤ n supposing ↑P[lg-label(G;n)] supposing lg-exists(G;x.↑P[x])
Definition: norm-lg
norm-lg(N) == norm-list(norm-pair(N;norm-pair(norm-list(λx.x);norm-list(λx.x))))
Lemma: norm-lg_wf
∀[T:Type]. ∀[N:id-fun(T)]. (norm-lg(N) ∈ id-fun(LabeledGraph(T))) supposing value-type(T)
Definition: dataflow
dataflow(A;B) == corec(P.A ─→ (P × B))
Lemma: dataflow_wf
∀[A,B:Type]. (dataflow(A;B) ∈ Type)
Lemma: dataflow-valueall-type
∀[A:𝕌']. ∀[B:Type]. valueall-type(dataflow(A;B)) supposing ↓A
Lemma: dataflow-ext-eq
∀[A,B:Type]. dataflow(A;B) ≡ A ─→ (dataflow(A;B) × B)
Lemma: dataflow_subtype
∀[A1,B1,A2,B2:Type]. (dataflow(A1;B1) ⊆r dataflow(A2;B2)) supposing ((B1 ⊆r B2) and (A2 ⊆r A1))
Lemma: fix_wf_dataflow
∀[A,B:Type]. ∀[F:∩P:Type. (P ─→ A ─→ (P × B))]. (fix(F) ∈ dataflow(A;B))
Lemma: fix_wf_dataflow_w_state
∀[A,B,S:Type]. ∀[s0:S]. ∀[F:Top ─→ Top ─→ Top ∩ ∩P:Type. ((S ─→ P) ─→ S ─→ A ─→ (P × B))]. (fix(F) s0 ∈ dataflow(A;B))
Definition: stateless-dataflow
stateless-dataflow(m.f[m]) == fix((λstateless-dataflow,m. <stateless-dataflow, f[m]>))
Lemma: stateless-dataflow_wf
∀[A,B:Type]. ∀[f:A ─→ B]. (stateless-dataflow(m.f[m]) ∈ dataflow(A;B))
Definition: constant-dataflow
constant-dataflow(b) == stateless-dataflow(a.b)
Lemma: constant-dataflow_wf
∀[A,B:Type]. ∀[b:B]. (constant-dataflow(b) ∈ dataflow(A;B))
Definition: rec-dataflow
rec-dataflow(s0;s,m.next[s; m]) == fix((λrec-dataflow,s0,m. let s',ext = next[s0; m] in <rec-dataflow s', ext>)) s0
Lemma: rec-dataflow_wf
∀[S,A,B:Type]. ∀[s0:S]. ∀[next:S ─→ A ─→ (S × B)]. (rec-dataflow(s0;s,m.next[s;m]) ∈ dataflow(A;B))
Lemma: rec-dataflow_wf2
∀[S,A,B:Type ─→ Type].
(let Proc = corec(P.A[P] ─→ (P × B[P])) in
∀s0:S[Proc]. ∀next:∩T:{T:Type| Proc ⊆r T} . (S[A[T] ─→ (T × B[T])] ─→ A[T] ─→ (S[T] × B[T])).
(rec-dataflow(s0;s,m.next[s;m]) ∈ Proc)) supposing
(Continuous+(T.B[T]) and
Continuous+(T.A[T]) and
Continuous+(T.S[T]))
Definition: rec-dataflow-state
rec-dataflow-state(s0;s,m.next[s; m];L) ==
accumulate (with value s and list item m):
fst(next[s; m])
over list:
L
with starting value:
s0)
Lemma: rec-dataflow-state_wf
∀[S,A,B:Type]. ∀[s0:S]. ∀[next:S ─→ A ─→ (S × B)]. ∀[L:A List]. (rec-dataflow-state(s0;s,m.next[s;m];L) ∈ S)
Definition: dataflow-ap
df(a) == df a
Lemma: dataflow-ap_wf
∀[A,B:Type]. ∀[df:dataflow(A;B)]. ∀[a:A]. (df(a) ∈ dataflow(A;B) × B)
Lemma: rec_dataflow_ap_lemma
∀a,next,s0:Top. (rec-dataflow(s0;s,a.next[s;a])(a) ~ let s',b = next[s0;a] in <rec-dataflow(s';s,a.next[s;a]), b>)
Lemma: stateless_dataflow_ap_lemma
∀a,f:Top. (stateless-dataflow(a.f[a])(a) ~ <stateless-dataflow(a.f[a]), f[a]>)
Definition: dataflow-out
dataflow-out(df;a) == snd(df(a))
Lemma: dataflow-out_wf
∀[A,B:Type]. ∀[df:dataflow(A;B)]. ∀[a:A]. (dataflow-out(df;a) ∈ B)
Lemma: const_df_ap_lemma
∀a,b:Top. (constant-dataflow(b)(a) ~ <constant-dataflow(b), b>)
Definition: iterate-dataflow
P*(inputs) == accumulate (with value p and list item input): fst(p(input))over list: inputswith starting value: P)
Lemma: iterate-dataflow_wf
∀[A,B:Type]. ∀[P:dataflow(A;B)]. ∀[inputs:A List]. (P*(inputs) ∈ dataflow(A;B))
Lemma: iter_df_nil_lemma
∀P:Top. (P*([]) ~ P)
Lemma: iter_df_cons_lemma
∀as,a,P:Top. (P*([a / as]) ~ fst(P(a))*(as))
Lemma: iterate-dataflow-append
∀[as1:Top List]. ∀[as2,P:Top]. (P*(as1 @ as2) ~ P*(as1)*(as2))
Lemma: iterate-rec-dataflow
∀[S,A,B:Type]. ∀[next:S ─→ A ─→ (S × B)]. ∀[L:A List]. ∀[s0:S].
(rec-dataflow(s0;s,m.next[s;m])*(L) ~ rec-dataflow(rec-dataflow-state(s0;s,m.next[s;m];L);s,m.next[s;m]))
Definition: data-stream
data-stream(P;L) == map(λi.(snd(P*(firstn(i;L))(L[i])));upto(||L||))
Lemma: data-stream_wf
∀[A,B:Type]. ∀[L:A List]. ∀[P:dataflow(A;B)]. (data-stream(P;L) ∈ B List)
Lemma: data_stream_nil_lemma
∀P:Top. (data-stream(P;[]) ~ [])
Lemma: data-stream-cons
∀[L:Top List]. ∀[a,P:Top]. (data-stream(P;[a / L]) ~ [snd(P(a)) / data-stream(fst(P(a));L)])
Lemma: length-data-stream
∀[L:Top List]. ∀[P:Top]. (||data-stream(P;L)|| ~ ||L||)
Lemma: null-data-stream
∀[L:Top List]. ∀[P:Top]. (null(data-stream(P;L)) ~ null(L))
Lemma: data-stream-append
∀[as1,as2:Top List]. ∀[P:Top]. (data-stream(P;as1 @ as2) ~ data-stream(P;as1) @ data-stream(P*(as1);as2))
Lemma: firstn-data-stream
∀[n:ℕ]. ∀[L:Top List]. ∀[P:Top]. (firstn(n;data-stream(P;L)) ~ data-stream(P;firstn(n;L)))
Lemma: select-data-stream
∀[L:Top List]. ∀[P:Top]. ∀[i:ℕ]. (data-stream(P;L)[i] ~ if i <z ||L|| then snd(P*(firstn(i;L))(L[i])) else ⊥ fi )
Lemma: last-data-stream
∀[L:Top List]. ∀[P:Top]. (last(data-stream(P;L)) ~ if null(L) then ⊥ else snd(P*(firstn(||L|| - 1;L))(last(L))) fi )
Lemma: iterate-stateless-dataflow
∀[L:Top List]. ∀[f:Top ─→ Top]. (stateless-dataflow(m.f[m])*(L) ~ stateless-dataflow(m.f[m]))
Lemma: iterate-constant-dataflow
∀[L:Top List]. ∀[b:Top]. (constant-dataflow(b)*(L) ~ constant-dataflow(b))
Lemma: constant-data-stream
∀[L:Top List]. ∀[b:Top]. (data-stream(constant-dataflow(b);L) ~ map(λi.b;upto(||L||)))
Definition: dataflow-equiv
d1 ≡ d2 == ∀as:A List. (data-stream(d1;as) = data-stream(d2;as) ∈ (B List))
Lemma: dataflow-equiv_wf
∀[A,B:Type]. ∀[f,g:dataflow(A;B)]. (f ≡ g ∈ ℙ)
Lemma: dataflow-equiv_weakening
∀[A,B:Type]. ∀[f,g:dataflow(A;B)]. f ≡ g supposing f = g ∈ dataflow(A;B)
Lemma: dataflow-equiv_transitivity
∀[A,B:Type]. ∀[f,g,h:dataflow(A;B)]. (f ≡ h) supposing (f ≡ g and g ≡ h)
Lemma: dataflow-equiv_inversion
∀[A,B:Type]. ∀[f,g:dataflow(A;B)]. g ≡ f supposing f ≡ g
Comment: process model notes
This version of the process model is based on the CSL paper.
We will have a parameter M for constructing process input messages
(see pMsg).
We will also need two parameters, nat_to_msg and loc_to_msg.
The "commands" in transit will have four kinds:
interprocess messages, creation messages, choose number messages,
and new loc messages. We define the type of commands as a tagged union.
see Com.
When a process outputs some commands, it addresses each of them to a
particular location (so each has the type ⌈Id × (Com(P.M[P]) P)⌉)
and it may add precedence constraints between them.
So the output forms a "labeled graph", where an edge <x,c1> -> <y,c2>
means that the environment may not choose and act on <y,c2> until
after it has chosen and acted on <x,c1>.
Thus, we define ⌈Process(P.M[P])⌉ to be ⌈process(P.M[P];P.LabeledGraph(Id × (Com(P.M[P]) P)))⌉
pMsg(M) = M[Process(P.M[P])]
pCom(M) = Com(P.M[P]) Process(P.M[P])
pExt(M) = LabeledGraph(Id × pCom(P.M[P])).
A system is a list of labelled processes (components) together with
a graph of commands in transit.
A command in transit will be marked with the "event" that generated it.
Such an event is a pair ⌈ℤ × Id⌉ of a time and a location.
Thus we define
pInTransit(M) = ⌈ℤ × Id × Id × pCom(P.M[P])⌉
component(M) = Id x Process(M)
System(M) = component(P.M[P]) List × LabeledGraph(pInTransit(P.M[P]))
A choice is a triple (n,m,x) of two natural numbers and a location.
If the nth node of the intransit graph G has no predecessors, then
we act on the choice by getting the label <ev, to ,com> of the nth node,
and removing the nth node to get new graph G'.
If com is "msg",ms then deliver (to,ms) to all the components.
If com is "create",P then add a new component <x,P>.
If com is "choose",z then deliver (to, nat2msg(m)) to all the components.
If com is "new" then deliver (to, loc2msg(x)) to all the components
The details are in the definition do-chosen-command.
This lets us define a run of a system: Error :pRun-def
Since processes are only reactive, nothing will happen in a run unless
there are some commands in transit initially. So the initial intransit graph
G of the initial system should be non-empty.
For each run, r, we can define the events runEvents in that run,
and a location function run-event-loc and causal ordering run-lt
on the events.
These satisfy the axioms of an event-ordering Error :event_ordering
and by defining the information associated with each event in the run to be
the message delivered at that event, run-event-msg, we get an
extended-event-ordering: event-ordering+.
The full construction of the extended event ordering of a run of a system
S in environment env is given in the definition of runEO.
To guarantee the well-foundedness of the causal ordering, we need an extra
assumption, run-initialization, that relates the run with its initial
intransit graph G. Under this assumption, the proof of Error :runEO_wf, shows how we construct the extended event ordering.
The extra assumption can easily be guaranteed by using the
"standard" initial assumption, std-initial, that says that in the
intial intransit graph, all commands have a "cause" event with time = (-1).
⋅
Definition: Com
Com(P.M[P]) == λP."msg":M[P] |+ "create":P |+ "choose":Id |+ "new":Unit
Lemma: Com_wf
∀[M:Type ─→ Type]. (Com(P.M[P]) ∈ Type ─→ Type)
Lemma: Com-subtype
∀[M:Type ─→ Type]
∀[A,B:Type]. (Com(P.M[P]) A) ⊆r (Com(P.M[P]) B) supposing A ⊆r B supposing ∀A,B:Type. ((A ⊆r B) ⇒ (M[A] ⊆r M[B]))
Definition: Process
Process(P.M[P]) == process(P.M[P];P.LabeledDAG(Id × (Com(P.M[P]) P)))
Lemma: Process_wf
∀[M:Type ─→ Type]. (Process(P.M[P]) ∈ Type)
Lemma: Process-value-type
∀[M:Type ─→ Type]. value-type(Process(P.M[P])) supposing M[Top]
Definition: pMsg
pMsg(P.M[P]) == M[Process(P.M[P])]
Lemma: pMsg_wf
∀[M:Type ─→ Type]. (pMsg(P.M[P]) ∈ Type)
Definition: pCom
pCom(P.M[P]) == Com(P.M[P]) Process(P.M[P])
Lemma: pCom_wf
∀[M:Type ─→ Type]. (pCom(P.M[P]) ∈ Type)
Lemma: mk-tagged_wf_pCom_msg
∀[M:Type ─→ Type]
∀[Q:Type]. ∀[m:pMsg(T.M[T])]. (mk-tagged("msg";m) ∈ Com(P.M[P]) Q) supposing Process(P.M[P]) ⊆r Q
supposing Monotone(T.M[T])
Lemma: mk-tagged_wf_pCom_choose
∀[M:Type ─→ Type]
∀[Q:Type]. ∀[m:Id]. (mk-tagged("choose";m) ∈ Com(P.M[P]) Q) supposing Process(P.M[P]) ⊆r Q supposing Monotone(T.M[T])
Lemma: mk-tagged_wf_pCom_new
∀[M:Type ─→ Type]
∀[Q:Type]. ∀[m:Unit]. (mk-tagged("new";m) ∈ Com(P.M[P]) Q) supposing Process(P.M[P]) ⊆r Q supposing Monotone(T.M[T])
Lemma: mk-tagged_wf_pCom_create
∀[M:Type ─→ Type]
∀[Q:Type]. ∀[P:Process(T.M[T])]. (mk-tagged("create";P) ∈ Com(P.M[P]) Q) supposing Process(P.M[P]) ⊆r Q
supposing Monotone(T.M[T])
Definition: com-kind
com-kind(c) == c.tag
Lemma: com-kind_wf
∀[M:Type ─→ Type]. ∀[c:pCom(P.M[P])]. (com-kind(c) ∈ Atom)
Definition: comm-msg
comm-msg(c) == c.val
Lemma: comm-msg_wf
∀[M:Type ─→ Type]. ∀[c:pCom(P.M[P])]. comm-msg(c) ∈ pMsg(P.M[P]) supposing com-kind(c) = "msg" ∈ Atom
Definition: comm-create
comm-create(c) == c.val
Lemma: comm-create_wf
∀[M:Type ─→ Type]. ∀[c:pCom(P.M[P])]. comm-create(c) ∈ Process(P.M[P]) supposing com-kind(c) = "create" ∈ Atom
Definition: pExt
pExt(P.M[P]) == LabeledDAG(Id × pCom(P.M[P]))
Lemma: pExt_wf
∀[M:Type ─→ Type]. (pExt(P.M[P]) ∈ Type)
Lemma: rec-process_wf_Process
∀[S,M:Type ─→ Type].
(∀[s0:S[Process(T.M[T])]]. ∀[next:∩T:{T:Type| Process(T.M[T]) ⊆r T}
(S[M[T] ─→ (T × LabeledDAG(Id × (Com(T.M[T]) T)))]
─→ M[T]
─→ (S[T] × LabeledDAG(Id × (Com(T.M[T]) T))))].
(RecProcess(s0;s,m.next[s;m]) ∈ Process(T.M[T]))) supposing
(Continuous+(T.M[T]) and
Continuous+(T.S[T]))
Definition: Process-apply
Process-apply(P;m) == P m
Lemma: Process-apply_wf
∀[M:Type ─→ Type]
∀[P:Process(P.M[P])]. ∀[m:pMsg(P.M[P])]. (Process-apply(P;m) ∈ Process(P.M[P]) × pExt(P.M[P]))
supposing Continuous+(P.M[P])
Definition: iterate-Process
iterate-Process(P;msgs) == P*(msgs)
Lemma: iterate-Process_wf
∀[M:Type ─→ Type]
∀[msgs:pMsg(P.M[P]) List]. ∀[P:Process(P.M[P])]. (iterate-Process(P;msgs) ∈ Process(P.M[P]))
supposing Continuous+(P.M[P])
Definition: Process-stream
Process-stream(P;msgs) == data-stream(P;msgs)
Lemma: Process-stream_wf
∀[M:Type ─→ Type]
∀[msgs:pMsg(P.M[P]) List]. ∀[P:Process(P.M[P])]. (Process-stream(P;msgs) ∈ pExt(P.M[P]) List)
supposing Continuous+(P.M[P])
Definition: process-equiv
P≡Q == ∀msgs:pMsg(P.M[P]) List. (Process-stream(P;msgs) = Process-stream(Q;msgs) ∈ (pExt(P.M[P]) List))
Lemma: process-equiv_wf
∀[M:Type ─→ Type]. ∀[P,Q:Process(T.M[T])]. (P≡Q ∈ ℙ) supposing Continuous+(T.M[T])
Lemma: process-equiv-is-equiv
∀[M:Type ─→ Type]. EquivRel(Process(T.M[T]);P,Q.P≡Q) supposing Continuous+(T.M[T])
Definition: dataflow-to-Process
dataflow-to-Process(F;g) == RecProcess(F;s,m.let s',x = s(m) in <s', g x>)
Lemma: dataflow-to-Process_wf
∀[A,B:Type]. ∀[F:dataflow(A;B)]. ∀[g:B ─→ LabeledDAG(Id × (Com(P.A) Process(P.A)))].
(dataflow-to-Process(
F;
g) ∈ Process(P.A))
Lemma: datastream-dataflow-to-Process
∀[A,B:Type]. ∀[g:B ─→ LabeledDAG(Id × (Com(P.A) Process(P.A)))]. ∀[L:A List]. ∀[F:dataflow(A;B)].
(data-stream(dataflow-to-Process(
F;
g);L) ~ map(g;data-stream(F;L)))
Lemma: dataflow-to-Process_functionality
∀[A,B:Type]. ∀[F1,F2:dataflow(A;B)]. ∀[g:B ─→ LabeledDAG(Id × (Com(P.A) Process(P.A)))].
dataflow-to-Process(F1;g)≡dataflow-to-Process(F2;g) supposing F1 ≡ F2
Definition: component
component(P.M[P]) == Id × Process(P.M[P])
Lemma: component_wf
∀[M:Type ─→ Type]. (component(P.M[P]) ∈ Type)
Definition: component-loc
component-loc(c) == fst(c)
Lemma: component-loc_wf
∀[M:Type ─→ Type]. ∀[c:component(P.M[P])]. (component-loc(c) ∈ Id)
Definition: component-process
component-process(c) == snd(c)
Lemma: component-process_wf
∀[M:Type ─→ Type]. ∀[c:component(P.M[P])]. (component-process(c) ∈ Process(P.M[P]))
Lemma: component-has-value
∀[M:Type ─→ Type]. value-type(component(P.M[P]))
Definition: norm-component
norm-component == norm-pair(λx.x;λx.x)
Lemma: norm-component_wf
∀[M:Type ─→ Type]. norm-component ∈ id-fun(component(P.M[P])) supposing M[Top]
Definition: norm-components
norm-components == norm-list(norm-component)
Lemma: norm-components_wf
∀[M:Type ─→ Type]. norm-components ∈ id-fun(component(P.M[P]) List) supposing M[Top]
Definition: pInTransit
pInTransit(P.M[P]) == ℤ × Id × Id × pCom(P.M[P])
Lemma: pInTransit_wf
∀[M:Type ─→ Type]. (pInTransit(P.M[P]) ∈ Type)
Definition: norm-intransit
norm-intransit(intr) ==
let ev,x,com = intr in
let t,z = ev
in eval t' = t in
eval z' = z in
eval x' = x in
eval com' = com in
<<t', z'>, x', com'>
Lemma: norm-intransit_wf
∀[M:Type ─→ Type]. ∀[intr:pInTransit(P.M[P])].
(norm-intransit(intr) ∈ {intr':pInTransit(P.M[P])| intr' = intr ∈ pInTransit(P.M[P])} )
Definition: System
System(P.M[P]) == component(P.M[P]) List × LabeledDAG(pInTransit(P.M[P]))
Lemma: System_wf
∀[M:Type ─→ Type]. (System(P.M[P]) ∈ Type)
Definition: system-equiv
system-equiv(T.M[T];S1;S2) ==
let Cs1,G1 = S1
in let Cs2,G2 = S2
in (G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P])))
∧ (||Cs1|| = ||Cs2|| ∈ ℤ)
∧ (∀k:ℕ||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z ∈ Id) ∧ P≡Q)
Lemma: system-equiv_wf
∀[M:Type ─→ Type]. ∀[S1,S2:System(P.M[P])]. (system-equiv(P.M[P];S1;S2) ∈ ℙ) supposing Continuous+(P.M[P])
Lemma: system-equiv-implies-equal
∀[M:Type ─→ Type]
∀[S1,S2:System(P.M[P])]. S1 = S2 ∈ (Top × LabeledDAG(pInTransit(P.M[P]))) supposing system-equiv(P.M[P];S1;S2)
supposing Continuous+(P.M[P])
Lemma: system-equiv-is-equiv
∀[M:Type ─→ Type]. EquivRel(System(P.M[P]);S1,S2.system-equiv(P.M[P];S1;S2)) supposing Continuous+(P.M[P])
Definition: system-fpf
system-fpf(S) ==
let Cs,G = S
in let dom = remove-repeats(IdDeq;map(λp.(fst(p));Cs) @ map(λnd.(snd(fst(fst(nd))));G)) in
mkfpf(dom;λx.<mapfilter(λc.(snd(c));λc.fst(c) = x;Cs), lg-filter(λtr.snd(fst(tr)) = x;G)>)
Lemma: system-fpf_wf
∀[M:Type ─→ Type]. ∀[S:System(P.M[P])].
(system-fpf(S) ∈ x:Id fp-> Process(P.M[P]) List × LabeledGraph(pInTransit(P.M[P])))
Definition: system-function
system-function(S) == λx.system-fpf(S)(x)?<[], []>
Lemma: system-function_wf
∀[M:Type ─→ Type]. ∀[S:System(P.M[P])].
(system-function(S) ∈ Id ─→ (Process(P.M[P]) List × LabeledGraph(pInTransit(P.M[P]))))
Definition: norm-system
norm-system == norm-pair(norm-components;norm-lg(λx.x))
Lemma: norm-system_wf
∀[M:Type ─→ Type]. norm-system ∈ id-fun(System(P.M[P])) supposing M[Top]
Definition: add-cause
add-cause(ev;ext) == lg-map(λx.<ev, x>;ext)
Lemma: add-cause_wf
∀[M:Type ─→ Type]. ∀[ev:ℕ × Id]. ∀[ext:pExt(P.M[P])]. (add-cause(ev;ext) ∈ LabeledDAG(pInTransit(P.M[P])))
Definition: deliver-msg-to-comp
deliver-msg-to-comp(t;m;x;S;C) ==
let Cs,L = S
in let z,P = C
in if z = x then let Q,ext = Process-apply(P;m) in <[<z, Q> / Cs], lg-append(L;add-cause(<t, x>;ext))> else <[C / C\000Cs], L> fi
Lemma: deliver-msg-to-comp_wf
∀[M:Type ─→ Type]
∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[S:System(P.M[P])]. ∀[C:component(P.M[P])].
(deliver-msg-to-comp(t;m;x;S;C) ∈ System(P.M[P]))
supposing Continuous+(P.M[P])
Definition: deliver-msg
deliver-msg(t;m;x;Cs;L) ==
accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
Cs
with starting value:
<[], L>)
Lemma: deliver-msg_wf
∀[M:Type ─→ Type]
∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[L:LabeledDAG(pInTransit(P.M[P]))]. ∀[Cs:component(P.M[P]) List].
(deliver-msg(t;m;x;Cs;L) ∈ System(P.M[P]))
supposing Continuous+(P.M[P])
Lemma: deliver-msg_functionality
∀[M:Type ─→ Type]
∀t:ℕ. ∀x:Id. ∀m:pMsg(P.M[P]). ∀G1,G2:LabeledDAG(pInTransit(P.M[P])). ∀Cs1,Cs2:component(P.M[P]) List.
((∀k:ℕ||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z ∈ Id) ∧ P≡Q)
⇒ (system-equiv(P.M[P];deliver-msg(t;m;x;Cs1;G1);deliver-msg(t;m;x;Cs2;G2))
∧ (deliver-msg(t;m;x;Cs1;G1)
= deliver-msg(t;m;x;Cs2;G2)
∈ (Top × LabeledDAG(pInTransit(P.M[P])))))) supposing
((||Cs1|| = ||Cs2|| ∈ ℤ) and
(G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))))
supposing Continuous+(P.M[P])
Lemma: lg-size-deliver-msg-general
∀[M:Type ─→ Type]
∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[Cs,X:component(P.M[P]) List]. ∀[G:LabeledDAG(pInTransit(P.M[P]))].
(lg-size(G) ≤ lg-size(snd(accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
Cs
with starting value:
<X, G>))))
supposing Continuous+(P.M[P])
Lemma: lg-size-deliver-msg
∀[M:Type ─→ Type]
∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[Cs:component(P.M[P]) List]. ∀[G:LabeledDAG(pInTransit(P.M[P]))].
(lg-size(G) ≤ lg-size(snd(deliver-msg(t;m;x;Cs;G))))
supposing Continuous+(P.M[P])
Lemma: lg-label-deliver-msg
∀[M:Type ─→ Type]
∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[Cs:component(P.M[P]) List]. ∀[G:LabeledDAG(pInTransit(P.M[P]))].
∀[i:ℕlg-size(G)].
(lg-label(snd(deliver-msg(t;m;x;Cs;G));i) = lg-label(G;i) ∈ pInTransit(P.M[P]))
supposing Continuous+(P.M[P])
Definition: create-component
create-component(t;P;x;Cs;L) == <[<x, P> / Cs], L>
Lemma: create-component_wf
∀[M:Type ─→ Type]. ∀[t:ℕ]. ∀[x:Id]. ∀[P:Process(P.M[P])]. ∀[L:LabeledDAG(pInTransit(P.M[P]))].
∀[Cs:component(P.M[P]) List].
(create-component(t;P;x;Cs;L) ∈ System(P.M[P]))
Definition: do-chosen-command
do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm) ==
let Cs,G = S
in if lg-is-source(G;n)
then let ev,x,c = lg-label(G;n) in
let G' = lg-remove(G;n) in
if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x, ms>, deliver-msg(t;ms;x;Cs;G')>
if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x;Cs;G')>
if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x, ms>, deliver-msg(t;ms;x;Cs;G')>
if com-kind(c) =a "new" then let ms = loc2msg nm in <inl <ev, x, ms>, deliver-msg(t;ms;x;Cs;G')>
else <inr ⋅ , Cs, G'>
fi
else <inr ⋅ , S>
fi
Lemma: do-chosen-command_wf
∀[M:Type ─→ Type]
∀[nat2msg:ℕ ─→ pMsg(P.M[P])]. ∀[loc2msg:Id ─→ pMsg(P.M[P])]. ∀[S:System(P.M[P])]. ∀[t,n,m:ℕ]. ∀[nm:Id].
(do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm) ∈ ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
supposing Continuous+(P.M[P])
Definition: pRunInfo
pRunInfo(P.M[P]) == ℤ × Id × Id × pMsg(P.M[P])?
Lemma: pRunInfo_wf
∀[M:Type ─→ Type]. (pRunInfo(P.M[P]) ∈ Type)
Definition: fulpRunType
fulpRunType(T.M[T]) == ℕ ─→ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
Lemma: fulpRunType_wf
∀[M:Type ─→ Type]. (fulpRunType(T.M[T]) ∈ Type)
Definition: pRunType
pRunType(T.M[T]) == ℕ ─→ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))
Lemma: pRunType_wf
∀[M:Type ─→ Type]. (pRunType(T.M[T]) ∈ Type)
Lemma: fulpRunType-subtype
∀[M:Type ─→ Type]. (fulpRunType(T.M[T]) ⊆r pRunType(T.M[T]))
Definition: norm-runinfo
norm-runinfo(info) ==
case info
of inl(tr) =>
let ev,x,ms = tr in
let t,z = ev
in eval t' = t in
eval z' = z in
eval x' = x in
eval ms' = ms in
inl <<t', z'>, x', ms'>
| inr(z) =>
inr ⋅
Lemma: norm-runinfo_wf
∀[M:Type ─→ Type]
∀[info:pRunInfo(P.M[P])]. (norm-runinfo(info) ∈ {info':pRunInfo(P.M[P])| info' = info ∈ pRunInfo(P.M[P])} )
supposing ∀P:Type. value-type(M[P])
Definition: pEnvType
pEnvType(T.M[T]) ==
t:ℕ+ ─→ (ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))) ─→ (ℕ × ℕ × Id)
Lemma: pEnvType_wf
∀[M:Type ─→ Type]. (pEnvType(T.M[T]) ∈ Type)
Definition: pRun
pRun(S0;env;nat2msg;loc2msg) ==
Y
(λpRun,t. if (t =z 0)
then <inr ⋅ , S0>
else let n,m,nm = env t pRun in
do-chosen-command(nat2msg;loc2msg;t;snd((pRun (t - 1)));n;m;nm)
fi )
Lemma: pRun_wf
∀[M:Type ─→ Type]
∀[nat2msg:ℕ ─→ pMsg(P.M[P])]. ∀[loc2msg:Id ─→ pMsg(P.M[P])]. ∀[S0:System(P.M[P])]. ∀[env:pEnvType(P.M[P])].
(pRun(S0;env;nat2msg;loc2msg) ∈ fulpRunType(P.M[P]))
supposing Continuous+(P.M[P])
Lemma: pRun_wf2
∀[M:Type ─→ Type]
∀[nat2msg:ℕ ─→ pMsg(P.M[P])]. ∀[loc2msg:Id ─→ pMsg(P.M[P])]. ∀[S0:System(P.M[P])]. ∀[env:pEnvType(P.M[P])].
(pRun(S0;env;nat2msg;loc2msg) ∈ pRunType(P.M[P]))
supposing Continuous+(P.M[P])
Lemma: pRun_functionality
∀[M:Type ─→ Type]
∀[nat2msg:ℕ ─→ pMsg(P.M[P])]. ∀[loc2msg:Id ─→ pMsg(P.M[P])]. ∀[env:pEnvType(P.M[P])]. ∀[S1,S2:System(P.M[P])].
pRun(S1;env;nat2msg;loc2msg) = pRun(S2;env;nat2msg;loc2msg) ∈ pRunType(P.M[P]) supposing system-equiv(P.M[P];S1;S2)
supposing Continuous+(P.M[P])
Definition: pRun2
pRun2(S0;env;nat2msg;loc2msg;t) ==
Y
(λpRun2,t. if (t =z 0)
then eval S = norm-system S0 in
[<inr ⋅ , S>]
else eval r = pRun2 (t - 1) in
eval nxt = let info,S = let n,m,nm = env t (λi.r[i]) in
do-chosen-command(nat2msg;loc2msg;t;snd(last(r));n;m;nm)
in eval info' = norm-runinfo(info) in
eval S' = norm-system S in
<info', S'> in
r @ [nxt]
fi )
t
Lemma: pRun2_wf
∀[M:Type ─→ Type]
(∀[nat2msg:ℕ ─→ pMsg(P.M[P])]. ∀[loc2msg:Id ─→ pMsg(P.M[P])]. ∀[S0:System(P.M[P])]. ∀[env:pEnvType(P.M[P])]. ∀[t:ℕ].
(pRun2(S0;env;nat2msg;loc2msg;t) ∈ {L:(ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) List| ||L|| = (t + 1) ∈ ℤ} )) \000Csupposing
(Continuous+(P.M[P]) and
(∀P:Type. value-type(M[P])) and
M[Top])
Definition: run-system
run-system(r;t) == snd((r (t - 1)))
Lemma: run-system_wf
∀[M:Type ─→ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[t:ℕ+]. (run-system(r;t) ∈ System(P.M[P]))
Definition: run-intransit
run-intransit(r;t) == snd(run-system(r;t))
Lemma: run-intransit_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+]. (run-intransit(r;t) ∈ LabeledDAG(pInTransit(P.M[P])))
Lemma: pRun-System-invariant
∀[M:Type ─→ Type]
∀[Q:ℕ ─→ System(P.M[P]) ─→ ℙ]
∀nat2msg:ℕ ─→ pMsg(P.M[P]). ∀loc2msg:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]).
(Q[0;S0]
⇒ (∀t:ℕ. ∀S:System(P.M[P]).
(Q[t;S]
⇒ (∀env:pEnvType(P.M[P])
let n,m,nm = env (t + 1) pRun(S0;env;nat2msg;loc2msg) in
Q[t + 1;snd(do-chosen-command(nat2msg;loc2msg;t + 1;S;n;m;nm))])))
⇒ {∀env:pEnvType(P.M[P]). ∀t:ℕ. Q[t;snd((pRun(S0;env;nat2msg;loc2msg) t))]})
supposing Continuous+(P.M[P])
Definition: is-run-event
is-run-event(r;t;x) == let info,S = r t in isl(info) ∧b let ev,z,m = outl(info) in x = z
Lemma: is-run-event_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ]. ∀[x:Id]. (is-run-event(r;t;x) ∈ 𝔹)
Definition: run-info
run-info(r;e) == let t,x = e in let info,S = r t in let ev,z,m = outl(info) in <ev, m>
Definition: runEvents
runEvents(r) == {tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}
Lemma: runEvents_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. (runEvents(r) ∈ Type)
Lemma: run-info_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)]. (run-info(r;e) ∈ ℤ × Id × pMsg(P.M[P]))
Definition: run-event-msg
run-event-msg(r;e) == snd(run-info(r;e))
Lemma: run-event-msg_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)]. (run-event-msg(r;e) ∈ pMsg(P.M[P]))
Definition: run-event-state
run-event-state(r;e) == let t,x = e in let info,Cs,G = r t in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
Lemma: run-event-state_wf
∀[M:Type ─→ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[e:runEvents(r)]. (run-event-state(r;e) ∈ Process(P.M[P]) List)
Definition: run-event-state-when
run-event-state-when(r;e) == let t,x = e in let info,Cs,G = r (t - 1) in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
Lemma: run-event-state-when_wf
∀[M:Type ─→ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[e:ℕ+ × Id]. (run-event-state-when(r;e) ∈ Process(P.M[P]) List)
Definition: run-event-in-transit
run-event-in-transit(r;e) == let t,x = e in let info,Cs,G = r t in G
Lemma: run-event-in-transit_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)].
(run-event-in-transit(r;e) ∈ LabeledGraph(pInTransit(P.M[P])))
Lemma: decidable__equal_runEvents
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀e1,e2:runEvents(r). Dec(e1 = e2 ∈ runEvents(r))
Definition: deq-runEvents-witness
deq-runEvents-witness() ==
λe1,e2. let a,y1 = e2
in let a1,x1 = e1
in if a=a1 then if x1=2 y1 then inl Ax else (inr (λ%6.Ax) ) else (inr (λ%6.Ax) )
Lemma: deq-runEvents-witness_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. (deq-runEvents-witness() ∈ ∀e1,e2:runEvents(r). Dec(e1 = e2 ∈ runEvents(r)))
Definition: run-event-loc
run-event-loc(e) == snd(e)
Lemma: run-event-loc_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)]. (run-event-loc(e) ∈ Id)
Definition: run-event-step
run-event-step(e) == fst(e)
Lemma: run-event-step_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)]. (run-event-step(e) ∈ ℕ)
Lemma: run-event-step-positive
∀[M:Type ─→ Type]
∀[S0:System(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[env:pEnvType(P.M[P])].
∀[e:runEvents(pRun(S0;env;n2m;l2m))].
0 < run-event-step(e)
supposing Continuous+(P.M[P])
Definition: run-event-interval
run-event-interval(r;e1;e2) ==
let x = run-event-loc(e1) in
mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[run-event-step(e1), run-event-step(e2) + 1))
Lemma: run-event-interval_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e1,e2:runEvents(r)]. (run-event-interval(r;e1;e2) ∈ runEvents(r) List)
Lemma: member-run-event-interval
∀[M:Type ─→ Type]
∀r:pRunType(P.M[P]). ∀e1,e2,e:runEvents(r).
((e ∈ run-event-interval(r;e1;e2))
⇐⇒ (run-event-loc(e) = run-event-loc(e1) ∈ Id)
∧ (run-event-step(e1) ≤ run-event-step(e))
∧ (run-event-step(e) ≤ run-event-step(e2)))
Definition: run-event-history
run-event-history(r;e) ==
let x = run-event-loc(e) in
mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, run-event-step(e)))
Lemma: run-event-history_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)]. (run-event-history(r;e) ∈ runEvents(r) List)
Definition: run-event-local-pred
run-event-local-pred(r;e) == if null(run-event-history(r;e)) then inr ⋅ else inl last(run-event-history(r;e)) fi
Lemma: run-event-local-pred_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)]. (run-event-local-pred(r;e) ∈ runEvents(r)?)
Definition: run-prior-state
run-prior-state(S0;r;e) ==
case run-event-local-pred(r;e)
of inl(e') =>
run-event-state(r;e')
| inr(x) =>
mapfilter(λc.(snd(c));λc.fst(c) = run-event-loc(e);fst(S0))
Lemma: run-prior-state_wf
∀[M:Type ─→ Type]. ∀[S0:System(P.M[P])]. ∀[r:fulpRunType(P.M[P])]. ∀[e:ℕ × Id].
(run-prior-state(S0;r;e) ∈ Process(P.M[P]) List)
Lemma: run-prior-state-property
∀[M:Type ─→ Type]
∀S0:System(P.M[P]). ∀r:fulpRunType(P.M[P]).
∀n:ℕ. ∀x:Id.
∃m:ℕn
((run-prior-state(S0;r;<n, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(P.M[P]\000C) List))
∧ (∀t:{m + 1..n-}. (¬↑is-run-event(r;t;x))))
supposing 0 < n
supposing (r 0) = <inr ⋅ , S0> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
Lemma: run-event-cases
∀[M:Type ─→ Type]
∀S0:System(P.M[P]). ∀r:pRunType(P.M[P]). ∀e1,e2:runEvents(r).
(((run-event-local-pred(r;e2) = run-event-local-pred(r;e1) ∈ (runEvents(r)?))
∧ (run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)))
∨ (∃e:runEvents(r)
(run-event-step(e) < run-event-step(e2)
∧ (run-event-step(e1) ≤ run-event-step(e))
∧ ((run-event-loc(e1) = run-event-loc(e) ∈ Id) ∧ (run-event-local-pred(r;e2) = (inl e) ∈ (runEvents(r)?)))
∧ (run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List))))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
Lemma: run-event-interval-cases
∀[M:Type ─→ Type]
∀S0:System(P.M[P]). ∀r:fulpRunType(P.M[P]). ∀e1,e2:runEvents(r).
(((run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1) ∈ (Process(P.M[P]) List))
∧ (run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)))
∨ (∃e:runEvents(r)
(run-event-step(e) < run-event-step(e2)
∧ (run-event-step(e1) ≤ run-event-step(e))
∧ ((run-event-loc(e1) = run-event-loc(e) ∈ Id)
∧ (run-prior-state(S0;r;e2) = run-event-state(r;e) ∈ (Process(P.M[P]) List)))
∧ (run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List))))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
Lemma: run-event-state-next
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S0;env;n2m;l2m) in
∀e:runEvents(r)
sub-mset(Process(P.M[P]); map(λP.(fst(Process-apply(P;run-event-msg(r;e))));run-prior-state(S0;r;e));
run-event-state(r;e))
supposing Continuous+(P.M[P])
Lemma: run-event-state-next2
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S0;env;n2m;l2m) in
∀e:runEvents(r)
(run-event-state(r;e)
= rev(map(λP.(fst(Process-apply(P;run-event-msg(r;e))));run-event-state-when(r;e)))
∈ (Process(P.M[P]) List))
supposing Continuous+(P.M[P])
Lemma: adjacent-run-states
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S:System(P.M[P]). ∀env:pEnvType(P.M[P]). ∀x:Id. ∀n,m:ℕ+.
(run-event-state-when(pRun(S;env;n2m;l2m);<n, x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<m, x>)) supposing
((∀a:runEvents(pRun(S;env;n2m;l2m))
¬((n ≤ run-event-step(a)) ∧ run-event-step(a) < m) supposing run-event-loc(a) = x ∈ Id) and
(n ≤ m))
supposing Continuous+(P.M[P])
Definition: run-pred
run-pred(r) ==
λe1,e2. (((run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2))
∨ (e1 = (fst(run-info(r;e2))) ∈ (ℤ × Id)))
Lemma: run-pred_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. (run-pred(r) ∈ runEvents(r) ─→ runEvents(r) ─→ ℙ)
Definition: run-cause
run-cause(r) == λe.let t,x = fst(run-info(r;e)) in if 0 ≤z t ∧b is-run-event(r;t;x) then inl <t, x> else inr ⋅ fi
Lemma: run-cause_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. (run-cause(r) ∈ runEvents(r) ─→ (runEvents(r)?))
Definition: prior-run-events
prior-run-events(r;t) == mapfilter(λt.<t, fst(snd(outl(fst((r t)))))>;λt.isl(fst((r t)));upto(t))
Lemma: prior-run-events_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ]. (prior-run-events(r;t) ∈ runEvents(r) List)
Lemma: member-prior-run-events
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀t:ℕ. ∀e:runEvents(r). ((e ∈ prior-run-events(r;t)) ⇐⇒ run-event-step(e) < t)
Lemma: run-pred-step-less
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])].
∀[x,y:runEvents(r)]. run-event-step(x) < run-event-step(y) supposing x run-pred(r) y
supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Lemma: finite-run-pred
∀[M:Type ─→ Type]
∀r:pRunType(P.M[P])
rel_finite(runEvents(r);run-pred(r)) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Lemma: pRun-intransit-invariant
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀Cs0:component(P.M[P]) List. ∀G0:LabeledDAG(pInTransit(P.M[P])).
∀env:pEnvType(P.M[P]). ∀t:ℕ.
let r = pRun(<Cs0, G0>;env;n2m;l2m) in
let info,Cs,G = r t in
∀x∈G.let ev = fst(x) in
((fst(ev)) ≤ t) ∨ (∃m:ℕlg-size(G0). (ev = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
supposing Continuous+(P.M[P])
Lemma: pRun-invariant1
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S0;env;n2m;l2m) in
∀e:runEvents(r)
(fst(fst(run-info(r;e))) < run-event-step(e)
∨ (∃m:ℕlg-size(snd(S0)). ((fst(run-info(r;e))) = (fst(lg-label(snd(S0);m))) ∈ (ℤ × Id))))
supposing Continuous+(P.M[P])
Lemma: pRun-invariant2
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S0;env;n2m;l2m) in
∀e1,e2:runEvents(r).
(∀P:Process(P.M[P])
((P ∈ run-prior-state(S0;r;e1))
⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)))
∈ run-event-state(r;e2)))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
supposing Continuous+(P.M[P])
Lemma: pRun-invariant3
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S0;env;n2m;l2m) in
∀e1,e2:runEvents(r).
(∀P:Process(P.M[P])
((P ∈ run-event-state-when(r;e1))
⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)))
∈ run-event-state(r;e2)))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
supposing Continuous+(P.M[P])
Lemma: well-founded-run-pred
∀[M:Type ─→ Type]
∀r:pRunType(P.M[P])
SWellFounded(x run-pred(r) y) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Lemma: decidable__run-pred
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀e1,e2:runEvents(r). Dec(e1 run-pred(r) e2)
Definition: run-local-pred
run-local-pred(r;i;t;t')
==r if (t' =z 0)
then <t, i>
else eval p = t' - 1 in
if is-run-event(r;p;i) then <p, i> else run-local-pred(r;i;t;p) fi
fi
Lemma: run-local-pred_wf
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀i:Id. ∀t',t:ℕ. (run-local-pred(r;i;t;t') ∈ ℕ × Id)
Definition: run_local_pred
run_local_pred(r;e) == run-local-pred(r;snd(e);fst(e);fst(e))
Lemma: run_local_pred_wf
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀e:runEvents(r). (run_local_pred(r;e) ∈ runEvents(r))
Lemma: run_local_pred_loc
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀e:runEvents(r). ((snd(run_local_pred(r;e))) = (snd(e)) ∈ Id)
Lemma: run_local_pred_time
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀e:runEvents(r). ((fst(run_local_pred(r;e))) ≤ (fst(e)))
Lemma: run_local_pred_time_less
∀M:Type ─→ Type. ∀r:pRunType(P.M[P]). ∀e,x:runEvents(r).
((run-event-loc(x) = run-event-loc(e) ∈ Id)
⇒ run-event-step(x) < run-event-step(e)
⇒ run-event-step(run_local_pred(r;e)) < run-event-step(e))
Lemma: run_local_pred_maximal
∀M:Type ─→ Type. ∀r:pRunType(P.M[P]). ∀e,x:runEvents(r).
(run-event-step(x) < run-event-step(e)
⇒ run-event-step(run_local_pred(r;e)) < run-event-step(x)
⇒ (¬(run-event-loc(x) = run-event-loc(e) ∈ Id)))
Definition: run-lt
run-lt(r) == run-pred(r)+
Lemma: run-lt_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. (run-lt(r) ∈ runEvents(r) ─→ runEvents(r) ─→ ℙ)
Lemma: run-lt-step-less
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])].
∀[x,y:runEvents(r)]. run-event-step(x) < run-event-step(y) supposing x run-lt(r) y
supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Lemma: decidable__run-lt
∀[M:Type ─→ Type]
∀r:pRunType(P.M[P])
∀e1,e2:runEvents(r). Dec(e1 run-lt(r) e2) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Lemma: finite-run-lt
∀[M:Type ─→ Type]
∀r:pRunType(P.M[P])
rel_finite(runEvents(r);run-lt(r)) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Lemma: well-founded-run-lt
∀[M:Type ─→ Type]
∀r:pRunType(P.M[P])
SWellFounded(x run-lt(r) y) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Lemma: total-run-lt
∀[M:Type ─→ Type]
∀r:pRunType(P.M[P]). ∀e1,e2:runEvents(r).
(e1 = e2 ∈ runEvents(r)) ∨ (e1 run-lt(r) e2) ∨ (e2 run-lt(r) e1)
supposing run-event-loc(e1) = run-event-loc(e2) ∈ Id
Lemma: run-lt-transitive
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). Trans(runEvents(r);x,y.x run-lt(r) y)
Definition: run-eo
EO(r) ==
mk-extended-eo(type: runEvents(r);
domain: λe.tt;
loc: λe.run-event-loc(e);
info: λe.run-event-msg(r;e);
causal: run-lt(r);
local: λe1,e2. run-event-step(e1) <z run-event-step(e2);
pred: λe.run_local_pred(r;e);
rank: λe.run-event-step(e))
Lemma: run-eo_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])].
EO(r) ∈ EO+(pMsg(P.M[P])) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
Definition: run-initialization
run-initialization(r;G) == ∀x∈G.∀e:runEvents(r). fst(fst(x)) < 1
Lemma: run-initialization_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[G:LabeledGraph(pInTransit(P.M[P]))]. (run-initialization(r;G) ∈ ℙ)
Lemma: run-initialization-property
∀[M:Type ─→ Type]
∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[S0:System(P.M[P])]. ∀[env:pEnvType(P.M[P])].
∀[e:runEvents(pRun(S0;env;n2m;l2m))]. fst(fst(run-info(pRun(S0;env;n2m;l2m);e))) < run-event-step(e)
supposing run-initialization(pRun(S0;env;n2m;l2m);snd(S0))
supposing Continuous+(P.M[P])
Definition: std-initial
std-initial(S) == ∀x∈snd(S).(fst(fst(x))) = (-1) ∈ ℤ
Lemma: std-initial_wf
∀[M:Type ─→ Type]. ∀[S:System(P.M[P])]. (std-initial(S) ∈ ℙ)
Lemma: std-initial-property
∀[M:Type ─→ Type]. ∀[S:System(P.M[P])]. ∀[r:pRunType(P.M[P])]. run-initialization(r;snd(S)) supposing std-initial(S)
Definition: runEO
runEO(n2m;l2m;env;S) == EO(pRun(S;env;n2m;l2m))
Lemma: runEO_wf
∀[M:Type ─→ Type]
∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[S0:System(P.M[P])]. ∀[env:pEnvType(P.M[P])].
runEO(n2m;l2m;env;S0) ∈ EO+(pMsg(P.M[P])) supposing run-initialization(pRun(S0;env;n2m;l2m);snd(S0))
supposing Continuous+(P.M[P])
Definition: InitialSystem
InitialSystem(P.M[P]) == {S:System(P.M[P])| std-initial(S)}
Lemma: InitialSystem_wf
∀[M:Type ─→ Type]. (InitialSystem(P.M[P]) ∈ Type)
Definition: stdEO
stdEO(n2m;l2m;env;S) == runEO(n2m;l2m;env;S)
Lemma: stdEO_wf
∀[M:Type ─→ Type]
∀[S0:InitialSystem(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[env:pEnvType(P.M[P])].
(stdEO(n2m;l2m;env;S0) ∈ EO+(pMsg(P.M[P])))
supposing Continuous+(P.M[P])
Lemma: stdEO-causal
∀[M:Type ─→ Type]
∀[S0:InitialSystem(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[env:pEnvType(P.M[P])]. ∀[e1,e2:E].
run-event-step(e1) < run-event-step(e2) supposing (e1 < e2)
supposing Continuous+(P.M[P])
Lemma: stdEO-locl
∀[M:Type ─→ Type]
∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e1,e2:E.
((e1 <loc e2) ⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2))
supposing Continuous+(P.M[P])
Lemma: stdEO-eq-E
∀[M:Type ─→ Type]
∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e1,e2:E.
(e1 = e2 ∈ E ⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ (run-event-step(e1) = run-event-step(e2) ∈ ℤ))
supposing Continuous+(P.M[P])
Lemma: stdEO-le
∀[M:Type ─→ Type]
∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e1,e2:E.
(e1 ≤loc e2 ⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ (run-event-step(e1) ≤ run-event-step(e2)))
supposing Continuous+(P.M[P])
Lemma: stdEO-event-history
∀[M:Type ─→ Type]
∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e1,e2:E.
((e1 <loc e2) ⇐⇒ (e1 ∈ run-event-history(pRun(S0;env;n2m;l2m);e2)))
supposing Continuous+(P.M[P])
Lemma: stdEO-E-property
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S2:InitialSystem(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e:E.
(e ∈ ℕ+ × Id)
supposing Continuous+(P.M[P])
Definition: choosable-command
choosable-command(P.M[P];r;t;x) ==
let Cs,G = run-system(r;t)
in ∃n:ℕ. ((↑lg-is-source(G;n)) ∧ (x = lg-label(G;n) ∈ pInTransit(P.M[P])))
Lemma: choosable-command_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+]. ∀[x:pInTransit(P.M[P])]. (choosable-command(P.M[P];r;t;x) ∈ ℙ)
Definition: chosen-command
chosen-command(P.M[P];env;r;t;x) ==
let Cs,G = run-system(r;t)
in let n = fst((env t r)) in
(↑lg-is-source(G;n)) ∧ (x = lg-label(G;n) ∈ pInTransit(P.M[P]))
Lemma: chosen-command_wf
∀[M:Type ─→ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[t:ℕ+]. ∀[x:pInTransit(P.M[P])]. ∀[env:pEnvType(P.M[P])].
(chosen-command(P.M[P];env;r;t;x) ∈ ℙ)
Definition: first-choosable
first-choosable(r;t) ==
let G = snd(run-system(r;t)) in
let s = search(lg-size(G);λn.lg-is-source(G;n)) in
if 0 <z s then s - 1 else s fi
Lemma: first-choosable_wf
∀[M:Type ─→ Type]. ∀[t:ℕ+]. ∀[r:ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))]. (first-choosable(r;t) ∈ ℕ)
Lemma: first-choosable-property
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+]. ∀[n:ℕ].
first-choosable(r;t) ≤ n supposing ↑lg-is-source(run-intransit(r;t);n)
Lemma: first-choosable-property2
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+]. ∀[n:ℕ].
↑lg-is-source(run-intransit(r;t);first-choosable(r;t)) supposing ↑lg-is-source(run-intransit(r;t);n)
Definition: reliable-env
reliable-env(env; r) == ∀t:ℕ. ∃t':ℕ. (t < t' ∧ ((fst((env t' r))) = 0 ∈ ℤ))
Lemma: reliable-env_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[env:pEnvType(P.M[P])]. (reliable-env(env; r) ∈ ℙ)
Definition: std-env
std-env(nm) == λt,r. <0, 0, nm>
Lemma: std-env_wf
∀[M:Type ─→ Type]. ∀[nm:Id]. (std-env(nm) ∈ pEnvType(P.M[P]))
Definition: run-command-node
run-command-node(r;t;n) == n < lg-size(snd(snd((r t))))
Lemma: run-command-node_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t,n:ℕ]. (run-command-node(r;t;n) ∈ ℙ)
Definition: run-command
run-command(r;t;n) == lg-label(snd(snd((r t)));n)
Lemma: run-command_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[t,n:ℕ].
run-command(r;t;n) ∈ pInTransit(P.M[P]) supposing run-command-node(r;t;n)
Definition: run-msg-commands
run-msg-commands(r) ==
t:ℕ × {n:ℕ| run-command-node(r;t;n) ∧ (com-kind(snd(snd(run-command(r;t;n)))) ∈ ``msg choose new``)}
Lemma: run-msg-commands_wf
∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. (run-msg-commands(r) ∈ Type)
Definition: command-to-msg
command-to-msg(c;nmsg;lmsg) ==
if com-kind(c) =a "msg" then comm-msg(c)
if com-kind(c) =a "choose" then nmsg
else lmsg
fi
Lemma: command-to-msg_wf
∀[M:Type ─→ Type]. ∀[c:pCom(P.M[P])]. ∀[nmsg,lmsg:pMsg(P.M[P])]. (command-to-msg(c;nmsg;lmsg) ∈ pMsg(P.M[P]))
Definition: intransit-to-info
intransit-to-info(n2m;l2m;r;env;t;lbl) ==
let n,m,nm = env t r in
let ev,x,c = lbl in
<ev, command-to-msg(c;n2m m;l2m nm)>
Lemma: intransit-to-info_wf
∀[M:Type ─→ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])].
∀[env:pEnvType(P.M[P])]. ∀[t:ℕ+]. ∀[lbl:pInTransit(P.M[P])].
(intransit-to-info(n2m;l2m;r;env;t;lbl) ∈ ℤ × Id × pMsg(P.M[P]))
Lemma: reliable-env-property1
∀[M:Type ─→ Type]
∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S0;env;n2m;l2m) in
reliable-env(env; r)
⇒ (∀tn:run-msg-commands(r)
let t,n = tn
in ∃t':ℕ
((t < t'
c∧ (((fst((env t' r))) ≤ n)
∧ ↑lg-is-source(run-intransit(r;t');fst((env t' r))) supposing 0 < lg-size(run-intransit(r;t'))))
∧ (∀i:ℕ
¬(t < i
c∧ (((fst((env i r))) ≤ n)
∧ ↑lg-is-source(run-intransit(r;i);fst((env i r)))
supposing 0 < lg-size(run-intransit(r;i))))
supposing i < t')))
supposing Continuous+(P.M[P])
Lemma: reliable-env-property
∀[M:Type ─→ Type]
∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S0;env;n2m;l2m) in
reliable-env(env; r)
⇒ (∀tn:run-msg-commands(r)
∃e:runEvents(r)
let t,n = tn
in (run-info(r;e)
= intransit-to-info(n2m;l2m;r;env;run-event-step(e);run-command(r;t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(r;t;n)))) ∈ Id))
supposing Continuous+(P.M[P])
Lemma: reliable-env-property2
∀[M:Type ─→ Type]
∀S:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S;env;n2m;l2m) in
reliable-env(env; r)
⇒ (∀e:runEvents(r). ∀P:Process(P.M[P]).
((P ∈ run-event-state-when(r;e))
⇒ ∀p∈snd((P (snd(run-info(r;e))))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(r)
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(r) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(r;e')))
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(r) e') = (inl e) ∈ (runEvents(r)?))))))
supposing Continuous+(P.M[P])
Lemma: std-env-reliable
∀nm:Id
∀[M:Type ─→ Type]
∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]).
reliable-env(std-env(nm); pRun(S0;std-env(nm);n2m;l2m))
supposing Continuous+(P.M[P])
Definition: system-realizes
assuming(env,r.A[env; r]) S |- eo.B[eo] == ∀env:pEnvType(P.M[P]). let r = pRun(S;env;n2m;l2m) in A[env; r] ⇒ B[EO(r)]
Lemma: system-realizes_wf
∀[M:Type ─→ Type]
∀[S:InitialSystem(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[A:pEnvType(P.M[P])
─→ pRunType(P.M[P])
─→ ℙ].
∀[B:EO+(pMsg(P.M[P])) ─→ ℙ].
(assuming(env,r.A[env;r])
S |- eo.B[eo] ∈ ℙ)
supposing Continuous+(P.M[P])
Definition: sub-system
sub-system(P.M[P];S1;S2) == let Cs,G = S1 in let Cs',G' = S2 in Cs ⊆ Cs' ∧ G ⊆ G'
Lemma: sub-system_wf
∀[M:Type ─→ Type]. ∀[S1,S2:System(P.M[P])]. (sub-system(P.M[P];S1;S2) ∈ ℙ)
Lemma: sub-system_transitivity
∀[M:Type ─→ Type]
∀S1,S2,S3:System(P.M[P]). (sub-system(P.M[P];S1;S2) ⇒ sub-system(P.M[P];S2;S3) ⇒ sub-system(P.M[P];S1;S3))
Lemma: sub-system_weakening
∀[M:Type ─→ Type]. ∀S1,S2:System(P.M[P]). sub-system(P.M[P];S1;S2) supposing S1 = S2 ∈ System(P.M[P])
Definition: system-append
S1 @ S2 == let Cs,G = S1 in let Cs',G' = S2 in <Cs @ Cs', lg-append(G;G')>
Lemma: system-append_wf
∀[M:Type ─→ Type]. ∀[S1,S2:System(P.M[P])]. (S1 @ S2 ∈ System(P.M[P]))
Lemma: sub-system-append
∀[M:Type ─→ Type]. ∀S1,S2:System(P.M[P]). (sub-system(P.M[P];S1;S1 @ S2) ∧ sub-system(P.M[P];S2;S1 @ S2))
Definition: system-strongly-realizes
assuming(env,r.A[env; r])
S |= eo.B[eo] ==
∀S2:InitialSystem(P.M[P]). (sub-system(P.M[P];S;S2) ⇒ assuming(env,r.A[env; r]) S2 |- eo.B[eo])
Lemma: system-strongly-realizes_wf
∀[M:Type ─→ Type]
∀[S:InitialSystem(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[A:pEnvType(P.M[P])
─→ pRunType(P.M[P])
─→ ℙ].
∀[B:EO+(pMsg(P.M[P])) ─→ ℙ].
(assuming(env,r.A[env;r])
S |= eo.B[eo] ∈ ℙ)
supposing Continuous+(P.M[P])
Lemma: system-strongly-realizes_functionality
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]).
∀[A:pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ]. ∀[B:EO+(pMsg(P.M[P])) ─→ ℙ].
∀X,Y:InitialSystem(P.M[P]).
(system-equiv(P.M[P];X;Y) ⇒ assuming(env,r.A[env;r]) X |= eo.B[eo] ⇒ assuming(env,r.A[env;r]) Y |= eo.B[eo])
supposing Continuous+(P.M[P])
Lemma: system-strongly-realizes-and1
∀[M:Type ─→ Type]
∀[A:pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S1,S2:InitialSystem(P.M[P]).
∀[B1,B2:EO+(pMsg(P.M[P])) ─→ ℙ].
(assuming(env,r.A[env;r])
S1 |= eo.B1[eo]
⇒ assuming(env,r.A[env;r])
S2 |= eo.B2[eo]
⇒ (∀S:InitialSystem(P.M[P])
(sub-system(P.M[P];S1;S)
⇒ sub-system(P.M[P];S2;S)
⇒ assuming(env,r.A[env;r])
S |= eo.B1[eo] ∧ B2[eo])))
supposing Continuous+(P.M[P])
Lemma: system-strongly-realizes-and
∀[M:Type ─→ Type]
∀[A:pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S1,S2:InitialSystem(P.M[P]).
∀[B1,B2:EO+(pMsg(P.M[P])) ─→ ℙ].
(assuming(env,r.A[env;r])
S1 |= eo.B1[eo]
⇒ assuming(env,r.A[env;r])
S2 |= eo.B2[eo]
⇒ assuming(env,r.A[env;r])
S1 @ S2 |= eo.B1[eo] ∧ B2[eo])
supposing Continuous+(P.M[P])
Lemma: std-components-property
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.∃cause:E ─→ (E?)
(∀C∈Cs.∀e:E
let G = last(data-stream(snd(C);map(λe.info(e);≤loc(e)))) in
∀p∈G.let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e') = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
supposing Continuous+(P.M[P])
Lemma: std-component-property
∀[M:Type ─→ Type]
∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀x:Id. ∀Q:Process(P.M[P]).
assuming(env,r.reliable-env(env; r))
<[<x, Q>], lg-nil()> |= es.∃cause:E ─→ (E?)
∀e:E
let G = last(data-stream(Q;map(λe.info(e);≤loc(e)))) in
∀p∈G.let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e') = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = x ∈ Id
supposing Continuous+(P.M[P])
Lemma: single-bag-not-null
∀T:Type. ∀x:T. (↑bag-null({x}) ~ False)
Lemma: null-bag-empty
∀T:Type. ∀x:bag(T). (↑bag-null(x) ⇐⇒ x = {} ∈ bag(T))
Lemma: the-member-bag-rep
∀[T:Type]. ∀[n:ℕ]. ∀[a:T]. a ↓∈ bag-rep(n;a) supposing 0 < n
Lemma: empty-bag-union
∀[T:Type]. ∀[bbs:bag(bag(T))]. ∀bs:bag(T). (bs ↓∈ bbs ⇒ (bs = {} ∈ bag(T))) supposing bag-union(bbs) = {} ∈ bag(T)
Lemma: bag-rep-is-single-valued
∀[A:Type]. ∀[n:ℕ]. ∀[a:A]. single-valued-bag(bag-rep(n;a);A)
Lemma: sv-list-equal
∀T:Type. ∀L1,L2:T List. ∀x:T.
(single-valued-list(L1;T)
⇒ single-valued-list(L2;T)
⇒ (x ∈ L1)
⇒ (x ∈ L2)
⇒ (||L1|| = ||L2|| ∈ ℤ)
⇒ (L1 = L2 ∈ (T List)))
Lemma: permutation-sv-list
∀[A:Type]. ∀[L1,L2:A List]. (single-valued-list(L1;A) ⇒ permutation(A;L1;L2) ⇒ (L1 = L2 ∈ (A List)))
Lemma: sv-list-tail
∀[A:Type]. ∀[L:A List]. 0 < ||L|| ⇒ single-valued-list(tl(L);A) supposing single-valued-list(L;A)
Lemma: single-valued-bag-is-list
∀[A:Type]. ∀[bs:bag(A)]. bs ∈ A List supposing single-valued-bag(bs;A)
Lemma: single-valued-bag-sv-list
∀[A:Type]. ∀[bs:bag(A)]. single-valued-list(bs;A) supposing single-valued-bag(bs;A)
Definition: sv-bag-tail
sv-bag-tail(bs) == tl(bs)
Lemma: sv-bag-tail_wf
∀[A:Type]. ∀[bs:bag(A)]. sv-bag-tail(bs) ∈ bag(A) supposing single-valued-bag(bs;A)
Lemma: sv-bag-equals-list
∀[A:Type]. ∀[L:A List]. ∀[bs:bag(A)]. (L = bs ∈ (A List)) supposing ((L = bs ∈ bag(A)) and single-valued-list(L;A))
Lemma: bag-member-sv-list
∀T:Type. ∀L:T List. ∀x:T. (x ↓∈ L ⇐⇒ (x ∈ L)) supposing single-valued-list(L;T)
Lemma: single-valued-list-sv-bag
∀[A:Type]. ∀[L:A List]. single-valued-bag(L;A) supposing single-valued-list(L;A)
Lemma: sv-bag-tail-single-valued
∀[A:Type]. ∀[bs:bag(A)]. (single-valued-bag(bs;A) ⇒ 0 < #(bs) ⇒ single-valued-bag(sv-bag-tail(bs);A))
Lemma: sv-bag-is-bag-rep
∀[A:Type]. ∀[as:bag(A)]. ∀a:A. (a ↓∈ as ⇒ (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)
Lemma: sv-bag-is-bag-rep-lousy-proof
∀[A:Type]. ∀[as:bag(A)]. ∀a:A. (a ↓∈ as ⇒ (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)
Definition: lifting-like
lifting-like(A;f) ==
(∀as:bag(A). ∀x:A. (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(f as) ⇐⇒ ↑bag-null(f {x}))))
∧ (↑bag-null(f {}))
Lemma: lifting-like_wf
∀[A,B:Type]. ∀[f:bag(A) ─→ bag(B)]. (lifting-like(A;f) ∈ ℙ)
Lemma: lifting1-loc-lifting-like
∀[A,B:Type]. ∀[f:Id ─→ A ─→ B]. ∀[i:Id]. lifting-like(A;λa.lifting1-loc(f;i;a))
Definition: lifting2-like
lifting2-like(A;B;f) ==
(∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
(single-valued-bag(as;A)
⇒ single-valued-bag(bs;B)
⇒ a ↓∈ as
⇒ b ↓∈ bs
⇒ (↑bag-null(f as bs) ⇐⇒ ↑bag-null(f {a} {b}))))
∧ (∀as:bag(A). (↑bag-null(f as {})))
∧ (∀bs:bag(B). (↑bag-null(f {} bs)))
Lemma: lifting2-like_wf
∀[A,B,C:Type]. ∀[f:bag(A) ─→ bag(B) ─→ bag(C)]. (lifting2-like(A;B;f) ∈ ℙ)
Lemma: lifting2-loc-lifting2-like
∀[A,B,C:Type]. ∀[f:Id ─→ A ─→ B ─→ C]. ∀[i:Id]. lifting2-like(A;B;λas,bs. lifting2-loc(f;i;as;bs))
Lemma: member-parallel-class
∀[Info,A:Type]. ∀[X,Y:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. uiff(↑e ∈b X || Y;↑(e ∈b X ∨be ∈b Y))
Lemma: member-parallel-class-bool
∀[Info,A:Type]. ∀[X,Y:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. (e ∈b X || Y ~ e ∈b X ∨be ∈b Y)
Lemma: member-disjoint-union-comb
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. uiff(↑e ∈b X (+) Y;↑(e ∈b X ∨be ∈b Y))
Lemma: member-disjoint-union-comb-bool
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. (e ∈b X (+) Y ~ e ∈b X ∨be ∈b Y)
Lemma: member-eclass-simple-comb-1
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:bag(A) ─→ bag(B)]. ∀[X:EClass(A)].
(↑e ∈b F|X|) supposing ((∀as:bag(A). ((¬↑bag-null(as)) ⇒ (¬↑bag-null(F as)))) and (↑e ∈b X))
Lemma: member-eclass-simple-comb-1-iff
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:bag(A) ─→ bag(B)]. ∀[X:EClass(A)].
(uiff(↑e ∈b F|X|;(↑e ∈b X) ∧ (¬↑bag-null(F {X@e})))) supposing (single-valued-classrel(es;X;A) and lifting-like(A;F))
Lemma: member-eclass-simple-comb-2-iff
∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:bag(A) ─→ bag(B) ─→ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
(uiff(↑e ∈b F|X, Y|;(↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(F {X@e} {Y@e})))) supposing
(single-valued-classrel(es;Y;B) and
single-valued-classrel(es;X;A) and
lifting2-like(A;B;F))
Lemma: member-base-class
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. header(e) = hdr ∈ Name supposing ↑e ∈b Base(hdr)
Lemma: member-base-class2
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. header(e) = hdr ∈ Name supposing ↑e ∈b Base(hdr)
Lemma: member-base-class_iff
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. uiff(↑e ∈b Base(hdr);header(e) = hdr ∈ Name)
Lemma: member-class-at
∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[locs:bag(Id)]. uiff(↑e ∈b X@locs;(↑e ∈b X) ∧ loc(e) ↓∈ locs)
Lemma: member-eclass-simple-loc-comb-1
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:Id ─→ bag(A) ─→ bag(B)]. ∀[X:EClass(A)].
(↑e ∈b F(Loc, X)) supposing ((∀loc:Id. ∀as:bag(A). ((¬↑bag-null(as)) ⇒ (¬↑bag-null(F loc as)))) and (↑e ∈b X))
Lemma: member-eclass-simple-loc-comb-1-iff
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:Id ─→ bag(A) ─→ bag(B)]. ∀[X:EClass(A)].
(uiff(↑e ∈b F(Loc, X);(↑e ∈b X) ∧ (¬↑bag-null(F loc(e) {X@e})))) supposing
(single-valued-classrel(es;X;A) and
lifting-like(A;F loc(e)))
Lemma: member-eclass-simple-loc-comb-2-iff
∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:Id ─→ bag(A) ─→ bag(B) ─→ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
(uiff(↑e ∈b F o (Loc,X, Y);(↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(F loc(e) {X@e} {Y@e})))) supposing
(single-valued-classrel(es;Y;B) and
single-valued-classrel(es;X;A) and
lifting2-like(A;B;F loc(e)))
Lemma: member-eclass-eclass1
∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ C]. ∀[es:EO]. ∀[e:E]. (e ∈b (f o X) ~ e ∈b X)
Lemma: member-eclass-eclass0
∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ bag(C)]. ∀[es:EO+(Info)]. ∀[e:E].
uiff(↑e ∈b (f o X);(↑e ∈b X) ∧ (¬↑bag-null(f loc(e) X@e))) supposing single-valued-classrel(es;X;B)
Lemma: member-eclass-eclass3
∀[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
uiff(↑e ∈b eclass3(X;Y);(↑e ∈b X) ∧ (↑e ∈b Y))
Lemma: member-eclass-eclass2-eclass1
∀[Info,A,B,C:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[f:Id ─→ A ─→ B ─→ bag(C)]. ∀[es:EO+(Info)]. ∀[e:E].
(uiff(↑e ∈b ((f o X) o Y);(↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(f loc(e) X@e Y@e)))) supposing
(single-valued-classrel(es;X;A) and
single-valued-classrel(es;Y;B))
Lemma: member-eclass-eclass2-eclass3-eclass1
∀[Info,A,B,C,D:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(C)]. ∀[f:Id ─→ A ─→ B ─→ C ─→ bag(D)]. ∀[es:EO+(Info)].
∀[e:E].
(uiff(↑e ∈b (eclass3((f o X);Y) o Z);(↑e ∈b X)
∧ (↑e ∈b Y)
∧ (↑e ∈b Z)
∧ (¬↑bag-null(f loc(e) X@e Y@e Z@e)))) supposing
(single-valued-classrel(es;X;A) and
single-valued-classrel(es;Y;B) and
single-valued-classrel(es;Z;C))
Lemma: member-loop-class-memory
∀[Info,B:Type]. ∀[X:EClass(B ─→ B)]. ∀[init:Id ─→ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E].
(e ∈b loop-class-memory(X;init) ~ 0 <z #(init loc(e)))
Lemma: member-memory-class3
∀[Info,A1,A2,A3,B:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[X1:EClass(A1)]. ∀[tr2:Id ─→ A2 ─→ B ─→ B].
∀[X2:EClass(A2)]. ∀[tr3:Id ─→ A3 ─→ B ─→ B]. ∀[X3:EClass(A3)]. ∀[es:EO+(Info)]. ∀[e:E].
(e ∈b memory-class3(init;tr1;X1;tr2;X2;tr3;X3) ~ tt)
Lemma: classfun-res-base
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. Base(hdr)@e ~ msgval(e) supposing header(e) = hdr ∈ Name
Lemma: classfun-res-member-base
∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. Base(hdr)@e ~ msgval(e) supposing ↑e ∈b Base(hdr)
Lemma: classfun-res-base-classrel
∀[f:Name ─→ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:T].
(Base(hdr)@e = v ∈ T) supposing (v ∈ Base(hdr)(e) and hdr encodes T)
Lemma: classfun-res-parallel-class-left
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)]. ∀[e:E].
(X || Y@e ~ X@e) supposing (disjoint-classrel(es;A;X;A;Y) and (↑e ∈b X))
Lemma: classfun-res-parallel-class-right
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)]. ∀[e:E].
(X || Y@e ~ Y@e) supposing (disjoint-classrel(es;A;X;A;Y) and (↑e ∈b Y))
Lemma: classfun-res-disjoint-union-comb-left
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].
(X (+) Y@e = (inl X@e) ∈ (A + B)) supposing
(single-valued-classrel(es;X;A) and
disjoint-classrel(es;A;X;B;Y) and
(↑e ∈b X))
Lemma: classfun-res-disjoint-union-comb-right
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].
(X (+) Y@e = (inr Y@e ) ∈ (A + B)) supposing
(single-valued-classrel(es;Y;B) and
disjoint-classrel(es;A;X;B;Y) and
(↑e ∈b Y))
Lemma: classfun-res-eclass1
∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ C]. ∀[es:EO+(Info)]. ∀[e:E].
((f o X)@e = (f loc(e) X@e) ∈ C) supposing (single-valued-classrel(es;X;B) and (↑e ∈b X))
Lemma: classfun-res-eclass3
∀[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
(eclass3(X;Y)@e = (X@e Y@e) ∈ C) supposing (X is functional at e and Y is functional at e)
Lemma: classfun-res-disjoint-union-comb-as-parallel-eclass1
∀[Info,A,B,S:Type]. ∀[es:EO+(Info)]. ∀[X1:EClass(A)]. ∀[X2:EClass(B)]. ∀[e:E]. ∀[f1:Id ─→ A ─→ S ─→ S]. ∀[f2:Id
─→ B
─→ S
─→ S].
∀[s:S].
((f1 + f2 loc(e) X1 (+) X2@e s) = ((f1 o X1) || (f2 o X2)@e s) ∈ S) supposing
(disjoint-classrel(es;A;X1;B;X2) and
single-valued-classrel(es;X1;A) and
single-valued-classrel(es;X2;B) and
((↑e ∈b X1) ∨ (↑e ∈b X2)))
Lemma: classfun-eclass3
∀[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
(eclass3(X;Y)(e) = (X(e) Y(e)) ∈ C) supposing (X is functional and Y is functional)
Lemma: in-simple-loc-comb-1-concat
∀[Info,A,B:Type]. ∀[f:Id ─→ A ─→ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
(Singlevalued(X) ⇒ (∀i:Id. ∀a:A. (#(f i a) ≤ 1)) ⇒ e ∈b f@(Loc, X) = e ∈b X ∧b (¬bbag-null(f loc(e) X(e))))
Lemma: loop-class-memory-fun-eq
∀[Info,B:Type]. ∀[X:EClass(B ─→ B)]. ∀[init:Id ─→ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E].
(loop-class-memory(X;init)(e)
= if first(e) then sv-bag-only(init loc(e))
if pred(e) ∈b X then X(pred(e)) loop-class-memory(X;init)(pred(e))
else loop-class-memory(X;init)(pred(e))
fi
∈ B) supposing
(single-valued-classrel(es;X;B ─→ B) and
(∀l:Id. single-valued-bag(init l;B)) and
(∀l:Id. (1 ≤ #(init l))))
Lemma: memory-class3-fun-eq
∀[Info,B,A1,A2,A3:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[X1:EClass(A1)]. ∀[tr2:Id ─→ A2 ─→ B ─→ B].
∀[X2:EClass(A2)]. ∀[tr3:Id ─→ A3 ─→ B ─→ B]. ∀[X3:EClass(A3)]. ∀[es:EO+(Info)]. ∀[e:E].
(memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(e)
= if first(e) then init loc(e)
if pred(e) ∈b X1 then tr1 loc(e) X1@pred(e) memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
if pred(e) ∈b X2 then tr2 loc(e) X2@pred(e) memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
if pred(e) ∈b X3 then tr3 loc(e) X3@pred(e) memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
else memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
fi
∈ B) supposing
(disjoint-classrel(es;A1;X1;A2;X2) and
disjoint-classrel(es;A1;X1;A3;X3) and
disjoint-classrel(es;A2;X2;A3;X3) and
single-valued-classrel(es;X1;A1) and
single-valued-classrel(es;X2;A2) and
single-valued-classrel(es;X3;A3))
Lemma: state-class1-fun-eq
∀[Info,B,A:Type]. ∀[init:Id ─→ B]. ∀[tr:Id ─→ A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
state-class1(init;tr;X)(e)
= if e ∈b X then if first(e) then tr loc(e) X@e (init loc(e)) else tr loc(e) X@e state-class1(init;tr;X)(pred(e)) fi
if first(e) then init loc(e)
else state-class1(init;tr;X)(pred(e))
fi
∈ B
supposing single-valued-classrel(es;X;A)
Lemma: state-class2-fun-eq
∀[Info,B,A1,A2:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[tr2:Id ─→ A2 ─→ B ─→ B]. ∀[X1:EClass(A1)].
∀[X2:EClass(A2)]. ∀[es:EO+(Info)]. ∀[e:E].
(state-class2(init;tr1;X1;tr2;X2)(e)
= if e ∈b X1
then if first(e)
then tr1 loc(e) X1@e (init loc(e))
else tr1 loc(e) X1@e state-class2(init;tr1;X1;tr2;X2)(pred(e))
fi
if e ∈b X2
then if first(e)
then tr2 loc(e) X2@e (init loc(e))
else tr2 loc(e) X2@e state-class2(init;tr1;X1;tr2;X2)(pred(e))
fi
if first(e) then init loc(e)
else state-class2(init;tr1;X1;tr2;X2)(pred(e))
fi
∈ B) supposing
(disjoint-classrel(es;A1;X1;A2;X2) and
single-valued-classrel(es;X1;A1) and
single-valued-classrel(es;X2;A2))
Lemma: state-class3-fun-eq
∀[Info,B,A1,A2,A3:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[tr2:Id ─→ A2 ─→ B ─→ B].
∀[tr3:Id ─→ A3 ─→ B ─→ B]. ∀[X1:EClass(A1)]. ∀[X2:EClass(A2)]. ∀[X3:EClass(A3)]. ∀[es:EO+(Info)]. ∀[e:E].
(state-class3(init;tr1;X1;tr2;X2;tr3;X3)(e)
= if e ∈b X1
then if first(e)
then tr1 loc(e) X1@e (init loc(e))
else tr1 loc(e) X1@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
fi
if e ∈b X2
then if first(e)
then tr2 loc(e) X2@e (init loc(e))
else tr2 loc(e) X2@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
fi
if e ∈b X3
then if first(e)
then tr3 loc(e) X3@e (init loc(e))
else tr3 loc(e) X3@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
fi
if first(e) then init loc(e)
else state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
fi
∈ B) supposing
(disjoint-classrel(es;A1;X1;A2;X2) and
disjoint-classrel(es;A1;X1;A3;X3) and
disjoint-classrel(es;A2;X2;A3;X3) and
single-valued-classrel(es;X1;A1) and
single-valued-classrel(es;X2;A2) and
single-valued-classrel(es;X3;A3))
Lemma: state-class2-inv
∀[Info,B,A1,A2:Type].
∀init:Id ─→ B. ∀tr1:Id ─→ A1 ─→ B ─→ B. ∀tr2:Id ─→ A2 ─→ B ─→ B. ∀X1:EClass(A1). ∀X2:EClass(A2). ∀es:EO+(Info). ∀e:E.
∀P:E ─→ B ─→ ℙ. ∀v:B.
(single-valued-classrel(es;X1;A1)
⇒ single-valued-classrel(es;X2;A2)
⇒ disjoint-classrel(es;A1;X1;A2;X2)
⇒ (∀s:B. ∀e':E.
(e' ≤loc e
⇒ if first(e')
then s = (init loc(e')) ∈ B
else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
fi
⇒ if e' ∈b X1 then ∀a:A1. (a ∈ X1(e') ⇒ P[e';tr1 loc(e') a s])
if e' ∈b X2 then ∀a:A2. (a ∈ X2(e') ⇒ P[e';tr2 loc(e') a s])
else P[e';s]
fi ))
⇒ v ∈ state-class2(init;tr1;X1;tr2;X2)(e)
⇒ P[e;v])
Lemma: memory-class3-classrel
∀[Info,A1,A2,A3,B:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[X1:EClass(A1)]. ∀[tr2:Id ─→ A2 ─→ B ─→ B].
∀[X2:EClass(A2)]. ∀[tr3:Id ─→ A3 ─→ B ─→ B]. ∀[X3:EClass(A3)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
uiff(v ∈ memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(e);↓if first(e)
then v = (init loc(e)) ∈ B
else ∃b:B
(b ∈ memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
∧ if pred(e) ∈b X1 ∨bpred(e) ∈b X2 ∨bpred(e) ∈b X3
then (∃a1:A1
(a1 ∈ X1(pred(e)) ∧ (v = (tr1 loc(e) a1 b) ∈ B)))
∨ (∃a2:A2
(a2 ∈ X2(pred(e))
∧ (v = (tr2 loc(e) a2 b) ∈ B)))
∨ (∃a3:A3
(a3 ∈ X3(pred(e))
∧ (v = (tr3 loc(e) a3 b) ∈ B)))
else v = b ∈ B
fi )
fi )
Home
Index