---

Step * 1 2 2 of Lemma decidable__archive-condition


1. [V] : Type
2. v0 : V@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ─→ V@i
6. u : consensus-rcv(V;A)
7. v : consensus-rcv(V;A) List
8. v1 : 𝔹@i
9. v3 : ℤ@i
10. v5 : {a:Id| (a ∈ A)}  List@i
11. v7 : V List@i
12. v8 : V@i
13. accumulate (with value s and list item r):
     consensus-accum-num((2 * t) + 1;f;s;r)
    over list:
      v
    with starting value:
     consensus-accum-num((2 * t) + 1;f;<ff, 0, [], [], v0>;u))
= <v1, v3, v5, v7, v8>
∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
14. ∀n:ℕ. ∀v@0:V.  (archive-condition(V;A;t;f;n;v@0;[u / v]) ⇐⇒ (↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v@0 = v8 ∈ V))@i
15. (¬False) ⇒ (1 ≤ v3)
⊢ Dec(∃n:ℕ. ∃v:V. ((↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v = v8 ∈ V)))
BY
{ (ThinTrivial
   THEN (AutoBoolCase ⌈v1⌉⋅
         THENL [(OrLeft THENM (InstConcl [⌈v3 - 1⌉;⌈v8⌉]⋅ THEN Auto))
               ; (OrRight THENM ((D 0 THENA Auto) THEN ExRepD THEN Auto'))]
   )
   THEN Auto) }

---

Latex:



1.  [V]  :  Type
2.  v0  :  V@i
3.  A  :  Id  List@i
4.  t  :  \mBbbN{}\msupplus{}@i
5.  f  :  (V  List)  {}\mrightarrow{}  V@i
6.  u  :  consensus-rcv(V;A)
7.  v  :  consensus-rcv(V;A)  List
8.  v1  :  \mBbbB{}@i
9.  v3  :  \mBbbZ{}@i
10.  v5  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
11.  v7  :  V  List@i
12.  v8  :  V@i
13.  accumulate  (with  value  s  and  list  item  r):
          consensus-accum-num((2  *  t)  +  1;f;s;r)
        over  list:
            v
        with  starting  value:
          consensus-accum-num((2  *  t)  +  1;f;<ff,  0,  [],  [],  v0>u))
=  <v1,  v3,  v5,  v7,  v8>@i
14.  \mforall{}n:\mBbbN{}.  \mforall{}v@0:V.
            (archive-condition(V;A;t;f;n;v@0;[u  /  v])  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}v1)  \mwedge{}  ((n  +  1)  =  v3)  \mwedge{}  (v@0  =  v8))@i
15.  (\mneg{}False)  {}\mRightarrow{}  (1  \mleq{}  v3)
\mvdash{}  Dec(\mexists{}n:\mBbbN{}.  \mexists{}v:V.  ((\muparrow{}v1)  \mwedge{}  ((n  +  1)  =  v3)  \mwedge{}  (v  =  v8)))


By

(ThinTrivial
  THEN  (AutoBoolCase  \mkleeneopen{}v1\mkleeneclose{}\mcdot{}
              THENL  [(OrLeft  THENM  (InstConcl  [\mkleeneopen{}v3  -  1\mkleeneclose{};\mkleeneopen{}v8\mkleeneclose{}]\mcdot{}  THEN  Auto))
                          ;  (OrRight  THENM  ((D  0  THENA  Auto)  THEN  ExRepD  THEN  Auto'))]
  )
  THEN  Auto)

---

Home Index