---

Step * of Lemma cs-ref-map-unchanged

∀[V:Type]
  ((∀v1,v2:V.  Dec(v1 = v2 ∈ V))
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.
        (two-intersection(A;W)
        ⇒ (∀f:ConsensusState ─→ (consensus-state3(V) List)
              (cs-ref-map-constraints(V;A;W;f)
              ⇒ (∀x,y:ts-reachable(consensus-ts4(V;A;W)).
                    ((x ts-rel(consensus-ts4(V;A;W)) y)
                    ⇒ (∀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||)))))))))
BY
{ ((RepeatFor 9 ((D 0 THENA Auto))
    THEN (Assert (x ∈ ConsensusState) ∧ (y ∈ ConsensusState) BY
                ((DVar `x' THEN DVar `y') THEN All (RepUR ``ts-type consensus-ts4``) THEN Complete (Auto)))
    THEN D -1
    THEN Auto)
   THEN (InstLemma `consensus-state3-cases` [⌈V⌉;⌈f x[i]⌉]⋅ THENA Auto)
   THEN SplitOrHyps
   THEN ExRepD
   THEN SplitOrHyps
   THEN OnMaybeHyp 7 (\h. ((Unfold `cs-ref-map-constraints` h
                            THEN (InstHyp [⌈x⌉;⌈i⌉] h⋅ THENA Auto)
                            THEN D -1
                            THEN Thin (-2)
                            THEN (D -1 THENA Auto))
                           THEN Auto
                           THEN Try ((SimpleInstHyp ⌈v⌉ (-1)⋅ THENA Auto))
                           THEN Auto
                           THEN ThinTrivial))) }

1
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. two-intersection(A;W)@i
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. ∀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
8. x : ts-reachable(consensus-ts4(V;A;W))@i
9. y : ts-reachable(consensus-ts4(V;A;W))@i
10. x ∈ ConsensusState
11. y ∈ ConsensusState
12. x ts-rel(consensus-ts4(V;A;W)) y@i
13. i : ℕ@i
14. i < ||f x||
15. i < ||f y||
16. ∀v:V. (in state x, inning i could commit v  ⇒ in state y, inning i could commit v )@i
17. f x[i] = INITIAL ∈ consensus-state3(V)
18. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
19. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
20. ∀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)))))
21. ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state x, inning i could commit v  ∧ in state x, inning i could commit v' )
22. f x[i] = INITIAL ∈ consensus-state3(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))))

2
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. two-intersection(A;W)@i
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. ∀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
8. x : ts-reachable(consensus-ts4(V;A;W))@i
9. y : ts-reachable(consensus-ts4(V;A;W))@i
10. x ∈ ConsensusState
11. y ∈ ConsensusState
12. x ts-rel(consensus-ts4(V;A;W)) y@i
13. i : ℕ@i
14. i < ||f x||
15. i < ||f y||
16. ∀v:V. (in state x, inning i could commit v  ⇒ in state y, inning i could commit v )@i
17. f x[i] = WITHDRAWN ∈ consensus-state3(V)
18. (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' ))
19. (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' )
20. ∀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)))))
21. ¬(∃v:V. in state x, inning i could commit v )
22. f x[i] = WITHDRAWN ∈ consensus-state3(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))))

3
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. two-intersection(A;W)@i
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. ∀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
8. x : ts-reachable(consensus-ts4(V;A;W))@i
9. y : ts-reachable(consensus-ts4(V;A;W))@i
10. x ∈ ConsensusState
11. y ∈ ConsensusState
12. x ts-rel(consensus-ts4(V;A;W)) y@i
13. i : ℕ@i
14. i < ||f x||
15. i < ||f y||
16. ∀v:V. (in state x, inning i could commit v  ⇒ in state y, inning i could commit v )@i
17. v : V
18. f x[i] = CONSIDERING[v] ∈ consensus-state3(V)
19. (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' ))
20. (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' )
21. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
22. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
23. ∀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)))))
24. (f x[i] = COMMITED[v] ∈ consensus-state3(V)) ⇒ in state x, inning i has committed v
25. (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)))
26. in state x, inning i could commit v 
27. ¬in state x, inning i has committed v
28. ∀v':V. (in state x, inning i could commit v'  ⇒ (v' = v ∈ 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))))

4
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. two-intersection(A;W)@i
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. ∀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
8. x : ts-reachable(consensus-ts4(V;A;W))@i
9. y : ts-reachable(consensus-ts4(V;A;W))@i
10. x ∈ ConsensusState
11. y ∈ ConsensusState
12. x ts-rel(consensus-ts4(V;A;W)) y@i
13. i : ℕ@i
14. i < ||f x||
15. i < ||f y||
16. ∀v:V. (in state x, inning i could commit v  ⇒ in state y, inning i could commit v )@i
17. v : V
18. f x[i] = COMMITED[v] ∈ consensus-state3(V)
19. (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' ))
20. (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' )
21. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇒ (¬(∃v:V. in state x, inning i could commit v ))
22. (f x[i] = WITHDRAWN ∈ consensus-state3(V)) ⇐ ¬(∃v:V. in state x, inning i could commit v )
23. ∀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)))))
24. (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))))
25. (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)))
26. in state x, inning i has committed v
27. f x[i] = COMMITED[v] ∈ consensus-state3(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))))

---

Latex:


\mforall{}[V:Type]
    ((\mforall{}v1,v2:V.    Dec(v1  =  v2))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
                (two-intersection(A;W)
                {}\mRightarrow{}  (\mforall{}f:ConsensusState  {}\mrightarrow{}  (consensus-state3(V)  List)
                            (cs-ref-map-constraints(V;A;W;f)
                            {}\mRightarrow{}  (\mforall{}x,y:ts-reachable(consensus-ts4(V;A;W)).
                                        ((x  ts-rel(consensus-ts4(V;A;W))  y)
                                        {}\mRightarrow{}  (\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||)))))))))


By

((RepeatFor  9  ((D  0  THENA  Auto))
    THEN  (Assert  (x  \mmember{}  ConsensusState)  \mwedge{}  (y  \mmember{}  ConsensusState)  BY
                            ((DVar  `x'  THEN  DVar  `y')
                              THEN  All  (RepUR  ``ts-type  consensus-ts4``)
                              THEN  Complete  (Auto)))
    THEN  D  -1
    THEN  Auto)
  THEN  (InstLemma  `consensus-state3-cases`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}f  x[i]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  SplitOrHyps
  THEN  OnMaybeHyp  7  (\mbackslash{}h.  ((Unfold  `cs-ref-map-constraints`  h
                                                    THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                                    THEN  D  -1
                                                    THEN  Thin  (-2)
                                                    THEN  (D  -1  THENA  Auto))
                                                  THEN  Auto
                                                  THEN  Try  ((SimpleInstHyp  \mkleeneopen{}v\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))
                                                  THEN  Auto
                                                  THEN  ThinTrivial)))

---

Home Index