Step
*
2
1
2
1
1
1
2
of Lemma
consensus-refinement4
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. 1 < ||W||@i
9. two-intersection(A;W)@i
10. x1 : ConsensusState@i
11. x2 : Knowledge(ConsensusState)@i
12. y1 : ConsensusState@i
13. y2 : Knowledge(ConsensusState)@i
14. a : {a:Id| (a ∈ A)} @i
15. ∀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
16. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
17. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
18. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))@i
19. v : V@i
20. ws : {a:Id| (a ∈ A)} List@i
21. (ws ∈ W)@i
22. ∀b:{a:Id| (a ∈ A)} . ((b ∈ ws) ⇒ ((↑b ∈ dom(Knowledge(x2;a))) ∧ (Inning(x1;a) = (fst(Knowledge(x2;a)(b))) ∈ ℤ)))@i
23. ∀ws':{a:Id| (a ∈ A)} List
((ws' ∈ W)
⇒ (∃b:{a:Id| (a ∈ A)}
((b ∈ ws)
∧ (b ∈ ws')
∧ ((↑isl(snd(Knowledge(x2;a)(b)))) ⇒ ((snd(outl(snd(Knowledge(x2;a)(b))))) = v ∈ V)))))@i
24. Estimate(y1;a) = Estimate(x1;a) ⊕ Inning(x1;a) : v ∈ i:ℤ fp-> V@i
25. <x1, x2> ∈ ts-reachable(consensus-ts5(V;A;W))
26. <y1, y2> ∈ ts-reachable(consensus-ts5(V;A;W))
27. ∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id)) ⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ) ∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)))
28. Inning(y1;a) = Inning(x1;a) ∈ ℤ
29. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))
30. (ws ∈ W)
31. ∀b:{a:Id| (a ∈ A)} . ((b ∈ ws) ⇒ (Inning(x1;a) ≤ Inning(x1;b)))
32. ws' : {a:Id| (a ∈ A)} List@i
33. (ws' ∈ W)@i
⊢ ¬in state x1, ws' blocks ws from archiving v in inning Inning(x1;a)
BY
{ ((D 0 THENA Auto) THEN D -1 THEN ExRepD) }
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. 1 < ||W||@i
9. two-intersection(A;W)@i
10. x1 : ConsensusState@i
11. x2 : Knowledge(ConsensusState)@i
12. y1 : ConsensusState@i
13. y2 : Knowledge(ConsensusState)@i
14. a : {a:Id| (a ∈ A)} @i
15. ∀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
16. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
17. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
18. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))@i
19. v : V@i
20. ws : {a:Id| (a ∈ A)} List@i
21. (ws ∈ W)@i
22. ∀b:{a:Id| (a ∈ A)} . ((b ∈ ws) ⇒ ((↑b ∈ dom(Knowledge(x2;a))) ∧ (Inning(x1;a) = (fst(Knowledge(x2;a)(b))) ∈ ℤ)))@i
23. ∀ws':{a:Id| (a ∈ A)} List
((ws' ∈ W)
⇒ (∃b:{a:Id| (a ∈ A)}
((b ∈ ws)
∧ (b ∈ ws')
∧ ((↑isl(snd(Knowledge(x2;a)(b)))) ⇒ ((snd(outl(snd(Knowledge(x2;a)(b))))) = v ∈ V)))))@i
24. Estimate(y1;a) = Estimate(x1;a) ⊕ Inning(x1;a) : v ∈ i:ℤ fp-> V@i
25. <x1, x2> ∈ ts-reachable(consensus-ts5(V;A;W))
26. <y1, y2> ∈ ts-reachable(consensus-ts5(V;A;W))
27. ∀b:{a:Id| (a ∈ A)}
((¬(b = a ∈ Id)) ⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ) ∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)))
28. Inning(y1;a) = Inning(x1;a) ∈ ℤ
29. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))
30. (ws ∈ W)
31. ∀b:{a:Id| (a ∈ A)} . ((b ∈ ws) ⇒ (Inning(x1;a) ≤ Inning(x1;b)))
32. ws' : {a:Id| (a ∈ A)} List@i
33. (ws' ∈ W)@i
34. j : ℤ@i
35. 0 ≤ j@i
36. j < Inning(x1;a)@i
37. v2 : V@i
38. ¬(v2 = v ∈ V)@i
39. ∀b:{a:Id| (a ∈ A)}
(((b ∈ ws) ∧ (b ∈ ws'))
⇒ ((↑j ∈ dom(Estimate(x1;b)))
∧ (Estimate(x1;b)(j) = v2 ∈ V)
∧ (∀k:ℤ. (((j < k ∧ k < Inning(x1;a)) ∧ (↑k ∈ dom(Estimate(x1;b)))) ⇒ (Estimate(x1;b)(k) = v2 ∈ V)))))@i
⊢ False
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. 1 < ||W||@i
9. two-intersection(A;W)@i
10. x1 : ConsensusState@i
11. x2 : Knowledge(ConsensusState)@i
12. y1 : ConsensusState@i
13. y2 : Knowledge(ConsensusState)@i
14. a : \{a:Id| (a \mmember{} A)\} @i
15. \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
16. Inning(y1;a) = Inning(x1;a)@i
17. Knowledge(y2;a) = Knowledge(x2;a)@i
18. \mneg{}(Inning(x1;a) \mmember{} fpf-domain(Estimate(x1;a)))@i
19. v : V@i
20. ws : \{a:Id| (a \mmember{} A)\} List@i
21. (ws \mmember{} W)@i
22. \mforall{}b:\{a:Id| (a \mmember{} A)\}
((b \mmember{} ws) {}\mRightarrow{} ((\muparrow{}b \mmember{} dom(Knowledge(x2;a))) \mwedge{} (Inning(x1;a) = (fst(Knowledge(x2;a)(b))))))@i
23. \mforall{}ws':\{a:Id| (a \mmember{} A)\} List
((ws' \mmember{} W)
{}\mRightarrow{} (\mexists{}b:\{a:Id| (a \mmember{} A)\}
((b \mmember{} ws)
\mwedge{} (b \mmember{} ws')
\mwedge{} ((\muparrow{}isl(snd(Knowledge(x2;a)(b)))) {}\mRightarrow{} ((snd(outl(snd(Knowledge(x2;a)(b))))) = v)))))@i
24. Estimate(y1;a) = Estimate(x1;a) \moplus{} Inning(x1;a) : v@i
25. <x1, x2> \mmember{} ts-reachable(consensus-ts5(V;A;W))
26. <y1, y2> \mmember{} ts-reachable(consensus-ts5(V;A;W))
27. \mforall{}b:\{a:Id| (a \mmember{} A)\}
((\mneg{}(b = a)) {}\mRightarrow{} ((Inning(y1;b) = Inning(x1;b)) \mwedge{} (Estimate(y1;b) = Estimate(x1;b))))
28. Inning(y1;a) = Inning(x1;a)
29. \mneg{}(Inning(x1;a) \mmember{} fpf-domain(Estimate(x1;a)))
30. (ws \mmember{} W)
31. \mforall{}b:\{a:Id| (a \mmember{} A)\} . ((b \mmember{} ws) {}\mRightarrow{} (Inning(x1;a) \mleq{} Inning(x1;b)))
32. ws' : \{a:Id| (a \mmember{} A)\} List@i
33. (ws' \mmember{} W)@i
\mvdash{} \mneg{}in state x1, ws' blocks ws from archiving v in inning Inning(x1;a)
By
((D 0 THENA Auto) THEN D -1 THEN ExRepD)
Home
Index