---

Step * 2 of Lemma consensus-refinement1


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)
BY
{ (All (RepUR ``consensus-ts1 consensus-ts2 ts-type ts-reachable ts-rel ts-init``)
   THEN DVar `x'
   THEN DVar `y'
   THEN SplitOrHyps
   THEN ExRepD
   THEN (Subst' cs-is-decided(x) ~ ff 0
         THENL [(Auto
                 THEN (ElimVar `x' ⋅ THENA Auto)
                 THEN RepUR ``cs-is-decided cs-ambivalent cs-predecided`` 0
                 THEN Auto
                 THEN RepUR ``consensus-state2`` 0
                 THEN Auto)
               ; (Reduce 0 THEN Auto)]
   )⋅
   THEN Try (SplitOrHyps)
   THEN Try ((ElimVar `y'
              ⋅
              THENA (Try (Complete (Auto))
                     THEN (D -1 THEN RepUR ``cs-is-decided`` 0)
                     THEN Auto
                     THEN Fold `cs-decided` 0
                     THEN Auto)
              ))
   THEN RepUR ``cs-is-decided cs-predecided cs-decided cs-ambivalent`` 0
   THEN Try (Fold `cs-decided` 0)
   THEN Auto
   THEN Try (((BLemma `rel_rel_star` THEN RepUR ``infix_ap`` 0) THEN Auto))) }

---

Latex:



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
\mvdash{}  ((\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)


By

(All  (RepUR  ``consensus-ts1  consensus-ts2  ts-type  ts-reachable  ts-rel  ts-init``)
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  (Subst'  cs-is-decided(x)  \msim{}  ff  0
              THENL  [(Auto
                              THEN  (ElimVar  `x'  \mcdot{}  THENA  Auto)
                              THEN  RepUR  ``cs-is-decided  cs-ambivalent  cs-predecided``  0
                              THEN  Auto
                              THEN  RepUR  ``consensus-state2``  0
                              THEN  Auto)
                          ;  (Reduce  0  THEN  Auto)]
  )\mcdot{}
  THEN  Try  (SplitOrHyps)
  THEN  Try  ((ElimVar  `y'
                        \mcdot{}
                        THENA  (Try  (Complete  (Auto))
                                      THEN  (D  -1  THEN  RepUR  ``cs-is-decided``  0)
                                      THEN  Auto
                                      THEN  Fold  `cs-decided`  0
                                      THEN  Auto)
                        ))
  THEN  RepUR  ``cs-is-decided  cs-predecided  cs-decided  cs-ambivalent``  0
  THEN  Try  (Fold  `cs-decided`  0)
  THEN  Auto
  THEN  Try  (((BLemma  `rel\_rel\_star`  THEN  RepUR  ``infix\_ap``  0)  THEN  Auto)))

---

Home Index