---

Step * 1 1 of Lemma archive-condition-threshold-accum


1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. L : consensus-rcv(V;A) List@i
7. v1 : 𝔹@i
8. v3 : ℤ@i
9. v5 : {a:Id| (a ∈ A)}  List@i
10. v7 : V List@i
11. v8 : V@i
12. consensus-accum-num-state(t;f;v0;L) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
13. ↑v1
⊢ (∀[v@0:V]. ∀[i:ℤ].  True supposing archive-condition(V;A;t;f;i;v@0;L))
⇒ archive-condition(V;A;t;f;v3 - 1;v8;L) supposing True
⇒ (∀n:ℕ. ∀v@0:V.  (archive-condition(V;A;t;f;n;v@0;L) ⇐⇒ True ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v@0 = v8 ∈ V)))
BY
{ ((UnivCD THENA Auto) THEN ThinTrivial) }

1
1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. L : consensus-rcv(V;A) List@i
7. v1 : 𝔹@i
8. v3 : ℤ@i
9. v5 : {a:Id| (a ∈ A)}  List@i
10. v7 : V List@i
11. v8 : V@i
12. consensus-accum-num-state(t;f;v0;L) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
13. ↑v1
14. ∀[v@0:V]. ∀[i:ℤ].  True supposing archive-condition(V;A;t;f;i;v@0;L)@i
15. n : ℕ@i
16. v@0 : V@i
17. archive-condition(V;A;t;f;v3 - 1;v8;L)
⊢ archive-condition(V;A;t;f;n;v@0;L) ⇐⇒ True ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v@0 = v8 ∈ V)

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  t  :  \mBbbN{}\msupplus{}@i
4.  f  :  (V  List)  {}\mrightarrow{}  V@i
5.  v0  :  V@i
6.  L  :  consensus-rcv(V;A)  List@i
7.  v1  :  \mBbbB{}@i
8.  v3  :  \mBbbZ{}@i
9.  v5  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
10.  v7  :  V  List@i
11.  v8  :  V@i
12.  consensus-accum-num-state(t;f;v0;L)  =  <v1,  v3,  v5,  v7,  v8>@i
13.  \muparrow{}v1
\mvdash{}  (\mforall{}[v@0:V].  \mforall{}[i:\mBbbZ{}].    True  supposing  archive-condition(V;A;t;f;i;v@0;L))
{}\mRightarrow{}  archive-condition(V;A;t;f;v3  -  1;v8;L)  supposing  True
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}v@0:V.    (archive-condition(V;A;t;f;n;v@0;L)  \mLeftarrow{}{}\mRightarrow{}  True  \mwedge{}  ((n  +  1)  =  v3)  \mwedge{}  (v@0  =  v8)))


By

((UnivCD  THENA  Auto)  THEN  ThinTrivial)

---

Home Index