diff options
| -rw-r--r-- | L-99.lisp | 16 |
1 files changed, 15 insertions, 1 deletions
@@ -244,7 +244,7 @@ ((endp x) (if (zp n) nil - (list (list prev n)))) + (list (list n prev)))) ((or (zp n) (equal (car x) prev)) (encode-1 (cdr x) (car x) (1+ n))) @@ -254,4 +254,18 @@ (defmacro encode (x) `(encode-1 ,x nil 0)) +(defun sum-of-cars (x) + (if (endp x) + 0 + (+ (caar x) + (sum-of-cars (cdr x))))) + +(defthm sum-of-cars-encode-1 + (implies (natp n) + (equal (sum-of-cars (encode-1 x sym n)) + (+ n (len x))))) + +(defthm sum-of-cars-encode + (equal (sum-of-cars (encode x)) + (len x))) |