---

Step * 2 of Lemma complete_wf

.....subterm..... T:t
2:n
1. S : System
⊢ ∃K:dl_KS. ∃f:node ⟶ worlds(K). (∀n∈S.(∀phi∈fst(n).dl_forces(K;tt;phi;f n)) ∧ (∀phi∈snd(n).dl_forces(K;ff;phi;f n)))
  ∈ ℙ'
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  S  :  System
\mvdash{}  \mexists{}K:dl\_KS
      \mexists{}f:node  {}\mrightarrow{}  worlds(K)
        (\mforall{}n\mmember{}S.(\mforall{}phi\mmember{}fst(n).dl\_forces(K;tt;phi;f  n))  \mwedge{}  (\mforall{}phi\mmember{}snd(n).dl\_forces(K;ff;phi;f  n)))  \mmember{}  \mBbbP{}'


By

---

Latex:
Auto

---

Home Index