---

Step * 1 1 1 1 1 1 of Lemma fdl-is-1_wf


1. X : Type
2. as : X List List
3. bs : X List List
4. ∀b:X List. ((b ∈ as) ⇒ (∃a:X List. ((a ∈ bs) ∧ a ⊆ b)))
5. ([] ∈ as)
6. True
7. u : X
8. v : X List
9. ([u / v] ∈ bs)
10. [u / v] ⊆ []
11. ([u / v] ∈ bs)
⊢ False
BY
{ (D -2 With ⌜0⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  as  :  X  List  List
3.  bs  :  X  List  List
4.  \mforall{}b:X  List.  ((b  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}a:X  List.  ((a  \mmember{}  bs)  \mwedge{}  a  \msubseteq{}  b)))
5.  ([]  \mmember{}  as)
6.  True
7.  u  :  X
8.  v  :  X  List
9.  ([u  /  v]  \mmember{}  bs)
10.  [u  /  v]  \msubseteq{}  []
11.  ([u  /  v]  \mmember{}  bs)
\mvdash{}  False


By

---

Latex:
(D  -2  With  \mkleeneopen{}0\mkleeneclose{}    THEN  Auto)

---

Home Index