---

Step * 2 1 2 of Lemma cs-ref-map-step


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. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
10. y : ConsensusState@i
11. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
12. a : {a:Id| (a ∈ A)} @i
13. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id)) ⇒ ((Inning(y;b) = Inning(x;b) ∈ ℤ) ∧ (Estimate(y;b) = Estimate(x;b) ∈ i:ℤ fp-> V)))@i
14. ((Inning(y;a) = (Inning(x;a) + 1) ∈ ℤ) ∧ (Estimate(y;a) = Estimate(x;a) ∈ i:ℤ fp-> V))
∨ ((Inning(y;a) = Inning(x;a) ∈ ℤ)
  ∧ (¬(Inning(x;a) ∈ fpf-domain(Estimate(x;a))))
  ∧ (∃v:V
      (state x may consider v in inning Inning(x;a)
      ∧ (Estimate(y;a) = Estimate(x;a) ⊕ Inning(x;a) : v ∈ i:ℤ fp-> V))))@i
15. ||f x|| ≤ ||f y||
16. j : ℕ||f x||@i
17. ¬(j = Inning(x;a) ∈ ℤ)
18. ∀b:{a:Id| (a ∈ A)} . ((j ∈ fpf-domain(Estimate(y;b))) ⇐⇒ (j ∈ fpf-domain(Estimate(x;b))))
⊢ f y[j] = f x[j] ∈ consensus-state3(V)
BY
{ Assert ⌈∀b:{a:Id| (a ∈ A)} 
            (((j ∈ fpf-domain(Estimate(y;b))) ∨ (j ∈ fpf-domain(Estimate(x;b))))
            ⇒ (Estimate(y;b)(j) = Estimate(x;b)(j) ∈ V))⌉⋅ }

1
.....assertion..... 
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. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
10. y : ConsensusState@i
11. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
12. a : {a:Id| (a ∈ A)} @i
13. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id)) ⇒ ((Inning(y;b) = Inning(x;b) ∈ ℤ) ∧ (Estimate(y;b) = Estimate(x;b) ∈ i:ℤ fp-> V)))@i
14. ((Inning(y;a) = (Inning(x;a) + 1) ∈ ℤ) ∧ (Estimate(y;a) = Estimate(x;a) ∈ i:ℤ fp-> V))
∨ ((Inning(y;a) = Inning(x;a) ∈ ℤ)
  ∧ (¬(Inning(x;a) ∈ fpf-domain(Estimate(x;a))))
  ∧ (∃v:V
      (state x may consider v in inning Inning(x;a)
      ∧ (Estimate(y;a) = Estimate(x;a) ⊕ Inning(x;a) : v ∈ i:ℤ fp-> V))))@i
15. ||f x|| ≤ ||f y||
16. j : ℕ||f x||@i
17. ¬(j = Inning(x;a) ∈ ℤ)
18. ∀b:{a:Id| (a ∈ A)} . ((j ∈ fpf-domain(Estimate(y;b))) ⇐⇒ (j ∈ fpf-domain(Estimate(x;b))))
⊢ ∀b:{a:Id| (a ∈ A)} 
    (((j ∈ fpf-domain(Estimate(y;b))) ∨ (j ∈ fpf-domain(Estimate(x;b)))) ⇒ (Estimate(y;b)(j) = Estimate(x;b)(j) ∈ V))

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. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
10. y : ConsensusState@i
11. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
12. a : {a:Id| (a ∈ A)} @i
13. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id)) ⇒ ((Inning(y;b) = Inning(x;b) ∈ ℤ) ∧ (Estimate(y;b) = Estimate(x;b) ∈ i:ℤ fp-> V)))@i
14. ((Inning(y;a) = (Inning(x;a) + 1) ∈ ℤ) ∧ (Estimate(y;a) = Estimate(x;a) ∈ i:ℤ fp-> V))
∨ ((Inning(y;a) = Inning(x;a) ∈ ℤ)
  ∧ (¬(Inning(x;a) ∈ fpf-domain(Estimate(x;a))))
  ∧ (∃v:V
      (state x may consider v in inning Inning(x;a)
      ∧ (Estimate(y;a) = Estimate(x;a) ⊕ Inning(x;a) : v ∈ i:ℤ fp-> V))))@i
15. ||f x|| ≤ ||f y||
16. j : ℕ||f x||@i
17. ¬(j = Inning(x;a) ∈ ℤ)
18. ∀b:{a:Id| (a ∈ A)} . ((j ∈ fpf-domain(Estimate(y;b))) ⇐⇒ (j ∈ fpf-domain(Estimate(x;b))))
19. ∀b:{a:Id| (a ∈ A)} 
      (((j ∈ fpf-domain(Estimate(y;b))) ∨ (j ∈ fpf-domain(Estimate(x;b)))) ⇒ (Estimate(y;b)(j) = Estimate(x;b)(j) ∈ V))
⊢ f y[j] = f x[j] ∈ consensus-state3(V)

---

Latex:



1.  V  :  Type
2.  \{\mexists{}v1,v2:V.  (\mneg{}(v1  =  v2))\}@i
3.  A  :  Id  List@i
4.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
5.  ||W||  \mgeq{}  1 
6.  f  :  ConsensusState  {}\mrightarrow{}  (consensus-state3(V)  List)@i
7.  cs-ref-map-constraints(V;A;W;f)@i
8.  x  :  ConsensusState@i
9.  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  x@i
10.  y  :  ConsensusState@i
11.  (\mlambda{}a.<-1,  \motimes{}>)  rel\_star(ConsensusState;  \mlambda{}x,y.  CR[x,y])  y@i
12.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
13.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
            ((\mneg{}(b  =  a))  {}\mRightarrow{}  ((Inning(y;b)  =  Inning(x;b))  \mwedge{}  (Estimate(y;b)  =  Estimate(x;b))))@i
14.  ((Inning(y;a)  =  (Inning(x;a)  +  1))  \mwedge{}  (Estimate(y;a)  =  Estimate(x;a)))
\mvee{}  ((Inning(y;a)  =  Inning(x;a))
    \mwedge{}  (\mneg{}(Inning(x;a)  \mmember{}  fpf-domain(Estimate(x;a))))
    \mwedge{}  (\mexists{}v:V
            (state  x  may  consider  v  in  inning  Inning(x;a)
            \mwedge{}  (Estimate(y;a)  =  Estimate(x;a)  \moplus{}  Inning(x;a)  :  v))))@i
15.  ||f  x||  \mleq{}  ||f  y||
16.  j  :  \mBbbN{}||f  x||@i
17.  \mneg{}(j  =  Inning(x;a))
18.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((j  \mmember{}  fpf-domain(Estimate(y;b)))  \mLeftarrow{}{}\mRightarrow{}  (j  \mmember{}  fpf-domain(Estimate(x;b))))
\mvdash{}  f  y[j]  =  f  x[j]


By

Assert  \mkleeneopen{}\mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
                    (((j  \mmember{}  fpf-domain(Estimate(y;b)))  \mvee{}  (j  \mmember{}  fpf-domain(Estimate(x;b))))
                    {}\mRightarrow{}  (Estimate(y;b)(j)  =  Estimate(x;b)(j)))\mkleeneclose{}\mcdot{}

---

Home Index