3. (listp l) => (delete x l) = (delete* x l)

phi: (listp l) => (delete-t x l nil) = (delete x l)

a. (not (listp l)) => phi
C1. (not (listp l))
C2. (listp l)
C3. (listp acc)
C4. nil { C1, C2 }

b. (listp l) /\ (endp l) => phi
C1. (listp l)
C2. (endp l)
C3. (listp acc)

(delete-t x l nil)
= { C2, def. delete-t }
nil
= { C2, def. delete }
(delete x l)

c. (listp l) /\ (equal x (first l)) /\ phi|((l (rest l)) (acc nil)) => phi
C1. (listp l)
C2. (listp acc)
C3. (equal x (first l))
C4. (listp (rest l)) => (delete-t x (rest l) nil) = (delete x (rest l))
C5. (listp (rest l)) { C1, def. listp }
C6. (delete-t x (rest l) nil) = (delete x (rest l)) { C3, C4, MP }

(delete-t x l nil)
= { C2, def. delete-t }
(delete-t x (rest l) nil)
= { C5 }
(delete x (rest l))

d. (listp l) /\ (not (equal x (first l))) /\ phi|((l (rest l)) (acc nil)) => phi
C1. (listp l)
C2. (listp acc)
C3. (not (equal x (first l)))
C4. (listp (rest l)) => (delete-t x (rest l) nil) = (delete x (rest l))
C5. (listp (rest l)) { C1, def. listp }
C6. (delete-t x (rest l) nil) = (delete x (rest l)) { C4, C5, MP }

(delete-t x l nil)
{ Lemma2|((acc nil)) }
(app (delete x l) nil)
{ def. app }
(delete x l)

Lemma2: (listp l) /\ (listp acc) => (delete-t x l acc) = (app (delete x l) acc)

1. (not (listp l)) /\ (not (listp acc)) => Lemma2
C1. (not (listp l))
C2. (not (listp acc))
C3. (listp l)
C4. (listp acc)
C5. nil { C1, C2, C3, C4 }

2. (listp l) /\ (listp acc) /\ (endp l) => Lemma2
C1. (listp l)
C2. (listp acc)
C3. (endp l)

(delete-t x l acc)
= { C3, def. delete-t }
acc
= { C3, def. app }
(app (delete x l) acc)

3. (listp l) /\ (listp acc) /\ (equal x (first l)) /\ Lemma2|((l (rest l))) => Lemma2
C1. (listp l)
C2. (listp acc)
C3. (equal x (first l))
C4. (listp (rest l)) /\ (listp acc) => (delete-t x (rest l) acc) = (delete x (rest l))
C5. (listp (rest l)) { C1, def. listp }
C6. (delete-t x (rest l) acc) = (app (delete x (rest l)) acc) { C2, C4, C5, MP }

(delete-t x l acc)
= { C3, def. delete-t }
(delete-t x (rest l) acc)
= { C6 }
(app (delete x (rest l)) acc)
= { C3, def. delete }
(app (delete x l) acc)

4. (listp l) /\ (listp acc) /\ (not (equal x (first l))) /\ Lemma2|((l (rest l)) (acc (app acc (list (first l))))) => Lemma2
C1. (listp l)
C2. (listp acc)
C3. (not (equal x (first l)))
C4. (listp (rest l)) /\ (listp (app acc (list (first l)))) => (delete-t x (rest l) (app acc (list (first l)))) = (app (delete x (rest l)) (app acc (list (first l))))
C5. (listp (rest l)) { C1, def. listp }
C6. (listp (app acc (list (first l)))) { C2, def. app, def. listp }
C7. (delete-t x (rest l) (app acc (list (first l)))) = (app (delete x (rest l)) (app acc (list (first l))))

(delete-t x l acc)
= { C3, def. delete-t }
(delete-t x (rest l) (app acc (list (first l))))
= { C7 }
(app (delete x (rest l)) (app acc (list (first l))))
= { associativity of app }
(app (app (delete x (rest l)) (list (first l))) acc)
= { def. app }
(app (cons (first l) (delete x (rest l))) acc)
= { C3, def. delete }
(app (delete x l) acc)