---

Step * 3 5 of Lemma consensus-refinement1


1. V : Type
2. ∀x,y:ts-reachable(consensus-ts2(V)).
     ((x ts-rel(consensus-ts2(V)) y)
     ⇒ (((λx.if cs-is-decided(x) then x else UNDECIDED fi ) x) 
         (ts-rel(consensus-ts1(V))^*) 
         ((λx.if cs-is-decided(x) then x else UNDECIDED fi ) y)))
3. x : ts-reachable(consensus-ts1(V))@i
4. v : V@i
5. x = Decided[v] ∈ consensus-state1(V)@i
6. y : ts-reachable(consensus-ts2(V))
7. ts-final(consensus-ts2(V)) y
8. cs-is-decided(y) ∈ 𝔹
9. ↑cs-is-decided(y)
⊢ y ∈ ts-type(consensus-ts1(V))
BY
{ DVar `y' }

1
1. V : Type
2. ∀x,y:ts-reachable(consensus-ts2(V)).
     ((x ts-rel(consensus-ts2(V)) y)
     ⇒ (((λx.if cs-is-decided(x) then x else UNDECIDED fi ) x) 
         (ts-rel(consensus-ts1(V))^*) 
         ((λx.if cs-is-decided(x) then x else UNDECIDED fi ) y)))
3. x : ts-reachable(consensus-ts1(V))@i
4. v : V@i
5. x = Decided[v] ∈ consensus-state1(V)@i
6. y : ts-type(consensus-ts2(V))
7. ts-init(consensus-ts2(V)) (ts-rel(consensus-ts2(V))^*) y
8. ts-final(consensus-ts2(V)) y
9. cs-is-decided(y) ∈ 𝔹
10. ↑cs-is-decided(y)
⊢ y ∈ ts-type(consensus-ts1(V))

---

Latex:



1.  V  :  Type
2.  \mforall{}x,y:ts-reachable(consensus-ts2(V)).
          ((x  ts-rel(consensus-ts2(V))  y)
          {}\mRightarrow{}  (((\mlambda{}x.if  cs-is-decided(x)  then  x  else  UNDECIDED  fi  )  x) 
                  rel\_star(ts-type(consensus-ts1(V));  ts-rel(consensus-ts1(V))) 
                  ((\mlambda{}x.if  cs-is-decided(x)  then  x  else  UNDECIDED  fi  )  y)))
3.  x  :  ts-reachable(consensus-ts1(V))@i
4.  v  :  V@i
5.  x  =  Decided[v]@i
6.  y  :  ts-reachable(consensus-ts2(V))
7.  ts-final(consensus-ts2(V))  y
8.  cs-is-decided(y)  \mmember{}  \mBbbB{}
9.  \muparrow{}cs-is-decided(y)
\mvdash{}  y  \mmember{}  ts-type(consensus-ts1(V))


By

DVar  `y'

---

Home Index