---

Step * 1 of Lemma complete_wf

.....subterm..... T:t
1:n
1. S : System
⊢ (∀n∈S.(∃y∈snd(n). |= dl-conj(fst(n)) ⇒ y)) ∈ ℙ'
BY
{ (RepUR ``l_all l_exists`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  S  :  System
\mvdash{}  (\mforall{}n\mmember{}S.(\mexists{}y\mmember{}snd(n).  |=  dl-conj(fst(n))  {}\mRightarrow{}  y))  \mmember{}  \mBbbP{}'


By

---

Latex:
(RepUR  ``l\_all  l\_exists``  0  THEN  Auto)

---

Home Index