---

Step * 3 1 3 3 of Lemma consensus-refinement2


1. V : Type
2. ∀x,y:ts-reachable(consensus-ts3(V)).
     ((x ts-rel(consensus-ts3(V)) y) ⇒ (((λL.cs-ref-map3(L)) x) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) y)))
3. x : ts-reachable(consensus-ts2(V))@i
4. v : V@i
5. x = Decided[v] ∈ consensus-state2(V)@i
⊢ [INITIAL] ts-rel(consensus-ts3(V)) [CONSIDERING[v]]
BY
{ (RepUR ``consensus-ts3 ts-rel ts-init`` 0 THEN (OrRight THEN Auto) THEN InstConcl [⌈0⌉]⋅ THEN Reduce 0) }

1
.....wf..... 
1. V : Type
2. ∀x,y:ts-reachable(consensus-ts3(V)).
     ((x ts-rel(consensus-ts3(V)) y) ⇒ (((λL.cs-ref-map3(L)) x) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) y)))
3. x : ts-reachable(consensus-ts2(V))@i
4. v : V@i
5. x = Decided[v] ∈ consensus-state2(V)@i
6. 1 = 1 ∈ ℤ
⊢ 0 ∈ ℕ1

2
1. V : Type
2. ∀x,y:ts-reachable(consensus-ts3(V)).
     ((x ts-rel(consensus-ts3(V)) y) ⇒ (((λL.cs-ref-map3(L)) x) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) y)))
3. x : ts-reachable(consensus-ts2(V))@i
4. v : V@i
5. x = Decided[v] ∈ consensus-state2(V)@i
6. 1 = 1 ∈ ℤ
⊢ (∀j:ℕ1. ((¬(j = 0 ∈ ℤ)) ⇒ ([CONSIDERING[v]][j] = [INITIAL][j] ∈ consensus-state3(V))))
∧ (((INITIAL = INITIAL ∈ consensus-state3(V))
  ∧ ((CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))
    ∨ (∃v@0:V
        ((CONSIDERING[v] = CONSIDERING[v@0] ∈ consensus-state3(V))
        ∧ (∀j:ℕ0
             (([INITIAL][j] = WITHDRAWN ∈ consensus-state3(V))
             ∨ ([INITIAL][j] = CONSIDERING[v@0] ∈ consensus-state3(V))
             ∨ ([INITIAL][j] = COMMITED[v@0] ∈ consensus-state3(V))))))))
  ∨ (∃v@0:V
      ((INITIAL = CONSIDERING[v@0] ∈ consensus-state3(V))
      ∧ ((CONSIDERING[v] = COMMITED[v@0] ∈ consensus-state3(V)) ∨ (CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V))))))

3
.....wf..... 
1. V : Type
2. ∀x,y:ts-reachable(consensus-ts3(V)).
     ((x ts-rel(consensus-ts3(V)) y) ⇒ (((λL.cs-ref-map3(L)) x) (ts-rel(consensus-ts2(V))^*) ((λL.cs-ref-map3(L)) y)))
3. x : ts-reachable(consensus-ts2(V))@i
4. v : V@i
5. x = Decided[v] ∈ consensus-state2(V)@i
6. 1 = 1 ∈ ℤ
7. i : ℕ1
⊢ (∀j:ℕ1. ((¬(j = i ∈ ℤ)) ⇒ ([CONSIDERING[v]][j] = [INITIAL][j] ∈ consensus-state3(V))))
  ∧ ((([INITIAL][i] = INITIAL ∈ consensus-state3(V))
    ∧ (([CONSIDERING[v]][i] = WITHDRAWN ∈ consensus-state3(V))
      ∨ (∃v@0:V
          (([CONSIDERING[v]][i] = CONSIDERING[v@0] ∈ consensus-state3(V))
          ∧ (∀j:ℕi
               (([INITIAL][j] = WITHDRAWN ∈ consensus-state3(V))
               ∨ ([INITIAL][j] = CONSIDERING[v@0] ∈ consensus-state3(V))
               ∨ ([INITIAL][j] = COMMITED[v@0] ∈ consensus-state3(V))))))))
    ∨ (∃v@0:V
        (([INITIAL][i] = CONSIDERING[v@0] ∈ consensus-state3(V))
        ∧ (([CONSIDERING[v]][i] = COMMITED[v@0] ∈ consensus-state3(V))
          ∨ ([CONSIDERING[v]][i] = WITHDRAWN ∈ consensus-state3(V)))))) ∈ ℙ

---

Latex:



1.  V  :  Type
2.  \mforall{}x,y:ts-reachable(consensus-ts3(V)).
          ((x  ts-rel(consensus-ts3(V))  y)
          {}\mRightarrow{}  (((\mlambda{}L.cs-ref-map3(L))  x)  (ts-rel(consensus-ts2(V))\^{}*)  ((\mlambda{}L.cs-ref-map3(L))  y)))
3.  x  :  ts-reachable(consensus-ts2(V))@i
4.  v  :  V@i
5.  x  =  Decided[v]@i
\mvdash{}  [INITIAL]  ts-rel(consensus-ts3(V))  [CONSIDERING[v]]


By

(RepUR  ``consensus-ts3  ts-rel  ts-init``  0
  THEN  (OrRight  THEN  Auto)
  THEN  InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}
  THEN  Reduce  0)

---

Home Index