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