Step
*
1
2
1
2
of Lemma
consensus-ts4-ref-map
1. [V] : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. F : s:ConsensusState ⟶ i:ℤ ⟶ consensus-state3(V)
8. ∀s:ConsensusState. ∀i:ℤ.
(((F s i) = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ ((F s i) = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
(((F s i) = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ ((F s i) = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V)))))))
9. N : s:ConsensusState ⟶ ℕ
10. ∀s:ConsensusState. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
⊢ ∀s:ConsensusState. ∀i:ℕ.
((i < ||(λs.map(λi.(F s i);upto(N s))) s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
∧ (i < ||(λs.map(λi.(F s i);upto(N s))) s||
⇒ (((λs.map(λi.(F s i);upto(N s))) s[i] = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ ((λs.map(λi.(F s i);upto(N s))) s[i] = WITHDRAWN ∈ consensus-state3(V)
⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
(((λs.map(λi.(F s i);upto(N s))) s[i] = COMMITED[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i has committed v)
∧ ((λs.map(λi.(F s i);upto(N s))) s[i] = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V)))))))))
BY
{ (RepeatFor 2 (ParallelLast) THEN Reduce 0 THEN Subst' ||map(λi.(F s i);upto(N s))|| ~ N s 0) }
1
.....equality.....
1. V : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. F : s:ConsensusState ⟶ i:ℤ ⟶ consensus-state3(V)
8. ∀s:ConsensusState. ∀i:ℤ.
(((F s i) = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ ((F s i) = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
(((F s i) = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ ((F s i) = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V)))))))
9. N : s:ConsensusState ⟶ ℕ
10. ∀s:ConsensusState. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
11. s : ConsensusState@i
12. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
13. i : ℕ@i
14. i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a))
⊢ ||map(λi.(F s i);upto(N s))|| ~ N s
2
1. [V] : Type
2. ∃v,v':V. (¬(v = v' ∈ V))@i
3. ∀v,v':V. Dec(v = v' ∈ V)@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. two-intersection(A;W)@i
7. F : s:ConsensusState ⟶ i:ℤ ⟶ consensus-state3(V)
8. ∀s:ConsensusState. ∀i:ℤ.
(((F s i) = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ ((F s i) = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
(((F s i) = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ ((F s i) = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V)))))))
9. N : s:ConsensusState ⟶ ℕ
10. ∀s:ConsensusState. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
11. s : ConsensusState@i
12. ∀i:ℕ. (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
13. i : ℕ@i
14. i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a))
⊢ (i < N s ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
∧ (i < N s
⇒ ((map(λi.(F s i);upto(N s))[i] = INITIAL ∈ consensus-state3(V)
⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v ∧ in state s, inning i could commit v' ))
∧ (map(λi.(F s i);upto(N s))[i] = WITHDRAWN ∈ consensus-state3(V)
⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
∧ (∀v:V
((map(λi.(F s i);upto(N s))[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
∧ (map(λi.(F s i);upto(N s))[i] = CONSIDERING[v] ∈ consensus-state3(V)
⇐⇒ in state s, inning i could commit v
∧ (¬in state s, inning i has committed v)
∧ (∀v':V. (in state s, inning i could commit v' ⇒ (v' = v ∈ V))))))))
Latex:
Latex:
1. [V] : Type
2. \mexists{}v,v':V. (\mneg{}(v = v'))@i
3. \mforall{}v,v':V. Dec(v = v')@i
4. A : Id List@i
5. W : \{a:Id| (a \mmember{} A)\} List List@i
6. two-intersection(A;W)@i
7. F : s:ConsensusState {}\mrightarrow{} i:\mBbbZ{} {}\mrightarrow{} consensus-state3(V)
8. \mforall{}s:ConsensusState. \mforall{}i:\mBbbZ{}.
(((F s i) = INITIAL
\mLeftarrow{}{}\mRightarrow{} \mexists{}v,v':V
((\mneg{}(v = v'))
\mwedge{} in state s, inning i could commit v
\mwedge{} in state s, inning i could commit v' ))
\mwedge{} ((F s i) = WITHDRAWN \mLeftarrow{}{}\mRightarrow{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v ))
\mwedge{} (\mforall{}v:V
(((F s i) = COMMITED[v] \mLeftarrow{}{}\mRightarrow{} in state s, inning i has committed v)
\mwedge{} ((F s i) = CONSIDERING[v]
\mLeftarrow{}{}\mRightarrow{} in state s, inning i could commit v
\mwedge{} (\mneg{}in state s, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state s, inning i could commit v' {}\mRightarrow{} (v' = v)))))))
9. N : s:ConsensusState {}\mrightarrow{} \mBbbN{}
10. \mforall{}s:ConsensusState. \mforall{}i:\mBbbN{}. (i < N s \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a)))
\mvdash{} \mforall{}s:ConsensusState. \mforall{}i:\mBbbN{}.
((i < ||(\mlambda{}s.map(\mlambda{}i.(F s i);upto(N s))) s|| \mLeftarrow{}{}\mRightarrow{} \mexists{}a:\{a:Id| (a \mmember{} A)\} . (i \mleq{} Inning(s;a)))
\mwedge{} (i < ||(\mlambda{}s.map(\mlambda{}i.(F s i);upto(N s))) s||
{}\mRightarrow{} (((\mlambda{}s.map(\mlambda{}i.(F s i);upto(N s))) s[i] = INITIAL
\mLeftarrow{}{}\mRightarrow{} \mexists{}v,v':V
((\mneg{}(v = v'))
\mwedge{} in state s, inning i could commit v
\mwedge{} in state s, inning i could commit v' ))
\mwedge{} ((\mlambda{}s.map(\mlambda{}i.(F s i);upto(N s))) s[i] = WITHDRAWN
\mLeftarrow{}{}\mRightarrow{} \mneg{}(\mexists{}v:V. in state s, inning i could commit v ))
\mwedge{} (\mforall{}v:V
(((\mlambda{}s.map(\mlambda{}i.(F s i);upto(N s))) s[i] = COMMITED[v]
\mLeftarrow{}{}\mRightarrow{} in state s, inning i has committed v)
\mwedge{} ((\mlambda{}s.map(\mlambda{}i.(F s i);upto(N s))) s[i] = CONSIDERING[v]
\mLeftarrow{}{}\mRightarrow{} in state s, inning i could commit v
\mwedge{} (\mneg{}in state s, inning i has committed v)
\mwedge{} (\mforall{}v':V. (in state s, inning i could commit v' {}\mRightarrow{} (v' = v)))))))))
By
Latex:
(RepeatFor 2 (ParallelLast) THEN Reduce 0 THEN Subst' ||map(\mlambda{}i.(F s i);upto(N s))|| \msim{} N s 0)
Home
Index