---

Step * of Lemma cs-knowledge_wf

∀[V:Type]. ∀[A:Id List]. ∀[a:{a:Id| (a ∈ A)} ]. ∀[x:Knowledge(ConsensusState)].
  (Knowledge(x;a) ∈ b:Id fp-> ℤ × (ℤ × V + Top))
BY
{ (Unfolds ``consensus-state5 cs-knowledge`` 0 THEN Auto) }

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[a:\{a:Id|  (a  \mmember{}  A)\}  ].  \mforall{}[x:Knowledge(ConsensusState)].
    (Knowledge(x;a)  \mmember{}  b:Id  fp->  \mBbbZ{}  \mtimes{}  (\mBbbZ{}  \mtimes{}  V  +  Top))


By

(Unfolds  ``consensus-state5  cs-knowledge``  0  THEN  Auto)

---

Home Index