---

Step * of Lemma consensus-event-constraint_wf

∀[V:Type]. ∀[A:Id List]. ∀[a:{a:Id| (a ∈ A)} ]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[e:consensus-event(V;A)].
∀[x:consensus-state6(V;A)].
  (e@a allowed in state x ∈ ℙ)
BY
{ (Auto
   THEN Unfold `consensus-event-constraint` 0
   THEN Auto
   THEN GenConclAtAddr [2;1]
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (DVar  `z' THEN Try ((DVar `x1' THEN (DVar `x2' THENA Auto))))
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[a:\{a:Id|  (a  \mmember{}  A)\}  ].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].
\mforall{}[e:consensus-event(V;A)].  \mforall{}[x:consensus-state6(V;A)].
    (e@a  allowed  in  state  x  \mmember{}  \mBbbP{})


By

(Auto
  THEN  Unfold  `consensus-event-constraint`  0
  THEN  Auto
  THEN  GenConclAtAddr  [2;1]
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (DVar    `z'  THEN  Try  ((DVar  `x1'  THEN  (DVar  `x2'  THENA  Auto))))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index