---

Step * 1 1 1 1 1 1 1 1 of Lemma consensus-ts5-true-knowledge


1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. x1 : ConsensusState@i
5. x2 : Knowledge(ConsensusState)@i
6. a : {a:Id| (a ∈ A)} @i
7. v : b:Id fp-> ℤ × (ℤ × V + Top)@i
8. Knowledge(x2;a) = v ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
9. b : Id@i
10. \\%2 : (b ∈ A)@i
11. ↑b ∈ dom(v)
12. v2 : ℤ@i
13. x : ℤ × V@i
14. v(b) = <v2, inl x> ∈ (ℤ × (ℤ × V + Top))@i
⊢ SqStable((v2 ≤ Inning(x1;b))
           ∧ let k,v = x 
             in k < v2
                ∧ (↑k ∈ dom(Estimate(x1;b)))
                ∧ (Estimate(x1;b)(k) = v ∈ V)
                ∧ (∀i:ℤ. ¬↑i ∈ dom(Estimate(x1;b)) supposing k < i ∧ i < v2) 
           supposing True)
BY
{ (D -2 THEN Reduce 0) }

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. x1 : ConsensusState@i
5. x2 : Knowledge(ConsensusState)@i
6. a : {a:Id| (a ∈ A)} @i
7. v : b:Id fp-> ℤ × (ℤ × V + Top)@i
8. Knowledge(x2;a) = v ∈ b:Id fp-> ℤ × (ℤ × V + Top)@i
9. b : Id@i
10. \\%2 : (b ∈ A)@i
11. ↑b ∈ dom(v)
12. v2 : ℤ@i
13. x3 : ℤ@i
14. x4 : V@i
15. v(b) = <v2, inl <x3, x4>> ∈ (ℤ × (ℤ × V + Top))@i
⊢ SqStable((v2 ≤ Inning(x1;b))
           ∧ x3 < v2
           ∧ (↑x3 ∈ dom(Estimate(x1;b)))
           ∧ (Estimate(x1;b)(x3) = x4 ∈ V)
           ∧ (∀i:ℤ. ¬↑i ∈ dom(Estimate(x1;b)) supposing x3 < i ∧ i < v2) 
           supposing True)

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
4.  x1  :  ConsensusState@i
5.  x2  :  Knowledge(ConsensusState)@i
6.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
7.  v  :  b:Id  fp->  \mBbbZ{}  \mtimes{}  (\mBbbZ{}  \mtimes{}  V  +  Top)@i
8.  Knowledge(x2;a)  =  v@i
9.  b  :  Id@i
10.  \mbackslash{}\mbackslash{}\%2  :  (b  \mmember{}  A)@i
11.  \muparrow{}b  \mmember{}  dom(v)
12.  v2  :  \mBbbZ{}@i
13.  x  :  \mBbbZ{}  \mtimes{}  V@i
14.  v(b)  =  <v2,  inl  x>@i
\mvdash{}  SqStable((v2  \mleq{}  Inning(x1;b))
                      \mwedge{}  let  k,v  =  x 
                          in  k  <  v2
                                \mwedge{}  (\muparrow{}k  \mmember{}  dom(Estimate(x1;b)))
                                \mwedge{}  (Estimate(x1;b)(k)  =  v)
                                \mwedge{}  (\mforall{}i:\mBbbZ{}.  \mneg{}\muparrow{}i  \mmember{}  dom(Estimate(x1;b))  supposing  k  <  i  \mwedge{}  i  <  v2) 
                      supposing  True)


By

(D  -2  THEN  Reduce  0)

---

Home Index