---

Step * of Lemma correct-consistent-class_wf

∀[Correct:Id ─→ ℙ]. ∀[Info,T:Type]. ∀[R:T ─→ T ─→ ℙ]. ∀[X:EClass(T)]. ∀[es:EO+(Info)].
  (any x,y from X satisfy
   R[x;y]
   at locations i.Correct[i] ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[Correct:Id  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Info,T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].
    (any  x,y  from  X  satisfy
      R[x;y]
      at  locations  i.Correct[i]  \mmember{}  \mBbbP{})


By

ProveWfLemma

---

Home Index