Definition: mData
mData ==  T:Type × T

Lemma: mData_wf
mData ∈ 𝕌'

Lemma: mData-examples
(<ℤ33> ∈ mData) ∧ (<𝔹tt> ∈ mData) ∧ (<ℤ ⟶ ℤ, λx.(x 1)> ∈ mData) ∧ (<ℤ × 𝔹33, ff> ∈ mData)

Definition: mdata-type
mdata-type(mdata) ==  fst(mdata)

Lemma: mdata-type_wf
[mdata:mData]. (mdata-type(mdata) ∈ Type)

Definition: mdata-val
mdata-val(mdata) ==  snd(mdata)

Lemma: mdata-val_wf
[mdata:mData]. (mdata-val(mdata) ∈ mdata-type(mdata))

Definition: header-type-spec
header-type-spec{i:l}(L;g) ==  {f:Name ⟶ ValueAllType| no_repeats(Name;L) ∧ (∀hdr∈L.(f hdr) (g hdr) ∈ Type)} 

Lemma: header-type-spec_wf
[L:Name List]. ∀[g:Name ⟶ Type].  (header-type-spec{i:l}(L;g) ∈ 𝕌')

Lemma: subtype_rel_header-type-spec
[L:Name List]. ∀[g:Name ⟶ Type].  (header-type-spec{i:l}(L;g) ⊆header-type-spec{i':l}(L; g))

Definition: basicMessage
basic message is header and value whose type depends on the header.⋅

basicMessage(f) ==  h:Name × (f h)

Lemma: basicMessage_wf
[f:Name ⟶ Type]. (basicMessage(f) ∈ Type)

Definition: make-basicMsg
make-basicMsg(hdr;val) ==  <hdr, val>

Lemma: make-basicMsg_wf
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[val:f hdr].  (make-basicMsg(hdr;val) ∈ basicMessage(f))

Definition: Message
message is basic message together with boolean that indicates
whether the basic message was authenticated or not.⋅

Message(f) ==  𝔹 × basicMessage(f)

Lemma: Message_wf
[f:Name ⟶ Type]. (Message(f) ∈ Type)

Lemma: basicMessage-valueall-type
[f:Name ⟶ ValueAllType]. valueall-type(basicMessage(f))

Lemma: Message-valueall-type
[f:Name ⟶ ValueAllType]. valueall-type(Message(f))

Definition: msg-authentic
msg-authentic(m) ==  fst(m)

Lemma: msg-authentic_wf
[f:Name ⟶ Type]. ∀[m:Message(f)].  (msg-authentic(m) ∈ 𝔹)

Definition: msg-msg
msg-msg(m) ==  snd(m)

Lemma: msg-msg_wf
[f:Name ⟶ Type]. ∀[m:Message(f)].  (msg-msg(m) ∈ basicMessage(f))

Definition: msg-header
msg-header(m) ==  fst(msg-msg(m))

Lemma: msg-header_wf
[f:Name ⟶ Type]. ∀[m:Message(f)].  (msg-header(m) ∈ Name)

Definition: msg-mdata
msg-mdata(f;msg) ==  let hdr,val msg-msg(msg) in <hdr, val>

Lemma: msg-mdata_wf
[f:Name ⟶ Type]. ∀[msg:Message(f)].  (msg-mdata(f;msg) ∈ mData)

Definition: msg-type
msg-type(msg;f) ==  msg-header(msg)

Lemma: msg-type_wf
[f:Name ⟶ Type]. ∀[m:Message(f)].  (msg-type(m;f) ∈ Type)

Lemma: msg-type_wf2
[f:Name ⟶ ValueAllType]. ∀[m:Message(f)].  (msg-type(m;f) ∈ {T:Type| valueall-type(T)} )

Definition: msg-has-type
msg-has-type(m;f;T) ==  msg-type(m;f) ⊆T

Lemma: msg-has-type_wf
[f:Name ⟶ Type]. ∀[m:Message(f)]. ∀[T:Type].  (msg-has-type(m;f;T) ∈ ℙ)

Definition: msg-body
msg-body(msg) ==  snd(msg-msg(msg))

Lemma: msg-body_wf2
[f:Name ⟶ Type]. ∀[m:Message(f)]. ∀[T:Type].  msg-body(m) ∈ supposing msg-type(m;f) ⊆T

Lemma: msg-body_wf
[f:Name ⟶ Type]. ∀[m:Message(f)].  (msg-body(m) ∈ msg-type(m;f))

Lemma: Message-extensionality
[f:Name ⟶ Type]. ∀[m1,m2:Message(f)].
  uiff(m1 m2 ∈ Message(f);msg-authentic(m1) msg-authentic(m2)
  ∧ (msg-header(m1) msg-header(m2) ∈ Name)
  ∧ (msg-body(m1) msg-body(m2) ∈ (f msg-header(m1))))

Lemma: eclass_wf2
[f:Name ⟶ Type]. ∀[T:𝕌'].  (EClass(T) ∈ 𝕌{i''})

Lemma: eclass_wf3
[f:Name ⟶ Type]. ∀[T:Type].  (EClass(T) ∈ 𝕌')

Definition: es-authentic
es-authentic(es;e) ==  msg-authentic(info(e))

Lemma: es-authentic_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  (es-authentic(es;e) ∈ 𝔹)

Definition: es-header
header(e) ==  msg-header(info(e))

Lemma: es-header_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  (header(e) ∈ Name)

Definition: es-info-type
es-info-type(es;e;f) ==  msg-type(info(e);f)

Lemma: es-info-type_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  (es-info-type(es;e;f) ∈ Type)

Definition: has-es-info-type
has-es-info-type(es;e;f;T) ==  es-info-type(es;e;f) ⊆T

Lemma: has-es-info-type_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type].  (has-es-info-type(es;e;f;T) ∈ Type)

Lemma: eo-forward-has-es-info-type
[f,es,e',e,T:Top].  (has-es-info-type(es.e';e;f;T) has-es-info-type(es;e;f;T))

Lemma: has-es-info-type-is-msg-has-type
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type].  (has-es-info-type(es;e;f;T) msg-has-type(info(e);f;T))

Lemma: has-es-info-type-subtype
[T,U:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].
  (has-es-info-type(es;e;f;T)) supposing (has-es-info-type(es;e;f;U) and (U ⊆T))

Lemma: sq_stable__has-es-info-type
[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  SqStable(has-es-info-type(es;e;f;T))

Lemma: eo-forward-info-type
[f,es,e,e':Top].  (es-info-type(es.e;e';f) es-info-type(es;e';f))

Lemma: eo-forward-header
[es,e,e':Top].  (header(e') header(e'))

Definition: es-info-body
msgval(e) ==  msg-body(info(e))

Lemma: es-info-body_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  (msgval(e) ∈ es-info-type(es;e;f))

Lemma: es-info-body-equal
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e,e':E]. ∀[T:Type].
  (msgval(e) msgval(e') ∈ T) supposing ((e e' ∈ E) and ((f header(e)) ⊆T))

Lemma: es-info-type-implies
[f:Name ⟶ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  (has-es-info-type(es;e;f;T)  (msgval(e) ∈ T))

Lemma: eo-forward-info-body
[es,e,e':Top].  (msgval(e') msgval(e'))

Definition: equal-info-body
body(e) ==  has-es-info-type(es;e;f;T) ∧ (v msgval(e) ∈ T)

Lemma: equal-info-body_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type]. ∀[v:T].  (v body(e) ∈ ℙ)

Lemma: sq_stable__equal-info-body
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type]. ∀[v:T].  SqStable(v body(e))

Lemma: eo-forward-equal-info-body
[f,es,T,e,e',v:Top].  (v body(e) body(e))

Lemma: trivial-equal-info-body
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type].
  uiff(msgval(e) body(e);True) supposing has-es-info-type(es;e;f;T)

Definition: es-info-auth
es-info-auth(es;e) ==  msg-authentic(info(e))

Lemma: es-info-auth_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  (es-info-auth(es;e) ∈ 𝔹)

Definition: encodes-msg-type
hdr encodes ==  (f hdr) ⊆T

Lemma: encodes-msg-type_wf
[hdr:Name]. ∀[f:Name ⟶ Type]. ∀[T:Type].  (hdr encodes T ∈ Type)

Lemma: encodes-msg-type-trivial
[f:Name ⟶ Type]. ∀[hdr:Name].  hdr encodes hdr

Lemma: msg-has-type-encodes
[f,m,T:Top].  (msg-has-type(m;f;T) msg-header(m) encodes T)

Lemma: sq_stable__encodes-msg-type
[f:Name ⟶ Type]. ∀[h:Name]. ∀[T:Type].  SqStable(h encodes T)

Definition: get-mdata
get-mdata(f;msg;hdr) ==  if name_eq(msg-header(msg);hdr) then {msg-mdata(f;msg)} else {} fi 

Lemma: get-mdata_wf
[f:Name ⟶ Type]. ∀[msg:Message(f)]. ∀[hdr:Name].  (get-mdata(f;msg;hdr) ∈ bag(mData))

Definition: mdata-class
mdata-class(f;hdr) ==  λes,e. get-mdata(f;info(e);hdr)

Lemma: mdata-class_wf
[f:Name ⟶ Type]. ∀[hdr:Name].  (mdata-class(f;hdr) ∈ EClass(mData))

Definition: cond-msg-body
cond-msg-body(hdr;msg) ==  if name_eq(msg-header(msg);hdr) then {msg-body(msg)} else {} fi 

Lemma: cond-msg-body_wf
[f:Name ⟶ Type]. ∀[T:Type]. ∀[hdr:Name]. ∀[m:Message(f)].  cond-msg-body(hdr;m) ∈ bag(T) supposing hdr encodes T

Lemma: map-cond-msg-body
[g,hdr,m:Top].  (map(g;cond-msg-body(hdr;m)) if name_eq(msg-header(m);hdr) then {g msg-body(m)} else {} fi )

Lemma: cond-msg-body-cbva
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[msg:Message(f)]. ∀[G:Top].
  let x ⟵ cond-msg-body(hdr;msg) in G[x] G[cond-msg-body(hdr;msg)] supposing valueall-type(f hdr)

Lemma: cond-msg-body-single-valued
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[m:Message(f)]. ∀[T:Type].
  single-valued-bag(cond-msg-body(hdr;m);T) supposing hdr encodes T

Lemma: cond-msg-body-sv-bag-only
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type].
  (sv-bag-only(cond-msg-body(hdr;info(e))) ∈ T) supposing ((header(e) hdr ∈ Name) and hdr encodes T)

Definition: base-headers-msg-val
Base(hdr) ==  λes,e. cond-msg-body(hdr;info(e))

Lemma: base-headers-msg-val_wf
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type].  Base(hdr) ∈ EClass(T) supposing hdr encodes T

Lemma: base-headers-msg-val-es-sv
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name].  es-sv-class(es;Base(hdr))

Lemma: base-headers-msg-val-single-val
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[T:Type].
  single-valued-classrel(es;Base(hdr);T) supposing hdr encodes T

Definition: test-msg-header-and-loc
test-msg-header-and-loc(msg;hdr;loc) ==  name_eq(msg-header(msg);hdr) ∧b loc fst(msg-body(msg))

Lemma: test-msg-header-and-loc_wf
[f:Name ⟶ Type]. ∀[msg:Message(f)]. ∀[hdr:Name]. ∀[loc:Id].
  test-msg-header-and-loc(msg;hdr;loc) ∈ 𝔹 supposing hdr encodes Id × Top

Lemma: assert-test-msg-header-and-loc
[f:Name ⟶ Type]
  ∀msg:Message(f). ∀hdr:Name. ∀loc:Id.
    uiff(↑test-msg-header-and-loc(msg;hdr;loc);(msg-header(msg) hdr ∈ Name) ∧ (loc (fst(msg-body(msg))) ∈ Id)) 
    supposing hdr encodes Id × Top

Definition: base-process-inputs
The base-process-inputs (upto to event e) are the list of m:Info
for which message ⌜<hdr, loc, m>⌝ has been received ⌜≤loc(e)⌝.
(For this to be well-formed, the header hdr must encode the type
Id × Info⌝). ⋅

base-process-inputs(loc;hdr;es;e) ==

Lemma: base-process-inputs_wf
[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[es:EO+(Message(f))]. ∀[e:E].  (base-process-inputs(loc;hdr;es;e) ∈ Info List) supposing hdr encodes Id × Info

Lemma: base-process-inputs-non-null
[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[es:EO+(Message(f))]. ∀[e:E].
    0 < ||base-process-inputs(loc;hdr;es;e)|| supposing ↑test-msg-header-and-loc(info(e);hdr;loc) 
  supposing hdr encodes Id × Info

Definition: base-process-class
The base-process-class does (at any location) what class does 
at location loc in the event ordering with only the events
in the base-process-inputs(loc;hdr;es;e)⋅

base-process-class(X;loc;hdr) ==
  λes,e. if test-msg-header-and-loc(info(e);hdr;loc)
        then let Infos base-process-inputs(loc;hdr;es;e) in
                 list-eo(Infos;loc) (||Infos|| 1)
        else {}

Lemma: base-process-class_wf
[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
  base-process-class(X;loc;hdr) ∈ EClass(T) supposing hdr encodes Id × Info

Comment: parallel composition of base-process-class
The `base-process-class` ⌜base-process-class(X;i;hdr)⌝ runs the program
for at location on just those messages for which it receives message
⌜<hdr, i, m>⌝.
The parallel composition ⌜(||i∈locs.base-process-class(X;i;hdr))⌝
will then simulate the class at all the locations in locs
on reciept of ⌜<hdr, i, m>⌝ messages.
So we define ⌜local-simulation-class(X;locs;hdr)⌝ = ⌜(||i∈locs.base-process-class(X;i;hdr))⌝.

Given any event e, the inputs to the simulation of class upto and including e
will be the list    
  ⌜local-simulation-inputs(es;e;hdr;locs) ==
and this defines `global ordering` of events 
from which we can construct an event ordering

  local-simulation-eo(es;e;hdr;locs) ==  global-eo(local-simulation-inputs(es;e;hdr;locs))

If ⌜↑has-header-and-in-locs(info(e);hdr;locs)⌝ then event corresponds to an event
local-simulation-event(es;e;hdr;locs)⌝ in the ⌜local-simulation-eo(es;e;hdr;locs)⌝,
and the output of the  ⌜local-simulation-class(X;locs;hdr)⌝ at event e  will be the
output of the class at that corresponding event in ⌜local-simulation-eo(es;e;hdr;locs)⌝

Thus the `classrel` for ⌜local-simulation-class(X;locs;hdr)⌝ should be
 ⌜v ∈ local-simulation-class(X;locs;hdr)(e)
  ⇐⇒ has-header-and-in-locs(info(e);hdr;locs) ∧ v ∈ X(local-simulation-eo(es;e;hdr;locs))⌝.

Definition: local-simulation-class
local simulation of class for given (bag of) locs is the parallel
composition of the base-process-class for at each of the locs.
The classrel lemma is: Error :local-simulation-classrel⋅

local-simulation-class(X;locs;hdr) ==  (||i∈locs.base-process-class(X;i;hdr))

Lemma: local-simulation-class_wf
[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[locs:bag(Id)]. ∀[hdr:Name].
  local-simulation-class(X;locs;hdr) ∈ EClass(T) supposing hdr encodes Id × Info

Definition: has-header-and-in-locs
has-header-and-in-locs(msg;hdr;locs) ==  name_eq(msg-header(msg);hdr) ∧b bag-deq-member(IdDeq;fst(msg-body(msg));locs)

Lemma: has-header-and-in-locs_wf
[f:Name ⟶ Type]. ∀[msg:Message(f)]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  has-header-and-in-locs(msg;hdr;locs) ∈ 𝔹 supposing hdr encodes Id × Top

Lemma: assert-has-header-and-in-locs
[f:Name ⟶ Type]
  ∀msg:Message(f). ∀hdr:Name. ∀locs:bag(Id).
    ↑has-header-and-in-locs(msg;hdr;locs) ⇐⇒ (msg-header(msg) hdr ∈ Name) ∧ fst(msg-body(msg)) ↓∈ locs 
    supposing hdr encodes Id × Top

Definition: local-simulation-inputs
local-simulation-inputs(es;e;hdr;locs) ==

Lemma: local-simulation-inputs_wf
[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List) supposing hdr encodes Id × Info

Lemma: member-local-simulation-inputs
f:Name ⟶ Type
    ∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
      ∀e:E. ∀v:Id × Info.
        ((v ∈ local-simulation-inputs(es;e;hdr;locs))
        ⇐⇒ ∃e':E
             (e' ≤loc 
             ∧ (msg-header(info(e')) hdr ∈ Name)
             ∧ fst(v) ↓∈ locs
             ∧ (v msg-body(info(e')) ∈ (Id × Info)))) 
      supposing hdr encodes Id × Info

Lemma: iseg-local-simulation-inputs
f:Name ⟶ Type
    ∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
      ∀e1,e2:E.  (e1 ≤loc e2   local-simulation-inputs(es;e1;hdr;locs) ≤ local-simulation-inputs(es;e2;hdr;locs)) 
      supposing hdr encodes Id × Info

Definition: local-simulation-eo
local-simulation-eo(es;e;hdr;locs) ==  global-eo(local-simulation-inputs(es;e;hdr;locs))

Lemma: local-simulation-eo_wf
[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]. (local-simulation-eo(es;e;hdr;locs) ∈ EO+(Info)) supposing hdr encodes Id × Info

Lemma: local-simulation-eo-loc
[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]. ∀[e1:E].  loc(e1) ↓∈ locs supposing hdr encodes Id × Info

Lemma: local-simulation-E-subtype
[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e1,e2:E].  (e1 ≤loc e2   (E ⊆E)) supposing hdr encodes Id × Info

Lemma: local-simulation-embedding
f:Name ⟶ Type
    ∀es:EO+(Message(f)). ∀hdr:Name. ∀locs:bag(Id).
        (e1 ≤loc e2   x.x embeds local-simulation-eo(es;e1;hdr;locs) into local-simulation-eo(es;e2;hdr;locs))) 
      supposing hdr encodes Id × Info

Definition: local-simulation-event
local-simulation-event(es;e;hdr;locs) ==  ||filter(λm.has-header-and-in-locs(m;hdr;locs);map(λ;before(e)))||

Lemma: local-simulation-event_wf
[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]. local-simulation-event(es;e;hdr;locs) ∈ supposing ↑has-header-and-in-locs(info(e);hdr;locs) 
  supposing hdr encodes Id × Info

Lemma: local-simulation-event-loc
[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
    loc(local-simulation-event(es;e;hdr;locs)) (fst(msg-body(info(e)))) ∈ Id 
    supposing ↑has-header-and-in-locs(info(e);hdr;locs) 
  supposing hdr encodes Id × Info

Lemma: local-simulation-event-info
[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
    info(local-simulation-event(es;e;hdr;locs)) (snd(msg-body(info(e)))) ∈ Info 
    supposing ↑has-header-and-in-locs(info(e);hdr;locs) 
  supposing hdr encodes Id × Info

Definition: typed-base-class
Base(hdr;T) ==  Base(hdr)

Lemma: typed-base-class_wf
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type].  Base(hdr;T) ∈ EClass(T) supposing hdr encodes T

Definition: cond-verify-msg-body
cond-verify-msg-body(hdr;msg) ==  if msg-authentic(msg) then cond-msg-body(hdr;msg) else {} fi 

Lemma: cond-verify-msg-body_wf
[f:Name ⟶ Type]. ∀[T:Type]. ∀[hdr:Name]. ∀[msg:Message(f)].
  cond-verify-msg-body(hdr;msg) ∈ bag(T) supposing hdr encodes T

Definition: verify-class
Verify(hdr) ==  λes,e. cond-verify-msg-body(hdr;info(e))

Lemma: verify-class_wf
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type].  Verify(hdr) ∈ EClass(T) supposing hdr encodes T

Definition: base-headers-msg-val-loc
Base(hdr;locs) ==  Base(hdr)@locs

Lemma: base-headers-msg-val-loc_wf
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[locs:bag(Id)]. ∀[T:Type].  Base(hdr;locs) ∈ EClass(T) supposing hdr encodes T

Lemma: eo-forward-base-classrel
[f:Name ⟶ Type]. ∀[eo:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type]. ∀[v:T].
  uiff(v ∈ Base(hdr)(e');v ∈ Base(hdr)(e')) supposing hdr encodes T

Lemma: eo-forward-base-classfun
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
  (Base(hdr)(e') Base(hdr)(e') ∈ T) supposing ((header(e') hdr ∈ Name) and hdr encodes T)

Lemma: eo-forward-base-classfun-sq
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
  (Base(hdr)(e') Base(hdr)(e')) supposing ((header(e') hdr ∈ Name) and hdr encodes T)

Lemma: eo-forward-base-classfun-res
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
  (Base(hdr)@e' Base(hdr)@e' ∈ T) supposing ((header(e') hdr ∈ Name) and hdr encodes T)

Lemma: eo-forward-base-classfun-res-sq
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
  (Base(hdr)@e' Base(hdr)@e') supposing ((header(e') hdr ∈ Name) and hdr encodes T)

Lemma: eo-forward-member-eclass
[Info:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[e',hdr:Top].  (e' ∈b Base(hdr) e' ∈b Base(hdr))

Definition: class-caused-by
X <-- ==  ∀e':E. ∀v:T.  (v ∈ X(e')  (↓∃e:E. ((e < e') ∧ <loc(e'), info(e')> ∈ Z(e))))

Lemma: class-caused-by_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[Z:EClass(Id × Message(f))]. ∀[T:Type]. ∀[X:EClass(T)].  (X <-- Z ∈ ℙ')

Definition: class-caused-by-some
X <-- p.Z[p] ==
  ∀e':E. ∀v:T.  (v ∈ X(e')  (↓∃e,start:E. ∃p:A. (start ≤loc e  ∧ (e < e') ∧ <loc(e'), info(e')> ∈ Z[p](e))))

Lemma: class-caused-by-some_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[A:Type]. ∀[Z:A ⟶ EClass(Id × Message(f))]. ∀[T:Type]. ∀[X:EClass(T)].
  (X <-- p.Z[p] ∈ ℙ')

Definition: base-class-caused-by
hdr.X <-- p.Z[p] ==
  ∀e':E. ∀v:f hdr.
    (v ∈ X(e')  (↓∃e,start:E. ∃p:A. (start ≤loc e  ∧ (e < e') ∧ <loc(e'), make-Msg(hdr;v)> ∈ Z[p](e))))

Definition: info-delivered
info-delivered{i:l}(Info;X) ==
  ∀es:EO+(Info). ∀e:E. ∀locnfo:Id × Info.
    (locnfo ∈ X(e)  (∃e':E. ((e < e') ∧ (loc(e') (fst(locnfo)) ∈ Id) ∧ (info(e') (snd(locnfo)) ∈ Info))))

Lemma: info-delivered_wf
[Info:Type]. ∀[X:EClass(Id × Info)].  (info-delivered{i:l}(Info;X) ∈ ℙ')

Definition: messages-delivered
messages-delivered{i:l}(es;X;f) ==
  ∀e:E. ∀locmsg:Id × Message(f).
    (locmsg ∈ X(e)  (∃e':E. ((e < e') ∧ (loc(e') (fst(locmsg)) ∈ Id) ∧ (info(e') (snd(locmsg)) ∈ Message(f)))))

Lemma: messages-delivered_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))].  (messages-delivered{i:l}(es;X;f) ∈ ℙ')

Definition: messages-delivered-with-omissions
messages-delivered-with-omissions{i:l}(es;X;faults;f) ==
   ((#(faulty) ≤ faults)
   ∧ (∀e:E. ∀locmsg:Id × Message(f).
        (locmsg ∈ X(e)
         loc(e) ↓∈ faulty)
         (∃e':E. ((e < e') ∧ (loc(e') (fst(locmsg)) ∈ Id) ∧ (info(e') (snd(locmsg)) ∈ Message(f)))))))

Lemma: messages-delivered-with-omissions_wf
[f:Name ⟶ Type]. ∀[faults:ℤ]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))].
  (messages-delivered-with-omissions{i:l}(es;X;faults;f) ∈ ℙ')

Definition: messages-delivered-with-omissions-sub
messages-delivered-with-omissions-sub{i:l}(es;X;failures;ids;f) ==
   ((#(faulty) ≤ failures)
   ∧ (∀e:E. ∀locmsg:Id × Message(f).
        (locmsg ∈ X(e)
         loc(e) ↓∈ faulty)
         loc(e) ↓∈ ids
         (∃e':E. ((e < e') ∧ (loc(e') (fst(locmsg)) ∈ Id) ∧ (info(e') (snd(locmsg)) ∈ Message(f)))))))

Lemma: messages-delivered-with-omissions-sub_wf
[failures:ℤ]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[ids:bag(Id)].
  (messages-delivered-with-omissions-sub{i:l}(es;X;failures;ids;f) ∈ ℙ')

Definition: message-constraint
message-constraint{i:l}(es;X;hdrs;f) ==  ∀e:E. ((header(e) ∈ hdrs)  (↓∃e':E. ((e' < e) ∧ <loc(e), info(e)> ∈ X(e'))))

Lemma: message-constraint_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (message-constraint{i:l}(es;X;hdrs;f) ∈ ℙ')

Definition: delivered-with-headers
delivered-with-headers(hdrs;es;e) ==  mapfilter(λe.<loc(e), info(e)>e.header(e) ∈b hdrs;≤loc(e))

Lemma: delivered-with-headers_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdrs:Name List].
  (delivered-with-headers(hdrs;es;e) ∈ {im:Id × Message(f)| (msg-header(snd(im)) ∈ hdrs)}  List)

Lemma: delivered-with-headers-no_repeats
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdrs:Name List].  no_repeats(E;filter(λe.header(e) ∈b hdrs;≤loc(e)))

Definition: strong-message-constraint
strong-message-constraint{i:l}(es;X;hdrs;f) ==
       ((∀e':E. (e' ↓∈ bg  (e' < e)))
       ∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))

Lemma: strong-message-constraint_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint{i:l}(es;X;hdrs;f) ∈ ℙ')

Lemma: strong-message-constraint-implies-message-constraint
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint{i:l}(es;X;hdrs;f)  message-constraint{i:l}(es;X;hdrs;f))

Definition: strong-message-constraint-no-rep
strong-message-constraint-no-rep{i:l}(es;X;hdrs;f) ==
       ∧ (∀e1,e2:E.  (e1 ↓∈ bg  e2 ↓∈ bg  (e1 <loc e2))))
       ∧ (∀e':E. (e' ↓∈ bg  (e' < e)))
       ∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))

Lemma: strong-message-constraint-no-rep_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-no-rep{i:l}(es;X;hdrs;f) ∈ ℙ')

Lemma: strong-message-constraint-no-rep-implies
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-no-rep{i:l}(es;X;hdrs;f)  strong-message-constraint{i:l}(es;X;hdrs;f))

Definition: strong-message-constraint-no-rep-large
strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) ==
       ∧ (∀e1,e2:E.  (e1 ↓∈ bg  e2 ↓∈ bg  (e1 <loc e2))))
       ∧ (∀e':E. (e' ↓∈ bg  (e' < e)))
       ∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
       ∧ (∀e':E. ((e' < e)  (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' ))))))

Lemma: strong-message-constraint-no-rep-large_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) ∈ ℙ')

Lemma: strong-message-constraint-no-rep-large-implies
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f)  message-constraint{i:l}(es;X;hdrs;f))

Lemma: mapfilter-bor-eq
T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
  ((mapfilter(f;P;L) mapfilter(f;Q;L))
  (mapfilter(f;λx.(P[x] ∨bQ[x]);L) mapfilter(f;λx.(P[x] ∧b Q[x]);L))
  ∈ bag(U))

Lemma: mapfilter-bor
T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
  sub-bag(U;mapfilter(f;λx.(P[x] ∨bQ[x]);L);mapfilter(f;P;L) mapfilter(f;Q;L))

Lemma: mapfilter-subbag
T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
  ((∀t:T. ((↑(P t))  (↑(Q t))))  sub-bag(U;mapfilter(f;P;L);mapfilter(f;Q;L)))

Lemma: strong-message-constraint-no-rep-large-1hdr
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
   (∀hdr:Name. ((hdr ∈ hdrs)  strong-message-constraint-no-rep-large{i:l}(es;X;[hdr];f))))

Definition: strong-message-constraint-bag
strong-message-constraint-bag{i:l}(es; X; hdrs; f) ==
     (∀e1,e2:E.  (e1 ↓∈ be  e2 ↓∈ be  (e1 <loc e2))))
          ∧ (∀e1,e2:E.  (e1 ↓∈ bg  e2 ↓∈ bg  (e1 <loc e2))))
          ∧ (∀e':E. (e' ↓∈ bg  (∃e:E. (e ↓∈ be ∧ (e' < e)))))
          ∧ sub-bag(Id × Message(f);⋃e∈be.delivered-with-headers(hdrs;es;e);class-output(X;es;bg)))))

Lemma: strong-message-constraint-bag_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-bag{i:l}(es; X; hdrs; f) ∈ ℙ')

Definition: std-ma
StandardMessageAutomaton(X;hdrs) ==  message-constraint{i:l}(es;X;hdrs;f) ∧ messages-delivered{i:l}(es;X;f)

Lemma: std-ma_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (StandardMessageAutomaton(X;hdrs) ∈ ℙ')

Definition: std-ma-with-omissions
StandardMessageAutomaton(X;hdrs) (with send omissions at fail locations) ==
  message-constraint{i:l}(es;X;hdrs;f) ∧ messages-delivered-with-omissions{i:l}(es;X;fail;f)

Lemma: std-ma-with-omissions_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List]. ∀[faults:ℤ].
  (StandardMessageAutomaton(X;hdrs) (with send omissions at faults locations) ∈ ℙ')

Definition: causal-class-rel-in-out
if class_out outputs (m) then class_in observed ==  ∀e:E. (m ∈ class_out(e)  (↓∃e':E. (e' c≤ e ∧ x ∈ class_in(e'))))

Lemma: causal-class-rel-in-out_wf
[f:Name ⟶ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[m:Id × Message(f)]. ∀[class_out:EClass(Id × Message(f))]. ∀[x:T].
  (if class_out outputs (m) then class_in observed x ∈ ℙ')

Definition: mk-msg
mk-msg(auth;hdr;val) ==  <auth, make-basicMsg(hdr;val)>

Lemma: mk-msg_wf
[f:Name ⟶ Type]. ∀[auth:𝔹]. ∀[hdr:Name]. ∀[val:f hdr].  (mk-msg(auth;hdr;val) ∈ Message(f))

Lemma: hdrmkmsg_lemma
val,hdr,auth:Top.  (msg-header(mk-msg(auth;hdr;val)) hdr)

Lemma: mk-msg-equal
[f:Name ⟶ Type]. ∀[auth1,auth2:𝔹]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
  (mk-msg(auth1;hdr1;val1) mk-msg(auth2;hdr2;val2) ∈ Message(f)
  ⇐⇒ {auth1 auth2 ∧ (hdr1 hdr2 ∈ Name) ∧ (val1 val2 ∈ (f hdr1))})

Definition: make-Msg
make-Msg(hdr;val) ==  <ff, make-basicMsg(hdr;val)>

Lemma: make-Msg_wf
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[val:f hdr].  (make-Msg(hdr;val) ∈ Message(f))

Lemma: make-Msg-equal
[f:Name ⟶ Type]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
  (make-Msg(hdr1;val1) make-Msg(hdr2;val2) ∈ Message(f) ⇐⇒ {(hdr1 hdr2 ∈ Name) ∧ (val1 val2 ∈ (f hdr1))})

Lemma: makeMsgfst_lemma
c,a:Top.  (fst(snd(make-Msg(a;c))) a)

Lemma: hdrmakeMsg_lemma
val,hdr:Top.  (msg-header(make-Msg(hdr;val)) hdr)

Lemma: make-Msg-as-mk-msg
[hdr,val:Top].  (make-Msg(hdr;val) mk-msg(ff;hdr;val))

Definition: make-Authentic-Msg
make-Authentic-Msg(hdr;val) ==  <tt, make-basicMsg(hdr;val)>

Lemma: make-Authentic-Msg_wf
[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[val:f hdr].  (make-Authentic-Msg(hdr;val) ∈ Message(f))

Lemma: bodymakeMsg_lemma
val,hdr:Top.  (msg-body(make-Msg(hdr;val)) val)

Lemma: Message-inhabited
[f:Name ⟶ Type]. ↓Message(f) supposing ↓∃h:Name. (↓h)

Lemma: Message-eta
[f:Name ⟶ Type]. ∀[m:Message(f)].
  if msg-authentic(m) then make-Authentic-Msg(msg-header(m);msg-body(m)) else make-Msg(msg-header(m);msg-body(m)) fi 
  ∈ Message(f))

Lemma: Message-eta2
[f:Name ⟶ Type]. ∀[m:Message(f)].  (m mk-msg(msg-authentic(m);msg-header(m);msg-body(m)) ∈ Message(f))

Lemma: base-class-caused-by_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[A:Type]. ∀[Z:A ⟶ EClass(Id × Message(f))]. ∀[hdr:Name]. ∀[X:EClass(f hdr)].
  (hdr.X <-- p.Z[p] ∈ ℙ')

Lemma: es-info-make-Msg
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
  (make-Msg(hdr;v) info(e) ∈ Message(f)) supposing 
     (msg-authentic(info(e)) ff and 
     (msg-body(info(e)) v ∈ (f hdr)) and 
     (header(e) hdr ∈ Name))

Lemma: es-info-mk-msg
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[auth:𝔹]. ∀[hdr:Name]. ∀[v:f hdr].
  (mk-msg(auth;hdr;v) info(e) ∈ Message(f)) supposing 
     (msg-authentic(info(e)) auth and 
     (msg-body(info(e)) v ∈ (f hdr)) and 
     (header(e) hdr ∈ Name))

Lemma: es-info-make-Msg-iff
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
  uiff(make-Msg(hdr;v) info(e) ∈ Message(f);msg-authentic(info(e)) ff
  ∧ (header(e) hdr ∈ Name)
  ∧ (msg-body(info(e)) v ∈ (f hdr)))

Lemma: es-info-make-Msg-iff2
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
  uiff(make-Msg(hdr;v) info(e) ∈ Message(f);es-authentic(es;e) ff
  ∧ (header(e) hdr ∈ Name)
  ∧ (msgval(e) v ∈ (f hdr)))

Definition: message-constraint-swap-hdr
message-constraint-swap-hdr{i:l}(f; es; X; hdr_in; hdrs_out) ==
    ((header(e) hdr_in ∈ Name)
           (((hdr ∈ hdrs_out) ∧ ((f hdr) (f hdr_in) ∈ Type)) ∧ (e' < e) ∧ <loc(e), make-Msg(hdr;msgval(e))> ∈ X(e'))))

Lemma: message-constraint-swap-hdr_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdr_in:Name]. ∀[hdrs_out:Name List].
  (message-constraint-swap-hdr{i:l}(f; es; X; hdr_in; hdrs_out) ∈ ℙ')

Definition: msg-interface
msg interface consists of delay, destination location, and message.

Interface ==  ℤ × Id × Message(f)

Lemma: msg-interface_wf
[f:Name ⟶ Type]. (Interface ∈ Type)

Definition: msg-interface-destination
mi.dst ==  fst(snd(mi))

Lemma: msg-interface-destination_wf
[f:Name ⟶ Type]. ∀[mi:Interface].  (mi.dst ∈ Id)

Definition: msg-interface-message
mi.msg ==  snd(snd(mi))

Lemma: msg-interface-message_wf
[f:Name ⟶ Type]. ∀[mi:Interface].  (mi.msg ∈ Message(f))

Definition: msg-interface-delay
mi.delay ==  fst(mi)

Lemma: msg-interface-delay_wf
[f:Name ⟶ Type]. ∀[mi:Interface].  (mi.delay ∈ ℤ)

Lemma: msg-interface-extensionality
[f:Name ⟶ Type]. ∀[x,y:Interface].
  uiff(x y ∈ Interface;(x.delay y.delay ∈ ℤ) ∧ (x.dst y.dst ∈ Id) ∧ (x.msg y.msg ∈ Message(f)))

Definition: constrained-msg-interface
Interface(to locs, with hdrs) ==  {mi:Interface| (mi.dst ∈ locs) ∧ (msg-header(mi.msg) ∈ hdrs)} 

Lemma: constrained-msg-interface_wf
[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List].  (Interface(to locs, with hdrs) ∈ Type)

Lemma: constrained-msg-interface-valueall-type
[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List].
  valueall-type(Interface(to locs, with hdrs)) supposing (∀h∈hdrs.valueall-type(f h))

Definition: make-msg-interface
make-msg-interface(i;l;m) ==  <i, l, m>

Lemma: make-msg-interface_wf
[f:Name ⟶ Type]. ∀[i:ℤ]. ∀[l:Id]. ∀[m:Message(f)].  (make-msg-interface(i;l;m) ∈ Interface)

Lemma: make-msg-interface-equal
[f:Name ⟶ Type]. ∀[i1,i2:ℤ]. ∀[l1,l2:Id]. ∀[m1,m2:Message(f)].
  (make-msg-interface(i1;l1;m1) make-msg-interface(i2;l2;m2) ∈ Interface
  ⇐⇒ (i1 i2 ∈ ℤ) ∧ (l1 l2 ∈ Id) ∧ (m1 m2 ∈ Message(f)))

Definition: mk-msg-interface
mk-msg-interface(l;m) ==  make-msg-interface(0;l;m)

Lemma: mk-msg-interface_wf
[f:Name ⟶ Type]. ∀[l:Id]. ∀[m:Message(f)].  (mk-msg-interface(l;m) ∈ Interface)

Definition: eo-msg-interface-constraint
eo-msg-interface-constraint(es;X;hdrs;f) ==
  ∀e:E. ((header(e) ∈ hdrs)  (↓∃e':E. ∃delay:ℤ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))

Lemma: eo-msg-interface-constraint_wf
[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdrs:Name List]. ∀[es:EO+(Message(f))].
  (eo-msg-interface-constraint(es;X;hdrs;f) ∈ ℙ)

Lemma: global-order-pairwise-compat-msg-interface-constraint
f:Name ⟶ Type. ∀hdrs:Name List. ∀X:EClass(Interface).
   (∀LL:(Id × Message(f)) List List
        ((∀L1,L2∈LL.  L1 || L2)
         (∃G:(Id × Message(f)) List
             ∧ (∀L∈LL.∃g:E ⟶ E. es-local-embedding(Message(f);global-eo(L);global-eo(G);g)))))))

Lemma: global-order-pairwise-compat-msg-and-classrel
f:Name ⟶ Type. ∀hdrs:Name List. ∀X:EClass(Interface).
   (∀LL:(Id × Message(f)) List List
        ((∀L1,L2∈LL.  L1 || L2)
         (∃G:(Id × Message(f)) List
             ∧ (∀L∈LL.∃g:E ⟶ E. ∀[e:E]. ∀[v:Interface].  (v ∈ X(e) ⇐⇒ v ∈ X(g e))))))))

Definition: msg-interface-constraint
msg-interface-constraint{i:l}(X;hdrs;f) ==
  ∀es:EO+(Message(f)). ∀e:E.
    ((header(e) ∈ hdrs)  (↓∃e':E. ∃delay:ℤ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))

Lemma: msg-interface-constraint_wf
[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdrs:Name List].  (msg-interface-constraint{i:l}(X;hdrs;f) ∈ ℙ')

Definition: msg-interface-constraint-byzantine
msg-interface-constraint-byzantine{i:l}(X;hdrs;faulty;f) ==
  ∀es:EO+(Message(f)). ∀e:E.
    ((header(e) ∈ hdrs)
     (↓∃e':E. ((∃delay:ℤ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))) ∨ (loc(e') ∈ faulty))))

Lemma: msg-interface-constraint-byzantine_wf
[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdrs:Name List]. ∀[faulty:Id List].
  (msg-interface-constraint-byzantine{i:l}(X;hdrs;faulty;f) ∈ ℙ')

Definition: msgs-interface-delivered
msgs-interface-delivered{i:l}(X;f) ==
  ∀es:EO+(Message(f)). ∀e:E. ∀msg:Interface.
    (msg ∈ X(e)  (↓∃e':E. ∃delay:ℤ((e < e') ∧ (msg make-msg-interface(delay;loc(e');info(e')) ∈ Interface))))

Lemma: msgs-interface-delivered_wf
[f:Name ⟶ Type]. ∀X:EClass(Interface). (msgs-interface-delivered{i:l}(X;f) ∈ ℙ')

Definition: eo-msgs-interface-delivered
eo-msgs-interface-delivered(es;X;f) ==
  ∀e:E. ∀msg:Interface.
    (msg ∈ X(e)  (↓∃e':E. ∃delay:ℤ((e < e') ∧ (msg make-msg-interface(delay;loc(e');info(e')) ∈ Interface))))

Lemma: eo-msgs-interface-delivered_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))].  ∀X:EClass(Interface). (eo-msgs-interface-delivered(es;X;f) ∈ ℙ)

Definition: msgs-interface-delivered-with-omissions
msgs-interface-delivered-with-omissions(f;es;X;faulty;failures;ids) ==
  (#(faulty) ≤ failures)
  ∧ (∀e:E. ∀dmsg:Interface.
       (dmsg ∈ X(e)
        loc(e) ↓∈ faulty)
        loc(e) ↓∈ ids
        (↓∃e':E. ∃delay:ℤ((e < e') ∧ (dmsg make-msg-interface(delay;loc(e');info(e')) ∈ Interface)))))

Lemma: msgs-interface-delivered-with-omissions_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Interface)]. ∀[faulty:bag(Id)]. ∀[failures:ℤ]. ∀[ids:bag(Id)].
  (msgs-interface-delivered-with-omissions(f;es;X;faulty;failures;ids) ∈ ℙ)

Definition: msgs-interface-with-omissions-sub
msgs-interface-with-omissions-sub{i:l}(X;failures;ids;f) ==
     ((#(faulty) ≤ failures)
     ∧ (∀e:E. ∀dmsg:Interface.
          (dmsg ∈ X(e)
           loc(e) ↓∈ faulty)
           loc(e) ↓∈ ids
           (↓∃e':E. ∃delay:ℤ((e < e') ∧ (dmsg make-msg-interface(delay;loc(e');info(e')) ∈ Interface))))))

Lemma: msgs-interface-with-omissions-sub_wf
[f:Name ⟶ Type]
  ∀X:EClass(Interface). ∀failures:ℤ. ∀ids:bag(Id).  (msgs-interface-with-omissions-sub{i:l}(X;failures;ids;f) ∈ ℙ')

Definition: msg-interface-hdf
This is the type of local program for main class in EventML.

msg-interface-hdf(f) ==  hdataflow(Message(f);ℤ × Id × Message(f))

Lemma: msg-interface-hdf_wf
[f:Name ⟶ Type]. (msg-interface-hdf(f) ∈ Type)

Definition: single-valued-on-header
single-valued-on-header{i:l}(Info;X;hdr) ==  ∀es:EO+(Info). ∀e:E.  (↑#([x∈X(e)|name_eq(msg-header(x.msg);hdr)]) ≤1)

Lemma: single-valued-on-header_wf
[Info:Type]. ∀[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[hdr:Name].  (single-valued-on-header{i:l}(Info;X;hdr) ∈ ℙ')

Definition: sequential-composition-inputs
sequential-composition-inputs(es;e;X;hdr) ==
  mapfilter(λxs.only([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst loc(e)]).msg;
            λxs.(#([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst loc(e)]) =z 1);

Lemma: sequential-composition-inputs_wf
[Info:Type]. ∀[f:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[hdr:Name].
  sequential-composition-inputs(es;e;X;hdr) ∈ Message(f) List supposing single-valued-on-header{i:l}(Info;X;hdr)

Definition: sequential-composition-class
sequential-composition-class(X;Y;hdr) ==
  λes,e. let xs X(e) in
          let not_hdr [x∈xs|¬bname_eq(msg-header(x.msg);hdr)] in
          let has_hdr [x∈xs|name_eq(msg-header(x.msg);hdr)] in
          if (#(has_hdr) =z 1)
            then let Infos sequential-composition-inputs(es;e;X;hdr) in
                     list-eo(Infos;loc(e)) (||Infos|| 1)
            else {}

Definition: local-simulation-input-validity
local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i) ==
    ((loc(e) i ∈ Id)
     (msg-header(snd(msgval(e))) ∈ hdrs)
     (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))

Lemma: local-simulation-input-validity_wf
[f,g:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[hdrs:Name List]. ∀[i:Id].  (local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i) ∈ ℙ
  supposing hdr encodes Id × Message(g)

Definition: local-simulation-input-consistency
local-simulation-input-consistency(g;X;hdr;locs;es;i;j) ==
    ((loc(e1) i ∈ Id)
     (loc(e2) j ∈ Id)
     local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))

Lemma: local-simulation-input-consistency_wf
[f,g:Name ⟶ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[i,j:Id].  (local-simulation-input-consistency(g;X;hdr;locs;es;i;j) ∈ ℙsupposing hdr encodes Id × Message(g)

Definition: hdf-single-valued-except
halting-dataflow from ⌜Message(f)⌝ to ⌜Interface⌝ is single valued
except on list of headers if after processing any list of messages
it is either halted or else, after filtering out the part of the output
with the given headers, what remains is single-valued bag.⋅

hdf-single-valued-except(f;hdrs;X) ==
  hdf-invariant(Message(f);b.single-valued-bag([x∈b|¬bmsg-header(snd(snd(x))) ∈b hdrs];Interface);X)

Lemma: hdf-single-valued-except_wf
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:msg-interface-hdf(f)].  (hdf-single-valued-except(f;hdrs;X) ∈ ℙ)

Lemma: hdf-ap-single-valued-except
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:{X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} ].
  ∀m:Message(f). (fst(X(m)) ∈ {X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} )

Lemma: hdf-ap-single-valued-except2
[f:Name ⟶ Type]. ∀[hdrs:Name List].
  ∀X:{X:msg-interface-hdf(f)| hdf-single-valued-except(f;hdrs;X)} . ∀m:Message(f).
    single-valued-bag([x∈snd(X(m))|¬bmsg-header(snd(snd(x))) ∈b hdrs];Interface)

Definition: hdf-only-headers
hdf-only-headers(f;hdrs;X) ==  hdf-invariant(Message(f);b.∀mi:Interface. (mi ↓∈  (msg-header(mi.msg) ∈ hdrs));X)

Lemma: hdf-only-headers_wf
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:msg-interface-hdf(f)].  (hdf-only-headers(f;hdrs;X) ∈ ℙ)

Lemma: hdf-ap-only-headers
[f:Name ⟶ Type]. ∀[hdrs:Name List].
  ∀X:{X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} . ∀m:Message(f).
    (fst(X(m)) ∈ {X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} )

Lemma: hdf-ap-only-headers2
[f:Name ⟶ Type]
  ∀hdrs:Name List. ∀X:{X:msg-interface-hdf(f)| hdf-only-headers(f;hdrs;X)} . ∀m:Message(f). ∀mi:Interface.
    (mi ↓∈ snd(X(m))  (msg-header(mi.msg) ∈ hdrs))

Definition: single-valued-class-except
single-valued-class-except{i:l}(f;hdrs;X) ==
  ∀es:EO+(Message(f)). ∀e:E.  single-valued-bag([v∈X(e)|¬bmsg-header(snd(snd(v))) ∈b hdrs];Interface)

Lemma: single-valued-class-except_wf
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)].  (single-valued-class-except{i:l}(f;hdrs;X) ∈ ℙ')

Definition: class-only-headers
is class of type ⌜Interface⌝ such that the only headers in its output
are members of the given list, hdrs.⋅

class-only-headers{i:l}(f;hdrs;X) ==
  ∀es:EO+(Message(f)). ∀e:E. ∀mi:Interface.  (mi ↓∈ X(e)  (msg-header(mi.msg) ∈ hdrs))

Lemma: class-only-headers_wf
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)].  (class-only-headers{i:l}(f;hdrs;X) ∈ ℙ')

Lemma: local-class-single-valued-class-except
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)].
  (single-valued-class-except{i:l}(f;hdrs;X)  (∀P:LocalClass(X). ∀a:Id.  hdf-single-valued-except(f;hdrs;P a)))

Lemma: local-class-only-headers
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[X:EClass(Interface)].
  (class-only-headers{i:l}(f;hdrs;X)  (∀P:LocalClass(X). ∀a:Id.  hdf-only-headers(f;hdrs;P a)))

Definition: msg-body-cmp
msg-body-cmp(mcmp) ==  λm1,m2. (mcmp msg-header(m1) msg-body(m1) msg-body(m2))

Lemma: msg-body-cmp_wf
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
  ∀a:{x:Message(f)| (msg-header(x) ∈ hdrs)} 
    (msg-body-cmp(mcmp) ∈ comparison({b:{m:Message(f)| (msg-header(m) ∈ hdrs)} 
                                      (list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) b) 0 ∈ ℤ))

Definition: message-cmp
message-cmp(hdrs;mcmp) ==
  comparison-seq(list-index-cmp(NameDeq;hdrs;λm.msg-header(m)); msg-body-cmp(mcmp)))

Lemma: message-cmp_wf
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
  (message-cmp(hdrs;mcmp) ∈ comparison({m:Message(f)| (msg-header(m) ∈ hdrs)} ))

Lemma: message-cmp-zero
[f:Name ⟶ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)]. ∀[x,y:{m:Message(f)| 
                                                                                    (msg-header(m) ∈ hdrs)} ].
  uiff((message-cmp(hdrs;mcmp) y) 0 ∈ ℤ;msg-authentic(x) msg-authentic(y)
  ∧ (msg-header(x) msg-header(y) ∈ Name)
  ∧ ((mcmp msg-header(x) msg-body(x) msg-body(y)) 0 ∈ ℤ))

Definition: interface-cmp
Compare members of Interface(to locs, with hdrs) 
"lexicographically" first on the delay,
 then on the index in locs of the dst,
 then on the index in hdrs of the message header,
 finally compare the message bodies using the 
 comparison given by the message header.⋅

interface-cmp(mcmp;locs;hdrs) ==
  comparison-seq(int-minus-comparison(λmi.mi.delay); comparison-seq(list-index-cmp(IdDeq;locs;λmi.mi.dst);

Lemma: interface-cmp_wf
[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
  (interface-cmp(mcmp;locs;hdrs) ∈ comparison(Interface(to locs, with hdrs)))

Lemma: interface-cmp-zero
[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
[x,y:Interface(to locs, with hdrs)].
  (((interface-cmp(mcmp;locs;hdrs) y) 0 ∈ ℤ)
   {(x.delay y.delay ∈ ℤ)
     ∧ (x.dst y.dst ∈ Id)
     ∧ msg-authentic(x.msg) msg-authentic(y.msg)
     ∧ (msg-header(x.msg) msg-header(y.msg) ∈ Name)
     ∧ ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) 0 ∈ ℤ)})

Definition: order-messages
order-messages(mcmp;locs;hdrs) ==  λb.bag-to-list(interface-cmp(mcmp;locs;hdrs);b)

Lemma: order-messages_wf
[allhdrs:Name List]. ∀[f:hdr:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ⟶ comparison(f hdr)].
  order-messages(mcmp;locs;allhdrs) ∈ {b:bag(Interface(to locs, with allhdrs))| 
                                       single-valued-bag([mi∈b|¬bmsg-header(mi.msg) ∈b hdrs];Interface)}  ⟶ (Interface(\000Cto locs, with allhdrs) List) 
  supposing (∀h∈allhdrs.valueall-type(f h)) ∧ (∀h∈hdrs.∀x,y:f h.  (((mcmp y) 0 ∈ ℤ (x y ∈ (f h))))

Definition: event-caused-by
e2 caused by e1 in ==  ∃delay:ℤmake-msg-interface(delay;loc(e2);info(e2)) ∈ S(e1)

Lemma: event-caused-by_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[S:EClass(Interface)]. ∀[e1,e2:E].  (e2 caused by e1 in S ∈ ℙ)

Definition: es-happened-before
e1 ⟶ e2 ==
  fix((λes-happened-before,e2. ∃e:E
                                ((e < e2)
                                ∧ ((¬(loc(e) loc(e2) ∈ Id))  e2 caused by in S)
                                ∧ ((e e1 ∈ E) ∨ (es-happened-before e))))) 

Lemma: es-happened-before_wf
[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[S:EClass(Interface)]. ∀[e1,e2:E].  (e1 ⟶ e2 ∈ ℙ)

Home Index