---

Step * 1 of Lemma l_disjoint_append


1. T : Type
2. a : T List
3. b : T List
4. c : T List
5. ∀x:T. (¬((x ∈ a) ∧ (x ∈ b)))
6. ∀x:T. (¬((x ∈ a) ∧ (x ∈ c)))
7. x : T
8. ¬((x ∈ a) ∧ (x ∈ c))
9. ¬((x ∈ a) ∧ (x ∈ b))
⊢ ¬((x ∈ a) ∧ ((x ∈ b) ∨ (x ∈ c)))
BY
{ TACTIC:(((D 0 THEN Auto THEN (D (-1))) 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{}  a)  \mwedge{}  (x  \mmember{}  b)))
6.  \mforall{}x:T.  (\mneg{}((x  \mmember{}  a)  \mwedge{}  (x  \mmember{}  c)))
7.  x  :  T
8.  \mneg{}((x  \mmember{}  a)  \mwedge{}  (x  \mmember{}  c))
9.  \mneg{}((x  \mmember{}  a)  \mwedge{}  (x  \mmember{}  b))
\mvdash{}  \mneg{}((x  \mmember{}  a)  \mwedge{}  ((x  \mmember{}  b)  \mvee{}  (x  \mmember{}  c)))


By

---

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

---

Home Index