---

Step * of Lemma complete_wf

∀[S:System]. (complete{i:l}(S) ∈ ℙ')
BY
{ (Intros THEN Unfold `complete` 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
1. S : System
⊢ (∀n∈S.(∃y∈snd(n). |= dl-conj(fst(n)) ⇒ y)) ∈ ℙ'

2
.....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)))
  ∈ ℙ'

---

Latex:

---

Latex:
\mforall{}[S:System].  (complete\{i:l\}(S)  \mmember{}  \mBbbP{}')


By

---

Latex:
(Intros  THEN  Unfold  `complete`  0  THEN  MemCD)

---

Home Index