---

Step * of Lemma decidable__archive-condition

∀[V:Type]
  (V
  ⇒ (∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀L:consensus-rcv(V;A) List.
        Dec(∃n:ℕ. ∃v:V. archive-condition(V;A;t;f;n;v;L))))
BY
{ (Auto
   THEN RenameVar `v0' 2
   THEN (InstLemma `archive-condition-threshold-accum` [⌈V⌉;⌈A⌉;⌈t⌉;⌈f⌉;⌈v0⌉;⌈L⌉]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddrType ⌈𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V⌉ [1;2;2;2;1]⋅ THENA Auto)
   THEN RepeatFor 4 (D -2)
   THEN Reduce 0
   THEN Auto
   THEN RWO "-1" 0
   THEN Auto) }

1
.....decidable?..... 
1. [V] : Type
2. v0 : V@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ─→ 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. accumulate (with value s and list item r):
     consensus-accum-num((2 * t) + 1;f;s;r)
    over list:
      L
    with starting value:
     <ff, 0, [], [], v0>)
= <v1, v3, v5, v7, v8>
∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
13. ∀n:ℕ. ∀v@0:V.  (archive-condition(V;A;t;f;n;v@0;L) ⇐⇒ (↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v@0 = v8 ∈ V))@i
⊢ Dec(∃n:ℕ. ∃v:V. ((↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v = v8 ∈ V)))

---

Latex:


\mforall{}[V:Type]
    (V
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.  \mforall{}L:consensus-rcv(V;A)  List.
                Dec(\mexists{}n:\mBbbN{}.  \mexists{}v:V.  archive-condition(V;A;t;f;n;v;L))))


By

(Auto
  THEN  RenameVar  `v0'  2
  THEN  (InstLemma  `archive-condition-threshold-accum`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}v0\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbB{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \{a:Id|  (a  \mmember{}  A)\}    List  \mtimes{}  V  List  \mtimes{}  V\mkleeneclose{}  [1;2;2;2;1]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  (D  -2)
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index