Step
*
3
1
2
2
of Lemma
consensus-ts5-archive-invariant
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v2 : V@i
4. v' : V@i
5. ¬(v2 = 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. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
19. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))@i
20. v1 : V@i
21. may consider v1 in inning Inning(x1;a) based on knowledge (Knowledge(x2;a))@i
22. Estimate(y1;a) = Estimate(x1;a) ⊕ Inning(x1;a) : v1 ∈ i:ℤ fp-> V@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. ¬(v1 = v ∈ V)
⊢ state y1 may consider v in inning i
BY
{ (Assert (↑i ∈ dom(Estimate(x1;b))) ∧ (Estimate(x1;b)(i) = v ∈ V) BY
((Decide b = a ∈ Id THENA Auto)
THEN Try (((Assert Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V BY Complete (Auto)) THEN Auto))
THEN ElimVar `b'
THEN (Assert ↑i ∈ dom(Estimate(x1;a) ⊕ Inning(x1;a) : v1) BY
Auto)
THEN FLemma `fpf-join-single-property` [-1]
THEN Auto
THEN (D 0 THENA Auto)
THEN ElimVar `i'
THEN D -2
THEN (Assert Estimate(x1;a) ⊕ Inning(x1;a) : v1(Inning(x1;a)) = v ∈ V BY
Auto)
THEN (RWO "fpf-join-ap-sq" (-1) THENM SplitOnHypITE -1 THENM Reduce (-2)⋅)
THEN Auto
THEN RWO "member-fpf-domain" (-1)
THEN Auto)) }
1
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. v2 : V@i
4. v' : V@i
5. ¬(v2 = 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. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
19. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))@i
20. v1 : V@i
21. may consider v1 in inning Inning(x1;a) based on knowledge (Knowledge(x2;a))@i
22. Estimate(y1;a) = Estimate(x1;a) ⊕ Inning(x1;a) : v1 ∈ i:ℤ fp-> V@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. ¬(v1 = v ∈ V)
29. (↑i ∈ dom(Estimate(x1;b))) ∧ (Estimate(x1;b)(i) = v ∈ V)
⊢ state y1 may consider v in inning i
Latex:
1. [V] : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. v2 : V@i
4. v' : V@i
5. \mneg{}(v2 = 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. Knowledge(y2;a) = Knowledge(x2;a)@i
19. \mneg{}(Inning(x1;a) \mmember{} fpf-domain(Estimate(x1;a)))@i
20. v1 : V@i
21. may consider v1 in inning Inning(x1;a) based on knowledge (Knowledge(x2;a))@i
22. Estimate(y1;a) = Estimate(x1;a) \moplus{} Inning(x1;a) : v1@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
28. \mneg{}(v1 = v)
\mvdash{} state y1 may consider v in inning i
By
(Assert (\muparrow{}i \mmember{} dom(Estimate(x1;b))) \mwedge{} (Estimate(x1;b)(i) = v) BY
((Decide b = a THENA Auto)
THEN Try (((Assert Estimate(y1;b) = Estimate(x1;b) BY Complete (Auto)) THEN Auto))
THEN ElimVar `b'
THEN (Assert \muparrow{}i \mmember{} dom(Estimate(x1;a) \moplus{} Inning(x1;a) : v1) BY
Auto)
THEN FLemma `fpf-join-single-property` [-1]
THEN Auto
THEN (D 0 THENA Auto)
THEN ElimVar `i'
THEN D -2
THEN (Assert Estimate(x1;a) \moplus{} Inning(x1;a) : v1(Inning(x1;a)) = v BY
Auto)
THEN (RWO "fpf-join-ap-sq" (-1) THENM SplitOnHypITE -1 THENM Reduce (-2)\mcdot{})
THEN Auto
THEN RWO "member-fpf-domain" (-1)
THEN Auto))
Home
Index