---

Step * 2 1 of Lemma consensus-refinement4


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. 1 < ||W||@i
7. two-intersection(A;W)@i
⊢ ∀x,y:ts-reachable(consensus-ts5(V;A;W)).
    ((x ts-rel(consensus-ts5(V;A;W)) y) ⇒ (((λs.(fst(s))) x) (ts-rel(consensus-ts4(V;A;W))^*) ((λs.(fst(s))) y)))
BY
{ ((Auto THEN Reduce 0)
   THEN (Assert (x ∈ ts-reachable(consensus-ts5(V;A;W))) ∧ (y ∈ ts-reachable(consensus-ts5(V;A;W))) BY
               Auto)
   THEN (D -4 THEN Thin (-4))
   THEN (D -3 THEN Thin (-3))
   THEN (RepUR ``ts-type consensus-ts5`` -4 THEN D -4)
   THEN RepUR ``ts-type consensus-ts5`` -3
   THEN D -3
   THEN RepUR ``consensus-ts4 ts-rel ts-type`` 0
   THEN RepUR ``consensus-ts5 ts-rel`` -2
   THEN RepeatFor 2 (D -2)
   THEN SplitOrHyps
   THEN All Reduce
   THEN D -2
   THEN ExRepD) }

1
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. v : V@i
4. v' : V@i
5. ¬(v = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)}  List List@i
8. 1 < ||W||@i
9. two-intersection(A;W)@i
10. x1 : ConsensusState@i
11. x2 : Knowledge(ConsensusState)@i
12. y1 : ConsensusState@i
13. y2 : Knowledge(ConsensusState)@i
14. a : {a:Id| (a ∈ A)} @i
15. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id))
      ⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
         ∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
         ∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
16. Inning(y1;a) = (Inning(x1;a) + 1) ∈ ℤ@i
17. Estimate(y1;a) = Estimate(x1;a) ∈ i:ℤ fp-> V@i
18. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
19. <x1, x2> ∈ ts-reachable(consensus-ts5(V;A;W))
20. <y1, y2> ∈ ts-reachable(consensus-ts5(V;A;W))
⊢ x1 ((λx,y. CR[x,y])^*) y1

2
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. v1 : V@i
4. v' : V@i
5. ¬(v1 = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)}  List List@i
8. 1 < ||W||@i
9. two-intersection(A;W)@i
10. x1 : ConsensusState@i
11. x2 : Knowledge(ConsensusState)@i
12. y1 : ConsensusState@i
13. y2 : Knowledge(ConsensusState)@i
14. a : {a:Id| (a ∈ A)} @i
15. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id))
      ⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
         ∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
         ∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
16. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
17. Knowledge(y2;a) = Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
18. ¬(Inning(x1;a) ∈ fpf-domain(Estimate(x1;a)))@i
19. v : V@i
20. may consider v in inning Inning(x1;a) based on knowledge (Knowledge(x2;a))@i
21. Estimate(y1;a) = Estimate(x1;a) ⊕ Inning(x1;a) : v ∈ i:ℤ fp-> V@i
22. <x1, x2> ∈ ts-reachable(consensus-ts5(V;A;W))
23. <y1, y2> ∈ ts-reachable(consensus-ts5(V;A;W))
⊢ x1 ((λx,y. CR[x,y])^*) y1

3
1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. v : V@i
4. v' : V@i
5. ¬(v = v' ∈ V)@i
6. A : Id List@i
7. W : {a:Id| (a ∈ A)}  List List@i
8. 1 < ||W||@i
9. two-intersection(A;W)@i
10. x1 : ConsensusState@i
11. x2 : Knowledge(ConsensusState)@i
12. y1 : ConsensusState@i
13. y2 : Knowledge(ConsensusState)@i
14. a : {a:Id| (a ∈ A)} @i
15. ∀b:{a:Id| (a ∈ A)} 
      ((¬(b = a ∈ Id))
      ⇒ ((Inning(y1;b) = Inning(x1;b) ∈ ℤ)
         ∧ (Estimate(y1;b) = Estimate(x1;b) ∈ i:ℤ fp-> V)
         ∧ (Knowledge(y2;b) = Knowledge(x2;b) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
16. Inning(y1;a) = Inning(x1;a) ∈ ℤ@i
17. Estimate(y1;a) = Estimate(x1;a) ∈ i:ℤ fp-> V@i
18. b : {a:Id| (a ∈ A)} @i
19. i : ℤ@i
20. i ≤ Inning(x1;b)@i
21. ((∀j:ℤ. (j < i ⇒ (¬↑j ∈ dom(Estimate(x1;b)))))
∧ (Knowledge(y2;a) = b : <i, inr ⋅ > ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top)))
∨ (∃j:ℤ
    (j < i
    ∧ (↑j ∈ dom(Estimate(x1;b)))
    ∧ (∀k:ℤ. (j < k ⇒ k < i ⇒ (¬↑k ∈ dom(Estimate(x1;b)))))
    ∧ (Knowledge(y2;a) = b : <i, inl <j, Estimate(x1;b)(j)>> ⊕ Knowledge(x2;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top))))@i
22. <x1, x2> ∈ ts-reachable(consensus-ts5(V;A;W))
23. <y1, y2> ∈ ts-reachable(consensus-ts5(V;A;W))
⊢ x1 ((λx,y. CR[x,y])^*) y1

---

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.  1  <  ||W||@i
7.  two-intersection(A;W)@i
\mvdash{}  \mforall{}x,y:ts-reachable(consensus-ts5(V;A;W)).
        ((x  ts-rel(consensus-ts5(V;A;W))  y)
        {}\mRightarrow{}  (((\mlambda{}s.(fst(s)))  x)  (ts-rel(consensus-ts4(V;A;W))\^{}*)  ((\mlambda{}s.(fst(s)))  y)))


By

((Auto  THEN  Reduce  0)
  THEN  (Assert  (x  \mmember{}  ts-reachable(consensus-ts5(V;A;W)))  \mwedge{}  (y  \mmember{}  ts-reachable(consensus-ts5(V;A;W)))  BY
                          Auto)
  THEN  (D  -4  THEN  Thin  (-4))
  THEN  (D  -3  THEN  Thin  (-3))
  THEN  (RepUR  ``ts-type  consensus-ts5``  -4  THEN  D  -4)
  THEN  RepUR  ``ts-type  consensus-ts5``  -3
  THEN  D  -3
  THEN  RepUR  ``consensus-ts4  ts-rel  ts-type``  0
  THEN  RepUR  ``consensus-ts5  ts-rel``  -2
  THEN  RepeatFor  2  (D  -2)
  THEN  SplitOrHyps
  THEN  All  Reduce
  THEN  D  -2
  THEN  ExRepD)

---

Home Index