Linear Encoding

Encoding integer sequences by summing adjacent pairs, modulo a given base ... and decoding them

Purpose of exercise

Activities

Terminology

Requirements

  1. Define a function, encode, that, given an encoding base m and a non-empty sequence x0, x1, ... xn-1 of encodable integers, delivers the sequence of encodable integers y0, y1, ... yn-1, with yi = (xi + xi+1) mod m, where xn = m-1
  2. Define a function, decode, that inverts encode: (decode m (encode m xs)) = xs
  3. Define a predicate, basep, such that (basep m) is true if and only if m is an encoding base
  4. Define a predicate, encodable-integerp, such that (encodable-integerp m x) is true if and only if x is an encodable integer
  5. Define a predicate, encodable-listp, such that (encodable-listp m xs) is true if and only if m is an encoding base and xs is a true-list, all of whose elements are encodable integers

Properties

  1. If m is an encoding base and xs is a true-list of encodable integers, then (encode m xs) is a true-list of encodable integers
  2. If m is an encoding base and ys is a true-list of encodable integers, then (decode m ys) is a true-list of encodable integers
  3. If m is an encoding base and xs is a true-list of encodable integers, then (a) the last element of (encode m xs) is the difference, mod m, of the last element of xs and 1, and (b) the i-th element of (encode m xs) is the sum, mod m, of the i-th and i-plus-first element of xs
  4. If m is an encoding base and xs is a true-list of encodable integers, then (decode (encode xs)) = xs

ACL2 intrinsics useful in this exercise

Useful books of theorems