---

Step * of Lemma consensus-refinement1

∀[V:Type]. ts-refinement(consensus-ts1(V);consensus-ts2(V);λx.if cs-is-decided(x) then x else UNDECIDED fi )
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. [V] : Type
⊢ ts-init(consensus-ts1(V)) 
  (ts-rel(consensus-ts1(V))^*) 
  ((λx.if cs-is-decided(x) then x else UNDECIDED fi ) ts-init(consensus-ts2(V)))

2
1. [V] : Type
2. x : ts-reachable(consensus-ts2(V))@i
3. y : ts-reachable(consensus-ts2(V))@i
4. x ts-rel(consensus-ts2(V)) y@i
⊢ ((λ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
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))))

---

Latex:


\mforall{}[V:Type]
    ts-refinement(consensus-ts1(V);consensus-ts2(V);\mlambda{}x.if  cs-is-decided(x)  then  x  else  UNDECIDED  fi  )


By

(Auto  THEN  D  0  THEN  Auto)

---

Home Index