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}() ⊆eo_record{j:l} supposing Type ⊆r 𝕌{j}

Definition: eo-record-type
eo-record-type{i:l}(r) ==
  λx.if =a "E" then Type
     if =a "dom" then r."E" ─→ 𝔹
     if =a "<then r."E" ─→ r."E" ─→ ℙ
     if =a "locless" then r."E" ─→ r."E" ─→ 𝔹
     if =a "loc" then r."E" ─→ Id
     if =a "pred" then r."E" ─→ r."E"
     if =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".  ((↓r."<y)  r."rank" x < r."rank" y))
  ∧ (∀e:r."E". ((r."loc" (r."pred" e)) (r."loc" e) ∈ Id))
  ∧ (∀e:r."E". (¬↓r."<(r."pred" e)))
  ∧ (∀e,x:r."E".
       ((↓r."<e)  ((r."loc" x) (r."loc" e) ∈ Id)  ((↓(r."pred" e) r."<e) ∧ (¬↓(r."pred" e) r."<x))))
  ∧ (∀x,y,z:r."E".  ((↓r."<y)  (↓r."<z)  (↓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 ⊆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.  ((↓y)  rank x < rank y))
  ∧ (∀e:E. ((l (pred e)) (l e) ∈ Id))
  ∧ (∀e:E. (¬↓(pred e)))
  ∧ (∀e,x:E.  ((↓e)  ((l x) (l e) ∈ Id)  ((↓(pred e) e) ∧ (¬↓(pred e) x))))
  ∧ (∀x,y,z:E.  ((↓y)  (↓z)  (↓z)))
  ∧ (∀e1,e2:E.
       (↓e1 e2 ⇐⇒ ↑(e1 locless e2)) ∧ ((¬↓e1 e2)  (¬↓e2 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: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') ==  ↓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' ==  es-eq(es) 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')

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

Lemma: assert-es-eq-E-2
[the_es:EO]. ∀[e,e':E].  uiff(↑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 pred1(e) in if es-dom(es) then if es-eq(es) then else es-pred 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 ∨bb(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) ∈ 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 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 else fi  e ∈ supposing e ≤loc 

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' TERMOF{decidable__es-E-equal:o, 1:l, 1:l} es e' e)

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

Lemma: event_system-level-subtype
EO ⊆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
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 )

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 )

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

Lemma: es-le_weakening_eq
es:EO. ∀a,b:E.  a ≤loc b  supposing 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 )

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)  c≤  (a < c))

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

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

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

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

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

Lemma: es-causle_weakening_locl
es:EO. ∀a,b:E.  (a ≤loc b   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 ≤loc c   (c < d)  c≤  c≤  (a < f))

Lemma: es-le-causle
es:EO. ∀e,e':E.  (e ≤loc 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 )

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 ⊆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≤ and 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 

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. c≤ x)  retraction(T;f)) supposing strong-subtype(T;E)

Lemma: es-causle-retraction-squash
es:EO. ∀[T:Type]. ∀f:T ─→ T. ((∀x:T. 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. c≤ supposing strong-subtype(T;E)

Lemma: es-fix-cases
[es,f,e:Top].  (f**(e) if then 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'  ⇐⇒ 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].  pred(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 ))))

Definition: es-last-event
es-last-event(es;P;e) ==
  fix((λes-last-event,e. if then inl 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 }  ─→ 𝔹].
  (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. i ≤loc k  supposing ∀i,j:ℕn.  (loc(f i) loc(f j) ∈ Id)

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

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 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 }  ─→ (T Top)].  (es-search-back(es;x.f[x];e) ∈ Top)

Lemma: es-search-back-cases
[es:EO]. ∀[e:E]. ∀[f:{e':E| e' ≤loc }  ─→ (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) ∈ 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 )

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

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

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

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 )

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'] ∈ 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') ∈ 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') ∈ 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 )

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 ∈ 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

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 )

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 )

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 then [e'] else [] fi  (e', e) [e]) ∈ (E List) supposing e' ≤loc 

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

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 )

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 }  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 ∈ 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].  before(x) ∈ (E List) supposing [x] ≤ ≤loc(e)

Lemma: iseg-es-before-is-before
[es:EO]. ∀[e,x:E]. ∀[L:E List].  before(x) ∈ (E List) supposing [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 }  ─→ 𝔹].
  (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) 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') ∈ 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 }  ─→ (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 }  ─→ (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
<>==  λ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
 ==  λe.((P e)  (Q e))

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

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

Lemma: es-not_wf
[es:EO]. ∀[P:E ─→ ℙ].  P ∈ E ─→ ℙ)

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

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

Definition: es-equiv
P ≡ ==  ∀e:E. (P ⇐⇒ 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
is first@ 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@ 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@ 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@ 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@ s.t.  e.P[e] and e1 is first@ 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@ 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@ s.t.  e.P[e]
       {∀[Q:{e:E| loc(e) i ∈ Id}  ─→ ℙ]
            (e is first@ s.t.  e.Q[e] ⇐⇒ Q[e] ∧ ∀e'<e.e' is first@ 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 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')  (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))  (∀[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 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).¬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].¬first e ≥ e1.p[e];∀e∈[e1,e2].¬p[e])

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

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

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) ∧ (m 1) ≤loc e2 )
    ∧ ((∀i:ℕ1. (f i <loc (i 1))) ∧ (∀i:ℕ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) <||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 mu(λn.(p <n ∨bK ≤n ∨bfst((f n)) =a1 x)) in
      if p <n ∨bK ≤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 <ptr(tab) ∧b n <||tab|| ) ∧b st-atom(tab;n) =a1 a
   inr(a) =>
   case k2 of inl(n) => (n <ptr(tab) ∧b n <||tab|| ) ∧b st-atom(tab;n) =a1 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, 1, if p <then f[p:=<fst((f p)), keyv>else 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 of inl(y) => [y] inr(y) => []

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

Definition: es-seq
es-seq(es;S) ==  ∀e1,e2:E.  (e1 before e2 ∈  (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 rcv(l,tg) then inl 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 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 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 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 s)
          (H accumulate (with value sofar and list item x): 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')))

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')))

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) 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) a)))

Definition: threshold_accum
threshold_accum(test;
nxt;
step;
g) ==
  λp,x. if test (fst(p)) 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 in case of inl(x) => {<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 of inl(xy) => if oob-hasleft(xy) then inl oob-getleft(xy) else ff fi  inr(_) => ff
             if (i =z 1)
               then case of inl(xy) => if oob-hasright(xy) then inl oob-getright(xy) else ff fi  inr(_) => ff
             else (i 1)
             fi 
         p)

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

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

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

Definition: collect_accm
collect_accm(v.P[v];v.num[v]) ==
  λs,v. eval num[v] in
        let i,vs,w in 
        if n <then <i, vs, inr 0 >
        if i <then if P[[v]] then <1, [], inl [v]> else <n, [v], inr 0 > fi 
        if P[vs [v]] then <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 num[v] in
        let i,a,w in 
        if n <then <i, a, inr 0 >
        if i <then if P[f[init; v]] then <1, init, inl f[init; v]> else <n, f[init; v], inr 0 > fi 
        if P[f[a; v]] then <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 num[v] in
        eval vok P[v] in
          let i,m,b,w 
          in if n <then <i, m, b, inr 0 >
             if vok
               then if i <n
                    then if (1 =z size) then <1, 0, f[base; v], inl tt> else <n, 1, f[base; v], inr 0 > fi 
                    else eval m' in
                         if (m' =z size) then <1, 0, f[base; v], inl tt> else <i, m', f[b; v], inr 0 > fi 
                    fi 
             if i <then <1, 0, f[base; v], inl ff>
             else <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 s))

Lemma: es-fset-at_wf
[es:EO]. ∀[i:Id]. ∀[s:fset(E)].  (s@i ∈ 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' ∈  (e <loc e'))))}  supposing i ∈ locs(s)

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

Lemma: conditional_wf
[T,V:Type]. ∀[A:T ─→ ℙ]. ∀[dcd_A:t:T ─→ Dec(A t)]. ∀[f:{t:T| t}  ─→ V]. ∀[g:{t:T| ¬(A t)}  ─→ V].
  ([A? 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]? 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 ∈ (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 then else fi x.(↑(A x))? 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| t}  ─→ V]. ∀[g:{t:T| t}  ─→ V]. ∀[t:{t:T| 
                                                                                                       (A t) ∨ (B t)} ].
  (([A? g] t) (f t) ∈ supposing t ∧ ([A? g] t) (g t) ∈ supposing ¬(A t))

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

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

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

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

Lemma: weak-antecedent-functions-compose
es:EO
  ∀[P,Q,R:E ─→ ℙ].
    ∀f:{e:E| e}  ─→ {e:E| e} . ∀g:{e:E| e}  ─→ {e:E| e} .  ((Q ←==f== P ∧ R ←==g== Q)  R ←==g 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? g]== λe.((P1 e) ∨ (P2 e)))

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

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

Lemma: weak-antecedent-surjection-property
[es:EO]. ∀[P,Q:E ─→ ℙ]. ∀[f:{e:E| e}  ─→ E].  f ∈ {e:E| e}  ─→ {e:E| 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| e}  ─→ {e:E| e} . ∀g:{e:E| e}  ─→ {e:E| e} .  ((Q ←←f== P ∧ R ←←g== Q)  R ←←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? 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? g]== P1 ∨ P2 
      supposing ∀e:E. ((P1 e)  (P2 e)))

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

Lemma: Q-R-pre-preserving_wf
[es:EO]. ∀[P:E ─→ ℙ]. ∀[Q,R:E ─→ E ─→ ℙ]. ∀[f:{e:E| 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  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  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 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| e}  ─→ E].
  (Inj({e:E| e} ;E;f)) supposing (f is Q-R-pre-preserving on and AntiSym(E;e,e'.R e') and Refl(E;e,e'.Q 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
is R-pre-preserving on ==  is R-R-pre-preserving on P

Lemma: rel-pre-preserving_wf
[es:EO]. ∀[P:E ─→ ℙ]. ∀[R:E ─→ E ─→ ℙ]. ∀[f:{e:E| 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| e}  ─→ {e:E| e} . ∀f2:{e:E| e}  ─→ E.
      ((f1 is R-pre-preserving on P ∧ f2 is R-pre-preserving on Q)  f2 f1 is R-pre-preserving on P)

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

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

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

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

Lemma: inject-composes
[A,B0,B1,C:Type]. ∀[f:A ─→ B0]. ∀[g:B1 ─→ C].
  (Inj(A;C;g 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≤  (∀j:Id. ((¬(j i ∈ Id))  ∀y@j.¬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 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≤  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 then else 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 then else 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@ 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── ==  ∀e:{e:E| e} ((f e < e) ∧ (Q (f e)))

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

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

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

Lemma: antecedent-surjection_wf
[es:EO]. ∀[P,Q:E ─→ ℙ]. ∀[f:{e:E| e}  ─→ {e:E| 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 ⇐⇒ P2 e))  (∀e:E. (Q1 ⇐⇒ 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) 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 w))

Definition: es-p-locl
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
p≤ 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<  p<  p< c)

Lemma: es-p-le_transitivity
es:EO. ∀p:E ─→ (E Top). ∀a,b,c:E.  (a p≤  p≤  p≤ c)

Lemma: es-p-le_weakening
es:EO. ∀p:E ─→ (E Top). ∀e,e':E.  (e p< e'  p≤ e')

Lemma: es-p-le_weakening_eq
es:EO. ∀p:E ─→ (E Top). ∀e,e':E.  p≤ e' supposing e' ∈ E

Lemma: es-p-locl_transitivity1
es:EO. ∀p:E ─→ (E Top). ∀a,b,c:E.  (a p<  p≤  p< c)

Lemma: es-p-locl_transitivity2
es:EO. ∀p:E ─→ (E Top). ∀a,b,c:E.  (a p≤  p<  p< c)

Lemma: es-p-locl-test
es:EO. ∀p:E ─→ (E Top). ∀a,b,c,d,e:E.  (c p≤  p≤  p≤  p<  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'  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≤  p≤ e'  e' p<  (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' ∈ 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< 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 y)
   => Q
      (∀x,y:T.  (((P x) ∧ (P y))  (((R y) ∨ (x y ∈ T)) ∨ (R x))))
      (∀x,y:T.  (((P x) ∧ (P y))  (R ⇐⇒ y))) 
     supposing ∀x,y:T.  ((Q y)  (Q 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 y) ∨ (x y ∈ E)) ∨ (R x))))
     (∀x,y:E.  (((P x) ∧ (P y))  (R ⇐⇒ (x < y)))))

Lemma: bool-tt-or-ff
b:𝔹(b tt ∨ 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| e}  ─→ {e:E| e} . ∀g:{e:E| e}  ─→ {e:E| 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) ∈ 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