---

Step * 3 1 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))^*) [COMMITED[v]]
BY
{ ((Using [`y',⌈[CONSIDERING[v]]⌉] (BLemma `rel_star_transitivity`)⋅
    THENA Try (Complete ((Auto THEN RepUR ``consensus-ts3 ts-type`` 0 THEN Auto)))
    )
   THEN Try ((BLemma `rel_rel_star` THENA Try (Complete ((Auto THEN RepUR ``consensus-ts3 ts-type`` 0 THEN Auto)))))
   ) }

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
⊢ [INITIAL] ∈ ts-type(consensus-ts3(V))

2
.....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
⊢ [INITIAL] ∈ ts-type(consensus-ts3(V))

3
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]]

4
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
⊢ [CONSIDERING[v]] ts-rel(consensus-ts3(V)) [COMMITED[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]  rel\_star(ts-type(consensus-ts3(V));  ts-rel(consensus-ts3(V)))  [COMMITED[v]]


By

((Using  [`y',\mkleeneopen{}[CONSIDERING[v]]\mkleeneclose{}]  (BLemma  `rel\_star\_transitivity`)\mcdot{}
    THENA  Try  (Complete  ((Auto  THEN  RepUR  ``consensus-ts3  ts-type``  0  THEN  Auto)))
    )
  THEN  Try  ((BLemma  `rel\_rel\_star`
                        THENA  Try  (Complete  ((Auto  THEN  RepUR  ``consensus-ts3  ts-type``  0  THEN  Auto)))
                        ))
  )

---

Home Index