---

Lemma: base-noloc-classrel
∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:T]. ∀[hdr:Name].
  uiff(v ∈ Base(hdr)(e);(header(e) = hdr ∈ Name) ∧ has-es-info-type(es;e;f;T) ∧ (v = msgval(e) ∈ T)) 
  supposing hdr encodes T

Lemma: base-noloc-classrel2
∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:T]. ∀[hdr:Name].
  uiff(v ∈ Base(hdr)(e);(header(e) = hdr ∈ Name) ∧ (v = msgval(e) ∈ T)) supposing hdr encodes T

Lemma: base-classrel-equal
∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:T]. ∀[hdr:Name].
  uiff(v ∈ Base(hdr)(e);(header(e) = hdr ∈ Name) ∧ v = body(e)) supposing hdr encodes T

Lemma: eclass0-base-classrel
∀[T,C:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:C]. ∀[hdr:Name]. ∀[g:Id ⟶ T ⟶ bag(C)].
  uiff(v ∈ (g o Base(hdr))(e);(header(e) = hdr ∈ Name) ∧ has-es-info-type(es;e;f;T) ∧ v ↓∈ g loc(e) msgval(e)) 
  supposing hdr encodes T

Lemma: eclass1-base-classrel
∀[T,C:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:C]. ∀[hdr:Name]. ∀[g:Id ⟶ T ⟶ C].
  uiff(v ∈ (g o Base(hdr))(e);(header(e) = hdr ∈ Name) ∧ has-es-info-type(es;e;f;T) ∧ (v = (g loc(e) msgval(e)) ∈ C)) 
  supposing hdr encodes T

Lemma: base-noloc-classrel-make-Msg
∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
  uiff(v ∈ Base(hdr)(e);info(e) = mk-msg(msg-authentic(info(e));hdr;v) ∈ Message(f))

Lemma: base-noloc-classrel-make-Msg2
∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:T].
  uiff(v ∈ Base(hdr)(e);info(e) = mk-msg(msg-authentic(info(e));hdr;v) ∈ Message(f)) supposing T = (f hdr) ∈ Type

Lemma: verify-classrel
∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:T]. ∀[hdr:Name].
  uiff(v ∈ Verify(hdr)(e);(↑es-info-auth(es;e)) ∧ (header(e) = hdr ∈ Name) ∧ v = body(e)) supposing hdr encodes T

Lemma: return-loc-bag-class-classrel
∀[Info,A:Type]. ∀[x:Id ⟶ bag(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].
  (v ∈ return-loc-bag-class(x)(e) ⇐⇒ v ↓∈ x loc(e) ∧ (↑first(e)))

Lemma: parallel-bag-classrel
∀[B,Info,T:Type]. ∀[X:T ⟶ EClass(B)]. ∀[as:bag(T)]. ∀[v:B]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(v ∈ (||a∈as.X[a])(e);↓∃a:T. (a ↓∈ as ∧ v ∈ X[a](e)))

Lemma: local-simulation-classrel
∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)].
  ∀locs:bag(Id). ∀hdr:Name.
    ∀es:EO+(Message(f)). ∀e:E.
      ∀[v:T]
        uiff(v ∈ local-simulation-class(X;locs;hdr)(e);(↑has-header-and-in-locs(info(e);hdr;locs))
        ∧ v ∈ X(local-simulation-event(es;e;hdr;locs))) 
      supposing LocalClass(X) 
    supposing hdr encodes Id × Info

Lemma: local-simulation-msg-constraint
∀[f,g:Name ⟶ Type]. ∀[X:EClass(Interface)].
  ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
    ∀[hdrs:Name List]. ∀[i:Id].
      (local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)
      ⇒ (∀e:E. ((loc(e) = i ∈ Id) ⇒ eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g)))) 
    supposing hdr encodes Id × Message(g) 
  supposing LocalClass(X)

Lemma: consistent-local-simulation
∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀es:EO+(Message(f)). ∀ee:E List.
          ((∀e1,e2∈ee.  local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))
          ⇒ (∀hdrs:Name List
                ((∀e∈ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
                ⇒ (∃eo:EO+(Message(g))
                     (eo-msg-interface-constraint(eo;X;hdrs;g)
                     ∧ (∀e∈ee.∀[v:Interface]
                                (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e')) 
                                supposing v ∈ local-simulation-class(X;locs;hdr)(e))))))) 
        supposing hdr encodes Id × Message(g)))

Lemma: local-simulation-agreement
∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀R:Interface ⟶ Interface ⟶ ℙ. ∀es:EO+(Message(f)).
          ((∀i,j:Id.  ((correct i) ⇒ (correct j) ⇒ local-simulation-input-consistency(g;X;hdr;locs;es;i;j)))
          ⇒ (∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀eo:EO+(Message(g)). (eo-msg-interface-constraint(eo;X;hdrs;g) ⇒ any v1,v2 from X satisfy R[v1;v2]))
          ⇒ any v1,v2 from local-simulation-class(X;locs;hdr) satisfy
             R[v1;v2]
             at locations i.correct i) 
        supposing hdr encodes Id × Message(g)))

Lemma: local-simulation-validity
∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀es:EO+(Message(f)).
          ((∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀P:Interface ⟶ ℙ. ∀R:Interface ⟶ Message(g) ⟶ ℙ.
                ((∀eo:EO+(Message(g))
                    (eo-msg-interface-constraint(eo;X;hdrs;g)
                    ⇒ (∀e:E. ∀v:Interface.  (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')]))))))
                ⇒ (∀e:E. ∀v:Interface.
                      ((correct loc(e))
                      ⇒ v ∈ local-simulation-class(X;locs;hdr)(e)
                      ⇒ P[v]
                      ⇒ (↓∃e':E
                            ((e' <loc e)
                            ∧ (↑has-header-and-in-locs(info(e');hdr;locs))
                            ∧ R[v;snd(msg-body(info(e')))]))))))) 
        supposing hdr encodes Id × Message(g)))

Lemma: local-simulation-validity2
∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀es:EO+(Message(f)).
          ((∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀R:Interface ⟶ Message(g) ⟶ ℙ. ∀R':Interface ⟶ Message(f) ⟶ ℙ.
                ((∀eo:EO+(Message(g))
                    (eo-msg-interface-constraint(eo;X;hdrs;g)
                    ⇒ for every v in X there is an
                       earlier event  with info=m such that
                       R[v;m]))
                ⇒ (∀e:E. ∀v:Interface.
                      ((correct loc(e))
                      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
                      ⇒ R[v;snd(msg-body(info(e)))]
                      ⇒ (↓∃e':E. ((e' < e) ∧ R'[v;info(e')]))))
                ⇒ for every v in local-simulation-class(X;locs;hdr) at location i s.t. correct i
                   there is an earlier event with info=m  such that R'[v;m]))) 
        supposing hdr encodes Id × Message(g)))

Definition: disjoint-union-tr
tr1 + tr2 ==  λl,a,s. if isl(a) then tr1 l outl(a) s else tr2 l outr(a) s fi 

Lemma: disjoint-union-tr_wf
∀[A,B,S:Type]. ∀[tr1:Id ⟶ A ⟶ S ⟶ S]. ∀[tr2:Id ⟶ B ⟶ S ⟶ S].  (tr1 + tr2 ∈ Id ⟶ (A + B) ⟶ S ⟶ S)

Definition: lifting-loc-gen-rev
lifting-loc-gen-rev(n;bags;loc;f) ==  lifting-gen-rev(n;f loc;bags)

Lemma: lifting-loc-gen-rev_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[loc:Id]. ∀[f:Id ⟶ funtype(n;A;B)].
  (lifting-loc-gen-rev(n;bags;loc;f) ∈ bag(B))

Definition: lifting-loc-gen
lifting-loc-gen(n;f) ==  λl,bags. lifting-loc-gen-rev(n;bags;l;f)

Lemma: lifting-loc-gen_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:Id ⟶ funtype(n;A;B)].
  (lifting-loc-gen(n;f) ∈ Id ⟶ (k:ℕn ⟶ bag(A k)) ⟶ bag(B))

Definition: lifting1-loc
lifting1-loc(f;loc;b) ==  lifting-loc-gen-rev(1;λx.b;loc;f)

Lemma: lifting1-loc_wf
∀[A,B:Type]. ∀[f:Id ⟶ A ⟶ B]. ∀[loc:Id]. ∀[b:bag(A)].  (lifting1-loc(f;loc;b) ∈ bag(B))

Definition: lifting2-loc
lifting2-loc(f;loc;abag;bbag) ==  lifting-loc-gen-rev(2;λn.[abag; bbag][n];loc;f)

Lemma: lifting2-loc_wf
∀[A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[loc:Id]. ∀[abag:bag(A)]. ∀[bbag:bag(B)].
  (lifting2-loc(f;loc;abag;bbag) ∈ bag(C))

Definition: lifting-loc-0
lifting-loc-0(f) ==  λl.lifting-loc-gen-rev(0;λn.[][n];l;f)

Lemma: lifting-loc-0_wf
∀[B:Type]. ∀[f:Id ⟶ B].  (lifting-loc-0(f) ∈ Id ⟶ bag(B))

Definition: lifting-loc-1
lifting-loc-1(f) ==  λl,b. lifting1-loc(f;l;b)

Lemma: lifting-loc-1_wf
∀[B,A:Type]. ∀[f:Id ⟶ A ⟶ B].  (lifting-loc-1(f) ∈ Id ⟶ bag(A) ⟶ bag(B))

Definition: lifting-loc-2
lifting-loc-2(f) ==  λl,a,b. lifting2-loc(f;l;a;b)

Lemma: lifting-loc-2_wf
∀[C,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C].  (lifting-loc-2(f) ∈ Id ⟶ bag(A) ⟶ bag(B) ⟶ bag(C))

Lemma: bag-member-lifting-loc-2
∀[C,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[i:Id]. ∀[c:C].
  uiff(c ↓∈ lifting-loc-2(f) i as bs;↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c = (f i a b) ∈ C)))

Definition: lifting-loc-3
lifting-loc-3(f) ==  λl,a,b,c. lifting-loc-gen-rev(3;λn.[a; b; c][n];l;f)

Lemma: lifting-loc-3_wf
∀[A,B,C,D:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C ⟶ D].  (lifting-loc-3(f) ∈ Id ⟶ bag(A) ⟶ bag(B) ⟶ bag(C) ⟶ bag(D))

Lemma: lifting-loc-member-simple
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:Id ⟶ funtype(n;A;B)]. ∀[b:B]. ∀[l:Id].
  (b ↓∈ lifting-loc-gen-rev(n;bags;l;f)
  ⇐⇒ ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ ((uncurry-rev(n;f l) lst) = b ∈ B)))

Definition: concat-lifting-loc
concat-lifting-loc(n;bags;loc;f) ==  concat-lifting(n;f loc;bags)

Lemma: concat-lifting-loc_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[loc:Id]. ∀[f:Id ⟶ funtype(n;A;bag(B))].
  (concat-lifting-loc(n;bags;loc;f) ∈ bag(B))

Lemma: concat-lifting-loc-member
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:Id ⟶ funtype(n;A;bag(B))]. ∀[b:B]. ∀[l:Id].
  (b ↓∈ concat-lifting-loc(n;bags;l;f)
  ⇐⇒ ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-rev(n;f l) lst))

Definition: concat-lifting-loc-gen
concat-lifting-loc-gen(n;f) ==  λl,bags. concat-lifting-loc(n;bags;l;f)

Lemma: concat-lifting-loc-gen_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:Id ⟶ funtype(n;A;bag(B))].
  (concat-lifting-loc-gen(n;f) ∈ Id ⟶ (k:ℕn ⟶ bag(A k)) ⟶ bag(B))

Definition: concat-lifting1-loc
concat-lifting1-loc(f;bag;loc) ==  concat-lifting-loc(1;λx.bag;loc;f)

Lemma: concat-lifting1-loc_wf
∀[A,B:Type]. ∀[f:Id ⟶ A ⟶ bag(B)]. ∀[b:bag(A)]. ∀[l:Id].  (concat-lifting1-loc(f;b;l) ∈ bag(B))

Definition: concat-lifting2-loc
concat-lifting2-loc(f;abag;bbag;loc) ==  concat-lifting-loc(2;λn.[abag; bbag][n];loc;f)

Lemma: concat-lifting2-loc_wf
∀[A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[abag:bag(A)]. ∀[bbag:bag(B)]. ∀[l:Id].
  (concat-lifting2-loc(f;abag;bbag;l) ∈ bag(C))

Definition: concat-lifting-loc-0
concat-lifting-loc-0(f) ==  λl.concat-lifting-loc(0;λn.[][n];l;f)

Lemma: concat-lifting-loc-0_wf
∀[B:Type]. ∀[f:Id ⟶ bag(B)].  (concat-lifting-loc-0(f) ∈ Id ⟶ bag(B))

Definition: concat-lifting-loc-1
f@ ==  λl,b. concat-lifting1-loc(f;b;l)

Lemma: concat-lifting-loc-1_wf
∀[B,A:Type]. ∀[f:Id ⟶ A ⟶ bag(B)].  (f@ ∈ Id ⟶ bag(A) ⟶ bag(B))

Lemma: concat-lifting-loc-1-strict
∀[f,i:Top].  (f@ i {} ~ {})

Definition: concat-lifting-loc-2
f@Loc ==  λl,a,b. concat-lifting2-loc(f;a;b;l)

Lemma: concat-lifting-loc-2_wf
∀[C,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)].  (f@Loc ∈ Id ⟶ bag(A) ⟶ bag(B) ⟶ bag(C))

Lemma: concat-lifting-loc-2-strict
∀[f:Top]. ∀[b:bag(Top)]. ∀[i:Top].  ((f@Loc i {} b ~ {}) ∧ (f@Loc i b {} ~ {}))

Definition: concat-lifting-loc-3
concat-lifting-loc-3(f) ==  λl,a,b,c. concat-lifting-loc(3;λn.[a; b; c][n];l;f)

Lemma: concat-lifting-loc-3_wf
∀[A,B,C,D:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C ⟶ bag(D)].
  (concat-lifting-loc-3(f) ∈ Id ⟶ bag(A) ⟶ bag(B) ⟶ bag(C) ⟶ bag(D))

Lemma: concat-lifting-loc-3-strict
∀[f,i:Top]. ∀[b,b':bag(Top)].
  ((concat-lifting-loc-3(f) i {} b b' ~ {})
  ∧ (concat-lifting-loc-3(f) i b {} b' ~ {})
  ∧ (concat-lifting-loc-3(f) i b b' {} ~ {}))

Lemma: class-opt-class-classrel
∀[Info,T:Type]. ∀[X,Y:EClass(T)]. ∀[v:T]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(v ∈ X?Y(e);↓((↑bag-null(X es e)) ∧ v ∈ Y(e)) ∨ ((¬↑bag-null(X es e)) ∧ v ∈ X(e)))

Lemma: class-opt-class-classrel2
∀[Info,T:Type]. ∀[X,Y:EClass(T)]. ∀[v:T]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(v ∈ X?Y(e);((↑bag-null(X es e)) ⇒ v ∈ Y(e)) ∧ ((¬↑bag-null(X es e)) ⇒ v ∈ X(e)))

Lemma: primed-class-opt-single-val0
∀[Info,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(B)]. ∀[init:Id ⟶ bag(B)].
  ∀e:E. ∀v1,v2:B.
    (single-valued-bag(init loc(e);B)
    ⇒ single-valued-classrel(es;X;B)
    ⇒ v1 ∈ Prior(X)?init(e)
    ⇒ v2 ∈ Prior(X)?init(e)
    ⇒ (v1 = v2 ∈ B))

Lemma: primed-class-opt-single-val
∀[Info,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(B)]. ∀[init:Id ⟶ bag(B)].
  ((∀l:Id. single-valued-bag(init l;B)) ⇒ single-valued-classrel(es;X;B) ⇒ single-valued-classrel(es;Prior(X)?init;B))

Lemma: primed-class-opt-es-sv0
∀[Info,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(B)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E].
  ((#(init loc(e)) ≤ 1) ⇒ (∀e':E. ((e' <loc e) ⇒ (#(X es e') ≤ 1))) ⇒ (#(Prior(X)?init es e) ≤ 1))

Lemma: primed-class-opt-es-sv
∀[Info,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(B)]. ∀[init:Id ⟶ bag(B)].
  ((∀l:Id. (#(init l) ≤ 1)) ⇒ es-sv-class(es;X) ⇒ es-sv-class(es;Prior(X)?init))

Lemma: on-loc-classrel
∀[Info,T:Type]. ∀[X:Id ⟶ EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].  (v ∈ on-loc-class(X)(e) ⇐⇒ v ∈ X loc(e)(e))

Lemma: simple-loc-comb1-classrel
∀[Info,B,C:Type]. ∀[f:Id ⟶ B ⟶ C]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ simple-loc-comb1(l,a.lifting1-loc(f;l;a);X)(e);↓∃b:B. (b ∈ X(e) ∧ (v = (f loc(e) b) ∈ C)))

Lemma: simple-loc-comb-1-classrel
∀[Info,B,C:Type]. ∀[f:Id ⟶ B ⟶ C]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ lifting-loc-1(f)(Loc, X)(e);↓∃b:B. (b ∈ X(e) ∧ (v = (f loc(e) b) ∈ C)))

Lemma: simple-loc-comb-1-classrel-weak
∀[Info,B,C:Type]. ∀[f:Id ⟶ B ⟶ C]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  (v ∈ lifting-loc-1(f)(Loc, X)(e) ⇐⇒ ↓∃b:B. (b ∈ X(e) ∧ (v = (f loc(e) b) ∈ C)))

Lemma: simple-loc-comb2-classrel
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ simple-loc-comb2(l,a,b.lifting2-loc(f;l;a;b);X;Y)(e);↓∃a:A
                                                                  ∃b:B
                                                                   (a ∈ X(e) ∧ b ∈ Y(e) ∧ (v = (f loc(e) a b) ∈ C)))

Lemma: simple-loc-comb-2-classrel
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ lifting-loc-2(f) o (Loc,X, Y)(e);↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ (v = (f loc(e) a b) ∈ C)))

Lemma: simple-loc-comb-2-classrel-weak
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  (v ∈ lifting-loc-2(f) o (Loc,X, Y)(e) ⇐⇒ ↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ (v = (f loc(e) a b) ∈ C)))

Lemma: simple-loc-comb-2-loc-bounded
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  ((LocBounded(A;X) ∨ LocBounded(B;Y)) ⇒ LocBounded(C;lifting-loc-2(f) o (Loc,X, Y)))

Lemma: simple-loc-comb-2-loc-bounded2
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (LocBounded(A;X) ⇒ LocBounded(C;lifting-loc-2(f) o (Loc,X, Y)))

Lemma: simple-loc-comb-2-loc-bounded3
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (LocBounded(B;Y) ⇒ LocBounded(C;lifting-loc-2(f) o (Loc,X, Y)))

Lemma: simple-loc-comb-concat-classrel
∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[Xs:k:ℕn ⟶ EClass(A k)]. ∀[f:Id ⟶ (k:ℕn ⟶ (A k)) ⟶ bag(B)].
∀[F:Id ⟶ (k:ℕn ⟶ bag(A k)) ⟶ bag(B)].
  ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
    uiff(v ∈ F|Loc; Xs|(e);↓∃vs:k:ℕn ⟶ (A k). ((∀k:ℕn. vs[k] ∈ Xs[k](e)) ∧ v ↓∈ f loc(e) vs)) 
  supposing ∀x:Id. ∀v:B. ∀bs:k:ℕn ⟶ bag(A k).
              (v ↓∈ F x bs ⇐⇒ ↓∃vs:k:ℕn ⟶ (A k). ((∀k:ℕn. vs k ↓∈ bs k) ∧ v ↓∈ f x vs))

Lemma: simple-comb-concat-classrel
∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[Xs:k:ℕn ⟶ EClass(A k)]. ∀[f:(k:ℕn ⟶ (A k)) ⟶ bag(B)].
∀[F:(k:ℕn ⟶ bag(A k)) ⟶ bag(B)].
  ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
    uiff(v ∈ simple-comb(F;Xs)(e);↓∃vs:k:ℕn ⟶ (A k). ((∀k:ℕn. vs[k] ∈ Xs[k](e)) ∧ v ↓∈ f vs)) 
  supposing ∀v:B. ∀bs:k:ℕn ⟶ bag(A k).  (v ↓∈ F bs ⇐⇒ ↓∃vs:k:ℕn ⟶ (A k). ((∀k:ℕn. vs k ↓∈ bs k) ∧ v ↓∈ f vs))

Lemma: simple-comb-classrel
∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[Xs:k:ℕn ⟶ EClass(A k)]. ∀[f:(k:ℕn ⟶ (A k)) ⟶ B].
∀[F:(k:ℕn ⟶ bag(A k)) ⟶ bag(B)].
  ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
    uiff(v ∈ simple-comb(F;Xs)(e);↓∃vs:k:ℕn ⟶ (A k). ((∀k:ℕn. vs[k] ∈ Xs[k](e)) ∧ (v = (f vs) ∈ B))) 
  supposing ∀v:B. ∀bs:k:ℕn ⟶ bag(A k).  (v ↓∈ F bs ⇐⇒ ↓∃vs:k:ℕn ⟶ (A k). ((∀k:ℕn. vs k ↓∈ bs k) ∧ (v = (f vs) ∈ B)))

Lemma: simple-loc-comb2-concat-classrel
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ simple-loc-comb2(l,a,b.concat-lifting2-loc(f;a;b;l);X;Y)(e);↓∃a:A
                                                                         ∃b:B
                                                                          (a ∈ X(e) ∧ b ∈ Y(e) ∧ v ↓∈ f loc(e) a b))

Lemma: simple-loc-comb1-concat-classrel
∀[Info,A,B:Type]. ∀[f:Id ⟶ A ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ simple-loc-comb1(l,a.concat-lifting1-loc(f;a;l);X)(e);↓∃a:A. (a ∈ X(e) ∧ v ↓∈ f loc(e) a))

Lemma: simple-comb1-concat-classrel
∀[Info,B,C:Type]. ∀[f:B ⟶ bag(C)]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ λa.concat-lifting1(f;a)|X|(e);↓∃b:B. (b ∈ X(e) ∧ v ↓∈ f b))

Lemma: simple-comb2-concat-classrel
∀[Info,A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ λa,b.concat-lifting2(f;a;b)|X;Y|(e);↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ v ↓∈ f a b))

Lemma: simple-comb1-classrel
∀[Info,B,C:Type]. ∀[f:B ⟶ C]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ λa.lifting1(f;a)|X|(e);↓∃b:B. (b ∈ X(e) ∧ (v = (f b) ∈ C)))

Lemma: simple-comb2-classrel
∀[Info,A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ λa,b.lifting2(f;a;b)|X;Y|(e);↓∃a:A. ∃b:B. ((a ∈ X(e) ∧ b ∈ Y(e)) ∧ (v = (f a b) ∈ C)))

Lemma: simple-loc-comb-2-concat-classrel
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ f@Loc o (Loc,X, Y)(e);↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ v ↓∈ f loc(e) a b))

Lemma: simple-loc-comb-2-concat-classrel-weak
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  (v ∈ f@Loc o (Loc,X, Y)(e) ⇐⇒ ↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ v ↓∈ f loc(e) a b))

Lemma: simple-loc-comb-1-concat-classrel
∀[Info,A,B:Type]. ∀[f:Id ⟶ A ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ f@(Loc, X)(e);↓∃a:A. (a ∈ X(e) ∧ v ↓∈ f loc(e) a))

Lemma: simple-loc-comb-1-concat-classrel-weak
∀[Info,A,B:Type]. ∀[f:Id ⟶ A ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  (v ∈ f@(Loc, X)(e) ⇐⇒ ↓∃a:A. (a ∈ X(e) ∧ v ↓∈ f loc(e) a))

Lemma: simple-comb-1-concat-classrel
∀[Info,B,C:Type]. ∀[f:B ⟶ bag(C)]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ f@|X|(e);↓∃b:B. (v ↓∈ f b ∧ b ∈ X(e)))

Lemma: simple-comb-1-concat-classrel-weak
∀[Info,B,C:Type]. ∀[f:B ⟶ bag(C)]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  (v ∈ f@|X|(e) ⇐⇒ ↓∃b:B. (v ↓∈ f b ∧ b ∈ X(e)))

Lemma: simple-comb-2-concat-classrel
∀[Info,A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ f@|X, Y|(e);↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ v ↓∈ f a b))

Lemma: simple-comb-2-concat-classrel-weak
∀[Info,A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  (v ∈ f@|X, Y|(e) ⇐⇒ ↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ v ↓∈ f a b))

Lemma: simple-comb-1-classrel
∀[Info,B,C:Type]. ∀[f:B ⟶ C]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ lifting-1(f)|X|(e);↓∃b:B. ((v = (f b) ∈ C) ∧ b ∈ X(e)))

Lemma: simple-comb-1-classrel-weak
∀[Info,B,C:Type]. ∀[f:B ⟶ C]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  (v ∈ lifting-1(f)|X|(e) ⇐⇒ ↓∃b:B. ((v = (f b) ∈ C) ∧ b ∈ X(e)))

Lemma: simple-comb-2-classrel
∀[Info,A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ lifting-2(f)|X, Y|(e);↓∃a:A. ∃b:B. ((v = (f a b) ∈ C) ∧ b ∈ Y(e) ∧ a ∈ X(e)))

Lemma: simple-comb-2-classrel-weak
∀[Info,A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  (v ∈ lifting-2(f)|X, Y|(e) ⇐⇒ ↓∃a:A. ∃b:B. ((v = (f a b) ∈ C) ∧ b ∈ Y(e) ∧ a ∈ X(e)))

Lemma: simple-loc-comb-2-concat-loc-bounded
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  ((LocBounded(A;X) ∨ LocBounded(B;Y)) ⇒ LocBounded(C;f@Loc o (Loc,X, Y)))

Lemma: simple-loc-comb-2-concat-loc-bounded2
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (LocBounded(A;X) ⇒ LocBounded(C;f@Loc o (Loc,X, Y)))

Lemma: simple-loc-comb-2-concat-loc-bounded3
∀[Info,A,B,C:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (LocBounded(B;Y) ⇒ LocBounded(C;f@Loc o (Loc,X, Y)))

Definition: Accum-class
Accum-class(f;init;X) ==  lifting-2(f)|X,Prior(self)?init|

Lemma: Accum-class_wf
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)].  (Accum-class(f;init;X) ∈ EClass(B))

Definition: Accum-loc-class
Accum-loc-class(f;init;X) ==  lifting-loc-2(f)|Loc, X, Prior(self)?init|

Lemma: Accum-loc-class_wf
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)].  (Accum-loc-class(f;init;X) ∈ EClass(B))

Lemma: Accum-loc-class-as-loop-class2
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)].
  (loop-class2((f o X);init) = Accum-loc-class(f;init;X) ∈ EClass(B))

Definition: Memory-class
Memory-class(f;init;X) ==  Prior(Accum-class(f;init;X))?init

Lemma: Memory-class_wf
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)].  (Memory-class(f;init;X) ∈ EClass(B))

Definition: Memory-loc-class
Memory-loc-class(f;init;X) ==  Prior(Accum-loc-class(f;init;X))?init

Lemma: Memory-loc-class_wf
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)].
  (Memory-loc-class(f;init;X) ∈ EClass(B))

Lemma: Accum-class-top
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (Accum-class(f;init;X) ∈ EClass(Top))

Lemma: Memory-class-top
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (Memory-class(f;init;X) ∈ EClass(Top))

Lemma: Accum-classrel-Memory-sq
∀[B,f,init,X,es,e,v:Top].  (v ∈ Accum-class(f;init;X)(e) ~ v ↓∈ lifting-2(f) (X es e) (Memory-class(f;init;X) es e))

Lemma: Accum-loc-classrel-Memory-sq
∀[B,f,init,X,es,e,v:Top].
  (v ∈ Accum-loc-class(f;init;X)(e) ~ v ↓∈ lifting-loc-2(f) loc(e) (X es e) (Memory-loc-class(f;init;X) es e))

Lemma: Accum-classrel-Memory
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  (v ∈ Accum-class(f;init;X)(e) ⇐⇒ ↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Memory-class(f;init;X)(e) ∧ (v = (f a b) ∈ B)))

Lemma: Accum-loc-classrel-Memory
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  (v ∈ Accum-loc-class(f;init;X)(e)
  ⇐⇒ ↓∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Memory-loc-class(f;init;X)(e) ∧ (v = (f loc(e) a b) ∈ B)))

Lemma: Memory-classrel1
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ Memory-class(f;init;X)(e);↓((↑first(e)) ∧ v ↓∈ init loc(e))
                                      ∨ ((¬↑first(e))
                                        ∧ ((∃a:A
                                             (a ∈ X(pred(e))
                                             ∧ (∃b:B. (b ∈ Memory-class(f;init;X)(pred(e)) ∧ (v = (f a b) ∈ B)))))
                                          ∨ ((∀a:A. (¬a ∈ X(pred(e)))) ∧ v ∈ Memory-class(f;init;X)(pred(e))))))

Lemma: Memory-loc-classrel1
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ Memory-loc-class(f;init;X)(e);↓((↑first(e)) ∧ v ↓∈ init loc(e))
                                          ∨ ((¬↑first(e))
                                            ∧ ((∃a:A
                                                 (a ∈ X(pred(e))
                                                 ∧ (∃b:B
                                                     (b ∈ Memory-loc-class(f;init;X)(pred(e))
                                                     ∧ (v = (f loc(e) a b) ∈ B)))))
                                              ∨ ((∀a:A. (¬a ∈ X(pred(e)))) ∧ v ∈ Memory-loc-class(f;init;X)(pred(e))))))

Lemma: iterated-classrel-Memory-classrel
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      uiff(iterated_classrel(es;B;A;f;init;X;e;v);↓(∃a:A
                                                     ∃b:B
                                                      (a ∈ X(e) ∧ b ∈ Memory-class(f;init;X)(e) ∧ (v = (f a b) ∈ B)))
                                                   ∨ ((∀a:A. (¬a ∈ X(e))) ∧ v ∈ Memory-class(f;init;X)(e)))

Lemma: iterated-classrel-Memory-loc-classrel
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      uiff(iterated_classrel(es;B;A;f loc(e);init;X;e;v);↓(∃a:A
                                                            ∃b:B
                                                             (a ∈ X(e)
                                                             ∧ b ∈ Memory-loc-class(f;init;X)(e)
                                                             ∧ (v = (f loc(e) a b) ∈ B)))
                                                          ∨ ((∀a:A. (¬a ∈ X(e))) ∧ v ∈ Memory-loc-class(f;init;X)(e)))

Lemma: Memory-classrel
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      (v ∈ Memory-class(f;init;X)(e)
      ⇐⇒ ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ iterated_classrel(es;B;A;f;init;X;pred(e);v)))

Lemma: Memory-classrel2
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]. (v ∈ Memory-class(f;init;X)(e) ⇐⇒ ↓prior-iterated-classrel(es;A;B;v;X;f;init;e))

Lemma: Memory-loc-classrel
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      (v ∈ Memory-loc-class(f;init;X)(e)
      ⇐⇒ ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ iterated_classrel(es;B;A;f loc(e);init;X;pred(e);v)))

Lemma: Memory-classrel-loc
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ Memory-loc-class(f;init;X)(e);v ∈ Memory-class(f loc(e);init;X)(e))

Lemma: Memory-classrel-single-val
∀[Info,B,A:Type].
  ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (uiff(v ∈ Memory-class(f;init;X)(e);prior-iterated-classrel(es;A;B;v;X;f;init;e))) supposing 
       (single-valued-classrel(es;X;A) and 
       single-valued-bag(init loc(e);B))

Lemma: Memory-loc-classrel-single-val
∀[Info,B,A:Type].
  ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (uiff(v ∈ Memory-loc-class(f;init;X)(e);prior-iterated-classrel(es;A;B;v;X;f loc(e);init;e))) supposing 
       (single-valued-classrel(es;X;A) and 
       single-valued-bag(init loc(e);B))

Lemma: Memory-class-exists
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  ↓∃v:B. v ∈ Memory-class(f;init;X)(e) supposing 0 < #(init loc(e))

Lemma: Memory-loc-class-exists
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  ↓∃v:B. v ∈ Memory-loc-class(f;init;X)(e) supposing 0 < #(init loc(e))

Lemma: Memory-class-total
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:A ⟶ S ⟶ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  es-total-class(es;Memory-class(f;init;X)) supposing ∀l:Id. (1 ≤ #(init l))

Lemma: Memory-loc-class-total
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:Id ⟶ A ⟶ S ⟶ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  es-total-class(es;Memory-loc-class(f;init;X)) supposing ∀l:Id. (1 ≤ #(init l))

Lemma: Memory-class-single-val
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:A ⟶ S ⟶ S]. ∀[X:EClass(A)].
  ∀es:EO+(Info)
    (single-valued-classrel(es;X;A)
    ⇒ (∀l:Id. single-valued-bag(init l;S))
    ⇒ single-valued-classrel(es;Memory-class(f;init;X);S))

Lemma: Memory-class-single-val2
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:A ⟶ S ⟶ S]. ∀[X:EClass(A)].
  ∀es:EO+(Info). ∀e:E. ∀s1,s2:S.
    (single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e);S)
    ⇒ s1 ∈ Memory-class(f;init;X)(e)
    ⇒ s2 ∈ Memory-class(f;init;X)(e)
    ⇒ (s1 = s2 ∈ S))

Lemma: Memory-loc-class-single-val
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:Id ⟶ A ⟶ S ⟶ S]. ∀[X:EClass(A)].
  ∀es:EO+(Info)
    (single-valued-classrel(es;X;A)
    ⇒ (∀l:Id. single-valued-bag(init l;S))
    ⇒ single-valued-classrel(es;Memory-loc-class(f;init;X);S))

Lemma: Memory-class-functional
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:A ⟶ S ⟶ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (Memory-class(f;init;X) is functional) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;S)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: Memory-loc-class-functional
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:Id ⟶ A ⟶ S ⟶ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (Memory-loc-class(f;init;X) is functional) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;S)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: Memory-class-invariant
∀[Info,B,A:Type].
  ∀P:B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    ((∀s:B. SqStable(P[s]))
    ⇒ (∀a:A. ∀e':E.  ((e' <loc e) ⇒ a ∈ X(e') ⇒ (∀s:B. (P[s] ⇒ P[f a s]))))
    ⇒ (∀v:B. (v ↓∈ init loc(e) ⇒ P[v]))
    ⇒ v ∈ Memory-class(f;init;X)(e)
    ⇒ P[v])

Lemma: Memory-class-invariant-sv
∀[Info,B,A:Type].
  ∀P:B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e);B)
    ⇒ (∀a:A. ∀e':E.  ((e' <loc e) ⇒ a ∈ X(e') ⇒ (∀s:B. (P[s] ⇒ P[f a s]))))
    ⇒ (∀v:B. (v ↓∈ init loc(e) ⇒ P[v]))
    ⇒ v ∈ Memory-class(f;init;X)(e)
    ⇒ P[v])

Lemma: Memory-class-invariant-sv1
∀[Info,B,A:Type].
  ∀P:B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e);B)
    ⇒ (∀v:B. (v ↓∈ init loc(e) ⇒ P[v]))
    ⇒ (∀a:A. ∀e':E. ∀s:B.  ((e' <loc e) ⇒ a ∈ X(e') ⇒ s ∈ Memory-class(f;init;X)(e') ⇒ P[s] ⇒ P[f a s]))
    ⇒ v ∈ Memory-class(f;init;X)(e)
    ⇒ P[v])

Lemma: Memory-class-trans
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E.  (a ∈ X(e) ⇒ (∀s:B. R[s;f a s])))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (∃a:A. a ∈ X(e))))
    ⇒ R[v1;v2])

Lemma: Memory-class-trans1
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.  (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-class(f;init;X)(e) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (∃a:A. a ∈ X(e))))
    ⇒ R[v1;v2])

Lemma: Memory-class-trans2
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.  (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-class(f;init;X)(e) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∀e:E. (e1 ≤loc e  ⇒ (e <loc e2) ⇒ (∀a:A. (¬a ∈ X(e)))))
    ⇒ (v1 = v2 ∈ B))

Lemma: Memory-class-trans-refl
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Refl(B;x,y.R[x;y])
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.  (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-class(f;init;X)(e) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-class(f;init;X)(e2)
    ⇒ e1 ≤loc e2 
    ⇒ R[v1;v2])

Lemma: Memory-class-progress
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀P:A ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    ((∀a:A. ∀s:B.  Dec(P[a;s]))
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E. ∀s:B.
          (e1 ≤loc e 
          ⇒ (e <loc e2)
          ⇒ a ∈ X(e)
          ⇒ s ∈ Memory-class(f;init;X)(e)
          ⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B)))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. ∃a:A. ∃s:B. (e1 ≤loc e  ∧ (e <loc e2) ∧ s ∈ Memory-class(f;init;X)(e) ∧ a ∈ X(e) ∧ P[a;s]))
    ⇒ R[v1;v2])

Lemma: Memory-class-mem
∀[Info,B,A:Type].
  ∀R:A ⟶ B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B. ∀a:A.
    ((∀a:A. ∀s:B. ∀e:E.  (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s]))
    ⇒ (∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
          (e1 ≤loc e 
          ⇒ (e <loc e')
          ⇒ (e' <loc e2)
          ⇒ a1 ∈ X(e)
          ⇒ s1 ∈ Memory-class(f;init;X)(e)
          ⇒ a2 ∈ X(e')
          ⇒ s2 ∈ Memory-class(f;init;X)(e')
          ⇒ R[a1;s1;s2]
          ⇒ R[a1;s1;f a2 s2]))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ (e1 <loc e2)
    ⇒ a ∈ X(e1)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-class(f;init;X)(e2)
    ⇒ R[a;v1;v2])

Lemma: Memory-loc-class-invariant
∀[Info,B,A:Type].
  ∀P:B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    ((∀s:B. SqStable(P[s]))
    ⇒ (∀a:A. ∀e':E.  ((e' <loc e) ⇒ a ∈ X(e') ⇒ (∀s:B. (P[s] ⇒ P[f loc(e') a s]))))
    ⇒ (∀v:B. (v ↓∈ init loc(e) ⇒ P[v]))
    ⇒ v ∈ Memory-loc-class(f;init;X)(e)
    ⇒ P[v])

Lemma: Memory-loc-class-invariant-sv
∀[Info,B,A:Type].
  ∀P:B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e);B)
    ⇒ (∀a:A. ∀e':E.  ((e' <loc e) ⇒ a ∈ X(e') ⇒ (∀s:B. (P[s] ⇒ P[f loc(e') a s]))))
    ⇒ (∀v:B. (v ↓∈ init loc(e) ⇒ P[v]))
    ⇒ v ∈ Memory-loc-class(f;init;X)(e)
    ⇒ P[v])

Lemma: Memory-loc-class-invariant-sv1
∀[Info,B,A:Type].
  ∀P:B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e);B)
    ⇒ (∀v:B. (v ↓∈ init loc(e) ⇒ P[v]))
    ⇒ (∀a:A. ∀e':E. ∀s:B.
          ((e' <loc e) ⇒ a ∈ X(e') ⇒ s ∈ Memory-loc-class(f;init;X)(e') ⇒ P[s] ⇒ P[f loc(e') a s]))
    ⇒ v ∈ Memory-loc-class(f;init;X)(e)
    ⇒ P[v])

Lemma: Memory-loc-class-trans1
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E.
          (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-loc-class(f;init;X)(e) ⇒ R[s;f loc(e) a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-loc-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-loc-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (∃a:A. a ∈ X(e))))
    ⇒ R[v1;v2])

Lemma: Memory-loc-class-trans2
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E.
          (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-loc-class(f;init;X)(e) ⇒ R[s;f loc(e) a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-loc-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-loc-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∀e:E. (e1 ≤loc e  ⇒ (e <loc e2) ⇒ (∀a:A. (¬a ∈ X(e)))))
    ⇒ (v1 = v2 ∈ B))

Lemma: Memory-loc-class-trans-refl
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Refl(B;x,y.R[x;y])
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E.
          (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-loc-class(f;init;X)(e) ⇒ R[s;f loc(e) a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-loc-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-loc-class(f;init;X)(e2)
    ⇒ e1 ≤loc e2 
    ⇒ R[v1;v2])

Lemma: Memory-loc-class-progress
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀P:A ⟶ B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E.
  ∀v1,v2:B.
    ((∀a:A. ∀s:B.  Dec(P[a;s]))
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E. ∀s:B.
          (e1 ≤loc e 
          ⇒ (e <loc e2)
          ⇒ a ∈ X(e)
          ⇒ s ∈ Memory-loc-class(f;init;X)(e)
          ⇒ ((P[a;s] ⇒ R[s;f loc(e) a s]) ∧ ((¬P[a;s]) ⇒ (s = (f loc(e) a s) ∈ B)))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Memory-loc-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-loc-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. ∃a:A. ∃s:B. (e1 ≤loc e  ∧ (e <loc e2) ∧ s ∈ Memory-loc-class(f;init;X)(e) ∧ a ∈ X(e) ∧ P[a;s]))
    ⇒ R[v1;v2])

Lemma: Memory-loc-class-mem
∀[Info,B,A:Type].
  ∀R:A ⟶ B ⟶ B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B. ∀a:A.
    ((∀a:A. ∀s:B. ∀e:E.
        (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-loc-class(f;init;X)(e) ⇒ R[a;s;f loc(e) a s]))
    ⇒ (∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
          (e1 ≤loc e 
          ⇒ (e <loc e')
          ⇒ (e' <loc e2)
          ⇒ a1 ∈ X(e)
          ⇒ s1 ∈ Memory-loc-class(f;init;X)(e)
          ⇒ a2 ∈ X(e')
          ⇒ s2 ∈ Memory-loc-class(f;init;X)(e')
          ⇒ R[a1;s1;s2]
          ⇒ R[a1;s1;f loc(e2) a2 s2]))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ (e1 <loc e2)
    ⇒ a ∈ X(e1)
    ⇒ v1 ∈ Memory-loc-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-loc-class(f;init;X)(e2)
    ⇒ R[a;v1;v2])

Definition: Threshold-Combinator
Threshold-Combinator(R;X;init_state;accum;f) ==
  let state_function = λv,state. if R v state then accum v state else state fi  in
   let output_function = λi,v,state. if R v state then f i v state else {} fi  in
   output_function@Loc o (Loc,X, Memory-class(state_function;init_state;X))

Definition: classrel-multi-list
classrel-multi-list(es;A;Xs;L;e;n1;n2) ==
  (∀x:n:{n1..n2-} × A n × E
     ((x ∈ L) ⇒ (fst(snd(x)) ∈ Xs (fst(x))(snd(snd(x))) ∧ (∀m:{n1..fst(x)-}. ∀v:A m.  (¬v ∈ Xs m(snd(snd(x))))))))
  ∧ sorted-by(λp1,p2. (snd(snd(p1)) <loc snd(snd(p2)));L)
  ∧ no_repeats(E;map(λp.(snd(snd(p)));L))
  ∧ (∀e':E
       (e' ≤loc e  ∧ (∃n:{n1..n2-}. ∃a:A n. (a ∈ Xs n(e') ∧ (∀m:{n1..n-}. ∀v:A m.  (¬v ∈ Xs m(e')))))
       ⇐⇒ (e' ∈ map(λp.(snd(snd(p)));L))))

Definition: disjoint-union-class
X + Y ==  λb1,b2. if bag-null(b1) then bag-map(λx.(inr x );b2) else bag-map(λx.(inl x);b1) fi |X, Y|

Lemma: disjoint-union-class_wf
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].  (X + Y ∈ EClass(A + B))

Lemma: disjoint-union-classrel
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  ∀v:A + B. uiff(v ∈ X + Y(e);case v of inl(x) => x ∈ X(e) | inr(x) => x ∈ Y(e) ∧ (∀w:A. (¬w ∈ X(e))))

Lemma: disjoint-union-classrel-ite
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A + B].
  uiff(v ∈ X + Y(e);↓((↑isl(v)) ∧ outl(v) ∈ X(e)) ∨ ((¬↑isl(v)) ∧ outr(v) ∈ Y(e) ∧ (∀w:A. (¬w ∈ X(e)))))

Lemma: disjoint-union-classrel-ite2
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A + B].
  uiff(v ∈ X + Y(e);↓((↑isl(v)) ∧ outl(v) ∈ X(e)) ∨ ((↑¬bisl(v)) ∧ outr(v) ∈ Y(e) ∧ (∀w:A. (¬w ∈ X(e)))))

Lemma: disjoint-union-classrel-ite-weak
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A + B].
  (v ∈ X + Y(e) ⇐⇒ ↓((↑isl(v)) ∧ outl(v) ∈ X(e)) ∨ ((¬↑isl(v)) ∧ outr(v) ∈ Y(e) ∧ (∀w:A. (¬w ∈ X(e)))))

Lemma: disjoint-union-classrel-ite-weak2
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A + B].
  (v ∈ X + Y(e) ⇐⇒ ↓((↑isl(v)) ∧ outl(v) ∈ X(e)) ∨ ((↑¬bisl(v)) ∧ outr(v) ∈ Y(e) ∧ (∀w:A. (¬w ∈ X(e)))))

Definition: disjoint-union-type
disjoint-union-type(L) ==  rec-case(L) of [] => Unit | T::Ts => r.if null(Ts) then T else T + r fi 

Lemma: disjoint-union-type_wf
∀[L:Type List]. (disjoint-union-type(L) ∈ Type)

Lemma: disj_un_tr_ap_inr_lemma
∀x,i,tr2,tr1:Top.  (tr1 + tr2 i (inr x ) ~ λs.(tr2 i x s))

Lemma: disj_un_tr_ap_inl_lemma
∀x,i,tr2,tr1:Top.  (tr1 + tr2 i (inl x) ~ λs.(tr1 i x s))

Lemma: event_in_sv_classrel_is_in_class
∀[Info,T:Type].  ∀eo:EO+(Info). ∀[e:E]. ∀[v:T]. ∀[X:EClass(T)].  ((v ∈ X(e) ∧ Singlevalued(X)) ⇒ (e ∈ E(X)))

Lemma: only_value_of_sv_class_in_classrel
∀[Info,T:Type].
  ∀eo:EO+(Info). ∀[e:E]. ∀[v:T]. ∀[X:EClass(T)].  ((v ∈ X(e) ∧ Singlevalued(X)) ⇒ (v = only(X eo e) ∈ T))

Lemma: prior-classrel
∀[T,Info:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
  uiff(v ∈ Prior(X)(e);↓∃e':E. (((last(λe'.0 <z #(X es e')) e) = (inl e') ∈ (E + Top)) ∧ v ∈ X(e')))

Lemma: es-local-pred-iff-es-p-local-pred
∀[Info,T:Type].
  ∀X:EClass(T). ∀es:EO+(Info). ∀e,e':E.
    uiff((last(λe'.0 <z #(X es e')) e) = (inl e') ∈ (E + Top);es-p-local-pred(es;λe'.inhabited-classrel(es;T;X;e')) e 
                                                              e')

Lemma: prior-classrel-p-local-pred
∀[T,Info:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
  uiff(v ∈ Prior(X)(e);↓∃e':E. ((es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e') ∧ v ∈ X(e')))

Lemma: rec-combined-loc-class-1-classrel
∀[B,F,X,es,e,v:Top].  (v ∈ rec-combined-loc-class-1(F;X)(e) ~ v ∈ F o (Loc,X, Prior(rec-combined-loc-class-1(F;X)))(e))

Lemma: rec-combined-class-1-classrel
∀[B,F,X,es,e,v:Top].  (v ∈ F|X,Prior(self)|(e) ~ v ∈ F|X, Prior(F|X,Prior(self)|)|(e))

Lemma: rec-combined-loc-class-2-classrel
∀[B,F,X,Y,es,e,v:Top].  (v ∈ F|Loc, X, Y, Prior(self)|(e) ~ v ∈ F|Loc, X, Y, Prior(F|Loc, X, Y, Prior(self)|)|(e))

Lemma: rec-combined-class-2-classrel
∀[B,F,X,Y,es,e,v:Top].  (v ∈ F|X, Y, Prior(self)|(e) ~ v ∈ F|X, Y, Y|(e))

Lemma: rec-combined-loc-class-3-classrel
∀[B,F,X,Y,Z,es,e,v:Top].
  (v ∈ rec-combined-loc-class-3(F;X;Y;Z)(e) ~ v ∈ simple-loc-comb-4(F;X;Y;Z;Prior(rec-combined-loc-class-3(F;X;Y;Z)))(
                                                  e))

Lemma: rec-combined-class-3-classrel
∀[B,F,X,Y,Z,es,e,v:Top].
  (v ∈ rec-combined-class-3(F;X;Y;Z)(e) ~ v ∈ simple-comb-4(F;X;Y;Z;Prior(rec-combined-class-3(F;X;Y;Z)))(e))

Lemma: rec-combined-loc-class-opt-1-classrel
∀[B,F,init,X,es,e,v:Top].
  (v ∈ F|Loc, X, Prior(self)?init|(e) ~ v ∈ F o (Loc,X, Prior(F|Loc, X, Prior(self)?init|)?init)(e))

Lemma: rec-combined-class-opt-1-classrel
∀[B,F,init,X,es,e,v:Top].  (v ∈ F|X,Prior(self)?init|(e) ~ v ∈ F|X, Prior(F|X,Prior(self)?init|)?init|(e))

Lemma: rec-combined-loc-class-opt-2-classrel
∀[B,F,init,X,Y,es,e,v:Top].
  (v ∈ F|Loc, X, Y, Prior(self)?;init|(e) ~ v ∈ F|Loc, X, Y, Prior(F|Loc, X, Y, Prior(self)?;init|)?init|(e))

Lemma: rec-combined-class-opt-2-classrel
∀[B,F,init,X,Y,es,e,v:Top].  (v ∈ F|X, Y, Prior(self)?init|(e) ~ v ∈ F|X, Y, Y|(e))

Lemma: rec-combined-loc-class-opt-3-classrel
∀[B,F,init,X,Y,Z,es,e,v:Top].
  (v ∈ rec-combined-loc-class-opt-3(F;init;X;Y;Z)(e) 
  ~ v ∈ simple-loc-comb-4(F;X;Y;Z;Prior(rec-combined-loc-class-opt-3(F;init;X;Y;Z))?init)(e))

Lemma: rec-combined-class-opt-3-classrel
∀[B,F,init,X,Y,Z,es,e,v:Top].
  (v ∈ rec-combined-class-opt-3(F;init;X;Y;Z)(e) 
  ~ v ∈ simple-comb-4(F;X;Y;Z;Prior(rec-combined-class-opt-3(F;init;X;Y;Z))?init)(e))

Lemma: rec-comb-classrel
∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[Xs:k:ℕn ⟶ EClass(A k)]. ∀[f:Id ⟶ (k:ℕn ⟶ (A k)) ⟶ B ⟶ B].
∀[F:Id ⟶ (k:ℕn ⟶ bag(A k)) ⟶ bag(B) ⟶ bag(B)]. ∀[init:Id ⟶ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ rec-comb(Xs;F;init)(e);↓∃vs:k:ℕn ⟶ (A k)
                                    ∃w:B
                                     ((∀k:ℕn. vs[k] ∈ Xs[k](e))
                                     ∧ w ∈ Prior(rec-comb(Xs;F;init))?init(e)
                                     ∧ (v = (f loc(e) vs w) ∈ B))) 
  supposing ∀x:Id. ∀v:B. ∀bs:k:ℕn ⟶ bag(A k). ∀b:bag(B).
              (v ↓∈ F x bs b ⇐⇒ ↓∃vs:k:ℕn ⟶ (A k). ∃w:B. ((∀k:ℕn. vs k ↓∈ bs k) ∧ w ↓∈ b ∧ (v = (f x vs w) ∈ B)))

Lemma: rec-comb-es-sv
∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[Xs:k:ℕn ⟶ EClass(A k)]. ∀[F:Id ⟶ (k:ℕn ⟶ bag(A k)) ⟶ bag(B) ⟶ bag(B)].
∀[init:Id ⟶ bag(B)]. ∀[es:EO+(Info)].
  (es-sv-class(es;rec-comb(Xs;F;init))) supposing 
     ((∀bs:k:ℕn ⟶ bag(A k). ∀l:Id. ∀b:bag(B).  ((∀k:ℕn. (#(bs k) ≤ 1)) ⇒ (#(b) ≤ 1) ⇒ (#(F l bs b) ≤ 1))) and 
     (∀k:ℕn. es-sv-class(es;Xs k)) and 
     (∀l:Id. (#(init l) ≤ 1)))

Lemma: single-valued-base-loc-classrel
∀[f:Name ⟶ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v1,v2:T]. ∀[hdr:Name].
  ∀[locs:bag(Id)]. (v1 ∈ Base(hdr;locs)(e) ⇒ v2 ∈ Base(hdr;locs)(e) ⇒ (v1 = v2 ∈ T)) supposing T = (f hdr) ∈ Type

Lemma: single-valued-base-classrel
∀[f:Name ⟶ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v1,v2:T]. ∀[hdr:Name].
  v1 ∈ Base(hdr)(e) ⇒ v2 ∈ Base(hdr)(e) ⇒ (v1 = v2 ∈ T) supposing T = (f hdr) ∈ Type

Definition: message-constraint2
message-constraint2{i:l}(es;X;hdrs) ==
  ∀e1,e2:E.
    ((header(e1) ∈ hdrs)
    ⇒ (header(e2) ∈ hdrs)
    ⇒ single-valued-classrel(es;X;Id × Message{i:l})
    ⇒ (¬(e1 = e2 ∈ E))
    ⇒ (↓∃e1',e2':E
          ((e1' < e1) ∧ (e2' < e2) ∧ (¬(e1' = e2' ∈ E)) ∧ <loc(e1), info(e1)> ∈ X(e1') ∧ <loc(e2), info(e2)> ∈ X(e2'))))

Lemma: disjoint-union-class-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (single-valued-classrel(es;X;A) ⇒ single-valued-classrel(es;Y;B) ⇒ single-valued-classrel(es;X + Y;A + B))

Lemma: simple-loc-comb-3-concat-single-val
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B,C,D:Type]. ∀[F:Id ⟶ A ⟶ B ⟶ C ⟶ bag(D)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
∀[Z:EClass(C)].
  single-valued-classrel(es;concat-lifting-loc-3(F)|Loc, X, Y, Z|;D) 
  supposing (∀i:Id. ∀a:A. ∀b:B. ∀c:C.  (#(F i a b c) ≤ 1))
  ∧ single-valued-classrel(es;X;A)
  ∧ single-valued-classrel(es;Y;B)
  ∧ single-valued-classrel(es;Z;C)

Lemma: simple-loc-comb-3-concat-es-sv
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B,C:Type]. ∀[F:Id ⟶ A ⟶ B ⟶ C ⟶ bag(Top)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
∀[Z:EClass(C)].
  es-sv-class(es;concat-lifting-loc-3(F)|Loc, X, Y, Z|) 
  supposing (∀i:Id. ∀a:A. ∀b:B. ∀c:C.  (#(F i a b c) ≤ 1)) ∧ es-sv-class(es;X) ∧ es-sv-class(es;Y) ∧ es-sv-class(es;Z)

Lemma: simple-loc-comb-2-concat-single-val
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B,C:Type]. ∀[F:Id ⟶ A ⟶ B ⟶ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  single-valued-classrel(es;F@Loc o (Loc,X, Y);C) 
  supposing (∀i:Id. ∀a:A. ∀b:B.  (#(F i a b) ≤ 1)) ∧ single-valued-classrel(es;X;A) ∧ single-valued-classrel(es;Y;B)

Lemma: simple-loc-comb-2-concat-es-sv
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:Id ⟶ A ⟶ B ⟶ bag(Top)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  es-sv-class(es;F@Loc o (Loc,X, Y)) 
  supposing (∀i:Id. ∀a:A. ∀b:B.  (#(F i a b) ≤ 1)) ∧ es-sv-class(es;X) ∧ es-sv-class(es;Y)

Lemma: simple-loc-comb-1-concat-single-val
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:Id ⟶ A ⟶ bag(B)]. ∀[X:EClass(A)].
  (single-valued-classrel(es;F@(Loc, X);B)) supposing 
     ((∀i:Id. ∀a:A. ∀e:E.  (a ∈ X(e) ⇒ single-valued-bag(F i a;B))) and 
     single-valued-classrel(es;X;A))

Lemma: simple-loc-comb-1-concat-es-sv
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[F:Id ⟶ A ⟶ bag(Top)]. ∀[X:EClass(A)].
  es-sv-class(es;F@(Loc, X)) supposing (∀i:Id. ∀a:A.  (#(F i a) ≤ 1)) ∧ es-sv-class(es;X)

Lemma: simple-comb-es-sv
∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[Xs:k:ℕn ⟶ EClass(A k)]. ∀[F:(k:ℕn ⟶ bag(A k)) ⟶ bag(B)]. ∀[es:EO+(Info)].
  (es-sv-class(es;simple-comb(F;Xs))) supposing 
     ((∀bs:k:ℕn ⟶ bag(A k). ((∀k:ℕn. (#(bs k) ≤ 1)) ⇒ (#(F bs) ≤ 1))) and 
     (∀k:ℕn. es-sv-class(es;Xs k)))

Lemma: simple-comb-1-single-val
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:A ⟶ B]. ∀[X:EClass(A)].
  single-valued-classrel(es;lifting-1(F)|X|;B) supposing single-valued-classrel(es;X;A)

Lemma: simple-comb-1-es-sv
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:A ⟶ B]. ∀[X:EClass(A)].
  es-sv-class(es;lifting-1(F)|X|) supposing es-sv-class(es;X)

Lemma: simple-comb-2-es-sv
∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[F:A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (es-sv-class(es;lifting-2(F)|X, Y|)) supposing (es-sv-class(es;Y) and es-sv-class(es;X))

Lemma: rec-combined-class-opt-1-single-val0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ lifting-2(F)|X,Prior(self)?init|(e) and 
     v2 ∈ lifting-2(F)|X,Prior(self)?init|(e) and 
     single-valued-classrel(es;X;A) and 
     single-valued-bag(init loc(e);B))

Lemma: rec-combined-class-opt-1-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (single-valued-classrel(es;lifting-2(F)|X,Prior(self)?init|;B)) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)))

Lemma: rec-combined-class-opt-1-es-sv0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (es-sv-class(es;lifting-2(F)|X,Prior(self)?init|)) supposing (es-sv-class(es;X) and (∀l:Id. (#(init l) ≤ 1)))

Lemma: rec-combined-class-opt-1-es-sv
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[F:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (es-sv-class(es;lifting-2(F)|X,Prior(self)?init|)) supposing (es-sv-class(es;X) and (∀l:Id. (#(init l) ≤ 1)))

Lemma: rec-combined-loc-class-opt-1-single-val0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ lifting-loc-2(F)|Loc, X, Prior(self)?init|(e) and 
     v2 ∈ lifting-loc-2(F)|Loc, X, Prior(self)?init|(e) and 
     single-valued-classrel(es;X;A) and 
     single-valued-bag(init loc(e);B))

Lemma: rec-combined-loc-class-opt-1-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (single-valued-classrel(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|;B)) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)))

Lemma: rec-combined-loc-class-opt-1-es-sv0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (es-sv-class(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|)) supposing 
     (es-sv-class(es;X) and 
     (∀l:Id. (#(init l) ≤ 1)))

Lemma: rec-combined-loc-class-opt-1-es-sv
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[F:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (es-sv-class(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|)) supposing 
     (es-sv-class(es;X) and 
     (∀l:Id. (#(init l) ≤ 1)))

Lemma: parallel-class-single-val
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)].
  (single-valued-classrel(es;X || Y;A)) supposing 
     (single-valued-classrel(es;X;A) and 
     single-valued-classrel(es;Y;A) and 
     disjoint-classrel(es;A;X;A;Y))

Lemma: parallel-class-es-sv
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X,Y:EClass(A)].
  (es-sv-class(es;X || Y)) supposing (es-sv-class(es;X) and es-sv-class(es;Y) and disjoint-classrel(es;A;X;A;Y))

Lemma: longer-list-not-member
∀[T:Type]
  ∀eq:∀x,y:T.  Dec(x = y ∈ T). ∀L1,L2:T List.
    (no_repeats(T;L1) ⇒ no_repeats(T;L2) ⇒ (||L2|| > ||L1||) ⇒ (∃x:T. ((x ∈ L2) ∧ (¬(x ∈ L1)))))

Lemma: length-eq-lists-diff-elts
∀[T:Type]
  ∀eq:∀x,y:T.  Dec(x = y ∈ T). ∀L1,L2:T List.
    (no_repeats(T;L1) ⇒ (||L1|| ≥ ||L2|| ) ⇒ (∃x:T. ((x ∈ L2) ∧ (¬(x ∈ L1)))) ⇒ (∃x:T. ((x ∈ L1) ∧ (¬(x ∈ L2)))))

Definition: prior-classrel-list
prior-classrel-list(es;A;X;L;e) ==
  (∀p∈L.fst(p) ∈ X(snd(p)))
  ∧ sorted-by(λp1,p2. (snd(p1) <loc snd(p2));L)
  ∧ no_repeats(E;map(λp.(snd(p));L))
  ∧ (∀e':E. ((e' <loc e) ∧ (∃a:A. a ∈ X(e')) ⇐⇒ (e' ∈ map(λp.(snd(p));L))))

Definition: classrel-list
classrel-list(es;A;X;L;e) ==
  (∀p:A × E. ((p ∈ L) ⇒ fst(p) ∈ X(snd(p))))
  ∧ sorted-by(λp1,p2. (snd(p1) <loc snd(p2));L)
  ∧ no_repeats(E;map(λp.(snd(p));L))
  ∧ (∀e':E. (e' ≤loc e  ∧ (∃a:A. a ∈ X(e')) ⇐⇒ (e' ∈ map(λp.(snd(p));L))))

Definition: es-history-accum
es-history-accum(es;A;B;x;f;L) ==
  accumulate (with value b and list item a):
   f a b
  over list:
    map(λp.(fst(p));L)
  with starting value:
   x)

Lemma: Accum-class-single-val0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ Accum-class(f;init;X)(e) and 
     v2 ∈ Accum-class(f;init;X)(e) and 
     single-valued-bag(init loc(e);B) and 
     single-valued-classrel(es;X;A))

Lemma: Accum-class-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)].
  ∀X:EClass(A)
    ∀[init:Id ⟶ bag(B)]. ∀[f:A ⟶ B ⟶ B].
      (single-valued-classrel(es;X;A)
      ⇒ (∀l:Id. single-valued-bag(init l;B))
      ⇒ single-valued-classrel(es;Accum-class(f;init;X);B))

Lemma: Accum-class-es-sv
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)]. ∀[f:Top].
  (es-sv-class(es;Accum-class(f;init;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Lemma: Accum-class-es-sv1
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[f:A ⟶ B ⟶ B].
  (es-sv-class(es;Accum-class(f;init;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Lemma: Prior-Accum-class-single-val0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ Prior(Accum-class(f;init;X))?init(e) and 
     v2 ∈ Prior(Accum-class(f;init;X))?init(e) and 
     single-valued-bag(init loc(e);B) and 
     single-valued-classrel(es;X;A))

Lemma: class-at-single-val
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[locs:bag(Id)].
  single-valued-classrel(es;X@locs;T) supposing single-valued-classrel(es;X;T)

Lemma: class-at-es-sv
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[locs:bag(Id)].
  es-sv-class(es;X@locs) supposing es-sv-class(es;X)

Lemma: on-loc-class-single-val
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:Id ⟶ EClass(T)].
  single-valued-classrel(es;on-loc-class(X);T) supposing ∀i:Id. single-valued-classrel(es;X i;T)

Lemma: on-loc-class-es-sv
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:Id ⟶ EClass(T)].
  es-sv-class(es;on-loc-class(X)) supposing ∀i:Id. es-sv-class(es;X i)

Lemma: Accum-loc-class-es-sv1
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[f:Id ⟶ A ⟶ B ⟶ B].
  (es-sv-class(es;Accum-loc-class(f;init;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Lemma: Accum-loc-class-es-sv
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)]. ∀[f:Top].
  (es-sv-class(es;Accum-loc-class(f;init;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Lemma: Accum-loc-class-exists
∀[Info,B,A:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)].
  ((↓∃x:B. x ↓∈ init loc(e)) ⇒ (↓∃u:A. u ∈ X(e)) ⇒ (↓∃v:B. v ∈ Accum-loc-class(f;init;X)(e)))

Lemma: Memory-class-es-sv1
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:A ⟶ S ⟶ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (es-sv-class(es;Memory-class(f;init;X))) supposing (es-sv-class(es;X) and (∀l:Id. (#(init l) ≤ 1)))

Lemma: Memory-class-es-sv
∀[Info,A:Type]. ∀[init:Id ⟶ bag(Top)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (es-sv-class(es;Memory-class(f;init;X))) supposing (es-sv-class(es;X) and (∀l:Id. (#(init l) ≤ 1)))

Lemma: Accum-class-invariant
∀[Info,B,A:Type].
  ∀P:B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    ((∀s:B. SqStable(P[s]))
    ⇒ (∀a:A. ∀e':E.  (e' ≤loc e  ⇒ a ∈ X(e') ⇒ (∀s:B. (P[s] ⇒ P[f a s]))))
    ⇒ (∀v:B. (v ↓∈ init loc(e) ⇒ P[v]))
    ⇒ v ∈ Accum-class(f;init;X)(e)
    ⇒ P[v])

Lemma: Accum-class-trans
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Accum-class(f;init;X)(e1)
    ⇒ v2 ∈ Accum-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ R[v1;v2])

Lemma: Accum-class-trans-refl
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Refl(B;x,y.R[x;y])
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Accum-class(f;init;X)(e1)
    ⇒ v2 ∈ Accum-class(f;init;X)(e2)
    ⇒ e1 ≤loc e2 
    ⇒ R[v1;v2])

Lemma: Accum-class-progress
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀P:A ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    ((∀a:A. ∀s:B.  Dec(P[a;s]))
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀s1,s2:B.  SqStable(R[s1;s2]))
    ⇒ (∀a:A. ∀e:E. ∀s:B.
          ((e1 <loc e)
          ⇒ e ≤loc e2 
          ⇒ a ∈ X(e)
          ⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
          ⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B)))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ Accum-class(f;init;X)(e1)
    ⇒ v2 ∈ Accum-class(f;init;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (((∃e:E. ∃a:A. ∃s:B. ((e1 <loc e) ∧ e ≤loc e2  ∧ s ∈ Prior(Accum-class(f;init;X))?init(e) ∧ a ∈ X(e) ∧ P[a;s]))
       ⇒ R[v1;v2])
       ∧ ((∀e:E. ∀s:B.
             ((e1 <loc e)
             ⇒ e ≤loc e2 
             ⇒ s ∈ Prior(Accum-class(f;init;X))?init(e)
             ⇒ (∀a:A. ((¬a ∈ X(e)) ∨ (¬P[a;s])))))
         ⇒ (v1 = v2 ∈ B))))

Lemma: simple-comb-1-disjoint-classrel
∀[Info,T,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[f:A ⟶ T].
  (disjoint-classrel(es;A;X;B;Y) ⇒ disjoint-classrel(es;T;lifting-1(f)|X|;B;Y))

Lemma: base-disjoint-classrel
∀A,B:Type. ∀f:Name ⟶ Type. ∀es:EO+(Message(f)). ∀hdr1,hdr2:Name.
  ((¬(hdr1 = hdr2 ∈ Name)) ⇒ hdr1 encodes A ⇒ hdr2 encodes B ⇒ disjoint-classrel(es;A;Base(hdr1);B;Base(hdr2)))

Lemma: parallel-class-disjoint-classrel
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)]. ∀[Z:EClass(B)].
  (disjoint-classrel(es;A;X;B;Z) ⇒ disjoint-classrel(es;A;Y;B;Z) ⇒ disjoint-classrel(es;A;X || Y;B;Z))

Lemma: disjoint-union-comb-classrel
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  ∀v:A + B. uiff(v ∈ X (+) Y(e);((↑isl(v)) ∧ outl(v) ∈ X(e)) ∨ ((¬↑isl(v)) ∧ outr(v) ∈ Y(e)))

Lemma: disjoint-union-comb-classrel-weak
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  ∀v:A + B. (v ∈ X (+) Y(e) ⇐⇒ ((↑isl(v)) ∧ outl(v) ∈ X(e)) ∨ ((¬↑isl(v)) ∧ outr(v) ∈ Y(e)))

Lemma: disjoint-union-comb-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (single-valued-classrel(es;X (+) Y;A + B)) supposing 
     (disjoint-classrel(es;A;X;B;Y) and 
     single-valued-classrel(es;Y;B) and 
     single-valued-classrel(es;X;A))

Lemma: disjoint-union-comb-es-sv
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (es-sv-class(es;X (+) Y)) supposing (disjoint-classrel(es;A;X;B;Y) and es-sv-class(es;Y) and es-sv-class(es;X))

Lemma: disjoint-union-comb-disjoint-classrel
∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(C)].
  (disjoint-classrel(es;B;Y;C;Z) ⇒ disjoint-classrel(es;A;X;C;Z) ⇒ disjoint-classrel(es;A + B;X (+) Y;C;Z))

Definition: Memory1
Memory1(init;tr;X) ==  Memory-loc-class(tr;λloc.{init loc};X)

Lemma: Memory1_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].  (Memory1(init;tr;X) ∈ EClass(B))

Lemma: Memory1-functional
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  ∀es:EO+(Info). (single-valued-classrel(es;X;A) ⇒ Memory1(init;tr;X) is functional)

Definition: Memory2
Memory2(init;tr1;X1;tr2;X2) ==  Memory-loc-class(tr1 + tr2;λloc.{init loc};X1 (+) X2)

Lemma: Memory2_wf
∀[Info,A1,A2,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  (Memory2(init;tr1;X1;tr2;X2) ∈ EClass(S))

Lemma: Memory2-functional
∀[Info,A1,A2,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  ∀es:EO+(Info)
    (single-valued-classrel(es;X1;A1)
    ⇒ single-valued-classrel(es;X2;A2)
    ⇒ disjoint-classrel(es;A1;X1;A2;X2)
    ⇒ Memory2(init;tr1;X1;tr2;X2) is functional)

Definition: Memory3
Memory3(init;tr1;X1;tr2;X2;tr3;X3) ==  Memory-loc-class(tr1 + tr2 + tr3;λloc.{init loc};X1 (+) X2 (+) X3)

Lemma: Memory3_wf
∀[Info,A1,A2,A3,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)].
  (Memory3(init;
           tr1;X1;
           tr2;X2;
           tr3;X3) ∈ EClass(S))

Lemma: Memory3-functional
∀[Info,A1,A2,A3,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)].
  ∀es:EO+(Info)
    (single-valued-classrel(es;X1;A1)
    ⇒ single-valued-classrel(es;X2;A2)
    ⇒ single-valued-classrel(es;X3;A3)
    ⇒ disjoint-classrel(es;A1;X1;A2;X2)
    ⇒ disjoint-classrel(es;A1;X1;A3;X3)
    ⇒ disjoint-classrel(es;A2;X2;A3;X3)
    ⇒ Memory3(init;
               tr1;X1;
               tr2;X2;
               tr3;X3) is functional)

Definition: Memory4
Memory4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4) ==
  Memory-loc-class(tr1 + tr2 + tr3 + tr4;λloc.{init loc};X1 (+) X2 (+) X3 (+) X4)

Lemma: Memory4_wf
∀[Info,A1,A2,A3,A4,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)]. ∀[tr4:Id ⟶ A4 ⟶ S ⟶ S]. ∀[X4:EClass(A4)].
  (Memory4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4) ∈ EClass(S))

Definition: Memory4-prc
Memory4-prc(A1;A2;A3;A4;B;init;tr1;Xpr1;tr2;Xpr2;tr3;Xpr3;tr4;Xpr4) ==
  TERMOF{Memory4-locally-programmable:o, 1:l, 1:l} A1 A2 A3 A4 B init tr1 tr2 tr3 tr4 Xpr1 Xpr2 Xpr3 Xpr4

Definition: State-class
State-class(init;f;X) ==  λx,s. if bag-null(x) then s else lifting-2(f) x s fi |X, Memory-class(f;init;X)|

Lemma: State-class_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ bag(B)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)].  (State-class(init;f;X) ∈ EClass(B))

Lemma: State-classrel
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  ∀[v:B]. (v ∈ State-class(init;f;X)(e) ⇐⇒ iterated_classrel(es;B;A;f;init;X;e;v))

Lemma: State-classrel2
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  ∀[v:B]. (v ∈ State-class(init;f;X)(e) ⇐⇒ ↓iterated-classrel(es;B;A;f;init;X;e;v))

Lemma: State-class-single-val0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ State-class(init;f;X)(e) and 
     v2 ∈ State-class(init;f;X)(e) and 
     single-valued-bag(init loc(e);B) and 
     single-valued-classrel(es;X;A))

Lemma: State-class-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (single-valued-classrel(es;State-class(init;f;X);B)) supposing 
     ((∀l:Id. single-valued-bag(init l;B)) and 
     single-valued-classrel(es;X;A))

Lemma: State-class-top
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (State-class(init;f;X) ∈ EClass(Top))

Lemma: State-class-es-sv1
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (es-sv-class(es;State-class(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Lemma: State-class-es-sv
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (es-sv-class(es;State-class(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Definition: State-comb
State-comb(init;f;X) ==  λx,s. if bag-null(x) then s else lifting-2(f) x s fi |X,Prior(self)?init|

Lemma: State-comb_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ bag(B)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)].  (State-comb(init;f;X) ∈ EClass(B))

Lemma: State-comb-exists
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  ↓∃v:B. v ∈ State-comb(init;f;X)(e) supposing #(init loc(e)) > 0

Lemma: State-comb-exists-iff
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀[es:EO+(Info)]. ∀[e:E].  uiff(#(init loc(e)) > 0;↓∃v:B. v ∈ State-comb(init;f;X)(e))

Lemma: State-comb-total
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  es-total-class(es;State-comb(init;f;X)) supposing ∀l:Id. (1 ≤ #(init l))

Lemma: State-comb-classrel-class
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  ∀[v:B]. (v ∈ State-comb(init;f;X)(e) ⇐⇒ v ∈ State-class(init;f;X)(e))

Lemma: State-comb-classrel
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  ∀[v:B]. (v ∈ State-comb(init;f;X)(e) ⇐⇒ iterated_classrel(es;B;A;f;init;X;e;v))

Lemma: State-comb-classrel2
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  ∀[v:B]. (v ∈ State-comb(init;f;X)(e) ⇐⇒ ↓iterated-classrel(es;B;A;f;init;X;e;v))

Lemma: State-comb-classrel-mem
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]. (v ∈ Prior(State-comb(init;f;X))?init(e) ⇐⇒ v ∈ Memory-class(f;init;X)(e))

Lemma: State-comb-classrel-mem2
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      (v ∈ State-comb(init;f;X)(e)
      ⇐⇒ if e ∈b X
          then ↓∃w:B. ∃a:A. (w ∈ Memory-class(f;init;X)(e) ∧ (v = (f a w) ∈ B) ∧ a ∈ X(e))
          else v ∈ Memory-class(f;init;X)(e)
          fi )

Lemma: State-comb-classrel-mem3
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      (v ∈ Memory-class(f;init;X)(e)
      ⇐⇒ ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ v ∈ State-comb(init;f;X)(pred(e))))

Lemma: State-comb-classrel-single-val
∀[Info,B,A:Type].
  ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (uiff(v ∈ State-comb(init;f;X)(e);iterated-classrel(es;B;A;f;init;X;e;v))) supposing 
       (single-valued-classrel(es;X;A) and 
       single-valued-bag(init loc(e);B))

Lemma: State-comb-single-val0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ State-comb(init;f;X)(e) and 
     v2 ∈ State-comb(init;f;X)(e) and 
     single-valued-bag(init loc(e);B) and 
     single-valued-classrel(es;X;A))

Lemma: State-comb-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (single-valued-classrel(es;State-comb(init;f;X);B)) supposing 
     ((∀l:Id. single-valued-bag(init l;B)) and 
     single-valued-classrel(es;X;A))

Lemma: State-comb-functional
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (State-comb(init;f;X) is functional) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: State-comb-fun-eq
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (State-comb(init;f;X)(e)
     = if e ∈b X then if first(e) then f X(e) sv-bag-only(init loc(e)) else f X(e) State-comb(init;f;X)(pred(e)) fi 
       if first(e) then sv-bag-only(init loc(e))
       else State-comb(init;f;X)(pred(e))
       fi 
     ∈ B) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: State-comb-fun-eq2
∀[Info,B,A:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (State-comb(init;f;X)(e)
     = if e ∈b X then if first(e) then f X@e sv-bag-only(init loc(e)) else f X@e State-comb(init;f;X)(pred(e)) fi 
       if first(e) then sv-bag-only(init loc(e))
       else State-comb(init;f;X)(pred(e))
       fi 
     ∈ B) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: State-comb-top
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].  (State-comb(init;f;X) ∈ EClass(Top))

Lemma: State-comb-es-sv1
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (es-sv-class(es;State-comb(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Lemma: State-comb-es-sv
∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(Top)].
  (es-sv-class(es;State-comb(init;f;X))) supposing ((∀l:Id. (#(init l) ≤ 1)) and es-sv-class(es;X))

Lemma: State-comb-invariant
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:A ⟶ S ⟶ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[P:S ⟶ ℙ]. ∀[e:E].
  ∀v:S
    ((∀s:S. SqStable(P[s]))
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E.  (e' ≤loc e  ⇒ a ∈ X(e') ⇒ (∀s:S. (s ∈ Memory-class(f;init;X)(e') ⇒ P[s] ⇒ P[f a s]))))
    ⇒ v ∈ State-comb(init;f;X)(e)
    ⇒ P[v])

Lemma: State-comb-invariant-sv
∀[Info,A,S:Type]. ∀[P:S ⟶ ℙ].
  ∀init:Id ⟶ bag(S). ∀f:A ⟶ S ⟶ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (single-valued-bag(init loc(e);S)
    ⇒ single-valued-classrel(es;X;A)
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E.  (e' ≤loc e  ⇒ a ∈ X(e') ⇒ (∀s:S. (s ∈ Memory-class(f;init;X)(e') ⇒ P[s] ⇒ P[f a s]))))
    ⇒ v ∈ State-comb(init;f;X)(e)
    ⇒ P[v])

Lemma: State-comb-invariant-or
∀[Info,A,S:Type]. ∀[P:S ⟶ ℙ].
  ∀init:Id ⟶ bag(S). ∀f:A ⟶ S ⟶ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (((single-valued-bag(init loc(e);S) ∧ single-valued-classrel(es;X;A)) ∨ (∀s:S. SqStable(P[s])))
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E.  (e' ≤loc e  ⇒ a ∈ X(e') ⇒ (∀s:S. (s ∈ Memory-class(f;init;X)(e') ⇒ P[s] ⇒ P[f a s]))))
    ⇒ v ∈ State-comb(init;f;X)(e)
    ⇒ P[v])

Lemma: State-comb-trans1
∀[Info,B,A:Type]. ∀[R:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ State-comb(init;f;X)(pred(e)) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ State-comb(init;f;X)(e1)
    ⇒ v2 ∈ State-comb(init;f;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. ((e1 <loc e) ∧ e ≤loc e2  ∧ (∃a:A. a ∈ X(e))))
    ⇒ R[v1;v2])

Lemma: State-comb-trans2
∀[Info,B,A:Type]. ∀[R:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ State-comb(init;f;X)(pred(e)) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ State-comb(init;f;X)(e1)
    ⇒ v2 ∈ State-comb(init;f;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∀e:E. ((e1 <loc e) ⇒ e ≤loc e2  ⇒ (∀a:A. (¬a ∈ X(e)))))
    ⇒ (v1 = v2 ∈ B))

Lemma: State-comb-trans-refl
∀[Info,B,A:Type]. ∀[R:B ⟶ B ⟶ ℙ].
  ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Refl(B;x,y.R[x;y])
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e) ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ State-comb(init;f;X)(pred(e)) ⇒ R[s;f a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ State-comb(init;f;X)(e1)
    ⇒ v2 ∈ State-comb(init;f;X)(e2)
    ⇒ e1 ≤loc e2 
    ⇒ R[v1;v2])

Lemma: State-comb-progress
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀P:A ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    ((∀a:A. ∀s:B.  Dec(P[a;s]))
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E. ∀s:B.
          ((e1 <loc e)
          ⇒ e ≤loc e2 
          ⇒ a ∈ X(e)
          ⇒ s ∈ State-comb(init;f;X)(pred(e))
          ⇒ ((P[a;s] ⇒ R[s;f a s]) ∧ ((¬P[a;s]) ⇒ (s = (f a s) ∈ B)))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ State-comb(init;f;X)(e1)
    ⇒ v2 ∈ State-comb(init;f;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. ∃a:A. ∃s:B. ((e1 <loc e) ∧ e ≤loc e2  ∧ s ∈ State-comb(init;f;X)(pred(e)) ∧ a ∈ X(e) ∧ P[a;s]))
    ⇒ R[v1;v2])

Lemma: State-comb-mem
∀[Info,B,A:Type]. ∀[R:A ⟶ B ⟶ B ⟶ ℙ]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
∀[e1,e2:E].
  ∀v1,v2:B. ∀a:A.
    ((∀a:A. ∀s:B. ∀e:E.  (e1 ≤loc e  ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s]))
    ⇒ (∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
          (e1 ≤loc e 
          ⇒ (e <loc e')
          ⇒ e' ≤loc e2 
          ⇒ a1 ∈ X(e)
          ⇒ s1 ∈ Memory-class(f;init;X)(e)
          ⇒ a2 ∈ X(e')
          ⇒ s2 ∈ State-comb(init;f;X)(pred(e'))
          ⇒ R[a1;s1;s2]
          ⇒ R[a1;s1;f a2 s2]))
    ⇒ (∀s1,s2:B. ∀a:A.  SqStable(R[a;s1;s2]))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ e1 ≤loc e2 
    ⇒ a ∈ X(e1)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ State-comb(init;f;X)(e2)
    ⇒ R[a;v1;v2])

Lemma: State-comb-mem2
∀[Info,B,A:Type]. ∀[R:A ⟶ B ⟶ B ⟶ ℙ]. ∀[f:A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
∀[e1,e2:E].
  ∀v1,v2:B. ∀a:A.
    ((∀a:A. ∀s:B. ∀e:E.  (e1 ≤loc e  ⇒ e ≤loc e2  ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s]))
    ⇒ (∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
          (e1 ≤loc e 
          ⇒ (e <loc e')
          ⇒ e' ≤loc e2 
          ⇒ a1 ∈ X(e)
          ⇒ s1 ∈ Memory-class(f;init;X)(e)
          ⇒ a2 ∈ X(e')
          ⇒ s2 ∈ State-comb(init;f;X)(pred(e'))
          ⇒ R[a1;s1;s2]
          ⇒ R[a1;s1;f a2 s2]))
    ⇒ (∀s1,s2:B. ∀a:A.  SqStable(R[a;s1;s2]))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ e1 ≤loc e2 
    ⇒ a ∈ X(e1)
    ⇒ v1 ∈ Prior(State-comb(init;f;X))?init(e1)
    ⇒ v2 ∈ State-comb(init;f;X)(e2)
    ⇒ R[a;v1;v2])

Definition: State-loc-comb
State-loc-comb(init;f;X) ==  λl,x,s. if bag-null(x) then s else lifting-loc-2(f) l x s fi |Loc, X, Prior(self)?init|

Lemma: State-loc-comb_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ bag(B)]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].  (State-loc-comb(init;f;X) ∈ EClass(B))

Lemma: State-loc-comb-is-loop-class-state
∀[Info,A,B:Type]. ∀[init:Id ⟶ bag(B)]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  (State-loc-comb(init;f;X) = loop-class-state((f o X);init) ∈ EClass(B))

Lemma: State-loc-comb-classrel-non-loc
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  ∀[v:B]. (v ∈ State-loc-comb(init;f;X)(e) ⇐⇒ v ∈ State-comb(init;f loc(e);X)(e))

Lemma: State-loc-comb-classrel
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]. (v ∈ State-loc-comb(init;f;X)(e) ⇐⇒ iterated_classrel(es;B;A;f loc(e);init;X;e;v))

Lemma: State-loc-comb-classrel2
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]. (v ∈ State-loc-comb(init;f;X)(e) ⇐⇒ ↓iterated-classrel(es;B;A;f loc(e);init;X;e;v))

Lemma: State-loc-comb-classrel-mem
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]. (v ∈ Prior(State-loc-comb(init;f;X))?init(e) ⇐⇒ v ∈ Memory-loc-class(f;init;X)(e))

Lemma: State-loc-comb-classrel-mem2
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      (v ∈ State-loc-comb(init;f;X)(e)
      ⇐⇒ if e ∈b X
          then ↓∃w:B. ∃a:A. (w ∈ Memory-loc-class(f;init;X)(e) ∧ (v = (f loc(e) a w) ∈ B) ∧ a ∈ X(e))
          else v ∈ Memory-loc-class(f;init;X)(e)
          fi )

Lemma: State-loc-comb-classrel-mem3
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.
    ∀[v:B]
      (v ∈ Memory-loc-class(f;init;X)(e)
      ⇐⇒ ((↑first(e)) ∧ v ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ v ∈ State-loc-comb(init;f;X)(pred(e))))

Lemma: State-loc-comb-classrel-single-val
∀[Info,B,A:Type].
  ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:B.
    (uiff(v ∈ State-loc-comb(init;f;X)(e);iterated-classrel(es;B;A;f loc(e);init;X;e;v))) supposing 
       (single-valued-classrel(es;X;A) and 
       single-valued-bag(init loc(e);B))

Lemma: State-loc-comb-non-empty
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  ((¬↑bag-null(init loc(e))) ⇒ (↓∃v:B. v ∈ State-loc-comb(init;f;X)(e)))

Lemma: State-loc-comb-non-empty-iff
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). ∀es:EO+(Info). ∀e:E.  (¬↑bag-null(init loc(e)) ⇐⇒ ↓∃v:B. v ∈ State-loc-comb(init;f;X)(e))

Lemma: Memory-loc-class-is-prior-State-loc-comb
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)].
  ∀X:EClass(A). (Memory-loc-class(f;init;X) = Prior(State-loc-comb(init;f;X))?init ∈ EClass(B))

Lemma: State-loc-comb-exists
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  ↓∃v:B. v ∈ State-loc-comb(init;f;X)(e) supposing #(init loc(e)) > 0

Lemma: State-loc-comb-total
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  es-total-class(es;State-loc-comb(init;f;X)) supposing ∀l:Id. (1 ≤ #(init l))

Lemma: State-loc-comb-single-val0
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ State-loc-comb(init;f;X)(e) and 
     v2 ∈ State-loc-comb(init;f;X)(e) and 
     single-valued-bag(init loc(e);B) and 
     single-valued-classrel(es;X;A))

Lemma: State-loc-comb-single-val
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)].
  (single-valued-classrel(es;State-loc-comb(init;f;X);B)) supposing 
     ((∀l:Id. single-valued-bag(init l;B)) and 
     single-valued-classrel(es;X;A))

Lemma: State-loc-comb-functional
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (State-loc-comb(init;f;X) is functional) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: State-loc-comb-fun-eq-non-loc
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (State-loc-comb(init;f;X)(e) = State-comb(init;f loc(e);X)(e) ∈ B) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: State-loc-comb-fun-eq
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (State-loc-comb(init;f;X)(e)
     = if e ∈b X
         then if first(e)
              then f loc(e) X(e) sv-bag-only(init loc(e))
              else f loc(e) X(e) State-loc-comb(init;f;X)(pred(e))
              fi 
       if first(e) then sv-bag-only(init loc(e))
       else State-loc-comb(init;f;X)(pred(e))
       fi 
     ∈ B) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: State-loc-comb-fun-eq2
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (State-loc-comb(init;f;X)(e)
     = if e ∈b X
         then if first(e)
              then f loc(e) X@e sv-bag-only(init loc(e))
              else f loc(e) X@e State-loc-comb(init;f;X)(pred(e))
              fi 
       if first(e) then sv-bag-only(init loc(e))
       else State-loc-comb(init;f;X)(pred(e))
       fi 
     ∈ B) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))

Lemma: State-loc-comb-invariant
∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f:Id ⟶ A ⟶ S ⟶ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[P:S ⟶ ℙ]. ∀[e:E].
  ∀v:S
    ((∀s:S. SqStable(P[s]))
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E.
          (e' ≤loc e  ⇒ a ∈ X(e') ⇒ (∀s:S. (s ∈ Memory-loc-class(f;init;X)(e') ⇒ P[s] ⇒ P[f loc(e') a s]))))
    ⇒ v ∈ State-loc-comb(init;f;X)(e)
    ⇒ P[v])

Lemma: State-loc-comb-invariant-sv
∀[Info,A,S:Type]. ∀[P:S ⟶ ℙ].
  ∀init:Id ⟶ bag(S). ∀f:Id ⟶ A ⟶ S ⟶ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (single-valued-bag(init loc(e);S)
    ⇒ single-valued-classrel(es;X;A)
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E.
          (e' ≤loc e  ⇒ a ∈ X(e') ⇒ (∀s:S. (s ∈ Memory-loc-class(f;init;X)(e') ⇒ P[s] ⇒ P[f loc(e') a s]))))
    ⇒ v ∈ State-loc-comb(init;f;X)(e)
    ⇒ P[v])

Lemma: State-loc-comb-invariant-sv1
∀[Info,A,S:Type]. ∀[P:S ⟶ ℙ].
  ∀init:Id ⟶ bag(S). ∀f:Id ⟶ A ⟶ S ⟶ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (single-valued-bag(init loc(e);S)
    ⇒ single-valued-classrel(es;X;A)
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E. ∀s:S.
          (e' ≤loc e 
          ⇒ a ∈ X(e')
          ⇒ if first(e') then s ↓∈ init loc(e') else s ∈ State-loc-comb(init;f;X)(pred(e')) fi 
          ⇒ P[s]
          ⇒ P[f loc(e') a s]))
    ⇒ v ∈ State-loc-comb(init;f;X)(e)
    ⇒ P[v])

Lemma: State-loc-comb-invariant-sv2
∀[Info,A,S:Type].
  ∀es:EO+(Info). ∀P:E ⟶ S ⟶ ℙ. ∀init:Id ⟶ bag(S). ∀f:Id ⟶ A ⟶ S ⟶ S. ∀X:EClass(A). ∀e:E. ∀v:S.
    (single-valued-bag(init loc(e);S)
    ⇒ single-valued-classrel(es;X;A)
    ⇒ (∀s:S. ∀e':E.
          (e' ≤loc e 
          ⇒ if first(e') then s ↓∈ init loc(e') else s ∈ State-loc-comb(init;f;X)(pred(e')) ∧ P[pred(e');s] fi 
          ⇒ if e' ∈b X then ∀a:A. (a ∈ X(e') ⇒ P[e';f loc(e') a s]) else P[e';s] fi ))
    ⇒ v ∈ State-loc-comb(init;f;X)(e)
    ⇒ P[e;v])

Lemma: State-loc-comb-invariant-or
∀[Info,A,S:Type]. ∀[P:S ⟶ ℙ].
  ∀init:Id ⟶ bag(S). ∀f:Id ⟶ A ⟶ S ⟶ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (((single-valued-bag(init loc(e);S) ∧ single-valued-classrel(es;X;A)) ∨ (∀s:S. SqStable(P[s])))
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E.
          (e' ≤loc e  ⇒ a ∈ X(e') ⇒ (∀s:S. (s ∈ Memory-loc-class(f;init;X)(e') ⇒ P[s] ⇒ P[f loc(e') a s]))))
    ⇒ v ∈ State-loc-comb(init;f;X)(e)
    ⇒ P[v])

Lemma: State-loc-comb-trans-refl
∀[Info,B,A:Type]. ∀[R:B ⟶ B ⟶ ℙ].
  ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Refl(B;x,y.R[x;y])
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e)
          ⇒ e ≤loc e2 
          ⇒ a ∈ X(e)
          ⇒ (∀s:B. (s ∈ State-loc-comb(init;f;X)(pred(e)) ⇒ R[s;f loc(e) a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ State-loc-comb(init;f;X)(e1)
    ⇒ v2 ∈ State-loc-comb(init;f;X)(e2)
    ⇒ e1 ≤loc e2 
    ⇒ R[v1;v2])

Lemma: State-loc-comb-trans1
∀[Info,B,A:Type]. ∀[R:B ⟶ B ⟶ ℙ].
  ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.
    (Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E.
          ((e1 <loc e)
          ⇒ e ≤loc e2 
          ⇒ a ∈ X(e)
          ⇒ (∀s:B. (s ∈ State-loc-comb(init;f;X)(pred(e)) ⇒ R[s;f loc(e) a s]))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ State-loc-comb(init;f;X)(e1)
    ⇒ v2 ∈ State-loc-comb(init;f;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. ((e1 <loc e) ∧ e ≤loc e2  ∧ (∃a:A. a ∈ X(e))))
    ⇒ R[v1;v2])

Lemma: State-loc-comb-progress
∀[Info,B,A:Type].
  ∀R:B ⟶ B ⟶ ℙ. ∀P:A ⟶ B ⟶ ℙ. ∀f:Id ⟶ A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E.
  ∀v1,v2:B.
    ((∀a:A. ∀s:B.  Dec(P[a;s]))
    ⇒ Trans(B;x,y.R[x;y])
    ⇒ (∀a:A. ∀e:E. ∀s:B.
          ((e1 <loc e)
          ⇒ e ≤loc e2 
          ⇒ a ∈ X(e)
          ⇒ s ∈ State-loc-comb(init;f;X)(pred(e))
          ⇒ ((P[a;s] ⇒ R[s;f loc(e) a s]) ∧ ((¬P[a;s]) ⇒ (s = (f loc(e) a s) ∈ B)))))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ v1 ∈ State-loc-comb(init;f;X)(e1)
    ⇒ v2 ∈ State-loc-comb(init;f;X)(e2)
    ⇒ (e1 <loc e2)
    ⇒ (∃e:E. ∃a:A. ∃s:B. ((e1 <loc e) ∧ e ≤loc e2  ∧ s ∈ State-loc-comb(init;f;X)(pred(e)) ∧ a ∈ X(e) ∧ P[a;s]))
    ⇒ R[v1;v2])

Definition: State1
State1(init;tr;X) ==  State-loc-comb(λloc.{init loc};tr;X)

Lemma: State1_wf
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].  (State1(init;tr;X) ∈ EClass(B))

Lemma: State1-functional
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  ∀es:EO+(Info). (single-valued-classrel(es;X;A) ⇒ State1(init;tr;X) is functional)

Lemma: State1-exists
∀[Info,A,B:Type]. ∀[init:B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:B. v ∈ State1(λloc.init;tr;X)(e))

Lemma: State1-loc-exists
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:B. v ∈ State1(init;tr;X)(e))

Lemma: State1-prior
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (Prior(State1(init;f;X))?λloc.{init loc}(e)
  = if first(e) then {init loc(e)} else State1(init;f;X)(pred(e)) fi 
  ∈ bag(B))

Lemma: State1-state-class1
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ B]. ∀[X:EClass(A)].
  (State1(init;f;X) = state-class1(init;f;X) ∈ EClass(B))

Lemma: Memory1-memory-class1
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[tr:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  (Memory1(init;tr;X) = memory-class1(initially initapplying tron X) ∈ EClass(B))

Lemma: state-class1-state1-classrel
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ State1(init;f;X)(e);v ∈ state-class1(init;f;X)(e))

Lemma: state-class1-exists
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:B. v ∈ state-class1(init;f;X)(e))

Lemma: state-class1-prior
∀[Info,A,B:Type]. ∀[init:Id ⟶ B]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (Prior(state-class1(init;f;X))?λloc.{init loc}(e)
  = if first(e) then {init loc(e)} else state-class1(init;f;X)(pred(e)) fi 
  ∈ bag(B))

Lemma: state-class1-state1-eq
∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (State1(init;f;X)(e) = state-class1(init;f;X)(e) ∈ bag(B))

Definition: State2
State2(init;tr1;X1;tr2;X2) ==  State-loc-comb(λloc.{init loc};tr1 + tr2;X1 (+) X2)

Lemma: State2_wf
∀[Info,A1,A2,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  (State2(init;tr1;X1;tr2;X2) ∈ EClass(S))

Lemma: State2-functional
∀[Info,A1,A2,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  ∀es:EO+(Info)
    (single-valued-classrel(es;X1;A1)
    ⇒ single-valued-classrel(es;X2;A2)
    ⇒ disjoint-classrel(es;A1;X1;A2;X2)
    ⇒ State2(init;tr1;X1;tr2;X2) is functional)

Lemma: State2-exists
∀[Info,A1,A2,S:Type]. ∀[init:S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:S. v ∈ State2(λloc.init;tr1;X1;tr2;X2)(e))

Lemma: State2-loc-exists
∀[Info,A1,A2,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:S. v ∈ State2(init;tr1;X1;tr2;X2)(e))

Lemma: State2-state-class2
∀[Info,A1,A2,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  (State2(init;tr1;X1;tr2;X2) = state-class2(init;tr1;X1;tr2;X2) ∈ EClass(S))

Lemma: Memory2-memory-class2
∀[Info,A1,A2,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  (Memory2(init;tr1;X1;tr2;X2) = memory-class2(init;tr1;X1;tr2;X2) ∈ EClass(S))

Definition: State3
State3(init;tr1;X1;tr2;X2;tr3;X3) ==  State-loc-comb(λloc.{init loc};tr1 + tr2 + tr3;X1 (+) X2 (+) X3)

Lemma: State3_wf
∀[Info,A1,A2,A3,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)].
  (State3(init;tr1;X1;tr2;X2;tr3;X3) ∈ EClass(S))

Lemma: State3-exists
∀[Info,A1,A2,A3,S:Type]. ∀[init:S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:S. v ∈ State3(λloc.init;tr1;X1;tr2;X2;tr3;X3)(e))

Lemma: State3-loc-exists
∀[Info,A1,A2,A3,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:S. v ∈ State3(init;tr1;X1;tr2;X2;tr3;X3)(e))

Definition: State3-prc
State3-prc(A1;A2;A3;B;init;tr1;Xpr1;tr2;Xpr2;tr3;Xpr3) ==
  TERMOF{State3-locally-programmable:o, 1:l, 1:l} A1 A2 A3 B init tr1 tr2 tr3 Xpr1 Xpr2 Xpr3

Lemma: State3-state-class3
∀[Info,A1,A2,A3,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)].
  (State3(init;tr1;X1;tr2;X2;tr3;X3) = state-class3(init;tr1;X1;tr2;X2;tr3;X3) ∈ EClass(S))

Lemma: Memory3-memory-class3
∀[Info,A1,A2,A3,S:Type]. ∀[init:Id ⟶ S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ S ⟶ S]. ∀[X3:EClass(A3)].
  (Memory3(init;tr1;X1;tr2;X2;tr3;X3) = memory-class3(init;tr1;X1;tr2;X2;tr3;X3) ∈ EClass(S))

Lemma: memory-classrel3-sv
∀[Info,A1,A2,A3,S:Type].
  ∀init:Id ⟶ S. ∀tr1:Id ⟶ A1 ⟶ S ⟶ S. ∀X1:EClass(A1). ∀tr2:Id ⟶ A2 ⟶ S ⟶ S. ∀X2:EClass(A2). ∀tr3:Id
                                                                                                        ⟶ A3
                                                                                                        ⟶ S
                                                                                                        ⟶ S.
  ∀X3:EClass(A3). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (disjoint-classrel(es;A2;X2;A3;X3)
    ⇒ disjoint-classrel(es;A3;X3;A1;X1)
    ⇒ disjoint-classrel(es;A2;X2;A1;X1)
    ⇒ single-valued-classrel(es;X3;A3)
    ⇒ single-valued-classrel(es;X2;A2)
    ⇒ single-valued-classrel(es;X1;A1)
    ⇒ (v ∈ memory-class3(init;tr1;X1;tr2;X2;tr3;X3)(e)
       ⇐⇒ prior-iterated-classrel(es;A1 + A2 + A3;S;v;X1 (+) X2 (+) X3;tr1 + tr2 + tr3 loc(e);λloc.{init loc};e)))

Lemma: memory-classrel2-sv
∀[Info,A1,A2,S:Type].
  ∀init:Id ⟶ S. ∀tr1:Id ⟶ A1 ⟶ S ⟶ S. ∀X1:EClass(A1). ∀tr2:Id ⟶ A2 ⟶ S ⟶ S. ∀X2:EClass(A2). ∀es:EO+(Info). ∀e:E.
  ∀v:S.
    (disjoint-classrel(es;A2;X2;A1;X1)
    ⇒ single-valued-classrel(es;X2;A2)
    ⇒ single-valued-classrel(es;X1;A1)
    ⇒ (v ∈ memory-class2(init;tr1;X1;tr2;X2)(e)
       ⇐⇒ prior-iterated-classrel(es;A1 + A2;S;v;X1 (+) X2;tr1 + tr2 loc(e);λloc.{init loc};e)))

Lemma: memory-classrel1-sv
∀[Info,A1,S:Type].
  ∀init:Id ⟶ S. ∀tr1:Id ⟶ A1 ⟶ S ⟶ S. ∀X1:EClass(A1). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (single-valued-classrel(es;X1;A1)
    ⇒ (v ∈ memory-class1(initially init
                          applying tr1
                          on X1)(e)
       ⇐⇒ prior-iterated-classrel(es;A1;S;v;X1;tr1 loc(e);λloc.{init loc};e)))

Lemma: memory-class3-functional
∀[Info,A1,A2,A3,B:Type]. ∀[init:Id ⟶ B]. ∀[tr1:Id ⟶ A1 ⟶ B ⟶ B]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ B ⟶ B].
∀[X2:EClass(A2)]. ∀[tr3:Id ⟶ A3 ⟶ B ⟶ B]. ∀[X3:EClass(A3)]. ∀[es:EO+(Info)].
  (memory-class3(init;tr1;X1;tr2;X2;tr3;X3) is functional) supposing 
     (single-valued-classrel(es;X1;A1) and 
     single-valued-classrel(es;X2;A2) and 
     single-valued-classrel(es;X3;A3) and 
     disjoint-classrel(es;A1;X1;A2;X2) and 
     disjoint-classrel(es;A1;X1;A3;X3) and 
     disjoint-classrel(es;A2;X2;A3;X3))

Lemma: rec-bind-classrel1
∀[Info,A,B:Type]. ∀[X:A ⟶ EClass(B)]. ∀[Y:A ⟶ EClass(A)].
  ∀[es:EO+(Info)]. ∀[e:E]. ∀[a:A]. ∀[v:B].
    uiff(v ∈ rec-bind-class(X;Y) a(e);↓v ∈ X a(e)
                                       ∨ (∃e':E. ∃a':A. (e' ≤loc e  ∧ a' ∈ Y a(e') ∧ v ∈ rec-bind-class(X;Y) a'(e)))) 
  supposing not-self-starting{i:l}(Info;A;Y)

Lemma: rec-bind-classrel2
∀[Info,A,B:Type]. ∀[X:A ⟶ EClass(B)]. ∀[Y:A ⟶ EClass(A)].
  ∀[es:EO+(Info)]. ∀[e:E]. ∀[a:A]. ∀[v:B].
    uiff(v ∈ rec-bind-class(X;Y) a(e);↓v ∈ X a(e)
                                       ∨ (∃a':A. (a' ∈ Y a(e) ∧ v ∈ X a'(e)))
                                       ∨ (∃e':E. ∃a':A. ((e' <loc e) ∧ a' ∈ Y a(e') ∧ v ∈ rec-bind-class(X;Y) a'(e)))) 
  supposing not-self-starting{i:l}(Info;A;Y)

Lemma: guard_functionality_wrt_iff
∀p,q:ℙ.  ({p ⇐⇒ q} ⇒ {{p} ⇐⇒ {q}})

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



Home Index