---

Definition: eo_record
eo_record{i:l}() ==
  "E":Type
  "dom":self."E" ⟶ 𝔹
  "<":self."E" ⟶ self."E" ⟶ ℙ
  "locless":self."E" ⟶ self."E" ⟶ 𝔹
  "loc":self."E" ⟶ Id
  "pred":self."E" ⟶ self."E"
  "rank":self."E" ⟶ ℕ

Lemma: eo_record_wf
eo_record{i:l}() ∈ 𝕌'

Lemma: eo_record_cumulative
eo_record{i:l}() ⊆r eo_record{j:l} supposing Type ⊆r 𝕌{j}

Definition: eo-record-type
eo-record-type{i:l}(r) ==
  λx.if x =a "E" then Type
     if x =a "dom" then r."E" ⟶ 𝔹
     if x =a "<" then r."E" ⟶ r."E" ⟶ ℙ
     if x =a "locless" then r."E" ⟶ r."E" ⟶ 𝔹
     if x =a "loc" then r."E" ⟶ Id
     if x =a "pred" then r."E" ⟶ r."E"
     if x =a "rank" then r."E" ⟶ ℕ
     else Top
     fi 

Lemma: eo-record-type_wf
∀r:eo_record{i:l}(). (eo-record-type{i:l}(r) ∈ Atom ⟶ 𝕌')

Lemma: eo-record-record
∀r:eo_record{i:l}(). (r ∈ record(x.eo-record-type{i:l}(r) x))

Lemma: eo-record-record-eq
∀r:eo_record{i:l}(). ∀r':record(x.eo-record-type{i:l}(r) x).
  ((r' = r ∈ record(x.eo-record-type{i:l}(r) x)) ⇒ (r' = r ∈ eo_record{i:l}()))

Definition: mk-eo-record
mk-eo-record(E;dom;l;R;locless;pred;rank) ==
  λx.x["E" := E]["dom" := dom]["loc" := l]["<" := R]["locless" := locless]["pred" := pred]["rank" := rank]

Lemma: mk-eo-record_wf
∀[E:Type]. ∀[dom:E ⟶ 𝔹]. ∀[l:E ⟶ Id]. ∀[R:E ⟶ E ⟶ ℙ]. ∀[locless:E ⟶ E ⟶ 𝔹]. ∀[pred:E ⟶ E]. ∀[rank:E ⟶ ℕ].
  (mk-eo-record(E;dom;l;R;locless;pred;rank) ∈ eo_record{i:l}())

Definition: eo_axioms
eo_axioms(r) ==
  (∀x,y:r."E".  ((↓x r."<" y) ⇒ r."rank" x < r."rank" y))
  ∧ (∀e:r."E". ((r."loc" (r."pred" e)) = (r."loc" e) ∈ Id))
  ∧ (∀e:r."E". (¬↓e r."<" (r."pred" e)))
  ∧ (∀e,x:r."E".
       ((↓x r."<" e) ⇒ ((r."loc" x) = (r."loc" e) ∈ Id) ⇒ ((↓(r."pred" e) r."<" e) ∧ (¬↓(r."pred" e) r."<" x))))
  ∧ (∀x,y,z:r."E".  ((↓x r."<" y) ⇒ (↓y r."<" z) ⇒ (↓x r."<" z)))
  ∧ (∀e1,e2:r."E".
       (↓e1 r."<" e2 ⇐⇒ ↑(e1 r."locless" e2)) ∧ ((¬↓e1 r."<" e2) ⇒ (¬↓e2 r."<" e1) ⇒ (e1 = e2 ∈ r."E")) 
       supposing (r."loc" e1) = (r."loc" e2) ∈ Id)

Lemma: eo_axioms_wf
∀[r:eo_record{i:l}()]. (eo_axioms(r) ∈ ℙ)

Lemma: sq_stable__eo_axioms
∀[r:eo_record{i:l}()]. SqStable(eo_axioms(r))

Definition: event_ordering
EO ==  {r:eo_record{i:l}()| eo_axioms(r)} 

Lemma: event_ordering_wf
EO ∈ 𝕌'

Lemma: event_ordering_axioms
∀eo:EO. eo_axioms(eo)

Lemma: event_ordering_cumulative
EO ⊆r event_ordering{j:l} supposing Type ⊆r 𝕌{j}

Definition: mk-eo
mk-eo(E;dom;l;R;locless;pred;rank) ==  mk-eo-record(E;dom;l;R;locless;pred;rank)

Lemma: mk-eo_wf
∀[E:Type]. ∀[dom:E ⟶ 𝔹]. ∀[l:E ⟶ Id]. ∀[R:E ⟶ E ⟶ ℙ]. ∀[locless:E ⟶ E ⟶ 𝔹]. ∀[pred:E ⟶ E]. ∀[rank:E ⟶ ℕ].
  mk-eo(E;dom;l;R;locless;pred;rank) ∈ EO 
  supposing (∀x,y:E.  ((↓x R y) ⇒ rank x < rank y))
  ∧ (∀e:E. ((l (pred e)) = (l e) ∈ Id))
  ∧ (∀e:E. (¬↓e R (pred e)))
  ∧ (∀e,x:E.  ((↓x R e) ⇒ ((l x) = (l e) ∈ Id) ⇒ ((↓(pred e) R e) ∧ (¬↓(pred e) R x))))
  ∧ (∀x,y,z:E.  ((↓x R y) ⇒ (↓y R z) ⇒ (↓x R z)))
  ∧ (∀e1,e2:E.
       (↓e1 R e2 ⇐⇒ ↑(e1 locless e2)) ∧ ((¬↓e1 R e2) ⇒ (¬↓e2 R e1) ⇒ (e1 = e2 ∈ E)) supposing (l e1) = (l e2) ∈ Id)

Definition: es-base-E
es-base-E(es) ==  es."E"

Lemma: es-base-E_wf
∀[es:EO]. (es-base-E(es) ∈ Type)

Definition: es-dom
es-dom(es) ==  es."dom"

Lemma: es-dom_wf
∀[es:EO]. (es-dom(es) ∈ es-base-E(es) ⟶ 𝔹)

Definition: es-E
E ==  {e:es."E"| ↑(es."dom" e)} 

Lemma: es-E_wf
∀[the_es:EO]. (E ∈ Type)

Lemma: es-E-subtype
∀[es:EO]. strong-subtype(E;es-base-E(es))

Definition: eo-reset-dom
eo-reset-dom(es;d) ==  es["dom" := d]

Lemma: eo-reset-dom_wf
∀[es:EO]. ∀[d:es-base-E(es) ⟶ 𝔹].  (eo-reset-dom(es;d) ∈ EO)

Lemma: eo-reset-dom-reset-dom
∀[es:EO]. ∀[d1,d2:es-base-E(es) ⟶ 𝔹].  (eo-reset-dom(eo-reset-dom(es;d1);d2) = eo-reset-dom(es;d2) ∈ EO)

Definition: eo-restrict
eo-restrict(eo;P) ==  eo["dom" := λe.((eo."dom" e) ∧b (P e))]

Lemma: eo-restrict_wf
∀[es:EO]. ∀[P:E ⟶ 𝔹].  (eo-restrict(es;P) ∈ EO)

Definition: es-loc
loc(e) ==  es."loc" e

Lemma: es-loc_wf
∀[the_es:EO]. ∀[e:E].  (loc(e) ∈ Id)

Lemma: es-loc-wf-base
∀[the_es:EO]. ∀[e:es-base-E(the_es)].  (loc(e) ∈ Id)

Definition: es-base-pred
pred1(e) ==  es."pred" e

Lemma: es-base-pred_wf
∀[the_es:EO]. ∀[e:es-base-E(the_es)].  (pred1(e) ∈ es-base-E(the_es))

Definition: es-causl
(e < e') ==  ↓e es."<" e'

Lemma: es-causl_wf
∀[the_es:EO]. ∀[e,e':E].  ((e < e') ∈ ℙ)

Lemma: sq_stable__es-causl
∀[the_es:EO]. ∀[e,e':E].  SqStable((e < e'))

Lemma: es-causl-wf-base
∀[the_es:EO]. ∀[e,e':es-base-E(the_es)].  ((e < e') ∈ ℙ)

Definition: es-locless
es-locless(es;e1;e2) ==  e1 es."locless" e2

Lemma: es-locless_wf
∀[es:EO]. ∀[e,e':E].  (es-locless(es;e;e') ∈ 𝔹)

Lemma: es-locless-wf-base
∀[the_es:EO]. ∀[e,e':es-base-E(the_es)].  (es-locless(the_es;e;e') ∈ 𝔹)

Definition: es-rank
es-rank(es;e) ==  es."rank" e

Lemma: es-rank_wf
∀[es:EO]. ∀[e:E].  (es-rank(es;e) ∈ ℕ)

Lemma: es-rank-wf-base
∀[es:EO]. ∀[e:es-base-E(es)].  (es-rank(es;e) ∈ ℕ)

Lemma: event_ordering_properties
∀eo:EO
  ((∀x,y:es-base-E(eo).  ((x < y) ⇒ es-rank(eo;x) < es-rank(eo;y)))
  ∧ (∀e:es-base-E(eo). (loc(pred1(e)) = loc(e) ∈ Id))
  ∧ (∀e:es-base-E(eo). (¬(e < pred1(e))))
  ∧ (∀e,x:es-base-E(eo).  ((x < e) ⇒ (loc(x) = loc(e) ∈ Id) ⇒ ((pred1(e) < e) ∧ (¬(pred1(e) < x)))))
  ∧ (∀x,y,z:es-base-E(eo).  ((x < y) ⇒ (y < z) ⇒ (x < z)))
  ∧ (∀e1,e2:es-base-E(eo).
       ((e1 < e2) ⇐⇒ ↑es-locless(eo;e1;e2)) ∧ ((¬(e1 < e2)) ⇒ (¬(e2 < e1)) ⇒ (e1 = e2 ∈ es-base-E(eo))) 
       supposing loc(e1) = loc(e2) ∈ Id))

Lemma: es-base-pred-properties
∀es:EO. ∀e:es-base-E(es).
  ((loc(pred1(e)) = loc(e) ∈ Id)
  ∧ (¬(e < pred1(e)))
  ∧ (∀x:es-base-E(es). ((x < e) ⇒ (loc(x) = loc(e) ∈ Id) ⇒ ((pred1(e) < e) ∧ (¬(pred1(e) < x))))))

Lemma: es-locless-property
∀es:EO. ∀x,y:es-base-E(es).
  ((loc(x) = loc(y) ∈ Id)
  ⇒ (((x < y) ⇐⇒ ↑es-locless(es;x;y))
     ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es)))))

Lemma: decidable__es-causl-same-loc
∀es:EO. ∀x,y:es-base-E(es).  ((loc(x) = loc(y) ∈ Id) ⇒ Dec((x < y)))

Lemma: assert-es-locless
∀es:EO. ∀x,y:es-base-E(es).  ↑es-locless(es;x;y) ⇐⇒ (x < y) supposing loc(x) = loc(y) ∈ Id

Lemma: eo-restrict_property
∀es:EO. ∀P:E ⟶ 𝔹.  (E ≡ {e:E| ↑(P e)}  ∧ (∀e:E. (loc(e) = loc(e) ∈ Id)) ∧ (∀e1,e2:E.  ((e1 < e2) ⇐⇒ (e1 < e2))))

Lemma: eo-restrict-restrict
∀[es:EO]. ∀[P:E ⟶ 𝔹]. ∀[Q:{e:E| ↑(P e)}  ⟶ 𝔹].
  (eo-restrict(eo-restrict(es;P);Q) = eo-restrict(es;λe.((P e) ∧b (Q e))) ∈ EO)

Lemma: es-causl_transitivity
∀es:EO. ∀x,y,z:es-base-E(es).  ((x < y) ⇒ (y < z) ⇒ (x < z))

Lemma: es-rank_property-base
∀[es:EO]. ∀[e1,e2:es-base-E(es)].  es-rank(es;e1) < es-rank(es;e2) supposing (e1 < e2)

Lemma: es-rank_property
∀[es:EO]. ∀[e1,e2:E].  es-rank(es;e1) < es-rank(es;e2) supposing (e1 < e2)

Lemma: es-causl-swellfnd-base
∀es:EO. SWellFounded((e < e'))

Lemma: es-causl-swellfnd
∀es:EO. SWellFounded((e < e'))

Lemma: es-causal-antireflexive
∀[the_es:EO]. ∀[e:es-base-E(the_es)].  (¬(e < e))

Lemma: es-causl-total-base
∀es:EO. ∀e,e':es-base-E(es).  (e = e' ∈ es-base-E(es)) ∨ (e < e') ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id

Lemma: es-causl-total
∀es:EO. ∀e,e':E.  (e = e' ∈ E) ∨ (e < e') ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id

Definition: es-eq
es-eq(es) ==  λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1)))

Lemma: es-eq_wf
∀[es:EO]. (es-eq(es) ∈ EqDecider(E))

Lemma: es-eq-wf-base
∀[es:EO]. (es-eq(es) ∈ EqDecider(es-base-E(es)))

Definition: es-eq-E
e = e' ==  es-eq(es) e e'

Lemma: es-eq-E_wf
∀[es:EO]. ∀[e,e':E].  (e = e' ∈ 𝔹)

Lemma: es-eq-E-wf-base
∀[es:EO]. ∀[e,e':es-base-E(es)].  (e = e' ∈ 𝔹)

Lemma: decidable__equal-es-E
∀es:EO. ∀e,e':E.  Dec(e = e' ∈ E)

Lemma: decidable__equal-es-base-E
∀es:EO. ∀e,e':es-base-E(es).  Dec(e = e' ∈ es-base-E(es))

Lemma: assert-es-eq-E
∀[the_es:EO]. ∀[e,e':E].  uiff(e = e' ∈ E;↑e = e')

Lemma: assert-es-eq-E-base
∀[es:EO]. ∀[e,e':es-base-E(es)].  uiff(e = e' ∈ es-base-E(es);↑e = e')

Lemma: assert-es-eq-E-2
∀[the_es:EO]. ∀[e,e':E].  uiff(↑e = e';e = e' ∈ E)

Lemma: es-base-pred-less
∀es:EO. ∀e:es-base-E(es).  ((¬↑(es-eq(es) pred1(e) e)) ⇒ (pred1(e) < e))

Lemma: es-base-pred-le
∀es:EO. ∀e:es-base-E(es).  ((pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es)))

Definition: es-pred
pred(e) ==  fix((λes-pred,e. let p = pred1(e) in if es-dom(es) p then p if es-eq(es) p e then e else es-pred p fi )) e

Lemma: es-pred-wf-base
∀[es:EO]. ∀[e:es-base-E(es)].  (pred(e) ∈ es-base-E(es))

Definition: es-first
first(e) ==  pred(e) = e ∨b(¬b(es-dom(es) pred(e)))

Lemma: es-first_wf
∀[es:EO]. ∀[e:es-base-E(es)].  (first(e) ∈ 𝔹)

Lemma: es-pred_wf
∀[the_es:EO]. ∀[e:E].  pred(e) ∈ E supposing ¬↑first(e)

Lemma: es-pred-loc-base
∀es:EO. ∀e:es-base-E(es).  (loc(pred(e)) = loc(e) ∈ Id)

Lemma: es-pred-less-base
∀es:EO. ∀e:es-base-E(es).  ((¬(pred(e) = e ∈ es-base-E(es))) ⇒ (pred(e) < e))

Lemma: es-pred-maximal-base
∀es:EO. ∀e:es-base-E(es). ∀e':E.  ((loc(e') = loc(e) ∈ Id) ⇒ (e' < e) ⇒ (pred(e) < e') ⇒ False)

Lemma: es-pred_property_base
∀es:EO. ∀e:es-base-E(es).
  ((loc(pred(e)) = loc(e) ∈ Id)
  ∧ ((pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es)))
  ∧ (∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ es-base-E(es)) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id))

Lemma: es-pred_property
∀es:EO. ∀e:E.
  {(loc(pred(e)) = loc(e) ∈ Id)
  ∧ (pred(e) < e)
  ∧ (∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id)} 
  supposing ¬↑first(e)

Lemma: es-pred-cle
∀es:EO. ∀e:es-base-E(es).  ((pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es)))

Lemma: assert-es-first
∀[es:EO]. ∀[e:E].  uiff(↑first(e);∀[e':E]. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id)

Definition: es-pred?
es-pred?(es;e) ==  if first(e) then inr ⋅  else inl pred(e) fi 

Lemma: es-pred?_property
∀es:EO. ∀e:E.
  case es-pred?(es;e)
   of inl(p) =>
   (loc(p) = loc(e) ∈ Id) ∧ (p < e) ∧ (∀e':E. (e' < e) ⇒ ((e' = p ∈ E) ∨ (e' < p)) supposing loc(e') = loc(e) ∈ Id)
   | inr(z) =>
   ∀e':E. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id

Definition: es-pred-eq
es-pred-eq(es;e) ==  if first(e) then e else pred(e) fi 

Lemma: es-pred-eq_wf
∀[es:EO]. ∀[e:E].  (es-pred-eq(es;e) ∈ E)

Definition: es-locl
(e <loc e') ==  (loc(e) = loc(e') ∈ Id) ∧ (e < e')

Lemma: es-locl_wf
∀[the_es:EO]. ∀[e,e':E].  ((e <loc e') ∈ ℙ)

Lemma: es-pred?_wf
∀[es:EO]. ∀[e:E].  (es-pred?(es;e) ∈ {e':E| (e' <loc e) ∧ (e' = pred(e) ∈ E)} ?)

Definition: es-le
e ≤loc e'  ==  (e <loc e') ∨ (e = e' ∈ E)

Definition: alle-at
∀e@i.P[e] ==  ∀e:E. ((loc(e) = i ∈ Id) ⇒ P[e])

Definition: existse-ge
∃e'≥e.P[e'] ==  ∃e':E. (e ≤loc e'  ∧ P[e'])

Definition: loc-ordered
loc-ordered(es;L) ==  l-ordered(E;x,y.(x <loc y);L)

Lemma: es-loc-pred
∀[the_es:EO]. ∀[e:E].  loc(pred(e)) = loc(e) ∈ Id supposing ¬↑first(e)

Lemma: es-loc-pred-plus
∀[es:EO]. ∀[x,y:E].  loc(x) = loc(y) ∈ Id supposing x λx,y. ((¬↑first(y)) c∧ (x = pred(y) ∈ E))+ y

Definition: es-blocl
es-blocl(es;e1;e2) ==  es-locless(es;e1;e2) ∧b loc(e1) = loc(e2)

Lemma: es-blocl_wf
∀[es:EO]. ∀[e1,e2:E].  (es-blocl(es;e1;e2) ∈ 𝔹)

Lemma: es-blocl-iff
∀es:EO. ∀e1,e2:E.  (↑es-blocl(es;e1;e2) ⇐⇒ (e1 <loc e2))

Lemma: es-le_wf
∀[the_es:EO]. ∀[e,e':E].  (e ≤loc e'  ∈ ℙ)

Lemma: reduce-bool-bfalse
∀T:Type. ∀f:T ⟶ 𝔹 ⟶ 𝔹. ∀L:T List.  (reduce(λx,b. (b ∧b f[x;b]);ff;L) ~ ff)

Lemma: es-locl-wellfnd
∀es:EO. WellFnd{i}(E;x,y.(x <loc y))

Lemma: es-locl-antireflexive
∀[the_es:EO]. ∀[e:E].  (¬(e <loc e))

Lemma: es-locl_irreflexivity
∀[the_es:EO]. ∀[e:E].  False supposing (e <loc e)

Lemma: pes-axioms
∀the_es:EO
  (Trans(E;e,e'.(e <loc e'))
  ∧ SWellFounded((e <loc e'))
  ∧ (∀e,e':E.  (loc(e) = loc(e') ∈ Id ⇐⇒ (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e)))
  ∧ (∀e:E. (↑first(e) ⇐⇒ ∀e':E. (¬(e' <loc e))))
  ∧ (∀e:E. (pred(e) <loc e) ∧ (∀e':E. (¬((pred(e) <loc e') ∧ (e' <loc e)))) supposing ¬↑first(e))
  ∧ Trans(E;e,e'.(e < e'))
  ∧ SWellFounded((e < e'))
  ∧ (∀e,e':E.  ((e <loc e') ⇒ (e < e'))))

Lemma: es-le-loc
∀[es:EO]. ∀[e,e':E].  loc(e) = loc(e') ∈ Id supposing e ≤loc e' 

Lemma: es-locl-iff
∀the_es:EO. ∀e,e':E.  ((e <loc e') ⇐⇒ (¬↑first(e')) ∧ ((e = pred(e') ∈ E) ∨ (e <loc pred(e'))))

Lemma: es-locl-first
∀[the_es:EO]. ∀[e,e':E].  first(e') = ff supposing (e <loc e')

Lemma: alle-at_wf
∀[es:EO]. ∀[i:Id]. ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ].  (∀e@i.P[e] ∈ ℙ)

Lemma: es-le-first
∀[es:EO]. ∀[j,e:E].  if first(j) then j else e fi  = e ∈ E supposing e ≤loc j 

Lemma: existse-ge_wf
∀[es:EO]. ∀[e:E]. ∀[P:{e':E| loc(e') = loc(e) ∈ Id}  ⟶ ℙ].  (∃e'≥e.P[e'] ∈ ℙ)

Lemma: loc-ordered_wf
∀[es:EO]. ∀[L:E List].  (loc-ordered(es;L) ∈ ℙ)

Lemma: loc-ordered-equality
∀es:EO. ∀as,bs:E List.
  (loc-ordered(es;as) ⇒ loc-ordered(es;bs) ⇒ (as = bs ∈ (E List) ⇐⇒ ∀e:E. ((e ∈ as) ⇐⇒ (e ∈ bs))))

Lemma: loc-ordered-filter
∀es:EO. ∀as:E List.  (loc-ordered(es;as) ⇒ (∀P:{e:E| (e ∈ as)}  ⟶ 𝔹. loc-ordered(es;filter(P;as))))

Lemma: es-first_wf2
∀[es:EO]. ∀[e:E].  (first(e) ∈ 𝔹)

Definition: event_system_typename
event_system_typename() ==  ℕ6

Lemma: event_system_typename_wf
event_system_typename() ∈ Type

Lemma: decidable__es-E-equal
∀the_es:EO. ∀e,e':E.  Dec(e = e' ∈ E)

Lemma: es-E-equality-univ-independent
∀[es:EO]. ∀[e,e':E].
  (TERMOF{decidable__es-E-equal:o, 1:l, i:l} es e' e ~ TERMOF{decidable__es-E-equal:o, 1:l, 1:l} es e' e)

Lemma: test-eq-E-update
∀[es:EO]. ∀[e:E].  (↑e = e)

Lemma: event_system-level-subtype
EO ⊆r event_ordering{i':l}

Definition: mk-eval
mk-eval(E;eq;prd;info;oax;T;w;a;sax;V;v) ==  <E, eq, prd, info, oax, T, w, a, sax, V, v, ⋅>

Definition: es-causle
e c≤ e' ==  (e < e') ∨ (e = e' ∈ E)

Lemma: es-causle_wf
∀[the_es:EO]. ∀[e,e':E].  (e c≤ e' ∈ ℙ)

Lemma: sq_stable__es-causle
∀the_es:EO. ∀e,e':E.  SqStable(e c≤ e')

Lemma: es-locl-trans
∀the_es:EO. Trans(E;x,y.(x <loc y))

Lemma: es-locl-trichotomy
∀the_es:EO. ∀e,e':E.  (loc(e) = loc(e') ∈ Id ⇐⇒ (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e))

Lemma: es-le-trans
∀the_es:EO. Trans(E;x,y.x ≤loc y )

Lemma: es-locl_transitivity
∀es:EO. ∀a,b,c:E.  ((a <loc b) ⇒ (b <loc c) ⇒ (a <loc c))

Lemma: es-locl_transitivity1
∀es:EO. ∀a,b,c:E.  (a ≤loc b  ⇒ (b <loc c) ⇒ (a <loc c))

Lemma: es-locl_transitivity2
∀es:EO. ∀a,b,c:E.  ((a <loc b) ⇒ b ≤loc c  ⇒ (a <loc c))

Lemma: es-le_transitivity
∀es:EO. ∀a,b,c:E.  (a ≤loc b  ⇒ b ≤loc c  ⇒ a ≤loc c )

Lemma: es-le_weakening
∀es:EO. ∀a,b:E.  ((a <loc b) ⇒ a ≤loc b )

Lemma: es-le_weakening_eq
∀es:EO. ∀a,b:E.  a ≤loc b  supposing a = b ∈ E

Lemma: es-locl-trans-test
∀es:EO. ∀a,b,c,d,e,f:E.  (a ≤loc b  ⇒ b ≤loc c  ⇒ (c <loc d) ⇒ d ≤loc e  ⇒ e ≤loc f  ⇒ a ≤loc f )

Lemma: es-locl-irreflex-test
∀[es:EO]. ∀[e2,e:E].  ¬(e = e2 ∈ E) supposing (e <loc e2)

Lemma: es-le-trans2
∀es:EO. ∀a,b,c:E.  (a ≤loc b  ⇒ (b <loc c) ⇒ (a <loc c))

Lemma: es-le-trans3
∀es:EO. ∀a,b,c:E.  ((a <loc b) ⇒ b ≤loc c  ⇒ (a <loc c))

Lemma: es-causle-trans
∀the_es:EO. Trans(E;x,y.x c≤ y)

Lemma: es-causl-trans3
∀es:EO. ∀a,b,c:E.  ((a < b) ⇒ b c≤ c ⇒ (a < c))

Lemma: es-causle_transitivity
∀es:EO. ∀x,y,z:E.  (x c≤ y ⇒ y c≤ z ⇒ x c≤ z)

Lemma: es-causl_transitivity1
∀es:EO. ∀x,y,z:E.  (x c≤ y ⇒ (y < z) ⇒ (x < z))

Lemma: es-causl_transitivity2
∀es:EO. ∀x,y,z:E.  ((x < y) ⇒ y c≤ z ⇒ (x < z))

Lemma: es-causle_weakening
∀es:EO. ∀a,b:E.  ((a < b) ⇒ a c≤ b)

Lemma: es-causle_weakening_eq
∀es:EO. ∀a,b:E.  a c≤ b supposing a = b ∈ E

Lemma: es-causle_weakening_locl
∀es:EO. ∀a,b:E.  (a ≤loc b  ⇒ a c≤ b)

Lemma: es-causl_weakening
∀es:EO. ∀a,b:E.  ((a <loc b) ⇒ (a < b))

Lemma: es-causl-trans-test
∀es:EO. ∀a,b,c,d,e,f:E.  (a c≤ b ⇒ b ≤loc c  ⇒ (c < d) ⇒ d c≤ e ⇒ e c≤ f ⇒ (a < f))

Lemma: es-le-causle
∀es:EO. ∀e,e':E.  (e ≤loc e'  ⇒ e c≤ e')

Lemma: es-locl-total
∀es:EO. ∀e,e':E.  (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e) supposing loc(e) = loc(e') ∈ Id

Lemma: es-locl-total2
∀es:EO. ∀e,e':E.  (e <loc e') ∨ (e' = e ∈ E) ∨ (e' <loc e) supposing loc(e) = loc(e') ∈ Id

Lemma: same-loc-total
∀es:EO. ∀e,e':E.  (e < e') ∨ (e = e' ∈ E) ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id

Lemma: same-loc-total2
∀es:EO. ∀e,e':E.  (e < e') ∨ (e' = e ∈ E) ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id

Lemma: es-le-total
∀es:EO. ∀e,e':E.  e ≤loc e'  ∨ e' ≤loc e  supposing loc(e) = loc(e') ∈ Id

Lemma: es-le-linorder
∀es:EO. ∀i:Id.  Linorder({e:E| loc(e) = i ∈ Id} ;a,b.a ≤loc b )

Lemma: es-locl-swellfnd
∀the_es:EO. SWellFounded((x <loc y))

Lemma: es-causl-wellfnd
∀the_es:EO. WellFnd{i}(E;x,y.(x < y))

Definition: es-locally-ordered
es-locally-ordered(es;L) ==
  rec-case(L) of
  [] => True
  e::rest =>
   r.if null(rest) then True
  if (||rest|| =z 1) then (e <loc hd(rest))
  else (e <loc hd(rest)) ∧ r
  fi 

Lemma: es-locally-ordered_wf
∀[es:EO]. ∀[L:E List].  (es-locally-ordered(es;L) ∈ ℙ)

Definition: es-locl-op
LocalOrderPreserving(f) ==  order-preserving(T;E;e1,e2.(e1 <loc e2);e1,e2.(e1 <loc e2);f)

Lemma: es-locl-op_wf
∀[es:EO]. ∀[T:Type]. ∀[f:T ⟶ E].  LocalOrderPreserving(f) ∈ ℙ supposing T ⊆r E

Lemma: es-le-not-locl
∀es:EO. ∀e,e':E.  e ≤loc e'  ⇐⇒ ¬(e' <loc e) supposing loc(e) = loc(e') ∈ Id

Lemma: es-causl_irreflexivity
∀[es:EO]. ∀[e:E].  False supposing (e < e)

Lemma: es-causal-antisymmetric
∀[es:EO]. ∀[e,e':E].  ¬(e' < e) supposing (e < e')

Lemma: es-causle_antisymmetry
∀[es:EO]. ∀[a,b:E].  (a = b ∈ E) supposing (b c≤ a and a c≤ b)

Lemma: es-causl-locl
∀the_es:EO. ∀e,e':E.  ((e < e') ⇒ (e <loc e') supposing loc(e) = loc(e') ∈ Id)

Lemma: es-causle-le
∀the_es:EO. ∀e,e':E.  (e c≤ e' ⇒ e ≤loc e'  supposing loc(e) = loc(e') ∈ Id)

Lemma: es-pred-locl
∀the_es:EO. ∀j:E.  (pred(j) <loc j) supposing ¬↑first(j)

Lemma: es-pred-le
∀the_es:EO. ∀j:E.  pred(j) ≤loc j  supposing ¬↑first(j)

Lemma: es-le-self
∀es:EO. ∀e:E.  e ≤loc e 

Lemma: es-pred-causl
∀the_es:EO. ∀j:E.  (pred(j) < j) supposing ¬↑first(j)

Lemma: es-causl-max-list
∀es:EO. ∀L:E List.  (0 < ||L|| ⇒ (¬(∀e:{e:E| (e ∈ L)} . ∃e':{e:E| (e ∈ L)} . (e < e'))))

Lemma: es-pred-exists-between
∀es:EO. ∀e1,e2:E.  ((e1 <loc e2) ⇒ (∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)))

Lemma: es-causl-if-pred
∀es:EO. ∀e1,e2:E.  ((¬↑first(e2)) ⇒ (e1 < pred(e2)) ⇒ (e1 < e2))

Lemma: es-causle-retraction
∀es:EO. ∀[T:Type]. ∀f:T ⟶ T. ((∀x:T. f x c≤ x) ⇒ retraction(T;f)) supposing strong-subtype(T;E)

Lemma: es-causle-retraction-squash
∀es:EO. ∀[T:Type]. ∀f:T ⟶ T. ((∀x:T. f x c≤ x) ⇒ retraction(T;f)) supposing strong-subtype(T;E)

Definition: es-fix
f**(e) ==  f**(e)

Lemma: es-fix_wf
∀[es:EO]. ∀[T:Type].  ∀[f:T ⟶ T]. ∀[e:T]. (f**(e) ∈ T) supposing ∀x:T. f x c≤ x supposing strong-subtype(T;E)

Lemma: es-fix-cases
∀[es,f,e:Top].  (f**(e) ~ if e = f e then e else f**(f e) fi )

Lemma: es-first-implies
∀[the_es:EO]. ∀[j,e:E].  ¬(e <loc j) supposing ↑first(j)

Lemma: es-le-iff
∀the_es:EO. ∀e,e':E.  (e ≤loc e'  ⇐⇒ ((¬↑first(e')) c∧ e ≤loc pred(e') ) ∨ (e = e' ∈ E))

Lemma: es-le-iff-causle
∀es:EO. ∀e,e':E.  (e ≤loc e'  ⇐⇒ e c≤ e' ∧ (loc(e) = loc(e') ∈ Id))

Lemma: es-first-le
∀es:EO. ∀e,e':E.  (e ≤loc e' ) supposing ((loc(e) = loc(e') ∈ Id) and (↑first(e)))

Lemma: es-le-antisymmetric
∀[es:EO]. ∀[e,e':E].  (e = e' ∈ E) supposing (e' ≤loc e  and e ≤loc e' )

Lemma: es-le_antisymmetry
∀[es:EO]. ∀[e,e':E].  (e = e' ∈ E) supposing (e' ≤loc e  and e ≤loc e' )

Lemma: es-first-unique
∀[es:EO]. ∀[e,e':E].  (e = e' ∈ E) supposing ((loc(e) = loc(e') ∈ Id) and (↑first(e')) and (↑first(e)))

Lemma: implies-es-pred
∀[the_es:EO]. ∀[e,e':E].  e = pred(e') ∈ E supposing (e <loc e') ∧ (∀e1:E. (¬((e <loc e1) ∧ (e1 <loc e'))))

Lemma: es-le-pred
∀the_es:EO. ∀e,e':E.  e ≤loc pred(e')  ⇐⇒ (e <loc e') supposing ¬↑first(e')

Lemma: implies-es-le-pred
∀the_es:EO. ∀e,e':E.  ((e <loc e') ⇒ e ≤loc pred(e') )

Lemma: implies-es-pred2
∀[es:EO]. ∀[e,e':E].  (e' = pred(e) ∈ E) supposing ((e' <loc e) and pred(e) ≤loc e'  and (¬↑first(e)))

Lemma: es-pred-locl-implies-le
∀es:EO. ∀e1,e2:E.  ((¬↑first(e1)) ⇒ (pred(e1) <loc e2) ⇒ e1 ≤loc e2 )

Lemma: es-locl-pred
∀es:EO. ∀e1,e2:E.  ((¬↑first(e1)) ⇒ (e1 <loc e2) ⇒ (pred(e1) <loc pred(e2)))

Lemma: es-pred-one-one
∀[es:EO]. ∀[a,b:E].  (a = b ∈ E) supposing ((pred(a) = pred(b) ∈ E) and (¬↑first(b)) and (¬↑first(a)))

Lemma: es-pred-exists-between2
∀es:EO. ∀e1,e2:E.  ((e1 <loc e2) ⇒ (∃e:{e:E| ¬↑first(e)} . ((e1 = pred(e) ∈ E) ∧ e ≤loc e2 )))

Lemma: es-next
∀es:EO. ∀e,a:E.  ((a <loc e) ⇒ (∃b:E. ((¬↑first(b)) c∧ ((a = pred(b) ∈ E) ∧ b ≤loc e ))))

Definition: es-last-event
es-last-event(es;P;e) ==
  fix((λes-last-event,e. if P e then inl e if first(e) then inr (λx.⋅)  else es-last-event pred(e) fi )) e

Lemma: es-last-event_wf
∀[es:EO]. ∀[e:E]. ∀[P:{e':E| e' ≤loc e }  ⟶ 𝔹].
  (es-last-event(es;P;e) ∈ (∃e':{E| (e' ≤loc e  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| (e' ≤loc e  ∧ (↑(P e')))})))

Definition: es-bless
e <loc e' ==  es-blocl(es;e;e')

Lemma: es-bless_wf
∀[es:EO]. ∀[e,e':E].  (e <loc e' ∈ 𝔹)

Lemma: assert-es-bless
∀es:EO. ∀e,e':E.  (↑e <loc e' ⇐⇒ (e <loc e'))

Lemma: es-blocl-is-bless
∀es:EO. ∀e,e':E.  (e <loc e' ~ es-blocl(es;e;e'))

Lemma: decidable__es-locl
∀the_es:EO. ∀e',e:E.  Dec((e <loc e'))

Lemma: decidable__es-le
∀the_es:EO. ∀e',e:E.  Dec(e ≤loc e' )

Lemma: es-locl-not-le
∀es:EO. ∀e,e':E.  (e <loc e') ⇐⇒ ¬e' ≤loc e  supposing loc(e) = loc(e') ∈ Id

Lemma: last-event-of-set
∀es:EO. ∀n:ℕ+. ∀f:ℕn ⟶ E.  ∃k:ℕn. ∀i:ℕn. f i ≤loc f k  supposing ∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)

Definition: es-ble
e ≤loc e' ==  e <loc e' ∨be = e'

Lemma: es-ble_wf
∀[es:EO]. ∀[e,e':E].  (e ≤loc e' ∈ 𝔹)

Lemma: es-ble-wf-base
∀[es:EO]. ∀[e,e':es-base-E(es)].  (e ≤loc e' ∈ 𝔹)

Lemma: assert-es-ble
∀es:EO. ∀e,e':E.  (↑e ≤loc e' ⇐⇒ e ≤loc e' )

Lemma: assert-es-ble-base
∀es:EO. ∀e,e':es-base-E(es).  (↑e ≤loc e' ⇐⇒ ((loc(e) = loc(e') ∈ Id) ∧ (e < e')) ∨ (e = e' ∈ es-base-E(es)))

Lemma: es-bless-not-ble
∀[es:EO]. ∀[e,e':E].  e <loc e' ~ ¬be' ≤loc e supposing loc(e) = loc(e') ∈ Id

Lemma: es-maximal-event
∀es:EO
  ∀[P:E ⟶ ℙ]
    ((∀e:E. Dec(P[e]))
    ⇒ (∀e:E
          ((∃m:E. (m ≤loc e  ∧ P[m] ∧ (∀e':E. ((m <loc e') ⇒ e' ≤loc e  ⇒ (¬P[e'])))))
          ∨ (∀e':E. (e' ≤loc e  ⇒ (¬P[e']))))))

Definition: es-search-back
es-search-back(es;x.f[x];e) ==  gensearch(λx.f[x];λe.es-pred?(es;e);e)

Lemma: es-search-back_wf
∀[es:EO]. ∀[T:Type]. ∀[e:E]. ∀[f:{e':E| e' ≤loc e }  ⟶ (T + Top)].  (es-search-back(es;x.f[x];e) ∈ T + Top)

Lemma: es-search-back-cases
∀[es:EO]. ∀[e:E]. ∀[f:{e':E| e' ≤loc e }  ⟶ (Top + Top)].
  (es-search-back(es;x.f[x];e) ~ if isl(f[e]) then f[e]
  if first(e) then inr ⋅ 
  else es-search-back(es;x.f[x];pred(e))
  fi )

Definition: es-before
before(e) ==  fix((λes-before,e. if first(e) then [] else (es-before pred(e)) @ [pred(e)] fi )) e

Lemma: es-before_wf
∀[the_es:EO]. ∀[e:E].  (before(e) ∈ E List)

Lemma: es-before_wf2
∀[the_es:EO]. ∀[e:E].  (before(e) ∈ {e':E| loc(e') = loc(e) ∈ Id}  List)

Lemma: member-es-before
∀the_es:EO. ∀e',e:E.  ((e ∈ before(e')) ⇐⇒ (e <loc e'))

Lemma: es-before_wf3
∀[es:EO]. ∀[e:E].  (before(e) ∈ {e':E| (e' <loc e)}  List)

Lemma: l_before-es-before
∀the_es:EO. ∀e,e',y:E.  (e' before y ∈ before(e) ⇒ (e' <loc y))

Lemma: l_before-es-before-iff
∀the_es:EO. ∀e,e',y:E.  (e' before y ∈ before(e) ⇐⇒ (e' <loc y) ∧ (y <loc e))

Definition: es-le-before
≤loc(e) ==  before(e) @ [e]

Lemma: es-le-before_wf
∀[es:EO]. ∀[e:E].  (≤loc(e) ∈ {a:E| loc(a) = loc(e) ∈ Id}  List)

Lemma: es-le-before-not-null
∀[es:EO]. ∀[e:E].  (null(≤loc(e)) ~ ff)

Lemma: member-es-le-before
∀es:EO. ∀e,e':E.  ((e' ∈ ≤loc(e)) ⇐⇒ e' ≤loc e )

Lemma: member-es-le-before2
∀es:EO. ∀e:E. ∀e':{a:E| loc(a) = loc(e) ∈ Id} .  ((e' ∈ ≤loc(e)) ⇐⇒ e' ≤loc e )

Lemma: es-le-before_wf2
∀[es:EO]. ∀[e:E].  (≤loc(e) ∈ {a:E| a ≤loc e }  List)

Lemma: member-es-le-before3
∀es:EO. ∀e:E. ∀e':{e':E| e' ≤loc e } .  ((e' ∈ ≤loc(e)) ⇐⇒ e' ≤loc e )

Lemma: es-le-before-pred
∀[es:EO]. ∀[e:E].  ≤loc(pred(e)) ~ before(e) supposing ¬↑first(e)

Lemma: l_before-es-le-before-iff
∀the_es:EO. ∀e,e',y:E.  (e' before y ∈ ≤loc(e) ⇐⇒ (e' <loc y) ∧ y ≤loc e )

Lemma: es-le-before-ordered
∀es:EO. ∀e:E.  l-ordered(E;x,y.(x <loc y);≤loc(e))

Lemma: ppcc-problem2
∀[es:EO]. ∀[e:E].  (False) supposing ((↑¬bfirst(e)) and (↑first(e)))

Lemma: ppcc-problem3
False supposing [] = [1] ∈ (ℤ List)

Definition: es-interval
[e, e'] ==  filter(λev.e ≤loc ev;before(e') @ [e'])

Lemma: es-interval_wf
∀[es:EO]. ∀[e,e':E].  ([e, e'] ∈ E List)

Definition: es-open-interval
(e, e') ==  filter(λev.e <loc ev;before(e'))

Lemma: es-open-interval_wf
∀[es:EO]. ∀[e,e':E].  ((e, e') ∈ E List)

Lemma: member-es-interval
∀es:EO. ∀e,e',ev:E.  ((ev ∈ [e, e']) ⇐⇒ e ≤loc ev  ∧ ev ≤loc e' )

Lemma: member-es-open-interval
∀es:EO. ∀e,e',ev:E.  ((ev ∈ (e, e')) ⇐⇒ (e <loc ev) ∧ (ev <loc e'))

Definition: es-closed-open-interval
[e;e') ==  filter(λev.e ≤loc ev;before(e'))

Lemma: es-closed-open-interval_wf
∀[es:EO]. ∀[e,e':E].  ([e;e') ∈ E List)

Lemma: member-es-closed-open-interval
∀es:EO. ∀e,e',ev:E.  ((ev ∈ [e;e')) ⇐⇒ e ≤loc ev  ∧ (ev <loc e'))

Lemma: es-closed-open-interval-nil
∀es:EO. ∀e:E.  ([e;e) = [] ∈ (E List))

Lemma: es-open-interval-nil
∀[es:EO]. ∀[e,e':E].  (e, e') ~ [] supposing (↑first(e')) ∨ ((¬↑first(e')) ∧ pred(e') ≤loc e )

Lemma: l_before-es-interval
∀es:EO. ∀e,e',a,b:E.  (a before b ∈ [e, e'] ⇐⇒ (a <loc b) ∧ e ≤loc a  ∧ b ≤loc e' )

Lemma: hd-es-interval
∀[es:EO]. ∀[e,e':E].  hd([e, e']) = e ∈ E supposing e ≤loc e' 

Lemma: es-interval-non-zero
∀es:EO. ∀e,e':E.  (e ≤loc e'  ⇐⇒ 0 < ||[e, e']||)

Lemma: es-interval-nil
∀es:EO. ∀e,e':E.  [e, e'] = [] ∈ (E List) ⇐⇒ (e' <loc e) supposing loc(e) = loc(e') ∈ Id

Lemma: es-interval-is-nil
∀[es:EO]. ∀[e,e':E].  ([e, e'] ~ []) supposing ((e' <loc e) and (loc(e) = loc(e') ∈ Id))

Lemma: es-interval-last
∀[es:EO]. ∀[e2,e1:E].  last([e1, e2]) ~ e2 supposing e1 ≤loc e2 

Lemma: es-interval-less
∀[es:EO]. ∀[e,e':E].  [e, e'] = ([e, pred(e')] @ [e']) ∈ (E List) supposing (e <loc e')

Lemma: es-interval-less-sq
∀[es:EO]. ∀[e,e':E].  [e, e'] ~ [e, pred(e')] @ [e'] supposing (e <loc e')

Lemma: es-interval-eq
∀[es:EO]. ∀[e:E].  ([e, e] ~ [e])

Lemma: es-interval-eq2
∀[es:EO]. ∀[e,e':E].  [e, e'] ~ [e'] supposing e = e' ∈ E

Lemma: es-interval-length-one-one
∀[es:EO]. ∀[d,b,a:E].  (b = d ∈ E) supposing ((||[a, b]|| = ||[a, d]|| ∈ ℤ) and a ≤loc d  and a ≤loc b )

Lemma: es-interval-one-one
∀[es:EO]. ∀[d,b,a,c:E].
  ({(a = c ∈ E) ∧ (b = d ∈ E)}) supposing (([a, b] = [c, d] ∈ (E List)) and c ≤loc d  and a ≤loc b )

Lemma: es-interval-iseg
∀es:EO. ∀e3,e2,e1:E.  (e1 ≤loc e2  ⇒ e1 ≤loc e3  ⇒ ([e1, e2] ≤ [e1, e3] ⇐⇒ e2 ≤loc e3 ))

Lemma: es-interval-partition
∀[es:EO]. ∀[e',e,a:E].  [e, e'] = ([e, pred(a)] @ [a, e']) ∈ (E List) supposing (e <loc a) ∧ a ≤loc e' 

Lemma: es-interval-select
∀[es:EO]. ∀[e',e:E]. ∀[i:ℕ].
  firstn(i;[e, e']) = if (i =z 0) then [] else [e, pred([e, e'][i])] fi  ∈ (E List) supposing i < ||[e, e']||

Lemma: es-interval_wf2
∀[es:EO]. ∀[e,e':E].  ([e, e'] ∈ {ev:E| loc(ev) = loc(e') ∈ Id}  List)

Lemma: es-interval-open-interval
∀[es:EO]. ∀[e,e':E].  [e', e] = (if e' <loc e then [e'] else [] fi  @ (e', e) @ [e]) ∈ (E List) supposing e' ≤loc e 

Lemma: es-le-before-partition
∀[es:EO]. ∀[e,a:E].  ≤loc(e) = (before(a) @ [a, e]) ∈ (E List) supposing a ≤loc e 

Lemma: es-le-before-partition2
∀[es:EO]. ∀[e,a:E].  (≤loc(e) = (≤loc(pred(a)) @ [a, e]) ∈ (E List)) supposing ((¬↑first(a)) and a ≤loc e )

Lemma: es-le-before-split-last
∀[es:EO]. ∀[e:E].  ≤loc(e) ~ ≤loc(pred(e)) @ [e] supposing ¬↑first(e)

Lemma: es-le-before-filter
∀es:EO. ∀e,b:E.  (b ≤loc e  ⇒ (≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ ({a:E| a ≤loc b }  List)))

Lemma: hd-es-le-before
∀es:EO. ∀e,fst:E.  ((↑first(fst)) ⇒ fst ≤loc e  ⇒ (hd(≤loc(e)) = fst ∈ E))

Lemma: hd-es-le-before-is-first
∀[es:EO]. ∀[e:E].  (first(hd(≤loc(e))) ~ tt)

Lemma: tl-es-le-before
∀es:EO. ∀e,e':E.  ((e' ∈ tl(≤loc(e))) ⇐⇒ e' ≤loc e  ∧ (¬↑first(e')))

Lemma: last-es-le-before
∀es:EO. ∀e:E.  (last(≤loc(e)) = e ∈ E)

Lemma: es-before-partition
∀[es:EO]. ∀[e,e':E].  before(e) = (≤loc(e') @ (e', e)) ∈ (E List) supposing (e' <loc e)

Lemma: firstn-before
∀[the_es:EO]. ∀[e:E]. ∀[n:ℕ].  firstn(n;before(e)) ~ before(before(e)[n]) supposing n < ||before(e)||

Lemma: nth_tl-es-before
∀[es:EO]. ∀[e:E]. ∀[n:ℕ||before(e)||].  (nth_tl(n;before(e)) = filter(λa.before(e)[n] ≤loc a;before(e)) ∈ (E List))

Lemma: firstn-le-before
∀[the_es:EO]. ∀[e:E]. ∀[n:ℕ].  firstn(n + 1;≤loc(e)) ~ ≤loc(before(e)[n]) supposing n < ||before(e)||

Lemma: es-interval-sorted-by
∀es:EO. ∀e1,e2:E.  sorted-by(λe1,e2. (e1 <loc e2);[e1, e2])

Lemma: es-interval-ordered
∀es:EO. ∀e1,e2:E.  l-ordered(E;e1,e2.(e1 <loc e2);[e1, e2])

Lemma: es-open-interval-ordered
∀es:EO. ∀e1,e2:E.  l-ordered(E;e1,e2.(e1 <loc e2);(e1, e2))

Lemma: es-open-interval-ordered-inst
∀es:EO. ∀e1,e2:E. ∀n1,n2:ℕ||(e1, e2)||.  (n1 < n2 ⇒ ((e1, e2)[n1] <loc (e1, e2)[n2]))

Lemma: es-open-interval-ordered-iff
∀es:EO. ∀e1,e2:E. ∀n1,n2:ℕ||(e1, e2)||.  (n1 < n2 ⇐⇒ ((e1, e2)[n1] <loc (e1, e2)[n2]))

Lemma: pred-hd-es-open-interval
∀[es:EO]. ∀[e1,e2:E].  pred(hd((e1, e2))) = e1 ∈ E supposing ||(e1, e2)|| > 0

Lemma: pred-member-es-open-interval
∀[es:EO]. ∀[e1,e2:E]. ∀[n:{1..||(e1, e2)||-}].  (pred((e1, e2)[n]) = (e1, e2)[n - 1] ∈ E)

Lemma: firstn-es-open-interval
∀[es:EO]. ∀[e1,e2:E]. ∀[n:ℕ||(e1, e2)||].  (firstn(n;(e1, e2)) = (e1, (e1, e2)[n]) ∈ (E List))

Lemma: es-open-interval-closed
∀[es:EO]. ∀[e1,e2:E].  (pred(e1), e2) = [e1;e2) ∈ (E List) supposing ¬↑first(e1)

Lemma: es-before-decomp
∀the_es:EO. ∀e',e:E.  ((e ∈ before(e')) ⇒ (∃l:E List. (before(e') = (before(e) @ [e] @ l) ∈ (E List))))

Lemma: es-before-split-last
∀[es,e:Top].  (before(e) ~ if first(e) then [] else before(pred(e)) @ [pred(e)] fi )

Lemma: es-closed-open-interval-decomp
∀[es:EO]. ∀[e1,e2:E].  [e1;e2) = [e1 / (e1, e2)] ∈ (E List) supposing (e1 <loc e2)

Lemma: nth_tl-es-open-interval
∀[es:EO]. ∀[e1,e2:E]. ∀[n:ℕ||(e1, e2)||].
  nth_tl(n + 1;(e1, e2)) = ((e1, e2)[n], e2) ∈ (E List) supposing loc(e1) = loc(e2) ∈ Id

Lemma: iseg-es-before
∀es:EO. ∀e',e:E.  ((e' <loc e) ⇒ ≤loc(e') ≤ before(e))

Lemma: iseg-es-le-before
∀es:EO. ∀e',e:E.  (e' ≤loc e  ⇒ ≤loc(e') ≤ ≤loc(e))

Lemma: es-before-pred-length
∀[es:EO]. ∀[e:E].  ||before(e)|| = (||before(pred(e))|| + 1) ∈ ℤ supposing ¬↑first(e)

Lemma: es-before-no_repeats
∀[es:EO]. ∀[e:E].  no_repeats(E;before(e))

Lemma: es-le-before-no_repeats
∀[es:EO]. ∀[e:E].  no_repeats(E;≤loc(e))

Lemma: es-before-is-nil-if-first
∀[es:EO]. ∀[e:E].  before(e) ~ [] supposing ↑first(e)

Lemma: es-le-before-if-first
∀[es:EO]. ∀[e:E].  ≤loc(e) ~ [e] supposing ↑first(e)

Lemma: iseg-es-le-before-is-before
∀[es:EO]. ∀[e,x:E]. ∀[L:E List].  L = before(x) ∈ (E List) supposing L @ [x] ≤ ≤loc(e)

Lemma: iseg-es-before-is-before
∀[es:EO]. ∀[e,x:E]. ∀[L:E List].  L = before(x) ∈ (E List) supposing L @ [x] ≤ before(e)

Lemma: iseg-es-interval
∀[es:EO]. ∀[L:E List]. ∀[e1,e2:E].  (L = [e1, last(L)] ∈ (E List)) supposing ((¬↑null(L)) and L ≤ [e1, e2])

Lemma: iseg-filter-es-interval
∀[es:EO]. ∀[L:E List]. ∀[e1,e2:E]. ∀[P:{x:E| (x ∈ [e1, e2])}  ⟶ 𝔹].
  (L = filter(P;[e1, last(L)]) ∈ (E List)) supposing ((¬↑null(L)) and L ≤ filter(P;[e1, e2]))

Definition: es-first-event
es-first-event(es;P;e) ==  l_find(≤loc(e);P)

Lemma: es-first-event_wf
∀[es:EO]. ∀[e:E]. ∀[P:{e':E| e' ≤loc e }  ⟶ 𝔹].
  (es-first-event(es;P;e) ∈ (∃e':{E| (e' ≤loc e  ∧ (↑(P e')) ∧ (∀e'':E. ((e'' <loc e') ⇒ (¬↑(P e'')))))})
   ∨ (↓∀e':E. (e' ≤loc e  ⇒ (¬↑(P e')))))

Definition: es-init
es-init(es;e) ==  final-iterate(λe.if first(e) then ff else inl pred(e) fi ;e)

Lemma: es-init_wf
∀[es:EO]. ∀[e:E].  (es-init(es;e) ∈ E)

Lemma: es-init-le
∀es:EO. ∀e:E.  (es-init(es;e) ≤loc e  ⇐⇒ True)

Lemma: es-first-init
∀[es:EO]. ∀[e:E].  (first(es-init(es;e)) ~ tt)

Lemma: es-init-identity
∀[es:EO]. ∀[e:E].  uiff(es-init(es;e) = e ∈ E;↑first(e))

Lemma: es-init-elim
∀[es:EO]. ∀[e:E].  es-init(es;e) ~ e supposing ↑first(e)

Lemma: es-init-elim2
∀[es:EO]. ∀[e:E].  es-init(es;e) ~ es-init(es;pred(e)) supposing ¬↑first(e)

Lemma: es-init-eq
∀[es:EO]. ∀[e,e':E].  es-init(es;e) = es-init(es;e') ∈ E supposing loc(e) = loc(e') ∈ Id

Lemma: es-loc-init
∀[es:EO]. ∀[e:E].  (loc(es-init(es;e)) ~ loc(e))

Lemma: es-init-le-iff
∀es:EO. ∀e,e':E.  (es-init(es;e) ≤loc e'  ⇐⇒ loc(e') = loc(e) ∈ Id)

Lemma: es-init-locl
∀es:EO. ∀e:E.  ((¬↑first(e)) ⇒ (es-init(es;e) <loc e))

Lemma: alle-at-iff
∀es:EO. ∀i:Id.
  ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]
    (∀e@i.P[e] ⇐⇒ ∀e@i.P[e] supposing ↑first(e) ∧ ∀e@i.P[pred(e)] ⇒ P[e] supposing ¬↑first(e))

Lemma: alle-at-not-first
∀es:EO. ∀i:Id.  ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]. (∀e@i.P[e] ⇒ ∀e@i.P[pred(e)] supposing ¬↑first(e))

Definition: existse-at
∃e@i.P[e] ==  ∃e:E. ((loc(e) = i ∈ Id) ∧ P[e])

Lemma: existse-at_wf
∀[es:EO]. ∀[i:Id]. ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ].  (∃e@i.P[e] ∈ ℙ)

Lemma: es-first-exists
∀es:EO. ∀e':E.  ∃e:E. ((↑first(e)) ∧ e ≤loc e' )

Definition: existse-le
∃e≤e'.P[e] ==  ∃e:E. (e ≤loc e'  c∧ P[e])

Lemma: existse-le_wf
∀[es:EO]. ∀[e':E]. ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ].  (∃e≤e'.P[e] ∈ ℙ)

Definition: existse-before
∃e<e'.P[e] ==  ∃e:E. ((e <loc e') c∧ P[e])

Lemma: existse-before_wf
∀[es:EO]. ∀[e':E]. ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ].  (∃e<e'.P[e] ∈ ℙ)

Lemma: existse-before-iff
∀es:EO. ∀e':E.
  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∃e<e'.P[e] ⇐⇒ (¬↑first(e')) c∧ (P[pred(e')] ∨ ∃e<pred(e').P[e]))

Lemma: decidable__existse-before
∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∀e@loc(e').Dec(P[e]) ⇒ Dec(∃e<e'.P[e]))

Lemma: es-minimal-event
∀es:EO
  ∀[P:E ⟶ ℙ]. ((∀e:E. Dec(P[e])) ⇒ (∀e:E. (P[e] ⇒ (∃m:E. (m ≤loc e  ∧ P[m] ∧ (∀e':E. ((e' <loc m) ⇒ (¬P[e']))))))))

Lemma: existse-le-iff
∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∃e≤e'.P[e] ⇐⇒ P[e'] ∨ ∃e<e'.P[e])

Lemma: decidable__existse-le
∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∀e@loc(e').Dec(P[e]) ⇒ Dec(∃e≤e'.P[e]))

Definition: alle-ge
∀e'≥e.P[e'] ==  ∀e':E. (e ≤loc e'  ⇒ P[e'])

Lemma: alle-ge_wf
∀[es:EO]. ∀[e':E]. ∀[P:E ⟶ ℙ].  (∀e≥e'.P[e] ∈ ℙ)

Definition: alle-lt
∀e<e'.P[e] ==  ∀e:E. ((e <loc e') ⇒ P[e])

Lemma: alle-lt_wf
∀[es:EO]. ∀[e':E]. ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ].  (∀e<e'.P[e] ∈ ℙ)

Lemma: alle-lt-iff
∀es:EO. ∀e':E.
  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∀e<e'.P[e] ⇐⇒ P[pred(e')] ∧ ∀e<pred(e').P[e] supposing ¬↑first(e'))

Lemma: not-alle-lt
∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∀e@loc(e').Dec(P[e]) ⇒ (¬∀e<e'.P[e] ⇐⇒ ∃e<e'.¬P[e]))

Lemma: decidable__alle-lt
∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∀e@loc(e').Dec(P[e]) ⇒ Dec(∀e<e'.P[e]))

Definition: alle-le
∀e≤e'.P[e] ==  ∀e:E. (e ≤loc e'  ⇒ P[e])

Lemma: alle-le_wf
∀[es:EO]. ∀[e':E]. ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ].  (∀e≤e'.P[e] ∈ ℙ)

Lemma: alle-le-iff
∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∀e≤e'.P[e] ⇐⇒ P[e'] ∧ ∀e<e'.P[e])

Lemma: decidable__alle-le
∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∀e@loc(e').Dec(P[e]) ⇒ Dec(∀e≤e'.P[e]))

Definition: alle-between1
∀e∈[e1,e2).P[e] ==  ∀e:E. (e1 ≤loc e  ⇒ (e <loc e2) ⇒ P[e])

Lemma: alle-between1_wf
∀[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].  ∀e∈[e1,e2).P[e] ∈ ℙ supposing loc(e2) = loc(e1) ∈ Id

Lemma: alle-between1-trivial
∀es:EO. ∀e:E. ∀P:Top.  ∀e∈[e,e).P[e]

Lemma: alle-between1-true
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ].  uiff(∀e∈[e1,e2).True;True)

Lemma: alle-between1-false
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∀e∈[e1,e2).False ⇐⇒ e2 ≤loc e1 )

Lemma: alle-between1_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[P,Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . (P[e] ⇐⇒ Q[e])) ⇒ (∀e∈[e1,e2).P[e] ⇐⇒ ∀e∈[e1,e2).Q[e]))

Lemma: decidable__alle-between1
∀es:EO. ∀e1,e2:E.
  ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]. ∀e@loc(e1).Dec(P[e]) ⇒ Dec(∀e∈[e1,e2).P[e]) supposing loc(e2) = loc(e1) ∈ Id

Definition: existse-between1
∃e∈[e1,e2).P[e] ==  ∃e:E. ((e1 ≤loc e  ∧ (e <loc e2)) c∧ P[e])

Lemma: existse-between1_wf
∀[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].  ∃e∈[e1,e2).P[e] ∈ ℙ supposing loc(e2) = loc(e1) ∈ Id

Lemma: existse-between1-true
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∃e∈[e1,e2).True ⇐⇒ (e1 <loc e2))

Lemma: existse-between1-false
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∃e∈[e1,e2).False ⇐⇒ False)

Lemma: existse-between1_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[P,Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . (P[e] ⇐⇒ Q[e])) ⇒ (∃e∈[e1,e2).P[e] ⇐⇒ ∃e∈[e1,e2).Q[e]))

Lemma: decidable__existse-between1
∀es:EO. ∀e1,e2:E.
  ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]. ∀e@loc(e1).Dec(P[e]) ⇒ Dec(∃e∈[e1,e2).P[e]) supposing loc(e2) = loc(e1) ∈ Id

Definition: alle-between2
∀e∈[e1,e2].P[e] ==  ∀e:E. (e1 ≤loc e  ⇒ e ≤loc e2  ⇒ P[e])

Lemma: alle-between2_wf
∀[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].  ∀e∈[e1,e2].P[e] ∈ ℙ supposing loc(e2) = loc(e1) ∈ Id

Lemma: alle-between2-true
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ].  uiff(∀e∈[e1,e2].True;True)

Lemma: alle-between2-false
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∀e∈[e1,e2].False ⇐⇒ (e2 <loc e1))

Lemma: alle-between2_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[P,Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . (P[e] ⇐⇒ Q[e])) ⇒ (∀e∈[e1,e2].P[e] ⇐⇒ ∀e∈[e1,e2].Q[e]))

Lemma: decidable__alle-between2
∀es:EO. ∀e1,e2:E.
  ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]. ∀e@loc(e1).Dec(P[e]) ⇒ Dec(∀e∈[e1,e2].P[e]) supposing loc(e2) = loc(e1) ∈ Id

Definition: existse-between2
∃e∈[e1,e2].P[e] ==  ∃e:E. ((e1 ≤loc e  ∧ e ≤loc e2 ) c∧ P[e])

Lemma: existse-between2_wf
∀[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].  ∃e∈[e1,e2].P[e] ∈ ℙ supposing loc(e2) = loc(e1) ∈ Id

Lemma: existse-between2-false
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∃e∈[e1,e2].False ⇐⇒ False)

Lemma: existse-between2-true
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∃e∈[e1,e2].True ⇐⇒ e1 ≤loc e2 )

Lemma: existse-between2_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[P,Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . (P[e] ⇐⇒ Q[e])) ⇒ (∃e∈[e1,e2].P[e] ⇐⇒ ∃e∈[e1,e2].Q[e]))

Lemma: decidable__existse-between2
∀es:EO. ∀e1,e2:E.
  ∀[P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]. ∀e@loc(e1).Dec(P[e]) ⇒ Dec(∃e∈[e1,e2].P[e]) supposing loc(e2) = loc(e1) ∈ Id

Definition: existse-between3
∃e∈(e1,e2].P[e] ==  ∃e:E. (((e1 <loc e) ∧ e ≤loc e2 ) c∧ P[e])

Lemma: existse-between3_wf
∀[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| (loc(e) = loc(e1) ∈ Id) ∧ (¬↑first(e))}  ⟶ ℙ].
  ∃e∈(e1,e2].P[e] ∈ ℙ supposing loc(e2) = loc(e1) ∈ Id

Lemma: existse-between3-false
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∃e∈(e1,e2].False ⇐⇒ False)

Lemma: existse-between3-true
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∃e∈(e1,e2].True ⇐⇒ (e1 <loc e2))

Lemma: existse-between3_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[P,Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . (P[e] ⇐⇒ Q[e])) ⇒ (∃e∈(e1,e2].P[e] ⇐⇒ ∃e∈(e1,e2].Q[e]))

Lemma: decidable__existse-between3
∀es:EO. ∀e1,e2:E.
  ∀[P:{e:E| (loc(e) = loc(e1) ∈ Id) ∧ (¬↑first(e))}  ⟶ ℙ]
    ∀e@loc(e1).Dec(P[e]) supposing ¬↑first(e) ⇒ Dec(∃e∈(e1,e2].P[e]) supposing loc(e2) = loc(e1) ∈ Id

Definition: alle-between3
∀e∈(e1,e2].P[e] ==  ∀e:E. ((e1 <loc e) ⇒ e ≤loc e2  ⇒ P[e])

Lemma: alle-between3_wf
∀[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| (loc(e) = loc(e1) ∈ Id) ∧ (¬↑first(e))}  ⟶ ℙ].
  ∀e∈(e1,e2].P[e] ∈ ℙ supposing loc(e2) = loc(e1) ∈ Id

Lemma: alle-between3-false
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .  (∀e∈(e1,e2].False ⇐⇒ e2 ≤loc e1 )

Lemma: es-subinterval
∀es:EO. ∀e2,e1:E.  (e1 ≤loc e2  ⇒ (∀n:ℕ. (∃e∈(e1,e2].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, e2]|| and 0 < n))\000C)

Lemma: isl-es-search-back
∀es:EO. ∀[T:Type]. ∀e:E. ∀f:{e':E| e' ≤loc e }  ⟶ (T + Top).  (↑isl(es-search-back(es;x.f[x];e)) ⇐⇒ ∃e'≤e.↑isl(f[e']))

Lemma: can-apply-es-search-back
∀es:EO
  ∀[T:Type]
    ∀e:E. ∀f:{e':E| e' ≤loc e }  ⟶ (T + Top).
      (↑can-apply(λe.es-search-back(es;x.f[x];e);e) ⇐⇒ ∃e'≤e.↑can-apply(λx.f[x];e'))

Definition: es-box
[]P ==  λe.∀e':E. (e ≤loc e'  ⇒ (P e'))

Lemma: es-box_wf
∀[es:EO]. ∀[P:E ⟶ ℙ].  ([]P ∈ E ⟶ ℙ)

Definition: es-diamond
<>P ==  λe.∃e':E. (e ≤loc e'  ∧ (P e'))

Lemma: es-diamond_wf
∀[es:EO]. ∀[P:E ⟶ ℙ].  (<>P ∈ E ⟶ ℙ)

Definition: es-until
(P ⋃ Q) ==  λe.∃e':E. (e ≤loc e'  ∧ (Q e') ∧ (∀e'':E. (e ≤loc e''  ⇒ (e'' <loc e') ⇒ (P e''))))

Lemma: es-until_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ].  ((P ⋃ Q) ∈ E ⟶ ℙ)

Definition: es-implies
P ⇒ Q ==  λe.((P e) ⇒ (Q e))

Lemma: es-implies_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ].  (P ⇒ Q ∈ E ⟶ ℙ)

Definition: es-not
¬P ==  λe.(¬(P e))

Lemma: es-not_wf
∀[es:EO]. ∀[P:E ⟶ ℙ].  (¬P ∈ E ⟶ ℙ)

Definition: es-iff
P ⇐⇒ Q ==  λe.(P e ⇐⇒ Q e)

Lemma: es-iff_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ].  (P ⇐⇒ Q ∈ E ⟶ ℙ)

Definition: es-equiv
P ≡ Q ==  ∀e:E. (P e ⇐⇒ Q e)

Lemma: es-equiv_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ].  (P ≡ Q ∈ ℙ)

Definition: es-TR
TR ==  λe.True

Lemma: es-TR_wf
∀[es:EO]. (TR ∈ E ⟶ ℙ)

Lemma: LTL-identities
∀es:EO. ∀[P:E ⟶ ℙ]. ([][]P ≡ []P ∧ <><>P ≡ <>P ∧ <>P ≡ (TR ⋃ P) ∧ []¬¬P ≡ ¬<>¬P ∧ ¬¬<>P ≡ ¬[]¬P)

Definition: es-first-at
e is first@ i s.t.  e.P[e] ==  (loc(e) = i ∈ Id) ∧ P[e] ∧ ∀e'<e.¬P[e']

Lemma: es-first-at_wf
∀[es:EO]. ∀[i:Id]. ∀[e':E]. ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ].  (e' is first@ i s.t.  e.P[e] ∈ ℙ)

Lemma: es-first-at-exists
∀es:EO. ∀i:Id.
  ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]
    ((∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e]))
    ⇒ (∀e:E. P[e] ⇒ (∃e':E. (e' ≤loc e  ∧ e' is first@ i s.t.  e.P[e])) supposing loc(e) = i ∈ Id))

Lemma: es-first-at-exists2
∀es:EO. ∀i:Id.
  ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]
    ((∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e]))
    ⇒ (∀e:E. (∃e'≤e.e' is first@ i s.t.  e'.P[e']) supposing ((¬∀e'≤e.¬P[e']) and (loc(e) = i ∈ Id))))

Lemma: es-first-at-exists-cases
∀es:EO. ∀e:E.
  ∀[P:{e':E| loc(e') = loc(e) ∈ Id}  ⟶ ℙ]
    ((∀e':{e':E| loc(e') = loc(e) ∈ Id} . Dec(P[e']))
    ⇒ ((∀e'≤e.¬P[e'] ∧ (¬∃e'≤e.e' is first@ loc(e) s.t.  e'.P[e']))
       ∨ ((¬∀e'≤e.¬P[e']) ∧ ∃e'≤e.e' is first@ loc(e) s.t.  e'.P[e'])))

Lemma: es-first-at-unique
∀[es:EO]. ∀[i:Id]. ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]. ∀[e1,e2:E].
  (e1 = e2 ∈ E) supposing (e2 is first@ i s.t.  e.P[e] and e1 is first@ i s.t.  e.P[e])

Lemma: es-first-at-implies
∀es:EO. ∀i:Id.
  ∀[P,Q:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = i ∈ Id} . Dec(Q[e]))
    ⇒ (∀e:{e:E| loc(e) = i ∈ Id} . (P[e] ⇒ ∃e':E. ((e' <loc e) ∧ P[e']) supposing ¬Q[e]))
    ⇒ (∀e:E. {e is first@ i s.t.  e.P[e] ⇒ Q[e]}))

Lemma: es-first-at-implies-first-at
∀es:EO. ∀i:Id.
  ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]
    ∀e:E
      (e is first@ i s.t.  e.P[e]
      ⇒ {∀[Q:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]
            (e is first@ i s.t.  e.Q[e] ⇐⇒ Q[e] ∧ ∀e'<e.e' is first@ i s.t.  e.Q[e] ⇒ P[e'])})

Definition: es-first-at-since
es-first-at-since(es;i;e;e.R[e];e.P[e]) ==
  (loc(e) = i ∈ Id) ∧ (P[e] ∧ (¬R[e])) ∧ ∀e'<e.P[e'] ⇒ (∃e'':E. (e' ≤loc e''  ∧ (e'' <loc e) ∧ R[e'']))

Lemma: es-first-at-since_wf
∀[es:EO]. ∀[i:Id]. ∀[e':E]. ∀[P,R:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ].  (es-first-at-since(es;i;e';e.R[e];e.P[e]) ∈ ℙ)

Definition: es-first-at-since'
es-first-at-since'(es;i;e;e.R[e];e.P[e]) ==
  (loc(e) = i ∈ Id) ∧ R[e] ∧ (∃e':E. ((e' <loc e) c∧ (P[e'] ∧ (∀e'':E. (e' ≤loc e''  ⇒ (e'' <loc e) ⇒ (¬R[e'']))))))

Lemma: es-first-at-since'_wf
∀[es:EO]. ∀[i:Id]. ∀[e':E]. ∀[P,R:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ].  (es-first-at-since'(es;i;e';e.R[e];e.P[e]) ∈ ℙ)

Lemma: previous-event-exists
∀es:EO. ∀i:Id.
  ∀[R:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]
    ∀e:E
      ((∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id)
      ⇒ (∃e':E. (e' ≤loc e  c∧ R[e']))
         ⇒ (∃e':E. (e' ≤loc e  c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬R[e''])))))) 
         supposing loc(e) = i ∈ Id)

Lemma: last-event
∀es:EO. ∀e:E.
  ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ⟶ ℙ]
    ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))
    ⇒ (∀e'≤e.¬P[e'] ∨ (∃e':E. (e' ≤loc e  c∧ (P[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬P[e'']))))))))

Lemma: es-bound-list
∀es:EO
  ∀[T:Type]
    ∀i:Id
      ∀[P:T ⟶ ℙ]. ∀[Q:E ⟶ T ⟶ ℙ].
        ((∀x:T. Dec(P[x]))
        ⇒ (∀L:T List
              (∀x∈L.P[x] ⇒ (∃e:E. Q[e;x]))
              ⇒ ∃e'@i.True supposing ¬(∃x∈L. P[x])
              ⇒ ∃e'@i.(∀x∈L.P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x]))) 
              supposing (∀x∈L.∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id)))))

Lemma: es-bound-list2
∀es:EO
  ∀[T:Type]
    ∀i:Id
      ∀[P:T ⟶ ℙ]
        ∀L:T List
          ∀[Q:E ⟶ {x:T| (x ∈ L)}  ⟶ ℙ]
            ((∀x:T. Dec(P[x]))
            ⇒ (∀x∈L.P[x] ⇒ (∃e:E. Q[e;x]))
               ⇒ ∃e'@i.True supposing ¬(∃x∈L. P[x])
               ⇒ ∃e'@i.(∀x∈L.P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x]))) 
               supposing (∀x∈L.∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id))))

Definition: last-solution
last-solution(es;P;d) ==  λe.case TERMOF{last-event:o, 1:l, i:l} es e d of inl(x) => inr ⋅  | inr(p) => inl (fst(p))

Lemma: last-solution_wf
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[d:a:E ⟶ Dec(P[a])].  (last-solution(es;P;d) ∈ E ⟶ (E + Top))

Lemma: last-transition
∀es:EO. ∀e:E. ∀P:{a:E| loc(a) = loc(e) ∈ Id}  ⟶ 𝔹.
  (∀e'≤e.P[e'] = P[e] ∨ ∃e'≤e.(¬P[e'] = P[e]) ∧ ∀e''∈(e',e].P[e''] = P[e])

Lemma: last-decidable
∀es:EO. ∀e:E.
  ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ⟶ ℙ]
    ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))
    ⇒ (∀e'≤e.P[e'] ⇐⇒ P[e] ∨ ∃e'≤e.(¬(P[e'] ⇐⇒ P[e])) ∧ ∀e''∈(e',e].P[e''] ⇐⇒ P[e]))

Lemma: es-interval-induction
∀es:EO. ∀i:Id.
  ∀[P:e1:{e:E| loc(e) = i ∈ Id}  ⟶ {e2:E| loc(e2) = i ∈ Id}  ⟶ ℙ]
    (∀e1@i.∀e2≥e1.(∀e:E. ((e1 <loc e) ⇒ e ≤loc e2  ⇒ P[e;e2])) ⇒ P[e1;e2] ⇒ ∀e1@i.∀e2≥e1.P[e1;e2])

Lemma: es-interval-induction2
∀es:EO. ∀i:Id.
  ∀[P:e1:{e:E| loc(e) = i ∈ Id}  ⟶ {e2:E| loc(e2) = i ∈ Id}  ⟶ ℙ]
    (∀e1@i.∀e2≥e1.(∀e:E. ((e1 <loc e) ⇒ e ≤loc e2  ⇒ P[e;e2])) ⇒ P[e1;e2]
    ⇒ ∀e1@i.∀e2<e1.P[e1;e2]
    ⇒ (∀e,e':E.  (P[e;e']) supposing ((loc(e') = i ∈ Id) and (loc(e) = i ∈ Id))))

Definition: possible-event
PossibleEvent(poss) ==  es:EO × E × (poss es)

Lemma: possible-event_wf
∀[poss:EO ⟶ ℙ']. (PossibleEvent(poss) ∈ ℙ')

Definition: pe-es
pe-es(e) ==  fst(e)

Lemma: pe-es_wf
∀[p:EO ⟶ ℙ']. ∀[e:PossibleEvent(p)].  (pe-es(e) ∈ EO)

Definition: pe-e
pe-e(p) ==  fst(snd(p))

Lemma: pe-e_wf
∀[p:EO ⟶ ℙ']. ∀[e:PossibleEvent(p)].  (pe-e(e) ∈ E)

Definition: pe-loc
pe-loc(p) ==  loc(pe-e(p))

Lemma: pe-loc_wf
∀[p:EO ⟶ ℙ']. ∀[e:PossibleEvent(p)].  (pe-loc(e) ∈ Id)

Definition: es-knows
K(P)@e ==  ∀e':PossibleEvent(poss). ((R e e') ⇒ (P e'))

Lemma: es-knows_wf
∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ']. ∀[P:PossibleEvent(poss) ⟶ ℙ'].
∀[e:PossibleEvent(poss)].
  (K(P)@e ∈ ℙ')

Lemma: es-knows-true
∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ'].
  ((∀e:PossibleEvent(poss). (R e e)) ⇒ (∀[P:PossibleEvent(poss) ⟶ ℙ']. ∀e:PossibleEvent(poss). (K(P)@e ⇒ (P e))))

Lemma: es-knows-knows
∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ'].
  (Trans(PossibleEvent(poss);a,b.R a b)
  ⇒ (∀[P:PossibleEvent(poss) ⟶ ℙ']. ∀e:PossibleEvent(poss). (K(P)@e ⇒ K(λe.K(P)@e)@e)))

Lemma: es-knows-not
∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ'].
  (EquivRel(PossibleEvent(poss))(R _1 _2)
  ⇒ (∀[P:PossibleEvent(poss) ⟶ ℙ']. ∀e:PossibleEvent(poss). K(λe.(¬K(P)@e))@e supposing ¬K(P)@e))

Lemma: es-knows-trans
∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ']. ∀[P,Q:PossibleEvent(poss) ⟶ ℙ'].
  ((∀e:PossibleEvent(poss). ((P e) ⇒ (Q e))) ⇒ (∀e:PossibleEvent(poss). (K(P)@e ⇒ K(Q)@e)))

Lemma: es-knows-valid
∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ']. ∀[P:PossibleEvent(poss) ⟶ ℙ'].
  ((∀e:PossibleEvent(poss). (P e)) ⇒ (∀e:PossibleEvent(poss). K(P)@e))

Definition: poss-le
e1 ≤ e2 ==  ((fst(e1)) = (fst(e2)) ∈ EO) c∧ fst(snd(e1)) ≤loc fst(snd(e2)) 

Lemma: poss-le_wf
∀[poss:EO ⟶ ℙ']. ∀[e1,e2:PossibleEvent(poss)].  (e1 ≤ e2 ∈ ℙ')

Lemma: es-knows-stable
∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ'].
  (Trans(PossibleEvent(poss))(R _1 _2)
  ⇒ (∀e1,e2:PossibleEvent(poss).  (e1 ≤ e2 ⇒ (R e1 e2)))
  ⇒ (∀[P:PossibleEvent(poss) ⟶ ℙ']. ∀e1,e2:PossibleEvent(poss).  (e1 ≤ e2 ⇒ K(P)@e1 ⇒ K(P)@e2)))

Definition: loc-on-path
loc-on-path(es;i;L) ==  (i ∈ map(λe.loc(e);L))

Lemma: loc-on-path_wf
∀[es:EO]. ∀[L:E List]. ∀[i:Id].  (loc-on-path(es;i;L) ∈ ℙ)

Lemma: loc-on-path-append
∀es:EO. ∀L1,L2:E List. ∀i:Id.  (loc-on-path(es;i;L1 @ L2) ⇐⇒ loc-on-path(es;i;L1) ∨ loc-on-path(es;i;L2))

Lemma: loc-on-path-cons
∀es:EO. ∀L:E List. ∀e:E. ∀i:Id.  (loc-on-path(es;i;[e / L]) ⇐⇒ (loc(e) = i ∈ Id) ∨ loc-on-path(es;i;L))

Lemma: loc-on-path-nil
∀es:EO. ∀i:Id.  (loc-on-path(es;i;[]) ⇐⇒ False)

Lemma: loc-on-path-singleton
∀es:EO. ∀e:E. ∀i:Id.  (loc-on-path(es;i;[e]) ⇐⇒ loc(e) = i ∈ Id)

Definition: es-first-since
e2 = first e ≥ e1.P[e] ==  e1 ≤loc e2  ∧ P[e2] ∧ ∀e∈[e1,e2).¬P[e]

Lemma: es-first-since_wf
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
  (e2 = first e ≥ e1.p[e] ∈ ℙ)

Lemma: es-first-since_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,p':{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . (p[e] ⇐⇒ p'[e])) ⇒ (e2 = first e ≥ e1.p[e] ⇐⇒ e2 = first e ≥ e1.p'[e]))

Lemma: alle-between1-not-first-since
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
  uiff(∀e∈[e1,e2).¬e = first e ≥ e1.p[e];∀e∈[e1,e2).¬p[e])

Lemma: alle-between2-not-first-since
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
  uiff(∀e∈[e1,e2].¬e = first e ≥ e1.p[e];∀e∈[e1,e2].¬p[e])

Lemma: es-increasing-sequence
∀es:EO. ∀m:ℕ+. ∀f:ℕm ⟶ E.  ((∀i:ℕm - 1. (f i <loc f (i + 1))) ⇒ (∀i:ℕm. ∀j:ℕi.  (f j <loc f i)))

Lemma: es-increasing-sequence2
∀es:EO. ∀m:ℕ+. ∀f:ℕm ⟶ E.  ((∀i:ℕm - 1. (f i <loc f (i + 1))) ⇒ (∀i:ℕm. ∀j:ℕi + 1.  f j ≤loc f i ))

Definition: es-pstar-q
[e1;e2]~([a,b].p[a; b])*[a,b].q[a; b] ==
  ∃m:ℕ+
   ∃f:ℕm ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
    ((((f 0) = e1 ∈ E) ∧ f (m - 1) ≤loc e2 )
    ∧ ((∀i:ℕm - 1. (f i <loc f (i + 1))) ∧ (∀i:ℕm - 1. p[f i; pred(f (i + 1))]))
    ∧ q[f (m - 1); e2])

Lemma: es-pstar-q_wf
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p,q:{e:E| loc(e) = loc(e1) ∈ Id} 
                                                             ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
                                                             ⟶ ℙ].
  ([e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ)

Lemma: es-pstar-q-trivial
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    (e1 ≤loc e2  ⇒ q[e1;e2] ⇒ [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b])

Lemma: es-pstar-q-le
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ([e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇒ e1 ≤loc e2 )

Lemma: es-pstar-q_functionality_wrt_implies
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q,p',q':{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {p[a;b] ⇒ p'[a;b]}))
    ⇒ (∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {q[a;b] ⇒ q'[a;b]}))
    ⇒ {[e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇒ [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]})

Lemma: es-pstar-q_functionality_wrt_rev_implies
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p',q',p,q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {p[a;b] ⇐ p'[a;b]}))
    ⇒ (∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {q[a;b] ⇐ q'[a;b]}))
    ⇒ {[e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇐ [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]})

Lemma: es-pstar-q_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q,p',q':{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ (p[a;b] ⇐⇒ p'[a;b])))
    ⇒ (∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ (q[a;b] ⇐⇒ q'[a;b])))
    ⇒ ([e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇐⇒ [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]))

Lemma: es-pstar-q-partition
∀es:EO. ∀e1,e2,b:E.
  ∀[Q,P:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((e1 <loc b)
    ⇒ b ≤loc e2 
    ⇒ [e1;pred(b)]~([a,b].P[a;b])*[a,b].P[a;b]
    ⇒ [b;e2]~([a,b].P[a;b])*[a,b].Q[a;b]
    ⇒ [e1;e2]~([a,b].P[a;b])*[a,b].Q[a;b])

Definition: es-pplus
[e1,e2]~([a,b].p[a; b])+ ==  [e1;e2]~([a,b].p[a; b])*[a,b].p[a; b]

Lemma: es-pplus_wf
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) = loc(e1) ∈ Id} 
                                                           ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
                                                           ⟶ ℙ].
  ([e1,e2]~([a,b].p[a;b])+ ∈ ℙ)

Lemma: es-pplus_functionality_wrt_implies
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,p':{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {p[a;b] ⇒ p'[a;b]}))
    ⇒ {[e1,e2]~([a,b].p[a;b])+ ⇒ [e1,e2]~([a,b].p'[a;b])+})

Lemma: es-pplus_functionality_wrt_rev_implies
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,p':{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {p[a;b] ⇐ p'[a;b]}))
    ⇒ {[e1,e2]~([a,b].p[a;b])+ ⇐ [e1,e2]~([a,b].p'[a;b])+})

Lemma: es-pplus_functionality_wrt_iff
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ (p[a;b] ⇐⇒ q[a;b])))
    ⇒ ([e1,e2]~([a,b].p[a;b])+ ⇐⇒ [e1,e2]~([a,b].q[a;b])+))

Lemma: es-pplus-trivial
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]
    (e1 ≤loc e2  ⇒ Q[e1;e2] ⇒ [e1,e2]~([a,b].Q[a;b])+)

Lemma: es-pplus-le
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]. ([e1,e2]~([a,b].Q[a;b])+ ⇒ e1 ≤loc e2 )

Lemma: es-pplus-alle-between2
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]. ([e1,e2]~([a,b].∀e∈[a,b].Q[e])+ ⇐⇒ e1 ≤loc e2  ∧ ∀e∈[e1,e2].Q[e])

Lemma: es-pplus-partition
∀es:EO. ∀e1,e2,b:E.
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]
    ((e1 <loc b) ⇒ b ≤loc e2  ⇒ [e1,pred(b)]~([a,b].Q[a;b])+ ⇒ [b,e2]~([a,b].Q[a;b])+ ⇒ [e1,e2]~([a,b].Q[a;b])+)

Lemma: es-pplus-first-since
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e])) ⇒ ([e1,e2]~([a,b].b = first e ≥ a.Q[e])+ ⇐⇒ e1 ≤loc e2  ∧ Q[e2]))

Lemma: es-pplus-first-since-exit
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q,R:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e]))
    ⇒ ([e1,e2]~([a,b].b = first e ≥ a.Q[e] ∧ ∀e∈[a,b).¬R[e])+ ⇐⇒ e1 ≤loc e2  ∧ Q[e2] ∧ ∀e∈[e1,e2].R[e] ⇒ Q[e]))

Definition: data
data(T) ==  x:Id × (T x)

Lemma: data_wf
∀[T:Id ⟶ Type]. (data(T) ∈ Type)

Definition: secret-table
secret-table(T) ==  K:ℕ × ℕ × (ℕK ⟶ (Atom1 × ℕ + Atom1 × data(T)))

Definition: st-length
||tab||  ==  fst(tab)

Definition: st-ptr
ptr(tab) ==  fst(snd(tab))

Definition: st-atom
st-atom(tab;n) ==  fst(((snd(snd(tab))) n))

Definition: st-next
next(tab) ==  if ptr(tab) <z ||tab||  then inl <ptr(tab), st-atom(tab;ptr(tab))> else inr ⋅  fi 

Definition: st-key
key(tab;n) ==  fst(snd(((snd(snd(tab))) n)))

Definition: st-data
data(tab;n) ==  snd(snd(((snd(snd(tab))) n)))

Definition: st-lookup
st-lookup(tab;x) ==
  let K,p,f = tab in 
  let n = mu(λn.(p <z n ∨bK ≤z n ∨bfst((f n)) =a1 x)) in
      if p <z n ∨bK ≤z n then inr ⋅  else inl (snd((f n))) fi 

Definition: st-key-match
st-key-match(tab;k1;k2) ==
  case k1
   of inl(n) =>
   case k2 of inl(m) => ff | inr(a) => (n <z ptr(tab) ∧b n <z ||tab|| ) ∧b st-atom(tab;n) =a1 a
   | inr(a) =>
   case k2 of inl(n) => (n <z ptr(tab) ∧b n <z ||tab|| ) ∧b st-atom(tab;n) =a1 a | inr(b) => ff

Definition: st-decrypt
decrypt(tab;kval) ==
  let k,x = kval 
  in if isl(st-lookup(tab;x))
     then let key,data = outl(st-lookup(tab;x)) 
          in if st-key-match(tab;key;k) then inl data else inr ⋅  fi 
     else inr ⋅ 
     fi 

Definition: st-encrypt
encrypt(tab;keyv) ==  let K,p,f = tab in <K, p + 1, if p <z K then f[p:=<fst((f p)), keyv>] else f fi >

Lemma: secret-table_wf
∀[T:Id ⟶ Type]. (secret-table(T) ∈ Type)

Lemma: st-length_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)].  (||tab||  ∈ ℕ)

Lemma: st-ptr_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)].  (ptr(tab) ∈ ℕ)

Lemma: st-atom_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[n:ℕ||tab|| ].  (st-atom(tab;n) ∈ Atom1)

Lemma: st-key_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[n:ℕ||tab|| ].  (key(tab;n) ∈ ℕ + Atom1)

Lemma: st-data_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[n:ℕ||tab|| ].  (data(tab;n) ∈ data(T))

Lemma: st-ptr-wf2
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)].  ptr(tab) ∈ ℕ||tab||  supposing ↑isl(next(tab))

Lemma: st-lookup_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[x:Atom1].  (st-lookup(tab;x) ∈ ℕ + Atom1 × data(T)?)

Definition: st-atoms-distinct
atoms-distinct(tab) ==  ∀i,j:ℕ||tab|| .  ((st-atom(tab;i) = st-atom(tab;j) ∈ Atom1) ⇒ (i = j ∈ ℤ))

Lemma: st-atoms-distinct_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)].  (atoms-distinct(tab) ∈ ℙ)

Lemma: st-lookup-property
∀[T:Id ⟶ Type]
  ∀tab:secret-table(T). ∀x:Atom1.
    (↑isl(st-lookup(tab;x)) ⇐⇒ ∃n:ℕ||tab|| . ((n ≤ ptr(tab)) ∧ (st-atom(tab;n) = x ∈ Atom1)))

Lemma: st-lookup-outl
∀[T:Id ⟶ Type]
  ∀tab:secret-table(T). ∀x:Atom1.
    ∃n:ℕ||tab|| 
     ((n ≤ ptr(tab))
     ∧ (st-atom(tab;n) = x ∈ Atom1)
     ∧ (outl(st-lookup(tab;x)) = <key(tab;n), data(tab;n)> ∈ (ℕ + Atom1 × data(T)))) 
    supposing ↑isl(st-lookup(tab;x))

Lemma: st-key-match_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[k1,k2:ℕ + Atom1].  (st-key-match(tab;k1;k2) ∈ 𝔹)

Lemma: st-lookup-distinct
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)].
  ∀[x:Atom1]. ∀[n:ℕ||tab|| ].
    ((↑isl(st-lookup(tab;x)))
       c∧ (outl(st-lookup(tab;x)) = <key(tab;n), data(tab;n)> ∈ (ℕ + Atom1 × data(T)))) supposing 
       ((st-atom(tab;n) = x ∈ Atom1) and 
       (n ≤ ptr(tab))) 
  supposing atoms-distinct(tab)

Lemma: st-next_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)].  (next(tab) ∈ ℕ||tab||  × Atom1?)

Lemma: st-decrypt_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[kx:ℕ + Atom1 × Atom1].  (decrypt(tab;kx) ∈ data(T)?)

Lemma: st-encrypt_wf
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[keyv:ℕ + Atom1 × data(T)].  (encrypt(tab;keyv) ∈ secret-table(T))

Lemma: st-length-encrypt
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[keyv:ℕ + Atom1 × data(T)].  (||encrypt(tab;keyv)||  = ||tab||  ∈ ℤ)

Lemma: st-atom-encrypt
∀[T:Id ⟶ Type]. ∀[tab:secret-table(T)]. ∀[keyv:ℕ + Atom1 × data(T)]. ∀[n:ℕ||tab|| ].
  (st-atom(encrypt(tab;keyv);n) = st-atom(tab;n) ∈ Atom1)

Definition: cond-to-list
?[x] ==  case x of inl(y) => [y] | inr(y) => []

Lemma: cond-to-list_wf
∀[A:Type]. ∀[x:A?].  (?[x] ∈ A List)

Definition: es-seq
es-seq(es;S) ==  ∀e1,e2:E.  (e1 before e2 ∈ S ⇒ (¬(e2 < e1)))

Lemma: es-seq_wf
∀[es:EO]. ∀[S:E List].  (es-seq(es;S) ∈ ℙ)

Definition: es-in-port-conds
es-in-port-conds(A;l;tg) ==  rcv(l,tg) : <A, λs,v. (inl v)>

Definition: es-is-interface
(e in X) ==  can-apply(X;e)

Definition: concrete-interface
CI ==  dd:DeclSet × T:Type × (es-information-type(dd) ⟶ (T + Top))

Definition: ci-decls
decls(ci) ==  fst(ci)

Definition: ci-type
type(ci) ==  let dd,T,f = ci in T

Definition: ci-fun
ci-fun(ci) ==  let dd,T,f = ci in f

Definition: mk_ci
mk_ci(dd;T;f) ==  <dd, T, f>

Definition: ci-port
ci-port(l;tg;T) ==
  mk_ci(es-decl-set-single(destination(l);⊗;rcv(l,tg) : T);T;λx.let i,k,s,v = x
                                                                 in if k = rcv(l,tg) then inl v else inr ⋅  fi )

Definition: ci-or
ci1 | ci2 ==
  let dd1,A,f = ci1 in 
  let dd2,B,g = ci2 in 
  mk_ci(es-decl-set-join(dd1;dd2);one_or_both(A;B);λx.oob-apply(λx.if es-info-loc(x) ∈b |dd1|
                                                                      ∧b es-info-kind(x) ∈ dom(da(dd1;es-info-loc(x)))
                                                                   then f x
                                                                   else inr ⋅ 
                                                                   fi ;
                                                                λx.if es-info-loc(x) ∈b |dd2|
                                                                      ∧b es-info-kind(x) ∈ dom(da(dd2;es-info-loc(x)))
                                                                   then g x
                                                                   else inr ⋅ 
                                                                   fi ;
                                                                x))

Definition: information-flow
information-flow(T;S) ==  {i:Id| (i ∈ S)}  ⟶ {i:Id| (i ∈ S)}  ⟶ {s:T List| 0 < ||s||}  ⟶ (T + Top)

Lemma: information-flow_wf
∀[T:Type]. ∀[S:Id List].  (information-flow(T;S) ∈ Type)

Definition: flow-graph
flow-graph(S;T;F;G) ==
  ∀i,j:Id.  ((i ∈ S) ⇒ (j ∈ S) ⇒ (∀s:{s:T List| 0 < ||s||} . ((↑can-apply(F i j;s)) ⇒ (i⟶j)∈G)))

Lemma: flow-graph_wf
∀[T:Type]. ∀[S:Id List]. ∀[F:information-flow(T;S)]. ∀[G:Graph(S)].  (flow-graph(S;T;F;G) ∈ ℙ)

Definition: flow-state-compression
flow-state-compression(S;T;F;H;start;c) ==
  ∀i,j:Id.
    ((i ∈ S)
    ⇒ (j ∈ S)
    ⇒ (∀s:{s:T List| 0 < ||s||} 
          ((F i j s)
          = (H i j accumulate (with value sofar and list item x): c sofar xover list:  swith starting value: start i))
          ∈ (T + Top))))

Lemma: flow-state-compression_wf
∀[T:Type]. ∀[S:Id List]. ∀[F:information-flow(T;S)]. ∀[A:Type]. ∀[start:{i:Id| (i ∈ S)}  ⟶ A]. ∀[c:A ⟶ T ⟶ A].
∀[H:{i:Id| (i ∈ S)}  ⟶ {i:Id| (i ∈ S)}  ⟶ A ⟶ (T + Top)].
  (flow-state-compression(S;T;F;H;start;c) ∈ ℙ)

Definition: es-p-local-pred
es-p-local-pred(es;P) ==  λe,e'. ((e' <loc e) ∧ (P e') ∧ (∀e'':E. ((e'' <loc e) ⇒ (e' <loc e'') ⇒ (¬(P e'')))))

Lemma: es-p-local-pred_wf
∀[es:EO]. ∀[P:E ⟶ ℙ].  (es-p-local-pred(es;P) ∈ E ⟶ E ⟶ ℙ)

Definition: es-p-le-pred
es-p-le-pred(es;P) ==  λe,e'. (e' ≤loc e  ∧ (P e') ∧ (∀e'':E. (e'' ≤loc e  ⇒ (e' <loc e'') ⇒ (¬(P e'')))))

Lemma: es-p-le-pred_wf
∀[es:EO]. ∀[P:E ⟶ ℙ].  (es-p-le-pred(es;P) ∈ E ⟶ E ⟶ ℙ)

Lemma: decidable__es-p-local-pred
∀es:EO. ∀[P:E ⟶ ℙ]. ((∀e:E. Dec(P e)) ⇒ (∀e,e':E.  Dec(es-p-local-pred(es;P) e e')))

Lemma: decidable__es-p-le-pred
∀es:EO. ∀[P:E ⟶ ℙ]. ((∀e:E. Dec(P e)) ⇒ (∀e,e':E.  Dec(es-p-le-pred(es;P) e e')))

Lemma: decidable__exists-es-p-local-pred
∀es:EO. ∀[P:E ⟶ ℙ]. ∀e:E. ((∀e:E. Dec(P e)) ⇒ Dec(∃a:E. (es-p-local-pred(es;P) e a)))

Lemma: decidable__exists-es-p-le-pred
∀es:EO. ∀[P:E ⟶ ℙ]. ∀e:E. ((∀e:E. Dec(P e)) ⇒ Dec(∃a:E. (es-p-le-pred(es;P) e a)))

Definition: threshold_accum
threshold_accum(test;
nxt;
step;
g) ==
  λp,x. if test (fst(p)) x then <nxt <fst(p), x>, g <fst(p), x>> else <step (fst(p)) x, ff> fi 

Lemma: threshold_accum_wf
∀[S,A,B:Type]. ∀[test:S ⟶ A ⟶ 𝔹]. ∀[nxt:(S × A) ⟶ S]. ∀[step:S ⟶ A ⟶ S]. ∀[g:(S × A) ⟶ (B?)].
  (threshold_accum(test;
   nxt;
   step;
   g) ∈ (S × (B?)) ⟶ A ⟶ (S × (B?)))

Definition: threshold_val
threshold_val(p) ==  snd(p)

Lemma: threshold_val_wf
∀[S,A:Type]. ∀[p:S × (A?)].  (threshold_val(p) ∈ A?)

Definition: collect_filter
collect_filter() ==  λs.let i,vs,w = s in case w of inl(x) => {<i - 1, x>} | inr(x) => {}

Lemma: collect_filter_wf
∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ⟶ 𝔹].
  (collect_filter() ∈ (ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top))
   ⟶ bag(ℤ × {L:A List| 0 < ||L|| ∧ (↑P[L])} ))

Lemma: collect_filter-wf2
∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ⟶ 𝔹].
  (collect_filter() ∈ {s:ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)| 
                       (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))}  ⟶ bag(ℕ × {L:A List| 0 < ||L|| ∧ (↑P[L])} ))

Definition: es-class-type
es-class-type(p) ==  fst(p)

Definition: modify-combinator1
modify-combinator1(f) ==
  λu,p. (f 
         (λi.if (i =z 0)
               then case u 0 of inl(xy) => if oob-hasleft(xy) then inl oob-getleft(xy) else ff fi  | inr(_) => ff
             if (i =z 1)
               then case u 0 of inl(xy) => if oob-hasright(xy) then inl oob-getright(xy) else ff fi  | inr(_) => ff
             else u (i - 1)
             fi ) 
         p)

Lemma: modify-combinator1_wf
∀[n:ℕ]
  ∀[A:ℕn ⟶ Type]. ∀[m:ℕ]. ∀[B:ℕm ⟶ Type]. ∀[T:Type]. ∀[f:(i:ℕn ⟶ (A i + Top)) ⟶ (i:ℕm ⟶ (B i + Top)) ⟶ T].
    (modify-combinator1(f) ∈ (i:ℕn - 1 ⟶ if (i =z 0) then one_or_both(A 0;A 1) + Top else A (i + 1) + Top fi )
     ⟶ (i:ℕm ⟶ (B i + Top))
     ⟶ T) 
  supposing 1 < n

Definition: modify-combinator2
modify-combinator2(f) ==
  λu,p. (f u 
         (λi.if (i =z 0)
               then case p 0 of inl(xy) => if oob-hasleft(xy) then inl oob-getleft(xy) else ff fi  | inr(_) => ff
             if (i =z 1)
               then case p 0 of inl(xy) => if oob-hasright(xy) then inl oob-getright(xy) else ff fi  | inr(_) => ff
             else p (i - 1)
             fi ))

Lemma: modify-combinator2_wf
∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[m:ℕ].
  ∀[B:ℕm ⟶ Type]. ∀[T:Type]. ∀[f:(i:ℕn ⟶ (A i + Top)) ⟶ (i:ℕm ⟶ (B i + Top)) ⟶ T].
    (modify-combinator2(f) ∈ (i:ℕn ⟶ (A i + Top))
     ⟶ (i:ℕm - 1 ⟶ if (i =z 0) then one_or_both(B 0;B 1) + Top else B (i + 1) + Top fi )
     ⟶ T) 
  supposing 1 < m

Definition: collect_accm
collect_accm(v.P[v];v.num[v]) ==
  λs,v. eval n = num[v] in
        let i,vs,w = s in 
        if n <z i then <i, vs, inr 0 >
        if i <z n then if P[[v]] then <n + 1, [], inl [v]> else <n, [v], inr 0 > fi 
        if P[vs @ [v]] then <i + 1, [], inl (vs @ [v])>
        else <i, vs @ [v], inr 0 >
        fi 

Lemma: collect_accm_wf
∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ⟶ 𝔹]. ∀[num:A ⟶ ℕ].
  (collect_accm(v.P[v];v.num[v]) ∈ (ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top))
   ⟶ A
   ⟶ (ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)))

Lemma: collect_accm-wf2
∀[A:Type]. ∀[P:{L:A List| 0 < ||L||}  ⟶ 𝔹]. ∀[num:A ⟶ ℕ].
  (collect_accm(v.P[v];v.num[v]) ∈ {s:ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)|\000C 
                                    (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} 
   ⟶ A
   ⟶ {s:ℤ × {L:A List| 0 < ||L|| ⇒ (¬↑P[L])}  × ({L:A List| 0 < ||L|| ∧ (↑P[L])}  + Top)| 
       (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} )

Definition: collect_accum
collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]) ==
  λs,v. eval n = num[v] in
        let i,a,w = s in 
        if n <z i then <i, a, inr 0 >
        if i <z n then if P[f[init; v]] then <n + 1, init, inl f[init; v]> else <n, f[init; v], inr 0 > fi 
        if P[f[a; v]] then <i + 1, init, inl f[a; v]>
        else <i, f[a; v], inr 0 >
        fi 

Lemma: collect_accum_wf
∀[A,B:Type]. ∀[P:B ⟶ 𝔹]. ∀[num:A ⟶ ℕ]. ∀[init:B]. ∀[f:B ⟶ A ⟶ B].
  (collect_accum(x.num[x];init;a,v.f[a;v];a.P[a]) ∈ (ℤ × B × (B + Top)) ⟶ A ⟶ (ℤ × B × (B + Top)))

Lemma: collect_accum-wf2
∀[A,B:Type]. ∀[P:B ⟶ 𝔹]. ∀[num:A ⟶ ℕ]. ∀[init:B]. ∀[f:B ⟶ A ⟶ B].
  (collect_accum(x.num[x];init;a,v.f[a;v];a.P[a]) ∈ {s:ℤ × B × (B + Top)| (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} 
   ⟶ A
   ⟶ {s:ℤ × B × (B + Top)| (↑isl(snd(snd(s)))) ⇒ (1 ≤ (fst(s)))} )

Definition: collect_filter_accum_fun
collect_filter_accum_fun(b,v.f[b; v];base;size;v.num[v];v.P[v]) ==
  λs,v. eval n = num[v] in
        eval vok = P[v] in
          let i,m,b,w = s 
          in if n <z i then <i, m, b, inr 0 >
             if vok
               then if i <z n
                    then if (1 =z size) then <n + 1, 0, f[base; v], inl tt> else <n, 1, f[base; v], inr 0 > fi 
                    else eval m' = m + 1 in
                         if (m' =z size) then <i + 1, 0, f[base; v], inl tt> else <i, m', f[b; v], inr 0 > fi 
                    fi 
             if i <z n then <n + 1, 0, f[base; v], inl ff>
             else <i + 1, 0, f[b; v], inl ff>
             fi   

Lemma: collect_filter_accum_fun_wf
∀[A,B:Type]. ∀[base:B]. ∀[f:B ⟶ A ⟶ B]. ∀[size:ℕ+]. ∀[num:A ⟶ ℕ]. ∀[P:A ⟶ 𝔹].
  (collect_filter_accum_fun(b,v.f[b;v];base;size;v.num[v];v.P[v]) ∈ {s:ℤ × ℕ × B × (𝔹 + Top)| 
                                                                     (↑isl(snd(snd(snd(s))))) ⇒ (1 ≤ (fst(s)))} 
   ⟶ A
   ⟶ {s:ℤ × ℕ × B × (𝔹 + Top)| (↑isl(snd(snd(snd(s))))) ⇒ (1 ≤ (fst(s)))} )

Lemma: es-fset-at-loc
∀es:EO. ∀i:Id. ∀s:fset(E).
  ∃L:E List. ((∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ L))) ∧ no_repeats(E;L) ∧ sorted-by(λe,e'. e ≤loc e' ;L))

Definition: es-fset-at
s@i ==  fst((TERMOF{es-fset-at-loc:o, 1:l, i:l} es i s))

Lemma: es-fset-at_wf
∀[es:EO]. ∀[i:Id]. ∀[s:fset(E)].  (s@i ∈ E List)

Lemma: es-fset-at-property
∀es:EO. ∀i:Id. ∀s:fset(E).
  ((∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ s@i))) ∧ no_repeats(E;s@i) ∧ sorted-by(λe,e'. e ≤loc e' ;s@i))

Lemma: es-empty-fset-at
∀[es:EO]. ∀[i:Id].  ({}@i ~ [])

Definition: es-fset-loc
i ∈ locs(s) ==  ¬↑null(s@i)

Lemma: es-fset-loc_wf
∀[es:EO]. ∀[s:fset(E)]. ∀[i:Id].  (i ∈ locs(s) ∈ ℙ)

Lemma: decidable__es-fset-loc
∀es:EO. ∀s:fset(E). ∀i:Id.  Dec(i ∈ locs(s))

Lemma: es-fset-loc-iff
∀es:EO. ∀s:fset(E). ∀i:Id.  (i ∈ locs(s) ⇐⇒ ∃e:E. ((loc(e) = i ∈ Id) ∧ e ∈ s))

Definition: es-fset-last
s(i) ==  last(s@i)

Lemma: es-fset-last_wf
∀[es:EO]. ∀[s:fset(E)]. ∀[i:Id].
  s(i) ∈ {e:E| (loc(e) = i ∈ Id) ∧ e ∈ s ∧ (∀e':E. (e' ∈ s ⇒ (¬(e <loc e'))))}  supposing i ∈ locs(s)

Definition: conditional
[P? f : g] ==  λx.if p:P x then f x else g x fi 

Lemma: conditional_wf
∀[T,V:Type]. ∀[A:T ⟶ ℙ]. ∀[dcd_A:t:T ⟶ Dec(A t)]. ∀[f:{t:T| A t}  ⟶ V]. ∀[g:{t:T| ¬(A t)}  ⟶ V].
  ([A? f : g] ∈ T ⟶ V)

Lemma: conditional_wf2
∀[T,V:Type]. ∀[A,B:T ⟶ ℙ]. ∀[dcd_A:t:T ⟶ Dec(A[t])]. ∀[f:{t:T| A[t]}  ⟶ V]. ∀[g:{t:T| B[t]}  ⟶ V].
  ([λt.A[t]? f : g] ∈ {t:T| A[t] ∨ B[t]}  ⟶ V)

Lemma: conditional-idempotent
∀[T,V:Type]. ∀[A:T ⟶ ℙ]. ∀[dcd_A:t:T ⟶ Dec(A t)]. ∀[g:T ⟶ V].  ([A? g : g] = g ∈ (T ⟶ V))

Lemma: conditional-ifthenelse
∀[T,V:Type]. ∀[A,B:T ⟶ 𝔹]. ∀[f:{x:T| ↑(A x)}  ⟶ V]. ∀[g:{x:T| ↑(B x)}  ⟶ V].
  ((λx.if A x then f x else g x fi ) = [λx.(↑(A x))? f : g] ∈ ({x:T| (↑(A x)) ∨ (↑(B x))}  ⟶ V))

Lemma: conditional-apply
∀[T,V:Type]. ∀[A,B:T ⟶ ℙ]. ∀[dcd_A:t:T ⟶ Dec(A t)]. ∀[f:{t:T| A t}  ⟶ V]. ∀[g:{t:T| B t}  ⟶ V]. ∀[t:{t:T| 
                                                                                                       (A t) ∨ (B t)} ].
  (([A? f : g] t) = (f t) ∈ V supposing A t ∧ ([A? f : g] t) = (g t) ∈ V supposing ¬(A t))

Definition: weak-antecedent-function
Q ←==f== P ==  ∀e:{e:E| P e} . (f e c≤ e ∧ (Q (f e)))

Lemma: weak-antecedent-function_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  (Q ←==f== P ∈ ℙ)

Lemma: weak-antecedent-function-property
∀[es:EO]. ∀[P,Q:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  f ∈ {e:E| P e}  ⟶ {e:E| Q e}  supposing Q ←==f== P

Lemma: weak-antecedent-function_functionality_wrt_pred_equiv
∀es:EO. ∀[P,Q,P',Q':E ⟶ ℙ].  ∀f:{e:E| P e}  ⟶ {e:E| Q e} . (P ⇐⇒ P' ⇒ Q ⇐⇒ Q' ⇒ (Q ←==f== P ⇐⇒ Q' ←==f== P'))

Lemma: weak-antecedent-functions-compose
∀es:EO
  ∀[P,Q,R:E ⟶ ℙ].
    ∀f:{e:E| P e}  ⟶ {e:E| Q e} . ∀g:{e:E| Q e}  ⟶ {e:E| R e} .  ((Q ←==f== P ∧ R ←==g== Q) ⇒ R ←==g o f== P)

Lemma: weak-antecedent-conditional
∀es:EO
  ∀[P1,Q1,P2,Q2:E ⟶ ℙ].
    ∀dcd_P1:e:E ⟶ Dec(P1 e). ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} . ∀g:{e:E| P2 e}  ⟶ {e:E| Q2 e} .
      ((Q1 ←==f== P1 ∧ Q2 ←==g== P2) ⇒ λe.((Q1 e) ∨ (Q2 e)) ←==[P1? f : g]== λe.((P1 e) ∨ (P2 e)))

Definition: weak-antecedent-surjection
Q ←←= f== P ==  Q ←==f== P ∧ (∀e:{e:E| Q e} . ∃e':{e:E| P e} . ((f e') = e ∈ E))

Lemma: weak-antecedent-surjection_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  (Q ←←= f== P ∈ ℙ)

Lemma: weak-antecedent-surjection-property
∀[es:EO]. ∀[P,Q:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  f ∈ {e:E| P e}  ⟶ {e:E| Q e}  supposing Q ←←= f== P

Lemma: weak-antecedent-surjection_functionality_wrt_pred_equiv
∀es:EO
  ∀[P1,P2,Q1,Q2:E ⟶ ℙ].  ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} . (P1 ⇐⇒ P2 ⇒ Q1 ⇐⇒ Q2 ⇒ (Q1 ←←= f== P1 ⇐⇒ Q2 ←←= f== P2))

Lemma: weak-antecedent-surjections-compose
∀es:EO
  ∀[P,Q,R:E ⟶ ℙ].
    ∀f:{e:E| P e}  ⟶ {e:E| Q e} . ∀g:{e:E| Q e}  ⟶ {e:E| R e} .  ((Q ←←= f== P ∧ R ←←= g== Q) ⇒ R ←←= g o f== P)

Lemma: weak-antecedent-surjection-conditional
∀es:EO
  ∀[P1,Q1,P2,Q2:E ⟶ ℙ].
    ∀dcd_P1:e:E ⟶ Dec(P1 e). ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} . ∀g:{e:E| P2 e}  ⟶ {e:E| Q2 e} .
      (∀e:E. Dec(Q1 e))
      ⇒ (∀e:E. Dec(Q2 e))
      ⇒ Q1 ←←= f== P1
      ⇒ Q2 ←←= g== P2
      ⇒ λe.((Q1 e) ∨ (Q2 e)) ←←= [P1? f : g]== λe.((P1 e) ∨ (P2 e)) 
      supposing ∀e:E. ((P1 e) ⇒ (¬(P2 e)))

Lemma: weak-antecedent-surjection-conditional2
∀es:EO
  ∀[P1,Q1,P2,Q2:E ⟶ ℙ].
    ∀dcd_P1:e:E ⟶ Dec(P1 e). ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} . ∀g:{e:E| P2 e}  ⟶ {e:E| Q2 e} .
      (∀e:E. Dec(Q1 e)) ⇒ (∀e:E. Dec(Q2 e)) ⇒ Q1 ←←= f== P1 ⇒ Q2 ←←= g== P2 ⇒ Q1 ∨ Q2 ←←= [P1? f : g]== P1 ∨ P2 
      supposing ∀e:E. ((P1 e) ⇒ (¬(P2 e)))

Definition: Q-R-pre-preserving
f is Q-R-pre-preserving on P ==  ∀e,e':{e:E| P e} .  ((Q (f e) (f e')) ⇒ (R e e'))

Lemma: Q-R-pre-preserving_wf
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[Q,R:E ⟶ E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  (f is Q-R-pre-preserving on P ∈ ℙ)

Lemma: Q-R-pre-preserving_functionality_wrt_implies
∀es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,R1,Q2,R2:E ⟶ E ⟶ ℙ].
    ∀f:{e:E| P1 e}  ⟶ E
      (P1 ⇐ P2 ⇒ Q1 ⇐ Q2 ⇒ R1 => R2 ⇒ {f is Q1-R1-pre-preserving on P1 ⇒ f is Q2-R2-pre-preserving on P2})

Lemma: Q-R-pre-preserving-rewrite-test
∀es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,R1,Q2,R2:E ⟶ E ⟶ ℙ].
    ∀f:{e:E| P1 e}  ⟶ E
      (P2 ⇒ P1 ⇒ Q2 => Q1 ⇒ R1 => R2 ⇒ {f is Q1-R1-pre-preserving on P1 ⇒ f is Q2-R2-pre-preserving on P2})

Lemma: Q-R-pre-preserving-compose
∀es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,Q2,Q3:E ⟶ E ⟶ ℙ].
    ∀f1:{e:E| P1 e}  ⟶ {e:E| P2 e} . ∀f2:{e:E| P2 e}  ⟶ E.
      (f1 is Q2-Q3-pre-preserving on P1 ⇒ f2 is Q1-Q2-pre-preserving on P2 ⇒ f2 o f1 is Q1-Q3-pre-preserving on P1)

Lemma: Q-R-pre-preserving-1-1
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[Q,R:E ⟶ E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].
  (Inj({e:E| P e} ;E;f)) supposing (f is Q-R-pre-preserving on P and AntiSym(E;e,e'.R e e') and Refl(E;e,e'.Q e e'))

Lemma: Q-R-pre-preserving-conditional
∀es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,R1,Q2,R2:E ⟶ E ⟶ ℙ].
    ∀dcd_P1:e:E ⟶ Dec(P1 e). ∀f1:{e:E| P1 e}  ⟶ E. ∀f2:{e:E| P2 e}  ⟶ E.
      (f1 is Q1-R1-pre-preserving on P1
         ⇒ f2 is Q2-R2-pre-preserving on P2
         ⇒ [P1? f1 : f2] is Q1 ∨ Q2-R1 ∨ R2-pre-preserving on P1 ∨ P2) supposing 
         ((∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
             ((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))) and 
         (∀e,e':{e:E| P2 e} .  (¬(Q1 (f2 e) (f2 e')))) and 
         (∀e,e':{e:E| P1 e} .  (¬(Q2 (f1 e) (f1 e')))))

Definition: rel-pre-preserving
f is R-pre-preserving on P ==  f is R-R-pre-preserving on P

Lemma: rel-pre-preserving_wf
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[R:E ⟶ E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  (f is R-pre-preserving on P ∈ ℙ)

Lemma: rel-pre-preserving-compose
∀es:EO
  ∀[P,Q:E ⟶ ℙ]. ∀[R:E ⟶ E ⟶ ℙ].
    ∀f1:{e:E| P e}  ⟶ {e:E| Q e} . ∀f2:{e:E| Q e}  ⟶ E.
      ((f1 is R-pre-preserving on P ∧ f2 is R-pre-preserving on Q) ⇒ f2 o f1 is R-pre-preserving on P)

Definition: locl-pre-preserving
f is locl-pre-preserving on P ==  f is λe,e'. e ≤loc e' -pre-preserving on P

Lemma: locl-pre-preserving_wf
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  (f is locl-pre-preserving on P ∈ ℙ)

Lemma: locl-pre-preserving-compose
∀es:EO
  ∀[P,Q:E ⟶ ℙ].
    ∀f1:{e:E| P e}  ⟶ {e:E| Q e} . ∀f2:{e:E| Q e}  ⟶ E.
      ((f1 is locl-pre-preserving on P ∧ f2 is locl-pre-preserving on Q) ⇒ f2 o f1 is locl-pre-preserving on P)

Lemma: locl-pre-preserving-1-1
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ E].  Inj({e:E| P e} ;E;f) supposing f is locl-pre-preserving on P

Lemma: inject-composes
∀[A,B0,B1,C:Type]. ∀[f:A ⟶ B0]. ∀[g:B1 ⟶ C].
  (Inj(A;C;g o f)) supposing (Inj(B1;C;g) and Inj(A;B0;f) and strong-subtype(B0;B1))

Definition: failure-known
failure-known(es;e;i) ==  ∀x@i.e c≤ x ⇒ (∀j:Id. ((¬(j = i ∈ Id)) ⇒ ∀y@j.¬x c≤ y))

Lemma: failure-known_wf
∀[es:EO]. ∀[i:Id]. ∀[e:E].  (failure-known(es;e;i) ∈ ℙ)

Lemma: failure-known-causle
∀[es:EO]. ∀[i:Id]. ∀[e,e':E].  (failure-known(es;e';i)) supposing (failure-known(es;e;i) and e c≤ e')

Definition: es-effective
es-effective(es;e) ==  ∃e':E. (e c≤ e' ∧ (¬(loc(e') = loc(e) ∈ Id)))

Lemma: es-effective_wf
∀[es:EO]. ∀[e:E].  (es-effective(es;e) ∈ ℙ)

Lemma: es-effective-causle
∀es:EO. ∀e,e':E.  (e c≤ e' ⇒ es-effective(es;e') ⇒ es-effective(es;e))

Lemma: failure-known-effective
∀[es:EO]. ∀[i:Id]. ∀[e:E].  uiff(failure-known(es;e;i);∀x@i.e c≤ x ⇒ (¬es-effective(es;x)))

Definition: thread
Thread ==  Id × Id

Lemma: thread_wf
Thread ∈ Type

Definition: thread-name
t.name ==  fst(t)

Lemma: thread-name_wf
∀[t:Thread]. (t.name ∈ Id)

Definition: thread-session
t.session ==  snd(t)

Lemma: thread-session_wf
∀[t:Thread]. (t.session ∈ Id)

Lemma: member-ite
∀b:𝔹. ∀[T:Type]. ∀A,B:T List. ∀x:T.  ((x ∈ if b then A else B fi ) ⇐⇒ ((↑b) ∧ (x ∈ A)) ∨ ((¬↑b) ∧ (x ∈ B)))

Lemma: bool-inhabited
𝔹

Lemma: decidable-exists-finite
∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Dec(P[x])) ⇒ finite-type(T) ⇒ Dec(∃x:T. P[x]))

Lemma: decidable__ex_unit
∀[P:Unit ⟶ ℙ]. (Dec(P[⋅]) ⇒ Dec(∃x:Unit. P[x]))

Lemma: ite-same
∀[b:𝔹]. ∀[x:Top].  (if b then x else x fi  ~ x)

Definition: onethird-consensus
onethird-consensus(es;t;Input;Vote;Output;voters;clients) ==
  no_repeats(Id;voters)
  ∧ (||voters|| = ((3 * t) + 1) ∈ ℤ)
  ∧ left(inning_val()[es-threshold(es; simple_consensus_init(); inning_step(); inning_test(1); nxt_inning(); Input+Vote
                                   )]) ⇐⇒  Vote@voters
  ∧ right(inning_val()[es-threshold(es; simple_consensus_init(); inning_step(); inning_test(1); nxt_inning(); Input+Vote
                                    )]) ⇐⇒  Output@clients

Lemma: es-rank_le
∀[es:EO]. ∀[e1,e2:E].  es-rank(es;e1) ≤ es-rank(es;e2) supposing e1 c≤ e2

Lemma: es-first-before
∀es:EO. ∀i:Id. ∀e':E.
  ∀[P:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ]
    (∀e@i.Dec(P[e]) ⇒ ∃e<e'.e is first@ i s.t.  e.P[e] ⇐⇒ ∃e<e'.P[e] supposing loc(e') = i ∈ Id)

Lemma: es-first-at-since-iff
∀es:EO. ∀i:Id. ∀e:E.
  ∀[P,R:{e:E| loc(e) = i ∈ Id}  ⟶ ℙ].
    ((∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id)
    ⇒ (es-first-at-since(es;i;e;e.R[e];e.P[e])
       ⇐⇒ (loc(e) = i ∈ Id)
           c∧ ((P[e] ∧ (¬R[e]))
              ∧ ((∃e'':E. ((e'' <loc e) c∧ P[e'']))
                ⇒ (∃e':E
                     ((e' <loc e)
                     c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ ((¬P[e'']) ∧ (¬R[e''])))))))))))

Lemma: es-first-before2
∀es:EO. ∀e':E.
  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]
    (∀e@loc(e').Dec(P[e]) ⇒ (∃e<e'.e is first@ loc(e') s.t.  e.P[e] ⇐⇒ ∃e<e'.P[e]))

Definition: sub-es-pred
sub-es-pred(es;dom;e) ==
  fix((λsub-es-pred,e. if first(e) then inr ⋅  if dom pred(e) then inl pred(e) else sub-es-pred pred(e) fi )) e

Lemma: sub-es-pred_wf
∀[es:EO]. ∀[dom:E ⟶ 𝔹]. ∀[e:E].  (sub-es-pred(es;dom;e) ∈ {e:E| ↑(dom e)} ?)

Definition: causale-order-preserving
a.f[a] is c≤ preserving on e.P[e] ==  ∀e,e':{e:E| P[e]} .  (e c≤ e' ⇒ f[e] c≤ f[e'])

Lemma: causale-order-preserving_wf
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[f:{e:E| P[e]}  ⟶ E].  (e.f[e] is c≤ preserving on e.P[e] ∈ ℙ)

Definition: causal-order-preserving
a.f[a] is c< preserving on e.P[e] ==  ∀e,e':{e:E| P[e]} .  ((e < e') ⇒ (f[e] < f[e']))

Lemma: causal-order-preserving_wf
∀[es:EO]. ∀[P:E ⟶ ℙ]. ∀[f:{e:E| P[e]}  ⟶ E].  (e.f[e] is c< preserving on e.P[e] ∈ ℙ)

Definition: antecedent-function
Q ⟵─f── P ==  ∀e:{e:E| P e} . ((f e < e) ∧ (Q (f e)))

Lemma: antecedent-function_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ {e:E| Q e} ].  (Q ⟵─f── P ∈ ℙ)

Lemma: antecedent-function_functionality_wrt_iff
∀es:EO
  ∀[P,Q,P',Q':E ⟶ ℙ].
    ∀f:{e:E| P e}  ⟶ {e:E| Q e} . ((∀e:E. (P e ⇐⇒ P' e)) ⇒ (∀e:E. (Q e ⇐⇒ Q' e)) ⇒ (Q ⟵─f── P ⇐⇒ Q' ⟵─f── P'))

Definition: antecedent-surjection
Q ←⟵ f── P ==  Q ⟵─f── P ∧ (∀e:{e:E| Q e} . ∃e':{e:E| P e} . ((f e') = e ∈ E))

Lemma: antecedent-surjection_wf
∀[es:EO]. ∀[P,Q:E ⟶ ℙ]. ∀[f:{e:E| P e}  ⟶ {e:E| Q e} ].  (Q ←⟵ f── P ∈ ℙ)

Lemma: antecedent-surjection_functionality_wrt_iff
∀es:EO
  ∀[P1,P2,Q1,Q2:E ⟶ ℙ].
    ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} 
      ((∀e:E. (P1 e ⇐⇒ P2 e)) ⇒ (∀e:E. (Q1 e ⇐⇒ Q2 e)) ⇒ (Q1 ←⟵ f── P1 ⇐⇒ Q2 ←⟵ f── P2))

Definition: causal-predecessor
causal-predecessor(es;p) ==  ∀e:E. ((↑can-apply(p;e)) ⇒ (do-apply(p;e) < e))

Lemma: causal-predecessor_wf
∀[es:EO]. ∀[p:E ⟶ (E + Top)].  (causal-predecessor(es;p) ∈ ℙ)

Lemma: causal-pred-wellfounded
∀es:EO. ∀p:E ⟶ (E + Top).  (causal-predecessor(es;p) ⇒ SWellFounded(p-graph(E;p) y x))

Definition: causal-weak-predecessor
causal-weak-predecessor(es;p) ==  ∀e:E. ((↑can-apply(p;e)) ⇒ do-apply(p;e) c≤ e)

Lemma: causal-weak-predecessor_wf
∀[es:EO]. ∀[p:E ⟶ (E + Top)].  (causal-weak-predecessor(es;p) ∈ ℙ)

Lemma: p-compose-causal-predecessor1
∀es:EO. ∀p,w:E ⟶ (E + Top).
  (causal-predecessor(es;p) ⇒ causal-weak-predecessor(es;w) ⇒ causal-predecessor(es;p o w))

Definition: es-p-locl
e p< e' ==  ∃n:ℕ+. (p-graph(E;p^n) e' e)

Lemma: es-p-locl_wf
∀[es:EO]. ∀[p:E ⟶ (E + Top)]. ∀[e,e':E].  (e p< e' ∈ ℙ)

Definition: es-p-le
e p≤ e' ==  e p< e' ∨ (e = e' ∈ E)

Lemma: es-p-le_wf
∀[es:EO]. ∀[p:E ⟶ (E + Top)]. ∀[e,e':E].  (e p≤ e' ∈ ℙ)

Lemma: es-p-locl_transitivity
∀es:EO. ∀p:E ⟶ (E + Top). ∀a,b,c:E.  (a p< b ⇒ b p< c ⇒ a p< c)

Lemma: es-p-le_transitivity
∀es:EO. ∀p:E ⟶ (E + Top). ∀a,b,c:E.  (a p≤ b ⇒ b p≤ c ⇒ a p≤ c)

Lemma: es-p-le_weakening
∀es:EO. ∀p:E ⟶ (E + Top). ∀e,e':E.  (e p< e' ⇒ e p≤ e')

Lemma: es-p-le_weakening_eq
∀es:EO. ∀p:E ⟶ (E + Top). ∀e,e':E.  e p≤ e' supposing e = e' ∈ E

Lemma: es-p-locl_transitivity1
∀es:EO. ∀p:E ⟶ (E + Top). ∀a,b,c:E.  (a p< b ⇒ b p≤ c ⇒ a p< c)

Lemma: es-p-locl_transitivity2
∀es:EO. ∀p:E ⟶ (E + Top). ∀a,b,c:E.  (a p≤ b ⇒ b p< c ⇒ a p< c)

Lemma: es-p-locl-test
∀es:EO. ∀p:E ⟶ (E + Top). ∀a,b,c,d,e:E.  (c p≤ d ⇒ d p≤ e ⇒ a p≤ b ⇒ b p< c ⇒ a p< e)

Lemma: es-causl_weakening_p-locl
∀es:EO. ∀p:E ⟶ (E + Top).  (causal-predecessor(es;p) ⇒ (∀e,e':E.  (e p< e' ⇒ (e < e'))))

Lemma: es-causle_weakening_p-le
∀es:EO. ∀p:E ⟶ (E + Top).  (causal-predecessor(es;p) ⇒ (∀e,e':E.  (e p≤ e' ⇒ e c≤ e')))

Lemma: es-causl-p-locl-test
∀es:EO. ∀p:E ⟶ (E + Top).  (causal-predecessor(es;p) ⇒ (∀e,e',a,b:E.  (a c≤ e ⇒ e p≤ e' ⇒ e' p< b ⇒ (a < b))))

Definition: same-thread
same-thread(es;p;e;e') ==  final-iterate(p;e) = final-iterate(p;e') ∈ E

Lemma: same-thread_wf
∀[es:EO]. ∀[p:E ⟶ (E + Top)].  ∀[e,e':E].  (same-thread(es;p;e;e') ∈ ℙ) supposing causal-predecessor(es;p)

Lemma: same-thread-do-apply
∀[es:EO]. ∀[p:E ⟶ (E + Top)].
  ∀[e:E]. same-thread(es;p;e;do-apply(p;e)) supposing ↑can-apply(p;e) supposing causal-predecessor(es;p)

Lemma: same-thread_weakening
∀[es:EO]. ∀[p:E ⟶ (E + Top)].
  ∀[e,e':E].  same-thread(es;p;e;e') supposing e = e' ∈ E supposing causal-predecessor(es;p)

Lemma: same-thread_inversion
∀[es:EO]. ∀[p:E ⟶ (E + Top)]. ∀[e,e':E].
  (same-thread(es;p;e';e)) supposing (same-thread(es;p;e;e') and causal-predecessor(es;p))

Lemma: same-thread_transitivity
∀[es:EO]. ∀[p:E ⟶ (E + Top)].
  ∀[a,b,c:E].  (same-thread(es;p;a;c)) supposing (same-thread(es;p;b;c) and same-thread(es;p;a;b)) 
  supposing causal-predecessor(es;p)

Lemma: decidable__same-thread
∀es:EO. ∀p:E ⟶ (E + Top).  (causal-predecessor(es;p) ⇒ (∀e,e':E.  Dec(same-thread(es;p;e;e'))))

Lemma: thread-p-ordered
∀es:EO. ∀p:E ⟶ (E + Top).
  ((causal-predecessor(es;p) ∧ p-inject(E;E;p))
  ⇒ (∀e,e':E.  (e p< e' ∨ (e = e' ∈ E)) ∨ e' p< e supposing same-thread(es;p;e;e')))

Lemma: thread-ordered
∀es:EO. ∀p:E ⟶ (E + Top).
  ((causal-predecessor(es;p) ∧ p-inject(E;E;p))
  ⇒ (∀e,e':E.  ((e < e') ∨ (e = e' ∈ E)) ∨ (e' < e) supposing same-thread(es;p;e;e')))

Lemma: cond_rel_equivalent
∀[T:Type]. ∀[R,Q:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].
  (Trans(T;x,y.Q x y)
  ⇒ R => Q
     ⇒ (∀x,y:T.  (((P x) ∧ (P y)) ⇒ (((R x y) ∨ (x = y ∈ T)) ∨ (R y x))))
     ⇒ (∀x,y:T.  (((P x) ∧ (P y)) ⇒ (R x y ⇐⇒ Q x y))) 
     supposing ∀x,y:T.  ((Q x y) ⇒ (¬(Q y x))))

Lemma: cond_equiv_to_causl
∀es:EO
  ∀[R:E ⟶ E ⟶ ℙ]. ∀[P:E ⟶ ℙ].
    (R => λe,e'. (e < e')
    ⇒ (∀x,y:E.  (((P x) ∧ (P y)) ⇒ (((R x y) ∨ (x = y ∈ E)) ∨ (R y x))))
    ⇒ (∀x,y:E.  (((P x) ∧ (P y)) ⇒ (R x y ⇐⇒ (x < y)))))

Lemma: bool-tt-or-ff
∀b:𝔹. (b = tt ∨ b = ff)

Lemma: the-first-event
∀es:EO. ∀e:E.  ∃x:E. (x ≤loc e  ∧ (↑first(x)))

Definition: first-event
first-event{i:l}(es;e) ==  es-init(es;e)

Lemma: first-event_wf
∀[es:EO]. ∀[e:E].  (first-event{i:l}(es;e) ∈ E)

Lemma: first-event-property
∀es:EO. ∀e:E.  (first-event{i:l}(es;e) ≤loc e  ∧ (↑first(first-event{i:l}(es;e))))

Lemma: max-of-intset
∀[P:ℕ ⟶ ℙ]
  ((∀n:ℕ. Dec(P[n]))
  ⇒ (∀n:ℕ. ((∀y:ℕ. ¬P[y] supposing y ≤ n) ∨ (∃y:ℕ. ((y ≤ n) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ n)))))))

Lemma: combine-antecedent-surjections
∀es:EO
  ∀[A,B,P,Q:E ⟶ ℙ].
    ((∀e:E. Dec(P e))
       ⇒ (∀e:E. Dec(A e))
       ⇒ (∀e:E. Dec(B e))
       ⇒ (∀f:{e:E| A e}  ⟶ {e:E| P e} . ∀g:{e:E| B e}  ⟶ {e:E| Q e} .
             (P ←⟵ f── A
             ⇒ Q ←⟵ g── B
             ⇒ (∃h:{e:E| (A e) ∨ (B e)}  ⟶ {e:E| (P e) ∨ (Q e)} 
                  (λe.((P e) ∨ (Q e)) ←⟵ h── λe.((A e) ∨ (B e))
                  ∧ (∀e:{e:E| (A e) ∨ (B e)} . ((A e) ⇒ ((h e) = (f e) ∈ E)))
                  ∧ (∀e:{e:E| (A e) ∨ (B e)} . (h e) = (g e) ∈ E supposing ¬(A e))))))) supposing 
       ((∀e:E. (¬((P e) ∧ (Q e)))) and 
       (∀e:E. (¬((A e) ∧ (B e)))))

Definition: es-quiet-until
es-quiet-until(es;i;e.P[e]) ==
  ∃e:E. ((loc(e) = i ∈ Id) ∧ (∀e':E. ((¬(loc(e') = i ∈ Id)) ⇒ (e < e') ⇒ (∃e'':E. ((e'' < e') ∧ P[e''])))))

Lemma: es-quiet-until_wf
∀[es:EO]. ∀[i:Id]. ∀[P:E ⟶ ℙ].  (es-quiet-until(es;i;e.P[e]) ∈ ℙ)

Lemma: es-locl-test
∀es:EO. ∀e1,e2:E.  ((e1 <loc e2) ⇒ (e2 <loc e1) ⇒ False)

Lemma: es-locl-test2
∀es:EO. ∀e1,e2,e3:E.  ((e1 <loc e2) ⇒ (e2 <loc e3) ⇒ (e1 <loc e3))

Lemma: es-causl-test
∀es:EO. ∀e1,e2,e3:E.  ((e1 < e2) ⇒ (e2 < e3) ⇒ (e1 < e3))

Lemma: test-es-first-reasoning
∀es:EO. ∀e1,e2:E.  (e1 ≤loc e2  ⇒ (¬↑first(e1)) ⇒ (¬↑first(e2)))

Lemma: assert-es-first-locl
∀[es:EO]. ∀[e:E].  uiff(↑first(e);∀[e':E]. ¬(e' <loc e) supposing loc(e') = loc(e) ∈ Id)



Home Index