---

Step * of Lemma cs-events-to-state_wf

∀[V:Type]. ∀[A:Id List]. ∀[s:consensus-state6(V;A)].
  (cs-events-to-state(A; s) ∈ ConsensusState × Knowledge(ConsensusState))
BY
{ (Unfolds ``consensus-state4 consensus-state5 consensus-state6`` 0
   THEN Unfold `cs-events-to-state` 0
   THEN Auto
   THEN GenConclAtAddr [2;1]
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[s:consensus-state6(V;A)].
    (cs-events-to-state(A;  s)  \mmember{}  ConsensusState  \mtimes{}  Knowledge(ConsensusState))


By

(Unfolds  ``consensus-state4  consensus-state5  consensus-state6``  0
  THEN  Unfold  `cs-events-to-state`  0
  THEN  Auto
  THEN  GenConclAtAddr  [2;1]
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index