---

Step * of Lemma archive-condition_wf

∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ]. ∀[f:(V List) ─→ V]. ∀[L:consensus-rcv(V;A) List]. ∀[n:ℤ]. ∀[v:V].
  (archive-condition(V;A;t;f;n;v;L) ∈ ℙ)
BY
{ (Unfold `archive-condition` 0 THEN Auto) }

---

Latex:


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


By

(Unfold  `archive-condition`  0  THEN  Auto)

---

Home Index