(defun insert (x y)
  (if (endp y)
      (list x)
      (cons (append x y)
            (insert (cons (car y) x)
                    (cdr y)))))

(defun mappend-insert (x y)
  (if (endp y)
      nil
      (append (insert x (car y))
              (mappend-insert x (cdr y)))))

(defun permutations (x)
  (if (endp x)
      (list nil)
      (mappend-insert (list (car x))
                      (permutations (cdr x)))))

(defun sum-of-lens (x)
  (if (endp x)
      0
      (+ (len (car x))
         (sum-of-lens (cdr x)))))

(defun sum-of-1+lens (x)
  (if (endp x)
      0
      (+ (+ 1 (len (car x)))
         (sum-of-1+lens (cdr x)))))

(defthm sum-of-lens-append
  (equal (sum-of-lens (append x y))
         (+ (sum-of-lens x)
            (sum-of-lens y))))

(defthm len-append
  (equal (len (append x y))
         (+ (len x) (len y))))

(defthm sum-of-lens-insert
  (equal (sum-of-lens (insert x y))
         (* (+ (len x) (len y))
            (+ 1 (len y)))))

(defthm len-insert
  (equal (len (insert x y))
         (+ 1 (len y))))

(defthm len-mappend-insert
  (equal (len (mappend-insert (list x) y))
         (sum-of-1+lens y)))

(defun mapcar-len (x)
  (if (endp x)
      nil
      (cons (len (car x))
            (mapcar-len (cdr x)))))

(defun sum (x)
  (if (endp x)
      0
      (+ (car x)
         (sum (cdr x)))))

(defun seq (x n)
  (if (zp n)
      nil
      (cons x (seq x (1- n)))))

(defun mapcar-product (x y)
  (if (or (endp x) (endp y))
      nil
      (cons (* (car x) (car y))
            (mapcar-product (cdr x) (cdr y)))))

(defun mapcar-sum (x y)
  (if (or (endp x) (endp y))
      nil
      (cons (+ (car x) (car y))
            (mapcar-sum (cdr x) (cdr y)))))

(defthm sum-of-lens-equal-sum-mapcar-len
  (equal (sum-of-lens x)
         (sum (mapcar-len x))))

(defthm sum-of-1+lens-equal-sum-1+-len
  (equal (sum-of-1+lens x)
         (sum (mapcar-sum (seq 1 (len x))
                          (mapcar-len x)))))

(defthm nat-listp-mapcar-len
  (nat-listp (mapcar-len x)))

(defthm sum-mapcar-sum
  (implies (equal (len x) (len y))
           (equal (sum (mapcar-sum x y))
                  (+ (sum x)
                     (sum y)))))

(defthm len-mapcar-len
  (equal (len (mapcar-len x)) (len x)))

(defthm len-mapcar-product
  (implies (equal (len x) (len y))
           (equal (len (mapcar-product x y))
                  (len x))))

(defthm mapcar-product-one-seq
  (implies (acl2-number-listp x)
           (equal (mapcar-product (seq 1 (len x)) x)
                  x)))

(defthm len-seq
  (implies (natp n)
           (equal (len (seq x n))
                  n)))

(defthm sum-seq
  (implies (natp n)
           (equal (sum (seq x n))
                  (* x n))))

(defthm mapcar-distributivity
  (equal (* x (sum y))
         (sum (mapcar-product (seq x (len y))
                              y))))

(defthm len-mapcar-sum
  (implies (equal (len x) (len y))
           (equal (len (mapcar-sum x y))
                  (len x))))

(defthm mapcar-product-com
  (implies (equal (len x) (len y))
           (equal (mapcar-product x y)
                  (mapcar-product y x))))

(defthm mapcar-len-insert
  (equal (mapcar-len (insert x y))
         (seq (+ (len x) (len y))
              (+ 1 (len y)))))

(defun mapcar-len-mappend-insert (x)
  (if (endp x)
      nil
      (append (seq (+ 1 (len (car x)))
                   (+ 1 (len (car x))))
              (mapcar-len-mappend-insert (cdr x)))))

(defthm mapcar-len-append
  (equal (mapcar-len (append x y))
         (append (mapcar-len x)
                 (mapcar-len y))))

(defthm theorem-of-mapcar-len-mappend-insert
  (equal (mapcar-len (mappend-insert (list x) y))
         (mapcar-len-mappend-insert y)))

(defun sum-mapcar-len-mappend-insert (x)
  (if (endp x)
      0
      (+ (* (+ 1 (len (car x)))
            (+ 1 (len (car x))))
         (sum-mapcar-len-mappend-insert (cdr x)))))

(defthm sum-append
  (equal (sum (append x y))
         (+ (sum x)
            (sum y))))

(defthm theorem-of-sum-mapcar-len-mappend-insert
  (equal (sum (mapcar-len-mappend-insert x))
         (sum-mapcar-len-mappend-insert x)))

(defun seqp (x)
  (if (or (endp x)
          (endp (cdr x)))
      t
      (and (equal (car x)
                  (cadr x))
           (seqp (cdr x)))))

(defmacro same-len-p (x)
  `(seqp (mapcar-len ,x)))

(defthm sum-mapcar-len-mappend-insert-permutations
  (implies (same-len-p x)
           (equal (sum-mapcar-len-mappend-insert x)
                  (if (consp x)
                      (* (+ 1 (len (car x)))
                         (+ 1 (len (car x)))
                         (len x))
                      0))))

(defthm same-len-p-insert
  (implies (true-listp y)
           (same-len-p (insert x y))))

(defthm seqp-append
  (iff (seqp (append x y))
       (if (consp x)
           (if (consp y)
               (and (seqp x)
                    (seqp y)
                    (equal (car x) (car y)))
               (seqp x))
           (seqp y))))

(defthm car-seq
  (implies (consp (seq x n))
           (equal (car (seq x n)) x)))

(defthm car-mapcar-len-mappend-insert
  (implies (consp (mapcar-len-mappend-insert x))
           (equal (car (mapcar-len-mappend-insert x))
                  (+ 1 (len (car x))))))

(defthm seqp-seq
  (seqp (seq x n)))

(defthm car-append
  (equal (car (append x y))
         (if (consp x)
             (car x)
             (car y))))

(defthm seqp-mapcar-len-mappend-insert
  (implies (same-len-p x)
           (seqp (mapcar-len-mappend-insert x))))

(defthm same-len-p-permutations
  (same-len-p (permutations x)))

(defthm len-car-insert
  (equal (len (car (insert x y)))
         (+ (len x) (len y))))

(defthm len-car-mappend-insert
  (implies (and (consp (mappend-insert (list x) y))
                (same-len-p y))
           (equal (len (car (mappend-insert (list x) y)))
                  (+ 1 (len (car y))))))

(defthm len-car-permutations
  (implies (consp (permutations x))
           (equal (len (car (permutations x)))
                  (len x))))

(defthm len-permutations-lemma
  (equal (sum (mapcar-len (permutations x)))
         (* (len x) (len (permutations x)))))

(defun factorial (n)
  (if (zp n)
      1
      (* n (factorial (1- n)))))

(defthm len-permutations
  (equal (len (permutations x))
         (factorial (len x))))