Step
*
1
3
1
1
of Lemma
consensus-refinement3
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. ∀L:V List. Dec(∃v:V. (¬(v ∈ L)))@i
5. A : Id List@i
6. a : Id
7. (a ∈ A)
8. W : {a:Id| (a ∈ A)} List List@i
9. ||W|| ≥ 1
10. two-intersection(A;W)@i
11. f : ConsensusState ─→ (consensus-state3(V) List)@i
12. cs-ref-map-constraints(V;A;W;f)@i
13. ∀x,y:ts-reachable(consensus-ts4(V;A;W)).
((x ts-rel(consensus-ts4(V;A;W)) y)
⇒ ((f x) (ts-rel(consensus-ts3(V))^*) (f y)))
14. x : ts-reachable(consensus-ts3(V))@i
15. v : V@i
16. x = [COMMITED[v]] ∈ (consensus-state3(V) List)@i
⊢ ts-final(consensus-ts4(V;A;W)) (λa.<0, 0 : v>)
BY
{ (RepUR ``ts-final consensus-ts4 cs-inning cs-estimate`` 0 THEN InstConcl [⌈v⌉]⋅ THEN Auto) }
Latex:
1. [V] : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. \{\mexists{}v,v':V. (\mneg{}(v = v'))\}@i
4. \mforall{}L:V List. Dec(\mexists{}v:V. (\mneg{}(v \mmember{} L)))@i
5. A : Id List@i
6. a : Id
7. (a \mmember{} A)
8. W : \{a:Id| (a \mmember{} A)\} List List@i
9. ||W|| \mgeq{} 1
10. two-intersection(A;W)@i
11. f : ConsensusState {}\mrightarrow{} (consensus-state3(V) List)@i
12. cs-ref-map-constraints(V;A;W;f)@i
13. \mforall{}x,y:ts-reachable(consensus-ts4(V;A;W)).
((x ts-rel(consensus-ts4(V;A;W)) y) {}\mRightarrow{} ((f x) (ts-rel(consensus-ts3(V))\^{}*) (f y)))
14. x : ts-reachable(consensus-ts3(V))@i
15. v : V@i
16. x = [COMMITED[v]]@i
\mvdash{} ts-final(consensus-ts4(V;A;W)) (\mlambda{}a.ɘ, 0 : v>)
By
(RepUR ``ts-final consensus-ts4 cs-inning cs-estimate`` 0 THEN InstConcl [\mkleeneopen{}v\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index