---

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


1. X : Type
2. as : X List List@i
3. bs : X List List@i
4. ∀b:X List. ((b ∈ as) ⇒ (∃a:X List. ((a ∈ bs) ∧ a ⊆ b)))
5. a : X List@i
6. (a ∈ as)
7. ↑isaxiom(a)
8. a1 : X List
9. (a1 ∈ bs)
10. a1 ⊆ a
11. (a1 ∈ bs)
⊢ ↑isaxiom(a1)
BY
{ ((DVar `a' THEN All Reduce THEN Try (Trivial)) THEN DVar `a1' THEN All Reduce THEN Try (Trivial)) }

1
1. X : Type
2. as : X List List@i
3. bs : X List List@i
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

---

Latex:

---

Latex:

1.  X  :  Type
2.  as  :  X  List  List@i
3.  bs  :  X  List  List@i
4.  \mforall{}b:X  List.  ((b  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}a:X  List.  ((a  \mmember{}  bs)  \mwedge{}  a  \msubseteq{}  b)))
5.  a  :  X  List@i
6.  (a  \mmember{}  as)
7.  \muparrow{}isaxiom(a)
8.  a1  :  X  List
9.  (a1  \mmember{}  bs)
10.  a1  \msubseteq{}  a
11.  (a1  \mmember{}  bs)
\mvdash{}  \muparrow{}isaxiom(a1)


By

---

Latex:
((DVar  `a'  THEN  All  Reduce  THEN  Try  (Trivial))  THEN  DVar  `a1'  THEN  All  Reduce  THEN  Try  (Trivial))

---

Home Index