Step
*
2
1
of Lemma
consensus-refinement5
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)} List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
⊢ ∀x,y:ts-reachable(consensus-ts6(V;A;W)).
((x ts-rel(consensus-ts6(V;A;W)) y)
⇒ (((λs.cs-events-to-state(A; s)) x) (ts-rel(consensus-ts5(V;A;W))^*) ((λs.cs-events-to-state(A; s)) y)))
BY
{ ((Auto THEN Reduce 0)
THEN (Assert (x ∈ ts-reachable(consensus-ts6(V;A;W))) ∧ (y ∈ ts-reachable(consensus-ts6(V;A;W))) BY
Auto)
THEN (D -4 THEN Thin (-4))
THEN (D -3 THEN Thin (-3))
THEN RepUR ``ts-type consensus-ts6 consensus-state6`` -4
THEN RepUR ``ts-type consensus-ts6 consensus-state6`` -3
THEN RepUR ``consensus-ts5 ts-rel ts-type`` 0
THEN RepUR ``consensus-ts6 ts-rel one-consensus-event consensus-event-constraint`` -2
THEN ExRepD
THEN (InstLemma `consensus-event-cases` [⌈V⌉;⌈A⌉;⌈e⌉]⋅ THENA Auto)
THEN (((SplitOrHyps
THEN ExRepD
THEN (BLemma `rel_rel_star` THEN Auto)
THEN RepUR ``infix_ap`` 0
THEN (With ⌈a⌉ (D 0)⋅ THENA Auto)
THEN (RepUR ``consensus-rel-knowledge-step`` 0
THEN RepUR ``cs-inning cs-estimate cs-knowledge cs-events-to-state`` 0
THEN Reduce 0
THEN D 0)
THEN Try ((RepeatFor 2 ((D 0 THENA Auto))⋅
THEN RenameVar `Z' (-2)
THEN (GenConclTerm ⌈consensus-accum-state(A;y Z)⌉⋅ THENA Auto)
THEN RenameVar `c' (-2)
THEN RepeatFor 2 (D (-2))
THEN Reduce 0
THEN Subst' consensus-accum-state(A;x Z)
= <c1, c3, c4>
∈ (ℤ × j:ℤ fp-> V × b:Id fp-> ℤ × (ℤ × V + Top)) 0
THEN Reduce 0
THEN Auto
THEN RepeatFor 2 (D (-2))
THEN Reduce 0
THEN Auto)))
THENL [Sel 1 (D 0); Sel 2 (D 0); Sel 3 (D 0)]
)
THENA Auto
)
THEN ((UnfoldTopAb 0 THEN RepUR ``cs-inning cs-estimate cs-knowledge`` 0)
THEN AllHyps h.((InstHyp [⌈v⌉] h⋅ THENA Complete (Auto)) THEN MoveToConcl (-1))
THEN (GenConcl ⌈consensus-accum-state(A;x a) = X ∈ (ℤ × j:ℤ fp-> V × b:Id fp-> ℤ × (ℤ × V + Top))⌉⋅ THENA Auto)
THEN (GenConcl ⌈consensus-accum-state(A;y a) = Y ∈ (ℤ × j:ℤ fp-> V × b:Id fp-> ℤ × (ℤ × V + Top))⌉⋅ THENA Auto)
THEN OnMaybeHyp 11 (\h.
UnitProgress ((((HypSubst' h (-1) THENM HypSubst' (-5) (-1)) THENA Auto)
THEN Unfold `consensus-accum-state` -1
THEN (RWO "list_accum_append" (-1) THENA Auto)
THEN Fold `consensus-accum-state` (-1)
THEN (HypSubst' (-3) (-1) THENA Auto)
THEN Try ((Reduce 0 THEN UsingVars [`A'] (BLemma `consensus-accum_wf`) THEN Auto))
THEN RepeatFor 2 (D -4)
THEN RepeatFor 2 (D -2)
THEN All Reduce
THEN RepUR ``consensus-accum inning-event archive-event consensus-message`` -1))⋅)
THEN RepeatFor 2 (AutoSimpHyp Auto (-1))
THEN Auto)⋅) }
1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)} List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
6. x : {a:Id| (a ∈ A)} ─→ (consensus-event(V;A) List)@i
7. y : {a:Id| (a ∈ A)} ─→ (consensus-event(V;A) List)@i
8. a : {a:Id| (a ∈ A)} @i
9. e : consensus-event(V;A)@i
10. ∀v:V
((e = Archive(v) ∈ consensus-event(V;A))
⇒ let i,est,knw = consensus-accum-state(A;x a) in
(¬(i ∈ fpf-domain(est))) ∧ may consider v in inning i based on knowledge (knw))@i
11. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀z:ℕi × V?.
((e = consensus-message(b;i;z) ∈ consensus-event(V;A))
⇒ let i',est,knw = consensus-accum-state(A;x b) in
(i ≤ i')
∧ case z
of inl(p) =>
let j,v = p
in (↑j ∈ dom(est)) ∧ (∀k:ℤ. (j < k ⇒ k < i ⇒ (¬↑k ∈ dom(est)))) ∧ (v = est(j) ∈ V)
| inr(a) =>
∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(est))))@i
12. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a ∈ Id)) ⇒ ((y b) = (x b) ∈ (consensus-event(V;A) List)))@i
13. (y a) = ((x a) @ [e]) ∈ (consensus-event(V;A) List)@i
14. x ∈ ts-reachable(consensus-ts6(V;A;W))
15. y ∈ ts-reachable(consensus-ts6(V;A;W))
16. b : {a:Id| (a ∈ A)}
17. i : ℕ
18. z : ℕi × V?
19. e = consensus-message(b;i;z) ∈ consensus-event(V;A)
20. X1 : ℤ@i
21. X3 : j:ℤ fp-> V@i
22. X4 : b:Id fp-> ℤ × (ℤ × V + Top)@i
23. consensus-accum-state(A;x a) = <X1, X3, X4> ∈ (ℤ × j:ℤ fp-> V × b:Id fp-> ℤ × (ℤ × V + Top))@i
24. Y1 : ℤ@i
25. Y3 : j:ℤ fp-> V@i
26. Y4 : b:Id fp-> ℤ × (ℤ × V + Top)@i
27. X1 = Y1 ∈ ℤ
28. X3 = Y3 ∈ j:ℤ fp-> V
29. b : <i, z> ⊕ X4 = Y4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)
30. Y1 = X1 ∈ ℤ
31. Y3 = X3 ∈ i:ℤ fp-> V
⊢ ∃b:{a:Id| (a ∈ A)}
∃i:ℤ
((i ≤ (fst(let i,est,knw = consensus-accum-state(A;x b) in
<i, est>)))
∧ (((∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>))))) ∧ (Y4 = b : <i, in\000Cr ⋅ > ⊕ X4 ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
∨ (∃j:ℤ
(j < i
∧ (↑j ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in
<i, est>)))
∧ (∀k:ℤ. (j < k ⇒ k < i ⇒ (¬↑k ∈ dom(snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>)))))
∧ (Y4 = b : <i, inl <j, snd(let i,est,knw = consensus-accum-state(A;x b) in <i, est>)(j)>> ⊕ X4 ∈ b:Id fp-> ℤ \000C× (ℤ × V + Top))))))
Latex:
1. [V] : Type
2. A : Id List@i
3. W : \{a:Id| (a \mmember{} A)\} List List@i
4. 1 < ||W||@i
5. two-intersection(A;W)@i
\mvdash{} \mforall{}x,y:ts-reachable(consensus-ts6(V;A;W)).
((x ts-rel(consensus-ts6(V;A;W)) y)
{}\mRightarrow{} (((\mlambda{}s.cs-events-to-state(A; s)) x)
rel\_star(ts-type(consensus-ts5(V;A;W)); ts-rel(consensus-ts5(V;A;W)))
((\mlambda{}s.cs-events-to-state(A; s)) y)))
By
((Auto THEN Reduce 0)
THEN (Assert (x \mmember{} ts-reachable(consensus-ts6(V;A;W))) \mwedge{} (y \mmember{} ts-reachable(consensus-ts6(V;A;W))) BY
Auto)
THEN (D -4 THEN Thin (-4))
THEN (D -3 THEN Thin (-3))
THEN RepUR ``ts-type consensus-ts6 consensus-state6`` -4
THEN RepUR ``ts-type consensus-ts6 consensus-state6`` -3
THEN RepUR ``consensus-ts5 ts-rel ts-type`` 0
THEN RepUR ``consensus-ts6 ts-rel one-consensus-event consensus-event-constraint`` -2
THEN ExRepD
THEN (InstLemma `consensus-event-cases` [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (((SplitOrHyps
THEN ExRepD
THEN (BLemma `rel\_rel\_star` THEN Auto)
THEN RepUR ``infix\_ap`` 0
THEN (With \mkleeneopen{}a\mkleeneclose{} (D 0)\mcdot{} THENA Auto)
THEN (RepUR ``consensus-rel-knowledge-step`` 0
THEN RepUR ``cs-inning cs-estimate cs-knowledge cs-events-to-state`` 0
THEN Reduce 0
THEN D 0)
THEN Try ((RepeatFor 2 ((D 0 THENA Auto))\mcdot{}
THEN RenameVar `Z' (-2)
THEN (GenConclTerm \mkleeneopen{}consensus-accum-state(A;y Z)\mkleeneclose{}\mcdot{} THENA Auto)
THEN RenameVar `c' (-2)
THEN RepeatFor 2 (D (-2))
THEN Reduce 0
THEN Subst' consensus-accum-state(A;x Z) = <c1, c3, c4> 0
THEN Reduce 0
THEN Auto
THEN RepeatFor 2 (D (-2))
THEN Reduce 0
THEN Auto)))
THENL [Sel 1 (D 0); Sel 2 (D 0); Sel 3 (D 0)]
)
THENA Auto
)
THEN ((UnfoldTopAb 0 THEN RepUR ``cs-inning cs-estimate cs-knowledge`` 0)
THEN AllHyps h.((InstHyp [\mkleeneopen{}v\mkleeneclose{}] h\mcdot{} THENA Complete (Auto)) THEN MoveToConcl (-1))
THEN (GenConcl \mkleeneopen{}consensus-accum-state(A;x a) = X\mkleeneclose{}\mcdot{} THENA Auto)
THEN (GenConcl \mkleeneopen{}consensus-accum-state(A;y a) = Y\mkleeneclose{}\mcdot{} THENA Auto)
THEN OnMaybeHyp 11 (\mbackslash{}h.
UnitProgress (
(((HypSubst' h (-1) THENM HypSubst' (-5) (-1)) THENA Auto)
THEN Unfold `consensus-accum-state` -1
THEN (RWO "list\_accum\_append" (-1) THENA Auto)
THEN Fold `consensus-accum-state` (-1)
THEN (HypSubst' (-3) (-1) THENA Auto)
THEN Try ((Reduce 0 THEN UsingVars [`A'] (BLemma `consensus-accum\_wf`) THEN Auto))
THEN RepeatFor 2 (D -4)
THEN RepeatFor 2 (D -2)
THEN All Reduce
THEN RepUR ``consensus-accum inning-event archive-event consensus-message`` -1))\mcdot{})
THEN RepeatFor 2 (AutoSimpHyp Auto (-1))
THEN Auto)\mcdot{})
Home
Index