#|

Author: Pete Manolios
Date:   9/23/2021

Code used in lecture 8 of Computer-Aided Reasoning.

|#

(in-package "ACL2S")
(set-gag-mode nil)

(definec ap (a :tl b :tl) :tl
  (if (endp a)
      b
    (cons (car a) 
          (ap (cdr a) b))))

(ap '(1 2 3) '(4 5 6))

(definec rv (x :tl) :tl
  (if (endp x)
      nil
    (ap (rv (cdr x))
        (list (car x)))))

(rv '(1 2 3))

; Show  ld

; (ld "l8-class.lisp")

#|

This is a classic example that shows ACL2 going through all of the
proof procedures.

|#

(property rev-rev (x :all)
  (== (rv (rv x))
      x))

(property app-nil (x :tl)
  (== (ap x nil) x))

(property ass-app (x :tl y :tl z :tl)
  (== (ap (ap x y) z)
      (ap x (ap y z))))

(property rev-app (x :tl y :tl)
  (== (rv (ap x y))
      (ap (rv y) (rv x))))

(property rev-rev (x :tl)
  (== (rv (rv x))
      x))