---

Step * 1 of Lemma l_disjoint_append2


1. T : Type
2. a : T List
3. b : T List
4. c : T List
5. ∀x:T. (¬((x ∈ b) ∧ (x ∈ a)))
6. ∀x:T. (¬((x ∈ c) ∧ (x ∈ a)))
7. x : T
8. ¬((x ∈ c) ∧ (x ∈ a))
9. ¬((x ∈ b) ∧ (x ∈ a))
⊢ ¬(((x ∈ b) ∨ (x ∈ c)) ∧ (x ∈ a))
BY
{ TACTIC:(((D 0 THEN Auto THEN (D (-2))) THENL [(D (-3)); (D (-4))]) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  T  List
3.  b  :  T  List
4.  c  :  T  List
5.  \mforall{}x:T.  (\mneg{}((x  \mmember{}  b)  \mwedge{}  (x  \mmember{}  a)))
6.  \mforall{}x:T.  (\mneg{}((x  \mmember{}  c)  \mwedge{}  (x  \mmember{}  a)))
7.  x  :  T
8.  \mneg{}((x  \mmember{}  c)  \mwedge{}  (x  \mmember{}  a))
9.  \mneg{}((x  \mmember{}  b)  \mwedge{}  (x  \mmember{}  a))
\mvdash{}  \mneg{}(((x  \mmember{}  b)  \mvee{}  (x  \mmember{}  c))  \mwedge{}  (x  \mmember{}  a))


By

---

Latex:
TACTIC:(((D  0  THEN  Auto  THEN  (D  (-2)))  THENL  [(D  (-3));  (D  (-4))])  THEN  Auto)

---

Home Index