---

Step * 3 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. ts-final(consensus-ts1(V)) x@i
⊢ ∃y:ts-reachable(consensus-ts2(V))
   ((ts-final(consensus-ts2(V)) y)
   ∧ (((λx.if cs-is-decided(x) then x else UNDECIDED fi ) y) = x ∈ ts-type(consensus-ts1(V))))
BY
{ (RepUR ``ts-final consensus-ts1`` -1 THEN Reduce 0 THEN ExRepD THEN InstConcl [⌈Decided[v]⌉]⋅ THEN Auto) }

1
.....wf..... 
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
⊢ Decided[v] ∈ ts-reachable(consensus-ts2(V))

2
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
⊢ ts-final(consensus-ts2(V)) Decided[v]

3
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. ts-final(consensus-ts2(V)) Decided[v]
⊢ if cs-is-decided(Decided[v]) then Decided[v] else UNDECIDED fi  = x ∈ ts-type(consensus-ts1(V))

4
.....wf..... 
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
⊢ cs-is-decided(y) ∈ 𝔹

5
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))

---

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.  ts-final(consensus-ts1(V))  x@i
\mvdash{}  \mexists{}y:ts-reachable(consensus-ts2(V))
      ((ts-final(consensus-ts2(V))  y)  \mwedge{}  (((\mlambda{}x.if  cs-is-decided(x)  then  x  else  UNDECIDED  fi  )  y)  =  x))


By

(RepUR  ``ts-final  consensus-ts1``  -1
  THEN  Reduce  0
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}Decided[v]\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index