---

Step * 1 of Lemma consensus-refinement1


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)))
BY
{ (BLemma `rel_star_weakening`
   THEN Auto
   THEN RepUR ``consensus-ts1 consensus-ts2 ts-init ts-type cs-is-decided cs-ambivalent`` 0
   THEN Auto) }

---

Latex:



1.  [V]  :  Type
\mvdash{}  ts-init(consensus-ts1(V)) 
    rel\_star(ts-type(consensus-ts1(V));  ts-rel(consensus-ts1(V))) 
    ((\mlambda{}x.if  cs-is-decided(x)  then  x  else  UNDECIDED  fi  )  ts-init(consensus-ts2(V)))


By

(BLemma  `rel\_star\_weakening`
  THEN  Auto
  THEN  RepUR  ``consensus-ts1  consensus-ts2  ts-init  ts-type  cs-is-decided  cs-ambivalent``  0
  THEN  Auto)

---

Home Index