Step
*
2
2
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:ts-reachable(consensus-ts5(V;A;W))
((ts-final(consensus-ts5(V;A;W)) x)
⇒ (∃y:ts-reachable(consensus-ts6(V;A;W))
((ts-final(consensus-ts6(V;A;W)) y)
∧ (((λs.cs-events-to-state(A; s)) y) = x ∈ ts-type(consensus-ts5(V;A;W))))))
BY
{ (Auto
THEN D -2
THEN (RepUR ``ts-type consensus-ts5`` -3 THEN D -3)
THEN RepUR ``ts-final consensus-ts5`` -1
THEN RepUR ``ts-type consensus-ts5`` 0
THEN ExRepD
THEN (InstConcl [⌈λa.[Archive(v)]⌉]⋅
THENA Try ((Auto THEN D -1 THEN RepUR ``ts-type consensus-ts6`` -2 THEN Auto))
)) }
1
.....wf.....
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. x1 : ConsensusState@i
7. x2 : Knowledge(ConsensusState)@i
8. ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
9. v : V@i
10. ∀a:{a:Id| (a ∈ A)}
((Inning(x1;a) = 0 ∈ ℤ)
∧ (Estimate(x1;a) = 0 : v ∈ i:ℤ fp-> V)
∧ (Knowledge(x2;a) = mk_fpf(A;λb.<0, ff>) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))@i
⊢ λa.[Archive(v)] ∈ ts-reachable(consensus-ts6(V;A;W))
2
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. x1 : ConsensusState@i
7. x2 : Knowledge(ConsensusState)@i
8. \\%4 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
9. v : V@i
10. ∀a:{a:Id| (a ∈ A)}
((Inning(x1;a) = 0 ∈ ℤ)
∧ (Estimate(x1;a) = 0 : v ∈ i:ℤ fp-> V)
∧ (Knowledge(x2;a) = mk_fpf(A;λb.<0, ff>) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))@i
⊢ (ts-final(consensus-ts6(V;A;W)) (λa.[Archive(v)]))
∧ (cs-events-to-state(A; λa.[Archive(v)]) = <x1, x2> ∈ (ConsensusState × Knowledge(ConsensusState)))
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:ts-reachable(consensus-ts5(V;A;W))
((ts-final(consensus-ts5(V;A;W)) x)
{}\mRightarrow{} (\mexists{}y:ts-reachable(consensus-ts6(V;A;W))
((ts-final(consensus-ts6(V;A;W)) y) \mwedge{} (((\mlambda{}s.cs-events-to-state(A; s)) y) = x))))
By
(Auto
THEN D -2
THEN (RepUR ``ts-type consensus-ts5`` -3 THEN D -3)
THEN RepUR ``ts-final consensus-ts5`` -1
THEN RepUR ``ts-type consensus-ts5`` 0
THEN ExRepD
THEN (InstConcl [\mkleeneopen{}\mlambda{}a.[Archive(v)]\mkleeneclose{}]\mcdot{}
THENA Try ((Auto THEN D -1 THEN RepUR ``ts-type consensus-ts6`` -2 THEN Auto))
))
Home
Index