---

Step * of Lemma three-cs-safety2

∀[V:Type]
  ∀eq:EqDecider(V). ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ⟶ V.
    ((∀vs:V List. (f vs ∈ vs) supposing ||vs|| ≥ 1 )
    ⇒ (∀v:V. ∀s:ts-reachable(three-consensus-ts(V;A;t;f)).
          (three-cs-decided(V;A;t;f;s;v) ⇒ (∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A))))))
BY
{ (InstLemma `three-cs-archive-invariant` []
   THEN RepeatFor 6 (ParallelLast')
   THEN Auto
   THEN (D -1 THEN ExRepD)
   THEN Try ((RepUR ``ts-type three-consensus-ts`` -2 THEN Trivial⋅))) }

1
1. [V] : Type
2. eq : EqDecider(V)@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ⟶ V@i
6. ∀vs:V List. (f vs ∈ vs) supposing ||vs|| ≥ 1 @i
7. ∀s:ts-reachable(three-consensus-ts(V;A;t;f)). ∀v:V. ∀a:{a:Id| (a ∈ A)} . ∀n:ℤ. ∀L:consensus-rcv(V;A) List.
     (L ≤ s a ⇒ archive-condition(V;A;t;f;n;v;L) ⇒ (∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A))))
8. v : V@i
9. s : ts-reachable(three-consensus-ts(V;A;t;f))@i
10. i : ℤ@i
11. ws : {a:Id| (a ∈ A)}  List@i
12. no_repeats({a:Id| (a ∈ A)} ;ws)@i
13. ||ws|| = ((2 * t) + 1) ∈ ℤ@i
14. (∀a∈ws.∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;v;L)))@i
⊢ (∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A)))

---

Latex:

---

Latex:
\mforall{}[V:Type]
    \mforall{}eq:EqDecider(V).  \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.
        ((\mforall{}vs:V  List.  (f  vs  \mmember{}  vs)  supposing  ||vs||  \mgeq{}  1  )
        {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)).
                    (three-cs-decided(V;A;t;f;s;v)  {}\mRightarrow{}  (\mexists{}a\mmember{}A.  (||s  a||  \mgeq{}  1  )  \mwedge{}  (hd(s  a)  =  Init[v])))))


By

---

Latex:
(InstLemma  `three-cs-archive-invariant`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Auto
  THEN  (D  -1  THEN  ExRepD)
  THEN  Try  ((RepUR  ``ts-type  three-consensus-ts``  -2  THEN  Trivial\mcdot{})))

---

Home Index