---

Step * 1 2 1 1 1 1 1 2 of Lemma consensus-refinement3


1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. ∀L:V List. Dec(∃v:V. (¬(v ∈ L)))@i
5. A : Id List@i
6. W : {a:Id| (a ∈ A)}  List List@i
7. ||W|| ≥ 1 
8. two-intersection(A;W)@i
9. f : ConsensusState ─→ (consensus-state3(V) List)@i
10. cs-ref-map-constraints(V;A;W;f)@i
11. x : ts-reachable(consensus-ts4(V;A;W))@i
12. y : ts-reachable(consensus-ts4(V;A;W))@i
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. x ∈ ConsensusState
15. y ∈ ConsensusState
16. CR[x,y]
17. ∀i:ℕ
      ((∀v:V. (in state x, inning i could commit v  ⇒ in state y, inning i could commit v ))
         ⇒ ((f y[i] = f x[i] ∈ consensus-state3(V))
            ∨ (∃v:V
                ((f y[i] = COMMITED[v] ∈ consensus-state3(V))
                ∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)))))) supposing 
         (i < ||f y|| and 
         i < ||f x||)
18. ∀i:ℕ
      (∀v:V
         ((in state x, inning i could commit v  ∧ (¬in state y, inning i could commit v ))
         ⇒ ((f y[i] = WITHDRAWN ∈ consensus-state3(V))
            ∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
              ∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
                ∨ (∃v':V
                    ((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))
                    ∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))
                    ∧ (∀j:ℕi. ∀v'':V.
                         (((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V))
                         ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))
                         ⇒ (v'' = v' ∈ V)))))))))) supposing 
         (i < ||f y|| and 
         i < ||f x||)
19. ||f x|| ≤ ||f y||
20. i : ℤ
21. ∀j:ℕ||f x||. f y[j] = f x[j] ∈ consensus-state3(V) supposing ¬(j = i ∈ ℤ)
22. (||f y|| = (||f x|| + 1) ∈ ℤ) ∧ (f y[||f x||] = INITIAL ∈ consensus-state3(V)) supposing ||f x|| < ||f y||
23. i < ||f x||
24. ¬(0 ≤ i)
⊢ (f x) (ts-rel(consensus-ts3(V))^*) (f y)
BY
{ (Assert ∀j:ℕ||f x||. (f y[j] = f x[j] ∈ consensus-state3(V)) BY
         (Auto THEN BackThruSomeHyp THEN Auto')) }

1
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. ∀L:V List. Dec(∃v:V. (¬(v ∈ L)))@i
5. A : Id List@i
6. W : {a:Id| (a ∈ A)}  List List@i
7. ||W|| ≥ 1 
8. two-intersection(A;W)@i
9. f : ConsensusState ─→ (consensus-state3(V) List)@i
10. cs-ref-map-constraints(V;A;W;f)@i
11. x : ts-reachable(consensus-ts4(V;A;W))@i
12. y : ts-reachable(consensus-ts4(V;A;W))@i
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. x ∈ ConsensusState
15. y ∈ ConsensusState
16. CR[x,y]
17. ∀i:ℕ
      ((∀v:V. (in state x, inning i could commit v  ⇒ in state y, inning i could commit v ))
         ⇒ ((f y[i] = f x[i] ∈ consensus-state3(V))
            ∨ (∃v:V
                ((f y[i] = COMMITED[v] ∈ consensus-state3(V))
                ∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)))))) supposing 
         (i < ||f y|| and 
         i < ||f x||)
18. ∀i:ℕ
      (∀v:V
         ((in state x, inning i could commit v  ∧ (¬in state y, inning i could commit v ))
         ⇒ ((f y[i] = WITHDRAWN ∈ consensus-state3(V))
            ∨ ((f x[i] = INITIAL ∈ consensus-state3(V))
              ∧ ((f y[i] = INITIAL ∈ consensus-state3(V))
                ∨ (∃v':V
                    ((∀j:ℕi. (¬(f x[j] = INITIAL ∈ consensus-state3(V))))
                    ∧ ((f y[i] = CONSIDERING[v'] ∈ consensus-state3(V)) ∨ (f y[i] = COMMITED[v'] ∈ consensus-state3(V)))
                    ∧ (∀j:ℕi. ∀v'':V.
                         (((f x[j] = CONSIDERING[v''] ∈ consensus-state3(V))
                         ∨ (f x[j] = COMMITED[v''] ∈ consensus-state3(V)))
                         ⇒ (v'' = v' ∈ V)))))))))) supposing 
         (i < ||f y|| and 
         i < ||f x||)
19. ||f x|| ≤ ||f y||
20. i : ℤ
21. ∀j:ℕ||f x||. f y[j] = f x[j] ∈ consensus-state3(V) supposing ¬(j = i ∈ ℤ)
22. (||f y|| = (||f x|| + 1) ∈ ℤ) ∧ (f y[||f x||] = INITIAL ∈ consensus-state3(V)) supposing ||f x|| < ||f y||
23. i < ||f x||
24. ¬(0 ≤ i)
25. ∀j:ℕ||f x||. (f y[j] = f x[j] ∈ consensus-state3(V))
⊢ (f x) (ts-rel(consensus-ts3(V))^*) (f y)

---

Latex:



1.  [V]  :  Type
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  \{\mexists{}v,v':V.  (\mneg{}(v  =  v'))\}@i
4.  \mforall{}L:V  List.  Dec(\mexists{}v:V.  (\mneg{}(v  \mmember{}  L)))@i
5.  A  :  Id  List@i
6.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
7.  ||W||  \mgeq{}  1 
8.  two-intersection(A;W)@i
9.  f  :  ConsensusState  {}\mrightarrow{}  (consensus-state3(V)  List)@i
10.  cs-ref-map-constraints(V;A;W;f)@i
11.  x  :  ts-reachable(consensus-ts4(V;A;W))@i
12.  y  :  ts-reachable(consensus-ts4(V;A;W))@i
13.  x  ts-rel(consensus-ts4(V;A;W))  y@i
14.  x  \mmember{}  ConsensusState
15.  y  \mmember{}  ConsensusState
16.  CR[x,y]
17.  \mforall{}i:\mBbbN{}
            ((\mforall{}v:V.  (in  state  x,  inning  i  could  commit  v    {}\mRightarrow{}  in  state  y,  inning  i  could  commit  v  ))
                  {}\mRightarrow{}  ((f  y[i]  =  f  x[i])
                        \mvee{}  (\mexists{}v:V.  ((f  y[i]  =  COMMITED[v])  \mwedge{}  (f  x[i]  =  CONSIDERING[v])))))  supposing 
                  (i  <  ||f  y||  and 
                  i  <  ||f  x||)
18.  \mforall{}i:\mBbbN{}
            (\mforall{}v:V
                  ((in  state  x,  inning  i  could  commit  v    \mwedge{}  (\mneg{}in  state  y,  inning  i  could  commit  v  ))
                  {}\mRightarrow{}  ((f  y[i]  =  WITHDRAWN)
                        \mvee{}  ((f  x[i]  =  INITIAL)
                            \mwedge{}  ((f  y[i]  =  INITIAL)
                                \mvee{}  (\mexists{}v':V
                                        ((\mforall{}j:\mBbbN{}i.  (\mneg{}(f  x[j]  =  INITIAL)))
                                        \mwedge{}  ((f  y[i]  =  CONSIDERING[v'])  \mvee{}  (f  y[i]  =  COMMITED[v']))
                                        \mwedge{}  (\mforall{}j:\mBbbN{}i.  \mforall{}v'':V.
                                                  (((f  x[j]  =  CONSIDERING[v''])  \mvee{}  (f  x[j]  =  COMMITED[v'']))
                                                  {}\mRightarrow{}  (v''  =  v'))))))))))  supposing 
                  (i  <  ||f  y||  and 
                  i  <  ||f  x||)
19.  ||f  x||  \mleq{}  ||f  y||
20.  i  :  \mBbbZ{}
21.  \mforall{}j:\mBbbN{}||f  x||.  f  y[j]  =  f  x[j]  supposing  \mneg{}(j  =  i)
22.  (||f  y||  =  (||f  x||  +  1))  \mwedge{}  (f  y[||f  x||]  =  INITIAL)  supposing  ||f  x||  <  ||f  y||
23.  i  <  ||f  x||
24.  \mneg{}(0  \mleq{}  i)
\mvdash{}  (f  x)  rel\_star(ts-type(consensus-ts3(V));  ts-rel(consensus-ts3(V)))  (f  y)


By

(Assert  \mforall{}j:\mBbbN{}||f  x||.  (f  y[j]  =  f  x[j])  BY
              (Auto  THEN  BackThruSomeHyp  THEN  Auto'))

---

Home Index