---

Step * of Lemma consensus-refinement5

∀[V:Type]
  ∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.
    ((1 < ||W|| ∧ two-intersection(A;W))
    ⇒ ts-refinement(consensus-ts5(V;A;W);consensus-ts6(V;A;W);λs.cs-events-to-state(A; s)))
BY
{ (Auto THEN D 0) }

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
⊢ ts-init(consensus-ts5(V;A;W)) 
  (ts-rel(consensus-ts5(V;A;W))^*) 
  ((λs.cs-events-to-state(A; s)) ts-init(consensus-ts6(V;A;W)))

2
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
⊢ (∀x,y:ts-reachable(consensus-ts6(V;A;W)).
     ((x ts-rel(consensus-ts6(V;A;W)) y)
     ⇒ (((λs.cs-events-to-state(A; s)) x) (ts-rel(consensus-ts5(V;A;W))^*) ((λs.cs-events-to-state(A; s)) y))))
∧ (∀x:ts-reachable(consensus-ts5(V;A;W))
     ((ts-final(consensus-ts5(V;A;W)) x)
     ⇒ (∃y:ts-reachable(consensus-ts6(V;A;W))
          ((ts-final(consensus-ts6(V;A;W)) y)
          ∧ (((λs.cs-events-to-state(A; s)) y) = x ∈ ts-type(consensus-ts5(V;A;W)))))))

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
        ((1  <  ||W||  \mwedge{}  two-intersection(A;W))
        {}\mRightarrow{}  ts-refinement(consensus-ts5(V;A;W);consensus-ts6(V;A;W);\mlambda{}s.cs-events-to-state(A;  s)))


By

(Auto  THEN  D  0)

---

Home Index