;; setting up emacs: M-x load-library (enter) "emacs-acl2"
;; switching buffers: C-x b 
;; vertical centering: C-l
;; sending a command to shell: C-t e

; -----------------------
; decompose and compose the tree

(defun treecopy (x) ;poznamka
  (if (consp x)
      (cons (treecopy (car x))
            (treecopy (cdr x)))
      x))

; ----------------------
; errorneous definition

(defun treecopy-err (x)
  (if (consp x)
      (cons (treecopy-err (car x))
            (treecopy-err x))   
      x))

   
; -----------------------
; theorem

(defthm treecopy-is-identity 
  (equal (treecopy x) x))


; -----------------------
; -----------------------
; dup - duplicates each element in the list

(defun dup (x) 
  (if (consp x)
      (cons (car x)
            (cons (car x)
                  (dup (cdr x))))
      nil))

(dup '(1 'ok 2 3))

; -----------------------
; app - appeands two lists

(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
      y))

(app '(1 2 3) '(4 5)) 
(dup (app '(1 2 3) (dup '(1))))

(defthm dup-duplicates-head-and-tail 
  (equal (dup (cons 1 y))
         (cons 1 (cons 1 (dup y)))))

(defthm dup-app-distributivity-general 
  (equal (dup (app x y))
         (app (dup x) (dup y)))) 

(defthm dup-app-distributivity 
  (equal (dup (app x x))
         (app (dup x) (dup x))))  

; -----------------------
; memp - is the element in the list?

(defun memp (e x)
  (if (consp x)
      (if (equal e (car x))
          t
          (memp e (cdr x)))
      nil))

; -----------------------
; theorem

(defthm memp-app
  (equal (memp e (app a b))
         (or (memp e a) (memp e b))))