---

Step * of Lemma cs-ref-map-step

∀[V:Type]
  ({∃v1,v2:V. (¬(v1 = v2 ∈ V))}
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.
        ∀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)
                ⇒ {(||f x|| ≤ ||f y||)
                   ∧ (∃i:ℤ
                       ((∀j:ℕ||f x||. f y[j] = f x[j] ∈ consensus-state3(V) supposing ¬(j = i ∈ ℤ))
                       ∧ (||f y|| = (||f x|| + 1) ∈ ℤ) ∧ (f y[||f x||] = INITIAL ∈ consensus-state3(V)) 
                         supposing ||f x|| < ||f y||))}))) 
        supposing ||W|| ≥ 1 ))
BY
{ (Auto
   THEN All (RepUR ``ts-reachable ts-rel consensus-ts4 ts-type ts-init``)⋅
   THEN D -3
   THEN D -2
   THEN Unfold `guard` 0
   THEN BetterSplitAndConcl) }

1
1. [V] : Type
2. {∃v1,v2:V. (¬(v1 = v2 ∈ V))}@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. ||W|| ≥ 1 
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. cs-ref-map-constraints(V;A;W;f)@i
8. x : ConsensusState@i
9. \\%5 : (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
10. y : ConsensusState@i
11. \\%7 : (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
12. CR[x,y]@i
⊢ ||f x|| ≤ ||f y||

2
1. [V] : Type
2. {∃v1,v2:V. (¬(v1 = v2 ∈ V))}@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. ||W|| ≥ 1 
6. f : ConsensusState ─→ (consensus-state3(V) List)@i
7. cs-ref-map-constraints(V;A;W;f)@i
8. x : ConsensusState@i
9. \\%5 : (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
10. y : ConsensusState@i
11. \\%7 : (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
12. CR[x,y]@i
13. ||f x|| ≤ ||f y||
⊢ ∃i:ℤ
   ((∀j:ℕ||f x||. f y[j] = f x[j] ∈ consensus-state3(V) supposing ¬(j = i ∈ ℤ))
   ∧ (||f y|| = (||f x|| + 1) ∈ ℤ) ∧ (f y[||f x||] = INITIAL ∈ consensus-state3(V)) supposing ||f x|| < ||f y||)

---

Latex:


\mforall{}[V:Type]
    (\{\mexists{}v1,v2:V.  (\mneg{}(v1  =  v2))\}
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.
                \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{}  \{(||f  x||  \mleq{}  ||f  y||)
                                      \mwedge{}  (\mexists{}i:\mBbbZ{}
                                              ((\mforall{}j:\mBbbN{}||f  x||.  f  y[j]  =  f  x[j]  supposing  \mneg{}(j  =  i))
                                              \mwedge{}  (||f  y||  =  (||f  x||  +  1))  \mwedge{}  (f  y[||f  x||]  =  INITIAL) 
                                                  supposing  ||f  x||  <  ||f  y||))\}))) 
                supposing  ||W||  \mgeq{}  1  ))


By

(Auto
  THEN  All  (RepUR  ``ts-reachable  ts-rel  consensus-ts4  ts-type  ts-init``)\mcdot{}
  THEN  D  -3
  THEN  D  -2
  THEN  Unfold  `guard`  0
  THEN  BetterSplitAndConcl)

---

Home Index