(in-package "ACL2")

(defun true-flistp (x)
  (if (endp x)
      (null x)
      (and (consp x)
           (true-flistp (car x)))))

(defun list-to-flist (x)
  (if (endp x)
      nil
      (cons (list-to-flist (cdr x))
            (car x))))

(defun flist-to-list (x)
  (if (endp x)
      nil
      (cons (cdr x)
            (flist-to-list (car x)))))

(defthm flist-to-list-to-flist
  (implies (true-flistp x)
           (equal (list-to-flist (flist-to-list x))
                  x)))

(defthm list-to-flist-to-list
  (implies (true-listp x)
           (equal (flist-to-list (list-to-flist x))
                  x)))


(defun fappend (x y)
  (if (endp x)
      y
      (cons (fappend (car x) y)
            (cdr x))))

(defthm assocativity-of-append
  (equal (fappend (fappend x y) z)
         (fappend x (fappend y z))))

(defthm fappend-append
  (implies (and (true-listp x)
                (true-listp y))
           (equal (flist-to-list (fappend (list-to-flist x)
                                          (list-to-flist y)))
                  (append x y))))