Step
*
of Lemma
consensus-ts3-invariant0
∀[V:Type]
∀L:ts-reachable(consensus-ts3(V)). ∀i:ℕ||L||.
∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j
supposing L[i] = INITIAL ∈ consensus-state3(V)
BY
{ (((D 0 THENA Auto) THEN (InstLemma `consensus-state3-unequal` [⌜V⌝]⋅ THENA Auto))
THEN BLemma `ts-reachable-induction`
THEN Auto
THEN (All (Unfold `ts-reachable`) THEN ∀h:hyp. (DSet h THEN Thin (h+1)) )
THEN All (RepUR ``consensus-ts3 ts-type ts-init ts-rel``)
THEN Auto
THEN SplitOrHyps
THEN ExRepD
THEN SplitOrHyps
THEN ExRepD
THEN SplitOrHyps
THEN ExRepD
THEN Try (((InstHyp [⌜v⌝] 3⋅ THENA Auto) THEN Thin 3 THEN PushBackThen (-1) (\i.Id ) ))
THEN Try (((Assert y[i] = L[i] ∈ consensus-state3(V) BY
(BackThruSomeHyp THEN D 0 THEN Complete (Auto)))
THEN (Assert (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) BY
OnMaybeHyp 6 (\h. (InstHyp [⌜i⌝;⌜j⌝] h⋅ THEN Complete (Auto))))
))) }
1
1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. ∀[v:V]
(((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[v':V]
((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V)))
supposing ¬(v = v' ∈ V))))
4. L : consensus-state3(V) List@i
5. y : consensus-state3(V) List@i
6. ∀i:ℕ||L||
∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j
supposing L[i] = INITIAL ∈ consensus-state3(V)@i
7. y = (L @ [INITIAL]) ∈ (consensus-state3(V) List)@i
8. i : ℕ||y||@i
9. y[i] = INITIAL ∈ consensus-state3(V)
10. j : ℕ||y||@i
11. i < j
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
2
1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. ∀[v:V]
(((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[v':V]
((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V)))
supposing ¬(v = v' ∈ V))))
4. L : consensus-state3(V) List@i
5. y : consensus-state3(V) List@i
6. ∀i:ℕ||L||
∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j
supposing L[i] = INITIAL ∈ consensus-state3(V)@i
7. ||y|| = ||L|| ∈ ℤ@i
8. i1 : ℕ||L||@i
9. ∀j:ℕ||L||. ((¬(j = i1 ∈ ℤ)) ⇒ (y[j] = L[j] ∈ consensus-state3(V)))@i
10. L[i1] = INITIAL ∈ consensus-state3(V)@i
11. y[i1] = WITHDRAWN ∈ consensus-state3(V)@i
12. i : ℕ||y||@i
13. y[i] = INITIAL ∈ consensus-state3(V)
14. j : ℕ||y||@i
15. i < j
16. y[i] = L[i] ∈ consensus-state3(V)
17. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V))
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
3
1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. L : consensus-state3(V) List@i
4. y : consensus-state3(V) List@i
5. ∀i:ℕ||L||
∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j
supposing L[i] = INITIAL ∈ consensus-state3(V)@i
6. ||y|| = ||L|| ∈ ℤ@i
7. i1 : ℕ||L||@i
8. ∀j:ℕ||L||. ((¬(j = i1 ∈ ℤ)) ⇒ (y[j] = L[j] ∈ consensus-state3(V)))@i
9. L[i1] = INITIAL ∈ consensus-state3(V)@i
10. v : V@i
11. ((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[v':V]
((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V)))
supposing ¬(v = v' ∈ V)))
12. y[i1] = CONSIDERING[v] ∈ consensus-state3(V)@i
13. ∀j:ℕi1
((L[j] = WITHDRAWN ∈ consensus-state3(V))
∨ (L[j] = CONSIDERING[v] ∈ consensus-state3(V))
∨ (L[j] = COMMITED[v] ∈ consensus-state3(V)))@i
14. i : ℕ||y||@i
15. y[i] = INITIAL ∈ consensus-state3(V)
16. j : ℕ||y||@i
17. i < j
18. y[i] = L[i] ∈ consensus-state3(V)
19. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V))
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
4
1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. L : consensus-state3(V) List@i
4. y : consensus-state3(V) List@i
5. ∀i:ℕ||L||
∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j
supposing L[i] = INITIAL ∈ consensus-state3(V)@i
6. ||y|| = ||L|| ∈ ℤ@i
7. i1 : ℕ||L||@i
8. ∀j:ℕ||L||. ((¬(j = i1 ∈ ℤ)) ⇒ (y[j] = L[j] ∈ consensus-state3(V)))@i
9. v : V@i
10. ((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[v':V]
((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V)))
supposing ¬(v = v' ∈ V)))
11. L[i1] = CONSIDERING[v] ∈ consensus-state3(V)@i
12. y[i1] = COMMITED[v] ∈ consensus-state3(V)@i
13. i : ℕ||y||@i
14. y[i] = INITIAL ∈ consensus-state3(V)
15. j : ℕ||y||@i
16. i < j
17. y[i] = L[i] ∈ consensus-state3(V)
18. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V))
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
5
1. [V] : Type
2. ¬(INITIAL = WITHDRAWN ∈ consensus-state3(V))
3. L : consensus-state3(V) List@i
4. y : consensus-state3(V) List@i
5. ∀i:ℕ||L||
∀j:ℕ||L||. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V)) supposing i < j
supposing L[i] = INITIAL ∈ consensus-state3(V)@i
6. ||y|| = ||L|| ∈ ℤ@i
7. i1 : ℕ||L||@i
8. ∀j:ℕ||L||. ((¬(j = i1 ∈ ℤ)) ⇒ (y[j] = L[j] ∈ consensus-state3(V)))@i
9. v : V@i
10. ((¬(COMMITED[v] = INITIAL ∈ consensus-state3(V))) ∧ (¬(CONSIDERING[v] = INITIAL ∈ consensus-state3(V))))
∧ (¬(COMMITED[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = WITHDRAWN ∈ consensus-state3(V)))
∧ (∀[v':V]
((¬(CONSIDERING[v] = COMMITED[v'] ∈ consensus-state3(V)))
∧ (¬(CONSIDERING[v] = CONSIDERING[v'] ∈ consensus-state3(V)))
∧ (¬(COMMITED[v] = COMMITED[v'] ∈ consensus-state3(V)))
supposing ¬(v = v' ∈ V)))
11. L[i1] = CONSIDERING[v] ∈ consensus-state3(V)@i
12. y[i1] = WITHDRAWN ∈ consensus-state3(V)@i
13. i : ℕ||y||@i
14. y[i] = INITIAL ∈ consensus-state3(V)
15. j : ℕ||y||@i
16. i < j
17. y[i] = L[i] ∈ consensus-state3(V)
18. (L[j] = INITIAL ∈ consensus-state3(V)) ∨ (L[j] = WITHDRAWN ∈ consensus-state3(V))
⊢ (y[j] = INITIAL ∈ consensus-state3(V)) ∨ (y[j] = WITHDRAWN ∈ consensus-state3(V))
Latex:
Latex:
\mforall{}[V:Type]
\mforall{}L:ts-reachable(consensus-ts3(V)). \mforall{}i:\mBbbN{}||L||.
\mforall{}j:\mBbbN{}||L||. (L[j] = INITIAL) \mvee{} (L[j] = WITHDRAWN) supposing i < j supposing L[i] = INITIAL
By
Latex:
(((D 0 THENA Auto) THEN (InstLemma `consensus-state3-unequal` [\mkleeneopen{}V\mkleeneclose{}]\mcdot{} THENA Auto))
THEN BLemma `ts-reachable-induction`
THEN Auto
THEN (All (Unfold `ts-reachable`) THEN \mforall{}h:hyp. (DSet h THEN Thin (h+1)) )
THEN All (RepUR ``consensus-ts3 ts-type ts-init ts-rel``)
THEN Auto
THEN SplitOrHyps
THEN ExRepD
THEN SplitOrHyps
THEN ExRepD
THEN SplitOrHyps
THEN ExRepD
THEN Try (((InstHyp [\mkleeneopen{}v\mkleeneclose{}] 3\mcdot{} THENA Auto) THEN Thin 3 THEN PushBackThen (-1) (\mbackslash{}i.Id ) ))
THEN Try (((Assert y[i] = L[i] BY
(BackThruSomeHyp THEN D 0 THEN Complete (Auto)))
THEN (Assert (L[j] = INITIAL) \mvee{} (L[j] = WITHDRAWN) BY
OnMaybeHyp 6 (\mbackslash{}h. (InstHyp [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}] h\mcdot{} THEN Complete (Auto))))
)))
Home
Index