---

Step * 2 of Lemma consensus-refinement5


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)))))))
BY
{ 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
⊢ ∀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)))

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



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  1  <  ||W||@i
5.  two-intersection(A;W)@i
\mvdash{}  (\mforall{}x,y:ts-reachable(consensus-ts6(V;A;W)).
          ((x  ts-rel(consensus-ts6(V;A;W))  y)
          {}\mRightarrow{}  (((\mlambda{}s.cs-events-to-state(A;  s))  x) 
                  rel\_star(ts-type(consensus-ts5(V;A;W));  ts-rel(consensus-ts5(V;A;W))) 
                  ((\mlambda{}s.cs-events-to-state(A;  s))  y))))
\mwedge{}  (\mforall{}x:ts-reachable(consensus-ts5(V;A;W))
          ((ts-final(consensus-ts5(V;A;W))  x)
          {}\mRightarrow{}  (\mexists{}y:ts-reachable(consensus-ts6(V;A;W))
                    ((ts-final(consensus-ts6(V;A;W))  y)  \mwedge{}  (((\mlambda{}s.cs-events-to-state(A;  s))  y)  =  x)))))


By

D  0

---

Home Index