Aggressive case splitting rule to reduce
Theorem:
(defthm take-of-take-split (equal (take a (take b x)) (if (<= (nfix a) (nfix b)) (take a x) (append (take b x) (repeat (- (nfix a) (nfix b)) nil)))))
This rule may sometimes cause too much case splitting. If you disable it,
nests of
Theorem:
(defthm take-of-take-same (equal (take a (take a x)) (take a x)))
Theorem:
(defthm take-more-of-take-fewer (implies (< (nfix b) (nfix a)) (equal (take a (take b x)) (append (take b x) (repeat (- (nfix a) (nfix b)) nil)))))
Theorem:
(defthm take-fewer-of-take-more (implies (<= (nfix a) (nfix b)) (equal (take a (take b x)) (take a x))))