Step
*
3
1
3
of Lemma
consensus-ts5-archive-invariant
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)} List List@i
8. x1 : ConsensusState@i
9. x2 : Knowledge(ConsensusState)@i
10. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
11. y1 : ConsensusState@i
12. y2 : Knowledge(ConsensusState)@i
13. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
14. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
(state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i
15. a : {a:Id| (a ∈ A)} @i
16. ∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id))
⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
17. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
18. Estimate(y1;a) = Estimate(x1;a) ∈ i:ℤ fp-> V@i
19. b1 : {a:Id| (a ∈ A)} @i
20. i1 : ℤ@i
21. i1 ≤ Inning(x1;b1)@i
22. ((∀j:ℤ. (j < i1
⇒ (¬↑j ∈ dom(Estimate(x1;b1)))))
∧ (Knowledge(y2;a) = b1 : <i1, inr ⋅ > ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
∨ (∃j:ℤ
(j < i1
∧ (↑j ∈ dom(Estimate(x1;b1)))
∧ (∀k:ℤ. (j < k
⇒ k < i1
⇒ (¬↑k ∈ dom(Estimate(x1;b1)))))
∧ (Knowledge(y2;a) = b1 : <i1, inl <j, Estimate(x1;b1)(j)>> ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
23. v : V@i
24. b : {a:Id| (a ∈ A)} @i
25. i : ℤ@i
26. ↑i ∈ dom(Estimate(y1;b))
27. Estimate(y1;b)(i) = v ∈ V
⊢ state y1 may consider v in inning i
BY
{ OnMaybeHyp 14 (\h. ((InstHyp [⌈v⌉;⌈b⌉;⌈i⌉] h⋅
THENA Complete ((Auto
THEN Decide b = a ∈ Id
THEN Auto
THEN (Assert Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V BY
Auto)
THEN Auto))
)
THEN RepeatFor 6 (ParallelLast)
)) }
1
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)} List List@i
8. x1 : ConsensusState@i
9. x2 : Knowledge(ConsensusState)@i
10. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
11. y1 : ConsensusState@i
12. y2 : Knowledge(ConsensusState)@i
13. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
14. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
(state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i
15. a : {a:Id| (a ∈ A)} @i
16. ∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id))
⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
17. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
18. Estimate(y1;a) = Estimate(x1;a) ∈ i:ℤ fp-> V@i
19. b1 : {a:Id| (a ∈ A)} @i
20. i1 : ℤ@i
21. i1 ≤ Inning(x1;b1)@i
22. ((∀j:ℤ. (j < i1
⇒ (¬↑j ∈ dom(Estimate(x1;b1)))))
∧ (Knowledge(y2;a) = b1 : <i1, inr ⋅ > ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
∨ (∃j:ℤ
(j < i1
∧ (↑j ∈ dom(Estimate(x1;b1)))
∧ (∀k:ℤ. (j < k
⇒ k < i1
⇒ (¬↑k ∈ dom(Estimate(x1;b1)))))
∧ (Knowledge(y2;a) = b1 : <i1, inl <j, Estimate(x1;b1)(j)>> ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
23. v : V@i
24. b : {a:Id| (a ∈ A)} @i
25. i : ℤ@i
26. ↑i ∈ dom(Estimate(y1;b))
27. Estimate(y1;b)(i) = v ∈ V
28. ws : {a:Id| (a ∈ A)} List
29. (ws ∈ W)
30. ∀ws':{a:Id| (a ∈ A)} List. ((ws' ∈ W)
⇒ (¬in state x1, ws' blocks ws from archiving v in inning i))
31. ∀b:{a:Id| (a ∈ A)} . ((b ∈ ws)
⇒ (i ≤ Inning(x1;b)))
32. b2 : {a:Id| (a ∈ A)} @i
33. (b2 ∈ ws)@i
34. i ≤ Inning(x1;b2)
⊢ i ≤ Inning(y1;b2)
2
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)} List List@i
8. x1 : ConsensusState@i
9. x2 : Knowledge(ConsensusState)@i
10. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
11. y1 : ConsensusState@i
12. y2 : Knowledge(ConsensusState)@i
13. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
14. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
(state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i
15. a : {a:Id| (a ∈ A)} @i
16. ∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id))
⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
17. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
18. Estimate(y1;a) = Estimate(x1;a) ∈ i:ℤ fp-> V@i
19. b1 : {a:Id| (a ∈ A)} @i
20. i1 : ℤ@i
21. i1 ≤ Inning(x1;b1)@i
22. ((∀j:ℤ. (j < i1
⇒ (¬↑j ∈ dom(Estimate(x1;b1)))))
∧ (Knowledge(y2;a) = b1 : <i1, inr ⋅ > ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
∨ (∃j:ℤ
(j < i1
∧ (↑j ∈ dom(Estimate(x1;b1)))
∧ (∀k:ℤ. (j < k
⇒ k < i1
⇒ (¬↑k ∈ dom(Estimate(x1;b1)))))
∧ (Knowledge(y2;a) = b1 : <i1, inl <j, Estimate(x1;b1)(j)>> ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
23. v : V@i
24. b : {a:Id| (a ∈ A)} @i
25. i : ℤ@i
26. ↑i ∈ dom(Estimate(y1;b))
27. Estimate(y1;b)(i) = v ∈ V
28. ws : {a:Id| (a ∈ A)} List
29. (ws ∈ W)
30. ∀b:{a:Id| (a ∈ A)} . ((b ∈ ws)
⇒ (i ≤ Inning(x1;b)))
31. ∀ws':{a:Id| (a ∈ A)} List. ((ws' ∈ W)
⇒ (¬in state x1, ws' blocks ws from archiving v in inning i))
32. ws' : {a:Id| (a ∈ A)} List@i
33. (ws' ∈ W)@i
34. ¬in state x1, ws' blocks ws from archiving v in inning i
⊢ ¬in state y1, ws' blocks ws from archiving v in inning i
Latex:
1. [V] : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. v1 : V@i
4. v' : V@i
5. \mneg{}(v1 = v')@i
6. A : Id List@i
7. W : \{a:Id| (a \mmember{} A)\} List List@i
8. x1 : ConsensusState@i
9. x2 : Knowledge(ConsensusState)@i
10. \mbackslash{}\mbackslash{}\%3 : ts-init(consensus-ts5(V;A;W))
(ts-rel(consensus-ts5(V;A;W))\^{}*)
<x1, x2>@i
11. y1 : ConsensusState@i
12. y2 : Knowledge(ConsensusState)@i
13. \mbackslash{}\mbackslash{}\%5 : ts-init(consensus-ts5(V;A;W))
(ts-rel(consensus-ts5(V;A;W))\^{}*)
<y1, y2>@i
14. \mforall{}v:V. \mforall{}b:\{a:Id| (a \mmember{} A)\} . \mforall{}i:\mBbbZ{}.
(state x1 may consider v in inning i) supposing
((Estimate(x1;b)(i) = v) and
(\muparrow{}i \mmember{} dom(Estimate(x1;b))))@i
15. a : \{a:Id| (a \mmember{} A)\} @i
16. \mforall{}b:\{a:Id| (a \mmember{} A)\}
((\mneg{}(b = a))
{}\mRightarrow{} ((Inning(y1;b) = Inning(x1;b))
\mwedge{} (Estimate(y1;b) = Estimate(x1;b))
\mwedge{} (Knowledge(y2;b) = Knowledge(x2;b))))@i
17. Inning(y1;a) = Inning(x1;a)@i
18. Estimate(y1;a) = Estimate(x1;a)@i
19. b1 : \{a:Id| (a \mmember{} A)\} @i
20. i1 : \mBbbZ{}@i
21. i1 \mleq{} Inning(x1;b1)@i
22. ((\mforall{}j:\mBbbZ{}. (j < i1 {}\mRightarrow{} (\mneg{}\muparrow{}j \mmember{} dom(Estimate(x1;b1)))))
\mwedge{} (Knowledge(y2;a) = b1 : <i1, inr \mcdot{} > \moplus{} Knowledge(x2;a)))
\mvee{} (\mexists{}j:\mBbbZ{}
(j < i1
\mwedge{} (\muparrow{}j \mmember{} dom(Estimate(x1;b1)))
\mwedge{} (\mforall{}k:\mBbbZ{}. (j < k {}\mRightarrow{} k < i1 {}\mRightarrow{} (\mneg{}\muparrow{}k \mmember{} dom(Estimate(x1;b1)))))
\mwedge{} (Knowledge(y2;a) = b1 : <i1, inl <j, Estimate(x1;b1)(j)>> \moplus{} Knowledge(x2;a))))@i
23. v : V@i
24. b : \{a:Id| (a \mmember{} A)\} @i
25. i : \mBbbZ{}@i
26. \muparrow{}i \mmember{} dom(Estimate(y1;b))
27. Estimate(y1;b)(i) = v
\mvdash{} state y1 may consider v in inning i
By
OnMaybeHyp 14 (\mbackslash{}h. ((InstHyp [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}] h\mcdot{}
THENA Complete ((Auto
THEN Decide b = a
THEN Auto
THEN (Assert Estimate(y1;b) = Estimate(x1;b) BY
Auto)
THEN Auto))
)
THEN RepeatFor 6 (ParallelLast)
))
Home
Index