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) ⊆LabeledGraph(B) supposing A ⊆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 
          map(λx.if x ≤then else fi ;filter(λx.(¬b(x =z n));in))
          map(λx.if x ≤then else 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) 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 
                  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>

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
  ∀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 <then else fi ;if b <then else fi ))

Lemma: lg-edge-add
  ∀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
  ∀g1,g2:LabeledGraph(T). ∀a,b:ℕlg-size(g1) lg-size(g2).
    ⇐⇒ (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
  ∀g:LabeledGraph(T). ∀i:ℕlg-size(g). ∀a,b:ℕlg-size(g) 1.
     lg-connected(g;if a <then else fi ;if b <then else 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 <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) ⊆LabeledDAG(B) supposing A ⊆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 <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) 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 <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 <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 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])) ≤ 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) ⊆dataflow(A2;B2)) supposing ((B1 ⊆B2) and (A2 ⊆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,[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,[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 ⊆T} (S[A[T] ─→ (T × B[T])] ─→ A[T] ─→ (S[T] × B[T])).
         (rec-dataflow(s0;s,[s;m]) ∈ Proc)) supposing 
     (Continuous+(T.B[T]) and 
     Continuous+(T.A[T]) and 

Definition: rec-dataflow-state
rec-dataflow-state(s0;s,[s; m];L) ==
  accumulate (with value and list item m):
   fst(next[s; m])
  over list:
  with starting value:

Lemma: rec-dataflow-state_wf
[S,A,B:Type]. ∀[s0:S]. ∀[next:S ─→ A ─→ (S × B)]. ∀[L:A List].  (rec-dataflow-state(s0;s,[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,[s;a])(a) let s',b next[s0;a] in <rec-dataflow(s';s,[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 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,[s;m])*(L) rec-dataflow(rec-dataflow-state(s0;s,[s;m];L);s,[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) ∈ 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 <||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 ≡ supposing g ∈ dataflow(A;B)

Lemma: dataflow-equiv_transitivity
[A,B:Type]. ∀[f,g,h:dataflow(A;B)].  (f ≡ h) supposing (f ≡ and g ≡ h)

Lemma: dataflow-equiv_inversion
[A,B:Type]. ∀[f,g:dataflow(A;B)].  g ≡ supposing f ≡ g

Comment: process model notes
This version of the process model is based on the CSL paper.
We will have parameter 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 tagged union.
see Com.

When 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 "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])).

system is list of labelled processes (components) together with
graph of commands in transit.
command in transit will be marked with the "event" that generated it.
Such an event is pair ⌈ℤ × Id⌉ of time and location.
Thus we define
pInTransit(M) = ⌈ℤ × Id × Id × pCom(P.M[P])⌉
component(M) Id Process(M)
System(M) component(P.M[P]) List × LabeledGraph(pInTransit(P.M[P]))

choice is triple (n,m,x) of two natural numbers and location.
If the nth node of the intransit graph 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 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 run of system: Error :pRun-def
Since processes are only reactive, nothing will happen in run unless
there are some commands in transit initially. So the initial intransit graph
of the initial system should be non-empty.

For each run, r, we can define the events runEvents in that run,
and 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-msgwe get an
extended-event-ordering: event-ordering+.

The full construction of the extended event ordering of run of system
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-initializationthat 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-initialthat says that in the 
intial intransit graph, all commands have "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) ⊆(Com(P.M[P]) B) supposing A ⊆supposing ∀A,B:Type.  ((A ⊆B)  (M[A] ⊆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]) ⊆
  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]) ⊆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]) ⊆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]) ⊆
  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]) ⊆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,[s;m]) ∈ Process(T.M[T]))) supposing 
     (Continuous+(T.M[T]) and 

Definition: Process-apply
Process-apply(P;m) ==  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≡==  ∀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', x>)

Lemma: dataflow-to-Process_wf
[A,B:Type]. ∀[F:dataflow(A;B)]. ∀[g:B ─→ LabeledDAG(Id × (Com(P.A) Process(P.A)))].
   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)].
               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' in
     eval z' in
     eval 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 
  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 
  in let z,P 
     in if 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 and list item C):
  over list:
  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)
          ∧ (deliver-msg(t;m;x;Cs1;G1)
            ∈ (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 and list item C):
                              over list:
                              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]))].
    (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 
  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 comm-create(c) in <inr ⋅ create-component(t;P;x;Cs;G')>
              if com-kind(c) =a "choose" then let ms nat2msg 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'>
     else <inr ⋅ S>

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]) ⊆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' in
      eval z' in
      eval 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) ==
  pRun,t. if (t =z 0)
           then <inr ⋅ S0>
           else let n,m,nm env 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) ==
  pRun2,t. if (t =z 0)
            then eval norm-system S0 in
                 [<inr ⋅ S>]
            else eval pRun2 (t 1) in
                 eval nxt let info,S let n,m,nm env i.r[i]) in 
                            in eval info' norm-runinfo(info) in
                               eval S' norm-system in
                                 <info', S'> in

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 

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]).
       (∀t:ℕ. ∀S:System(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 in isl(info) ∧b let ev,z,m outl(info) in 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 in let info,S 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 in let info,Cs,G 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 in let info,Cs,G (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 in let info,Cs,G 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])].
    0 < run-event-step(e) 
  supposing Continuous+(P.M[P])

Definition: run-event-interval
run-event-interval(r;e1;e2) ==
  let run-event-loc(e1) in
      mapfilter(λt.<t, x>;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 run-event-loc(e) in
      mapfilter(λt.<t, x>;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') =>
   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.
       ((run-prior-state(S0;r;<n, x>let info,Cs,G 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 < 
    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 pRun(S0;env;n2m;l2m) in
          sub-mset(Process(P.M[P]); map(λP.(fst(Process-apply(P;run-event-msg(r;e))));run-prior-state(S0;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 pRun(S0;env;n2m;l2m) in
          ∈ (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 
           ¬((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 ≤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 run-pred(r) 
  supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)

Lemma: finite-run-pred
[M:Type ─→ Type]
    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 pRun(<Cs0, G0>;env;n2m;l2m) in
        let info,Cs,G 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 pRun(S0;env;n2m;l2m) in
          (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 pRun(S0;env;n2m;l2m) in
             ((P ∈ run-prior-state(S0;r;e1))
                  ∈ 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 pRun(S0;env;n2m;l2m) in
             ((P ∈ run-event-state-when(r;e1))
                  ∈ 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]
    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
==r if (t' =z 0)
    then <t, i>
    else eval t' in
         if is-run-event(r;p;i) then <p, i> else run-local-pred(r;i;t;p) 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 run-lt(r) 
  supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)

Lemma: decidable__run-lt
[M:Type ─→ Type]
    ∀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]
    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]
    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: λ;
                 loc: λ;
                 info: λ;e);
                 causal: run-lt(r);
                 local: λe1,e2. run-event-step(e1) <run-event-step(e2);
                 pred: λe.run_local_pred(r;e);
                 rank: λ

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 ∈ ⇐⇒ (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 fst((env 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 snd(run-system(r;t)) in
   let search(lg-size(G);λn.lg-is-source(G;n)) in
   if 0 <then else 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) ≤ 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

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 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 pRun(S0;env;n2m;l2m) in
        reliable-env(env; 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 r))) ≤ n)
                          ∧ ↑lg-is-source(run-intransit(r;i);fst((env 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 pRun(S0;env;n2m;l2m) in
        reliable-env(env; r)
               let t,n tn 
               in (run-info(r;e)
                  ∈ (ℤ × 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 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 
                                                  in (com-kind(c) ∈ ``msg choose new``)
                                                          ((run-event-loc(e') y ∈ Id)
                                                          ∧ (e run-lt(r) e')
                                                          ∧ (∃n:ℕ
                                                               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
  ∀[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]) |- eo.B[eo] ==  ∀env:pEnvType(P.M[P]). let 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])) ─→ ℙ].
      |- 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])
 |= 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])) ─→ ℙ].
      |= 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])) ─→ ℙ].
        (system-equiv(P.M[P];X;Y)  assuming(env,r.A[env;r]) |= eo.B[eo]  assuming(env,r.A[env;r]) |= 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])) ─→ ℙ].
          S1 |= eo.B1[eo]
            S2 |= eo.B2[eo]
                  |= 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])) ─→ ℙ].
          S1 |= eo.B1[eo]
            S2 |= eo.B2[eo]
            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?)
                                   let last(data-stream(snd(C);map(λ;≤loc(e)))) in
                                       ∀p∈G.let y,c 
                                            in (com-kind(c) ∈ ``msg choose new``)
                                                    ((loc(e') y ∈ Id)
                                                    ∧ (e < e')
                                                    ∧ (∃n:ℕ
                                                         (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?)
                                 let last(data-stream(Q;map(λ;≤loc(e)))) in
                                     ∀p∈G.let y,c 
                                          in (com-kind(c) ∈ ``msg choose new``)
                                                  ((loc(e') y ∈ Id)
                                                  ∧ (e < e')
                                                  ∧ (∃n:ℕ
                                                       (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) ⇐⇒ {} ∈ 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.
   (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 ∈ 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 ↓∈ ⇐⇒ (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.
      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 || 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 || 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 (+) 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 (+) 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 

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 (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 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 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 X) Y);(↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(f loc(e) X@e Y@e)))) supposing 
     (single-valued-classrel(es;X;A) and 

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)].
  (uiff(↑e ∈b (eclass3((f X);Y) 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 

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 <#(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 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 and 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].
  ((f1 f2 loc(e) X1 (+) X2@e s) ((f1 X1) || (f2 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 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 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].
     if first(e) then sv-bag-only(init loc(e))
       if pred(e) ∈b then X(pred(e)) loop-class-memory(X;init)(pred(e))
       else loop-class-memory(X;init)(pred(e))
     ∈ 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].
     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))
     ∈ 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 

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].
  if e ∈b 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))
  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].
     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))
       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))
       if first(e) then init loc(e)
       else state-class2(init;tr1;X1;tr2;X2)(pred(e))
     ∈ B) supposing 
     (disjoint-classrel(es;A1;X1;A2;X2) and 
     single-valued-classrel(es;X1;A1) and 

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].
     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))
       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))
       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))
       if first(e) then init loc(e)
       else state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
     ∈ 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 

Lemma: state-class2-inv
  ∀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.
     (∀s:B. ∀e':E.
          (e' ≤loc 
           if first(e')
             then (init loc(e')) ∈ B
             else s ∈ state-class2(init;tr1;X1;tr2;X2)(pred(e')) ∧ P[pred(e');s]
           if e' ∈b X1 then ∀a:A1. (a ∈ X1(e')  P[e';tr1 loc(e') s])
             if e' ∈b X2 then ∀a:A2. (a ∈ X2(e')  P[e';tr2 loc(e') s])
             else P[e';s]
             fi ))
     v ∈ state-class2(init;tr1;X1;tr2;X2)(e)

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 (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 b ∈ B
                                                                fi )
                                                        fi )

Home Index