append

Purpose of exercise

Activities

Terminology

Properties

  1. The first (length xs) elements of (append xs ys) is xs
  2. (append xs ys) without its first (length xs) elements is ys
  3. The length of the list append delivers is the sum of the lengths of its arguments
  4. Appending the first n elements of a list with its elements beyond the first n reproduces the list

ACL2 instrinsics and other functions useful in this exercise

Useful books of theorems