---

Step * 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
⊢ (∀[v:V]. ∀[i:ℤ].  ↑(fst(consensus-accum-num-state(t;f;v0;L))) supposing archive-condition(V;A;t;f;i;v;L))
⇒ let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in archive-condition(V;A;t;f;i - 1;v;L) supposing ↑b
⇒ (∀n:ℕ. ∀v:V.
      (archive-condition(V;A;t;f;n;v;L)
      ⇐⇒ let b,i,as,vs,w = consensus-accum-num-state(t;f;v0;L) in (↑b) ∧ ((n + 1) = i ∈ ℤ) ∧ (v = w ∈ V)))
BY
{ (GenConclAtAddr [2;1;1] THEN RepeatFor 4 (D -2) THEN Reduce 0 THEN AutoBoolCase ⌈v1⌉⋅) }

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
⊢ (∀[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)))

2
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. ¬↑v1
9. v3 : ℤ@i
10. v5 : {a:Id| (a ∈ A)}  List@i
11. v7 : V List@i
12. v8 : V@i
13. consensus-accum-num-state(t;f;v0;L) = <ff, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
⊢ (∀[v@0:V]. ∀[i:ℤ].  False supposing archive-condition(V;A;t;f;i;v@0;L))
⇒ archive-condition(V;A;t;f;v3 - 1;v8;L) supposing False
⇒ (∀n:ℕ. ∀v@0:V.  (archive-condition(V;A;t;f;n;v@0;L) ⇐⇒ False ∧ ((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
\mvdash{}  (\mforall{}[v:V].  \mforall{}[i:\mBbbZ{}].
          \muparrow{}(fst(consensus-accum-num-state(t;f;v0;L)))  supposing  archive-condition(V;A;t;f;i;v;L))
{}\mRightarrow{}  let  b,i,as,vs,v  =  consensus-accum-num-state(t;f;v0;L)  in  archive-condition(V;A;t;f;i  -  1;v;L) 
                                                                                                                        supposing  \muparrow{}b
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}v:V.
            (archive-condition(V;A;t;f;n;v;L)
            \mLeftarrow{}{}\mRightarrow{}  let  b,i,as,vs,w  =  consensus-accum-num-state(t;f;v0;L)  in  (\muparrow{}b)  \mwedge{}  ((n  +  1)  =  i)  \mwedge{}  (v  =  w)))


By

(GenConclAtAddr  [2;1;1]  THEN  RepeatFor  4  (D  -2)  THEN  Reduce  0  THEN  AutoBoolCase  \mkleeneopen{}v1\mkleeneclose{}\mcdot{})

---

Home Index