---

Step * 1 4 of Lemma cs-ref-map-changed


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. two-intersection(A;W)@i
7. f : ConsensusState ─→ (consensus-state3(V) List)@i
8. ∀s:ConsensusState. ∀i:ℕ.
     ((i < ||f s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
     ∧ (i < ||f s||
       ⇒ ((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)))))))))@i
9. x : ts-reachable(consensus-ts4(V;A;W))@i
10. y : ts-reachable(consensus-ts4(V;A;W))@i
11. x ∈ ConsensusState
12. y ∈ ConsensusState
13. x ts-rel(consensus-ts4(V;A;W)) y@i
14. i : ℕ@i
15. i < ||f x||
16. i < ||f y||
17. v : V@i
18. in state x, inning i could commit v @i
19. ¬in state y, inning i could commit v @i
20. v1 : V
21. f x[i] = COMMITED[v1] ∈ consensus-state3(V)
22. (f x[i] = INITIAL ∈ consensus-state3(V))
⇒ (∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v  ∧ in state x, inning i could commit v' ))
23. (f x[i] = INITIAL ∈ consensus-state3(V)) ⇐ ∃v,v':V
                                                 ((¬(v = v' ∈ V))
                                                 ∧ in state x, inning i could commit v 
                                                 ∧ in state x, inning i could commit v' )
24. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
25. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
26. ∀v:V
      ((f x[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state x, inning i has committed v)
      ∧ (f x[i] = CONSIDERING[v] ∈ consensus-state3(V)
        ⇐⇒ in state x, inning i could commit v 
            ∧ (¬in state x, inning i has committed v)
            ∧ (∀v':V. (in state x, inning i could commit v'  ⇒ (v' = v ∈ V)))))
27. (f x[i] = CONSIDERING[v1] ∈ consensus-state3(V))
⇒ (in state x, inning i could commit v1 
   ∧ (¬in state x, inning i has committed v1)
   ∧ (∀v':V. (in state x, inning i could commit v'  ⇒ (v' = v1 ∈ V))))
28. (f x[i] = CONSIDERING[v1] ∈ consensus-state3(V)) ⇐ in state x, inning i could commit v1 
∧ (¬in state x, inning i has committed v1)
∧ (∀v':V. (in state x, inning i could commit v'  ⇒ (v' = v1 ∈ V)))
29. in state x, inning i has committed v1
30. f x[i] = COMMITED[v1] ∈ consensus-state3(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)))))))
BY
{ OnMaybeHyp 19 (\h. (D h
                      THEN (Subst' v = v1 ∈ V 0
                            THENA (InstLemma `cs-inning-committed-single` [⌈V⌉;⌈A⌉;⌈W⌉;⌈x⌉;⌈i⌉;⌈v⌉;⌈v1⌉]⋅ THEN Auto)
                            )
                      THEN (BLemma `cs-inning-committed-committable` THENA Auto)
                      THEN InstLemma `consensus-ts4-inning-committed-stable` [⌈V⌉;⌈A⌉;⌈W⌉;⌈v1⌉;⌈i⌉]⋅
                      THEN Complete (Auto)))⋅ }

---

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.  two-intersection(A;W)@i
7.  f  :  ConsensusState  {}\mrightarrow{}  (consensus-state3(V)  List)@i
8.  \mforall{}s:ConsensusState.  \mforall{}i:\mBbbN{}.
          ((i  <  ||f  s||  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (i  \mleq{}  Inning(s;a)))
          \mwedge{}  (i  <  ||f  s||
              {}\mRightarrow{}  ((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)))))))))@i
9.  x  :  ts-reachable(consensus-ts4(V;A;W))@i
10.  y  :  ts-reachable(consensus-ts4(V;A;W))@i
11.  x  \mmember{}  ConsensusState
12.  y  \mmember{}  ConsensusState
13.  x  ts-rel(consensus-ts4(V;A;W))  y@i
14.  i  :  \mBbbN{}@i
15.  i  <  ||f  x||
16.  i  <  ||f  y||
17.  v  :  V@i
18.  in  state  x,  inning  i  could  commit  v  @i
19.  \mneg{}in  state  y,  inning  i  could  commit  v  @i
20.  v1  :  V
21.  f  x[i]  =  COMMITED[v1]
22.  (f  x[i]  =  INITIAL)
{}\mRightarrow{}  (\mexists{}v,v':V
          ((\mneg{}(v  =  v'))  \mwedge{}  in  state  x,  inning  i  could  commit  v    \mwedge{}  in  state  x,  inning  i  could  commit  v'  ))
23.  (f  x[i]  =  INITIAL)  \mLeftarrow{}{}  \mexists{}v,v':V
                                                      ((\mneg{}(v  =  v'))
                                                      \mwedge{}  in  state  x,  inning  i  could  commit  v 
                                                      \mwedge{}  in  state  x,  inning  i  could  commit  v'  )
24.  (f  x[i]  =  WITHDRAWN)  {}\mRightarrow{}  (\mneg{}(\mexists{}v:V.  in  state  x,  inning  i  could  commit  v  ))
25.  (f  x[i]  =  WITHDRAWN)  \mLeftarrow{}{}  \mneg{}(\mexists{}v:V.  in  state  x,  inning  i  could  commit  v  )
26.  \mforall{}v:V
            ((f  x[i]  =  COMMITED[v]  \mLeftarrow{}{}\mRightarrow{}  in  state  x,  inning  i  has  committed  v)
            \mwedge{}  (f  x[i]  =  CONSIDERING[v]
                \mLeftarrow{}{}\mRightarrow{}  in  state  x,  inning  i  could  commit  v 
                        \mwedge{}  (\mneg{}in  state  x,  inning  i  has  committed  v)
                        \mwedge{}  (\mforall{}v':V.  (in  state  x,  inning  i  could  commit  v'    {}\mRightarrow{}  (v'  =  v)))))
27.  (f  x[i]  =  CONSIDERING[v1])
{}\mRightarrow{}  (in  state  x,  inning  i  could  commit  v1 
      \mwedge{}  (\mneg{}in  state  x,  inning  i  has  committed  v1)
      \mwedge{}  (\mforall{}v':V.  (in  state  x,  inning  i  could  commit  v'    {}\mRightarrow{}  (v'  =  v1))))
28.  (f  x[i]  =  CONSIDERING[v1])  \mLeftarrow{}{}  in  state  x,  inning  i  could  commit  v1 
\mwedge{}  (\mneg{}in  state  x,  inning  i  has  committed  v1)
\mwedge{}  (\mforall{}v':V.  (in  state  x,  inning  i  could  commit  v'    {}\mRightarrow{}  (v'  =  v1)))
29.  in  state  x,  inning  i  has  committed  v1
30.  f  x[i]  =  COMMITED[v1]
\mvdash{}  (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')))))))


By

OnMaybeHyp  19  (\mbackslash{}h.  (D  h
                                        THEN  (Subst'  v  =  v1  0
                                                    THENA  (InstLemma  `cs-inning-committed-single`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};
                                                                  \mkleeneopen{}v1\mkleeneclose{}]\mcdot{}
                                                                  THEN  Auto
                                                                  )
                                                    )
                                        THEN  (BLemma  `cs-inning-committed-committable`  THENA  Auto)
                                        THEN  InstLemma  `consensus-ts4-inning-committed-stable`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}W\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
                                        THEN  Complete  (Auto)))\mcdot{}

---

Home Index