From 29cfbf88b44bcfdf3d3a6c022c64a8521f583b24 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 23 Jul 2021 21:27:27 +0900 Subject: L-99: Fix encode function. --- L-99.lisp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'L-99.lisp') diff --git a/L-99.lisp b/L-99.lisp index a4e5a59..efd9e15 100644 --- a/L-99.lisp +++ b/L-99.lisp @@ -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))) -- cgit v1.2.3