Step
*
1
1
1
1
1
1
of Lemma
consensus-reachable
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)} List@i
10. (ws ∈ W)@i
11. ∃a:{a:Id| (a ∈ A)} . (a ∈ ws)
12. 0 < ||ws||
13. x : ts-reachable(consensus-ts4(V;A;W))@i
14. x ∈ ConsensusState
15. imax-list(map(λa.Inning(x;a);ws)) ∈ ℤ
16. i : ℤ@i
17. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ Inning(x;a) < i)@i
⊢ ∃x':ConsensusState
((x ((λx,y. CR(in ws)[x, y] )^*) x')
∧ (∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ ((Inning(x';a) = i ∈ ℤ) ∧ (¬(i ∈ fpf-domain(Estimate(x';a))))))))
BY
{ (InstConcl [⌜λa.<if a ∈b ws then i else Inning(x;a) fi , Estimate(x;a)>⌝]⋅ THEN Auto) }
1
1. [V] : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)} List@i
10. (ws ∈ W)@i
11. ∃a:{a:Id| (a ∈ A)} . (a ∈ ws)
12. 0 < ||ws||
13. x : ts-reachable(consensus-ts4(V;A;W))@i
14. x ∈ ConsensusState
15. imax-list(map(λa.Inning(x;a);ws)) ∈ ℤ
16. i : ℤ@i
17. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ Inning(x;a) < i)@i
⊢ x ((λx,y. CR(in ws)[x, y] )^*) (λa.<if a ∈b ws then i else Inning(x;a) fi , Estimate(x;a)>)
2
1. V : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)} List@i
10. (ws ∈ W)@i
11. ∃a:{a:Id| (a ∈ A)} . (a ∈ ws)
12. 0 < ||ws||
13. x : ts-reachable(consensus-ts4(V;A;W))@i
14. x ∈ ConsensusState
15. imax-list(map(λa.Inning(x;a);ws)) ∈ ℤ
16. i : ℤ@i
17. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ Inning(x;a) < i)@i
18. x ((λx,y. CR(in ws)[x, y] )^*) (λa.<if a ∈b ws then i else Inning(x;a) fi , Estimate(x;a)>)
19. a : {a:Id| (a ∈ A)} @i
20. (a ∈ ws)@i
⊢ Inning(λa.<if a ∈b ws then i else Inning(x;a) fi , Estimate(x;a)>;a) = i ∈ ℤ
3
1. V : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)} List@i
10. (ws ∈ W)@i
11. ∃a:{a:Id| (a ∈ A)} . (a ∈ ws)
12. 0 < ||ws||
13. x : ts-reachable(consensus-ts4(V;A;W))@i
14. x ∈ ConsensusState
15. imax-list(map(λa.Inning(x;a);ws)) ∈ ℤ
16. i : ℤ@i
17. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ Inning(x;a) < i)@i
18. x ((λx,y. CR(in ws)[x, y] )^*) (λa.<if a ∈b ws then i else Inning(x;a) fi , Estimate(x;a)>)
19. a : {a:Id| (a ∈ A)} @i
20. (a ∈ ws)@i
21. Inning(λa.<if a ∈b ws then i else Inning(x;a) fi , Estimate(x;a)>;a) = i ∈ ℤ
⊢ ¬(i ∈ fpf-domain(Estimate(λa.<if a ∈b ws then i else Inning(x;a) fi , Estimate(x;a)>;a)))
Latex:
Latex:
1. [V] : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. \{\mexists{}v,v':V. (\mneg{}(v = v'))\}@i
4. A : Id List@i
5. W : \{a:Id| (a \mmember{} A)\} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : \{a:Id| (a \mmember{} A)\} List@i
10. (ws \mmember{} W)@i
11. \mexists{}a:\{a:Id| (a \mmember{} A)\} . (a \mmember{} ws)
12. 0 < ||ws||
13. x : ts-reachable(consensus-ts4(V;A;W))@i
14. x \mmember{} ConsensusState
15. imax-list(map(\mlambda{}a.Inning(x;a);ws)) \mmember{} \mBbbZ{}
16. i : \mBbbZ{}@i
17. \mforall{}a:\{a:Id| (a \mmember{} A)\} . ((a \mmember{} ws) {}\mRightarrow{} Inning(x;a) < i)@i
\mvdash{} \mexists{}x':ConsensusState
((x rel\_star(ConsensusState; \mlambda{}x,y. CR(in ws)[x, y] ) x')
\mwedge{} (\mforall{}a:\{a:Id| (a \mmember{} A)\} . ((a \mmember{} ws) {}\mRightarrow{} ((Inning(x';a) = i) \mwedge{} (\mneg{}(i \mmember{} fpf-domain(Estimate(x';a)))))))\000C)
By
Latex:
(InstConcl [\mkleeneopen{}\mlambda{}a.<if a \mmember{}\msubb{} ws then i else Inning(x;a) fi , Estimate(x;a)>\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index