stp Welcome to Clozure Common Lisp Version 1.3-dev-r11184M-trunk (DarwinX8664)! ; Aside: *hons-init-hook*: Setting *ofv-note-printed* to nil. ; Aside: Type *HELP* outside the ACL2 loop for some documentation tips. ; Aside: (setq acl2::*hons-verbose* nil) to suppress asides. ; Aside: *hons-init-hook*: Setting *print-pretty* to t. ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. ACL2 Version 3.4 built February 9, 2009 23:17:57; then February 10, 2009 00:04:39. Copyright (C) 2008 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK ...). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-3-4 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. NOTE!! Proof trees are disabled in ACL2. To enable them in emacs, look under the ACL2 source directory in interface/emacs/README.doc; and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 command loop. Look in the ACL2 documentation under PROOF-TREE. MODIFICATION NOTICE: This ACL2 executable was created by saving a session. ACL2 Version 3.4. Level 1. Cbd "/Users/sswords/e/e4/". Distributed books directory "/Users/sswords/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. (in-package "GL") (defmacro qv (x) `(acl2::qv ,x)) (set-guard-checking :nowarn) (set-inhibit-warnings "theory") (acl2::break-on-error nil) (acl2::plev-max) (cw "END SETUP~%") "GL" GL !> Summary Form: ( DEFMACRO QV ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) QV GL !> Leaving guard checking on, but changing value to :NOWARN. GL !> ("theory") GL !>GL !> ACL2 Observation in ACL2::SET-IPRINT: Iprinting remains enabled. (:LENGTH NIL :LEVEL NIL :LINES NIL :CIRCLE NIL :READABLY NIL :PRETTY T) GL !>END SETUP NIL GL !> ;; For brevity, we'll use this macro EV as an abbreviation for ;; EVAL-G-BASE, an evaluator for symbolic objects (defmacro ev (x env) `(let ((env ,env)) (eval-g-base ,x (cons (car env) (hons-shrink-alist (cdr env) nil))))) Summary Form: ( DEFMACRO EV ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) EV GL !>(g-ite (g-boolean (qv 0)) 'foo (g-boolean (qv 1))) (:G-ITE (:G-BOOLEAN T) FOO :G-BOOLEAN (T) T) GL !>`(:G-ITE (:G-BOOLEAN . ,(qv 0)) FOO . (:G-BOOLEAN . ,(qv 1))) (:G-ITE (:G-BOOLEAN T) FOO :G-BOOLEAN (T) T) GL !> ;; This shows the evaluations of the object shown in the slides. ;; (QV n) gives the nth BDD variable. (ev (g-ite (g-boolean (qv 0)) 'foo (g-boolean (qv 1))) '((t nil))) FOO GL !>(ev (g-ite (g-boolean (qv 0)) 'foo (g-boolean (qv 1))) '((t t))) FOO GL !>(ev (g-ite (g-boolean (qv 0)) 'foo (g-boolean (qv 1))) '((nil t))) T GL !>(ev (g-ite (g-boolean (qv 0)) 'foo (g-boolean (qv 1))) '((nil nil))) NIL GL !>(ev (g-ite (g-boolean (qv 0)) 'foo (g-boolean (qv 1))) '((nil))) NIL GL !> ;; G-NUMBER objects represent numbers. ;; Here, a two's complement integer of one bit: (ev (g-number (list (list (qv 0)) )) '((t))) -1 GL !>(ev (g-number (list (list (qv 0)))) '((nil))) 0 GL !> ;; A two's complement integer with sign bit NIL and one free bit: (ev (g-number (list (list (qv 0) nil))) '((t))) 1 GL !>(ev (g-number (list (list (qv 0) nil))) '((nil))) 0 GL !> ;; A rational with denominator 3: (ev (g-number (list (list (qv 0)) '(t t))) '((t))) -1/3 GL !> ;; The APPLY construct represents some function applied to symbolic ;; arguments. But the evaluator must have that function built in -- (ev (g-apply '< (list (g-number (list (list (qv 0)))) 0)) '((t))) T GL !> (ev (g-apply '< (list (g-number (list (list (qv 0)))) 0)) '((nil))) NIL GL !>(g-apply '< (list (g-number (list (list (qv 0)))) 0)) (:G-APPLY < (:G-NUMBER ((T))) 0) GL !> ;; NTH is not built in to EVAL-G-BASE. But new evaluators can be ;; defined which extend the original one with more APPLYable ;; functions: (ev (g-apply 'nth (list 2 (list 'a 'b (g-boolean (qv 0))))) '((t))) ACL2 Error in ACL2::TOP-LEVEL: ACL2 cannot ev the call of undefined function APPLY-STUB on argument list: (NTH (2 (A B T))) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. GL !> ;; The G-VAR construct represents unknown values. (ev (g-var 'abc) '(nil . ((abc . 187)))) 187 GL !> ;; The G-VAR construct represents unknown values. (ev (g-var 'abc) '(nil . ((abc . 1879293)))) 1879293 GL !> ;; The G-VAR construct represents unknown values. (ev (g-var 'abc) '(nil . nil)) NIL GL !> ;; Conses and lists represent conses and lists of symbolic objects. (ev (list (g-var 'abc) (g-number (list (list (qv 0) nil)))) '((t) . ((abc . asdfasf)))) (ASDFASF 1) GL !> (cw "END DEMO 1~%") END DEMO 1 NIL GL !>(list (g-var 'abc) (g-number (list (list (qv 0) nil)))) ((:G-VAR . ABC) (:G-NUMBER ((T) NIL))) GL !>(ev '((:G-VAR . ABC) (:G-NUMBER ((T) NIL))) '((t))) (NIL 1) GL !>(ev '(:g-concrete . ((:G-VAR . ABC) (:G-NUMBER ((T) NIL)))) '((t nil))) ((:G-VAR . ABC) (:G-NUMBER ((T) NIL))) GL !>(ev '(:g-concrete . (:g-concrete . ((:G-VAR . ABC) (:G-NUMBER ((T) NIL))))) '((t nil))) (:G-CONCRETE (:G-VAR . ABC) (:G-NUMBER ((T) NIL))) GL !> ;; This shows the symbolic comparison of two natural numbers; in this ;; case the first is never less than the second: (g-< (mk-g-number (list nil (qv 0) nil)) ;; 0 or 2 (mk-g-number (list (qv 0) nil)) ;; 0 or 1 t 10) NIL GL !> ;; This shows the symbolic comparison of two natural numbers; in this ;; case the first is never less than the second: (g-< (mk-g-number (list nil (qv 0) nil)) ;; 0 or 2 (mk-g-number (list (qv 0) nil nil nil nil nil nil)) ;; 0 or 1 t 10) NIL GL !>(g-< (mk-g-number (list nil (qv 0) nil)) ;; 0 or 2 (mk-g-number (list (qv 1) nil nil nil nil nil nil)) ;; 0 or 1 t 10) (:G-BOOLEAN . (NIL . (T . nil))) GL !>(g-< (mk-g-number (list nil (qv 0) nil)) ;; 0 or 2 (mk-g-number (list (qv 1) nil nil nil nil nil nil)) ;; 0 or 1 t 0) (:G-BOOLEAN NIL T) GL !>(g-< (mk-g-number (list nil (qv 0) nil)) ;; 0 or 2 (mk-g-number (list (qv 1) nil nil nil nil nil nil)) ;; 0 or 1 nil 0) (:G-BOOLEAN NIL T) GL !>:pe g-<-correct d -3 (INCLUDE-BOOK "top") \ [Included books, outermost to innermost: "/Users/sswords/e/e4/top.lisp" "/Users/sswords/e/cbooks/g-logic/gl.lisp" "/Users/sswords/e/cbooks/g-logic/g-primitives.lisp" "/Users/sswords/e/cbooks/g-logic/g-lessthan.lisp" ] \ > (DEFTHM G-<-CORRECT (IMPLIES (AND (EVAL-BDD HYP (CAR ENV)) (GL-NORMP HYP)) (EQUAL (EVAL-G-BASE (G-< A B HYP CLK) ENV) (< (EVAL-G-BASE A ENV) (EVAL-G-BASE B ENV)))) :HINTS (("goal" :USE ((:INSTANCE G-<-CORRECT1 (A (GOBJ-FIX A)) (B (GOBJ-FIX B))))))) GL !> ;; The reverse: this time, < sometimes holds: (g-< (mk-g-number (list (qv 0) nil)) (mk-g-number (list nil (qv 0) nil)) t 10) (:G-BOOLEAN T) GL !> ;; Symbolic functions can also apply to concrete values: (g-< 1 2 t 10) T GL !> ;; or to a combination of concrete and symbolic: (g-< 1 (mk-g-number (list nil (qv 0) nil)) t 10) (:G-BOOLEAN T) GL !> ;; Symbolic functions can also apply to concrete values: (g-< t 2 t 10) ACL2 Error in ACL2::TOP-LEVEL: The guard for the function call (< X Y), which is (AND (RATIONALP X) (RATIONALP Y)), is violated by the arguments in the call (< T 2). To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. GL !>(set-guard-checking nil) Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. GL > ;; Symbolic functions can also apply to concrete values: (g-< t 2 t 10) T GL > ;; Symbolic functions can also apply to concrete values: (g-< 2 1 t 10) NIL GL > ;; Here we use MAKE-G-WORLD to create symbolic analogues of two ;; non-primitives: (make-g-world (nth len) nl-ev) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. T GL >:u 3:x(DEFMACRO EV (X ENV) ...) GL > ;; Here we use MAKE-G-WORLD to create symbolic analogues of two ;; non-primitives: (make-g-world (nth len) nl-ev :output (:off :all :gag-mode nil)) T GL >:u 3:x(DEFMACRO EV (X ENV) ...) GL > ;; Here we use MAKE-G-WORLD to create symbolic analogues of two ;; non-primitives: (make-g-world (nth len) nl-ev :output (:off :all :gag-mode t)) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. T GL > ;; The correctness theorem for G-LEN: (pe 'g-len-correct) d 4:x(MAKE-G-WORLD (NTH LEN) NL-EV ...) \ > (DEFTHM G-LEN-CORRECT (IMPLIES (AND (EVAL-BDD HYP (CAR ENV)) (NRMPF (GL-NORMP HYP))) (EQUAL (NL-EV (G-LEN X HYP CLK) ENV) (LEN (NL-EV X ENV)))) :RULE-CLASSES :REWRITE :DOC NIL :HINTS (("Goal" :IN-THEORY (THEORY 'MINIMAL-THEORY) :USE ((:INSTANCE G-LEN-CORRECT-LEMMA (FLAG 'G-LEN)))))) GL >:pe g-len d 4:x(MAKE-G-WORLD (NTH LEN) NL-EV ...) \ >LV (MUTUAL-RECURSION (DEFUN G-LEN (X HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP X) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 0) :HINTS (("goal" :IN-THEORY (E/D** ((:RULESET CLK-MEASURE-RULES)))))) (IGNORABLE HYP CLK)) (LET ((X (MBE :LOGIC (GOBJ-FIX X) :EXEC X))) (DECLARE (IGNORABLE X)) (IF (AND (GENERAL-CONCRETEP X)) (MK-G-CONCRETE (ECC (LEN (GENERAL-CONCRETE-OBJ X)))) (IF (ZP CLK) (G-APPLY 'LEN (LIST X)) (LET ((CLK (1- CLK))) (DECLARE (IGNORABLE CLK)) (G-LEN-IF-1 (G-CONSP X HYP CLK) X HYP CLK)))))) (DEFUN G-LEN-IF-1 (TEST X HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP TEST) (GOBJECTP X) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 2)) (IGNORABLE HYP CLK)) (LET ((TEST (MBE :LOGIC (GOBJ-FIX TEST) :EXEC TEST)) (X (MBE :LOGIC (GOBJ-FIX X) :EXEC X))) (DECLARE (IGNORABLE TEST X)) (G-IF TEST (G-LEN-THEN-1 X HYP CLK) (MK-G-CONCRETE '0)))) (DEFUN G-LEN-THEN-1 (X HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP X) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 1)) (IGNORABLE HYP CLK)) (LET ((X (MBE :LOGIC (GOBJ-FIX X) :EXEC X))) (DECLARE (IGNORABLE X)) (G-BINARY-+ (MK-G-CONCRETE '1) (G-LEN (G-CDR X HYP CLK) HYP CLK) HYP CLK)))) GL >:pe g-<-correct-for-nl-ev d 4:x(MAKE-G-WORLD (NTH LEN) NL-EV ...) \ > (DEFTHM G-<-CORRECT-FOR-NL-EV (IMPLIES (IF (EVAL-BDD HYP (CAR ENV)) (FORCE (GL-NORMP HYP)) 'NIL) (EQUAL (NL-EV (G-< A B HYP CLK) ENV) (< (NL-EV A ENV) (NL-EV B ENV)))) :HINTS (("goal" :IN-THEORY (THEORY 'MINIMAL-THEORY) :USE ((:FUNCTIONAL-INSTANCE G-<-CORRECT (APPLY-STUB (LAMBDA (F ARGS) (COND ((AND (EQ F 'ZP) (TRUE-LISTP ARGS) (EQL (LEN ARGS) 1)) (ECC (ZP (NTH 0 ARGS)))) ((AND (EQ F 'NTH) (TRUE-LISTP ARGS) (EQL (LEN ARGS) 2)) (ECC (NTH (NTH 0 ARGS) (NTH 1 ARGS)))) ((AND (EQ F 'LEN) (TRUE-LISTP ARGS) (EQL (LEN ARGS) 1)) (ECC (LEN (NTH 0 ARGS)))) ((AND (EQ F 'ACL2::FAIG-EVAL-PAT) (TRUE-LISTP ARGS) (EQL (LEN ARGS) 3)) (ECC (ACL2::FAIG-EVAL-PAT (NTH 0 ARGS) (NTH 1 ARGS) (NTH 2 ARGS)))) ((AND (EQ F 'ACL2::AIG-EVAL) (TRUE-LISTP ARGS) (EQL (LEN ARGS) 2)) (ECC (ACL2::AIG-EVAL (NTH 0 ARGS) (NTH 1 ARGS)))) ((AND (EQ F 'HIDE) (TRUE-LISTP ARGS) (EQL (LEN ARGS) 1)) (ECC (HIDE (NTH 0 ARGS)))) (T (APPLY-STUB F ARGS))))) (APPLY-BASE NL-EV-AP) (EVAL-G-BASE NL-EV)))))) GL >:pe g-nth d 4:x(MAKE-G-WORLD (NTH LEN) NL-EV ...) \ >LV (MUTUAL-RECURSION (DEFUN G-NTH (N L HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP N) (GOBJECTP L) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 0) :HINTS (("goal" :IN-THEORY (E/D** ((:RULESET CLK-MEASURE-RULES)))))) (IGNORABLE HYP CLK)) (LET ((N (MBE :LOGIC (GOBJ-FIX N) :EXEC N)) (L (MBE :LOGIC (GOBJ-FIX L) :EXEC L))) (DECLARE (IGNORABLE N L)) (IF (AND (GENERAL-CONCRETEP N) (GENERAL-CONCRETEP L)) (MK-G-CONCRETE (ECC (NTH (GENERAL-CONCRETE-OBJ N) (GENERAL-CONCRETE-OBJ L)))) (IF (ZP CLK) (G-APPLY 'NTH (LIST N L)) (LET ((CLK (1- CLK))) (DECLARE (IGNORABLE CLK)) (G-NTH-IF-1 (G-CONSP L HYP CLK) L N HYP CLK)))))) (DEFUN G-NTH-IF-1 (TEST L N HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP TEST) (GOBJECTP L) (GOBJECTP N) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 4)) (IGNORABLE HYP CLK)) (LET ((TEST (MBE :LOGIC (GOBJ-FIX TEST) :EXEC TEST)) (L (MBE :LOGIC (GOBJ-FIX L) :EXEC L)) (N (MBE :LOGIC (GOBJ-FIX N) :EXEC N))) (DECLARE (IGNORABLE TEST L N)) (G-IF TEST (G-NTH-THEN-1 L N HYP CLK) (MK-G-CONCRETE 'NIL)))) (DEFUN G-NTH-THEN-1 (L N HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP L) (GOBJECTP N) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 3)) (IGNORABLE HYP CLK)) (LET ((L (MBE :LOGIC (GOBJ-FIX L) :EXEC L)) (N (MBE :LOGIC (GOBJ-FIX N) :EXEC N))) (DECLARE (IGNORABLE L N)) (G-NTH-IF-6 (G-ZP N HYP CLK) L N HYP CLK))) (DEFUN G-NTH-IF-6 (TEST L N HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP TEST) (GOBJECTP L) (GOBJECTP N) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 2)) (IGNORABLE HYP CLK)) (LET ((TEST (MBE :LOGIC (GOBJ-FIX TEST) :EXEC TEST)) (L (MBE :LOGIC (GOBJ-FIX L) :EXEC L)) (N (MBE :LOGIC (GOBJ-FIX N) :EXEC N))) (DECLARE (IGNORABLE TEST L N)) (G-IF TEST (G-CAR L HYP CLK) (G-NTH-ELSE-6 L N HYP CLK)))) (DEFUN G-NTH-ELSE-6 (L N HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP L) (GOBJECTP N) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL :MEASURE (TWO-NATS-MEASURE CLK 1)) (IGNORABLE HYP CLK)) (LET ((L (MBE :LOGIC (GOBJ-FIX L) :EXEC L)) (N (MBE :LOGIC (GOBJ-FIX N) :EXEC N))) (DECLARE (IGNORABLE L N)) (G-NTH (G-BINARY-+ (MK-G-CONCRETE '-1) N HYP CLK) (G-CDR L HYP CLK) HYP CLK)))) GL >(defun foo (x y z a b c) (and x y z a b c)) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (OR (EQUAL (FOO X Y Z A B C) NIL) (EQUAL (FOO X Y Z A B C) C)). Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO GL >(make-g-world (foo) foo-ev) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. T GL >:pe g-foo d 6:x(MAKE-G-WORLD (FOO) FOO-EV) \ >LV (DEFUN G-FOO (X Y Z A B C HYP CLK) (DECLARE (XARGS :GUARD (AND (GOBJECTP X) (GOBJECTP Y) (GOBJECTP Z) (GOBJECTP A) (GOBJECTP B) (GOBJECTP C) (GL-NORMP HYP) (NATP CLK)) :VERIFY-GUARDS NIL) (IGNORABLE HYP CLK)) (LET ((X (MBE :LOGIC (GOBJ-FIX X) :EXEC X)) (Y (MBE :LOGIC (GOBJ-FIX Y) :EXEC Y)) (Z (MBE :LOGIC (GOBJ-FIX Z) :EXEC Z)) (A (MBE :LOGIC (GOBJ-FIX A) :EXEC A)) (B (MBE :LOGIC (GOBJ-FIX B) :EXEC B)) (C (MBE :LOGIC (GOBJ-FIX C) :EXEC C))) (DECLARE (IGNORABLE X Y Z A B C)) (IF (AND (GENERAL-CONCRETEP X) (GENERAL-CONCRETEP Y) (GENERAL-CONCRETEP Z) (GENERAL-CONCRETEP A) (GENERAL-CONCRETEP B) (GENERAL-CONCRETEP C)) (MK-G-CONCRETE (ECC (FOO (GENERAL-CONCRETE-OBJ X) (GENERAL-CONCRETE-OBJ Y) (GENERAL-CONCRETE-OBJ Z) (GENERAL-CONCRETE-OBJ A) (GENERAL-CONCRETE-OBJ B) (GENERAL-CONCRETE-OBJ C)))) (IF (ZP CLK) (G-APPLY 'FOO (LIST X Y Z A B C)) (LET ((CLK (1- CLK))) (DECLARE (IGNORABLE CLK)) (G-FOO-IF-1 X Y Z A B C HYP CLK)))))) GL >:u L 5:x(DEFUN FOO (X Y Z A B C) ...) GL > ;; Evaluations of the new symbolic functions: (g-len (list (g-var 'abc) (g-var 'asdf) (g-var 'sdfds)) t 10) 3 GL > ;; Either element 0 or 2 of a list: (g-nth (mk-g-number (list nil (qv 0) nil)) ;; 0 or 2 (list (g-var 'abc) (g-var 'asdf) (g-var 'sdfds)) t 10) (:G-ITE (:G-BOOLEAN NIL . T) (:G-VAR . ABC) :G-VAR . SDFDS) GL > ;; A function representing a conjecture: (defun minus-is-inverse (n) (equal (- n n) 0)) Since MINUS-IS-INVERSE is non-recursive, its admission is trivial. We observe that the type of MINUS-IS-INVERSE is described by the theorem (OR (EQUAL (MINUS-IS-INVERSE N) T) (EQUAL (MINUS-IS-INVERSE N) NIL)). We used primitive type reasoning. Summary Form: ( DEFUN MINUS-IS-INVERSE ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) MINUS-IS-INVERSE GL > ;; Make the symbolic analogue of this function: (make-g-world (minus-is-inverse) mii-ev) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. T GL > ;; Make a sequence of BDD variables: (defun make-list-of-qvs (start by n) (if (zp n) nil (cons (qv start) (make-list-of-qvs (+ start by) by (1- n))))) The admission of MAKE-LIST-OF-QVS is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). We observe that the type of MAKE-LIST-OF-QVS is described by the theorem (TRUE-LISTP (MAKE-LIST-OF-QVS START BY N)). We used primitive type reasoning. Summary Form: ( DEFUN MAKE-LIST-OF-QVS ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) MAKE-LIST-OF-QVS GL > ;; Show that minus-is-inverse holds for a (very large!) range of ;; integers: (g-minus-is-inverse (mk-g-number (make-list-of-qvs 0 1 1000)) t 10) T GL > (cw "End demo 2~%") End demo 2 NIL GL > (defun mk-number-list (start skip n) (declare (xargs :guard (and (natp n) (acl2-numberp start) (acl2-numberp skip)))) (if (zp (nfix n)) nil (cons start (mk-number-list (+ start skip) skip (1- n))))) For the admission of MK-NUMBER-LIST we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). The non-trivial part of the measure conjecture is Goal (IMPLIES (NOT (ZP (NFIX N))) (O< (ACL2-COUNT (+ -1 N)) (ACL2-COUNT N))). Q.E.D. That completes the proof of the measure theorem for MK-NUMBER-LIST. Thus, we admit this function under the principle of definition. We observe that the type of MK-NUMBER-LIST is described by the theorem (TRUE-LISTP (MK-NUMBER-LIST START SKIP N)). We used primitive type reasoning. Computing the guard conjecture for MK-NUMBER-LIST.... The non-trivial part of the guard conjecture for MK-NUMBER-LIST, given the :compound-recognizer rule NATP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription rule NFIX, is Goal (IMPLIES (AND (ACL2-NUMBERP SKIP) (ACL2-NUMBERP START) (NATP N) (NOT (ZP (NFIX N)))) (NATP (+ -1 N))). Q.E.D. That completes the proof of the guard theorem for MK-NUMBER-LIST. MK-NUMBER-LIST is compliant with Common Lisp. Summary Form: ( DEFUN MK-NUMBER-LIST ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION ACL2-COUNT) (:DEFINITION INTEGER-ABS) (:DEFINITION NATP) (:DEFINITION NFIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NFIX-NATP) (:REWRITE ZP-OPEN) (:TYPE-PRESCRIPTION NFIX)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) MK-NUMBER-LIST GL >(g-number (list (mk-number-list 0 1 10))) (:G-NUMBER (0 1 2 3 4 5 6 7 8 9)) GL > ;; This formalizes the previous informal claim that minus-is-inverse ;; holds for a large range of integers: (def-g-thm minus-is-inverse-holds-up-to-2^2000 :hyp (and (integerp x) (<= 0 x) (< x (expt 2 2000))) :concl (minus-is-inverse x) :g-bindings `((x ,(g-number (list (mk-number-list 0 1 2001)))))) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Warning: GIFYing undefined function UNARY-/ Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. ;;; Starting full GC, 1,255,669,760 bytes allocated. ;;; Finished full GC. 867,978,784 bytes freed in 1.613575 s ;;; 4905 soft faults, 31548 faults, 0 pageins ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. (ACL2_*1*_GL::G-MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-CONCL X GL::HYP GL::CLK) took 31,046 microseconds (0.031046 seconds) to run with 2 available CPU cores. During that period, 28,401 microseconds (0.028401 seconds) were spent in user mode 973 microseconds (0.000973 seconds) were spent in system mode 1,824,336 bytes of memory allocated. 11 minor page faults, 11 major page faults, 0 swaps. Result ok Q.E.D. Q.E.D. Summary Form: ( MAKE-EVENT (QUOTE ...)) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) T GL >:pe minus-is-inverse-holds-up-to-2^2000 10:x(DEF-G-THM MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000 :HYP ...) \ > (DEFTHM MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000 (IMPLIES (AND (INTEGERP X) (<= 0 X) (< X (EXPT 2 2000))) (MINUS-IS-INVERSE X)) :HINTS (("goal" :USE ((:INSTANCE MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-G-LEMMA (X (LIST X)))) :IN-THEORY (E/D** (MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-HYP MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-CONCL MINIMAL-THEORY CAR-CONS CDR-CONS))))) GL > ;; This formalizes the previous informal claim that minus-is-inverse ;; holds for a large range of integers: (def-g-thm minus-is-inverse-holds-up-to-2^2000-new :hyp (and (integerp x) (<= 0 x) (< x (expt 2 2000)) (evenp x)) :concl (and (minus-is-inverse x) (oddp x)) :g-bindings `((x ,(g-number (list (mk-number-list 0 1 2001)))))) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Warning: GIFYing undefined function UNARY-/ Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. (ACL2_*1*_GL::G-MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW-CONCL X GL::HYP GL::CLK) took 12,188 microseconds (0.012188 seconds) to run with 2 available CPU cores. During that period, 11,928 microseconds (0.011928 seconds) were spent in user mode 100 microseconds (0.000100 seconds) were spent in system mode 96,384 bytes of memory allocated. *** SYMBOLIC EXECUTION ERROR ***: Counterexample at ((X 0)) --- The key checkpoint goal, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Subgoal 8' NIL ACL2 Error in ( DEFTHM MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW-G-LEMMA ...): See :DOC failure. ******** FAILED ******** ACL2 Error in ( PROGN (DEFTHM MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW-G-LEMMA ...) ...): PROGN failed! ACL2 Error in ( PROGN (ACL2::WITH-SAVED-ERROR-MSG ...) ...): PROGN failed! Summary Form: ( MAKE-EVENT (QUOTE ...)) Rules: NIL Warnings: None Time: 0.08 seconds (prove: 0.06, print: 0.00, other: 0.02) ACL2 Error in ( MAKE-EVENT (QUOTE ...)): See :DOC failure. ******** FAILED ******** ACL2 Error in ACL2::WITH-FINAL-ERROR-PRINTING: The proof that the given hypothesis implies the given conclusion failed. This is most likely because symbolic simulation found a counterexample or was unable to complete satisfactorily. Try searching backwards in the proof output for "*** SYMBOLIC EXECUTION ERROR ***". If no such output exists then there was a different problem. GL > ;; This formalizes the previous informal claim that minus-is-inverse ;; holds for a large range of integers: (def-g-thm minus-is-inverse-holds-up-to-2^2000-new :hyp (and (integerp x) (<= 0 x) (< x (expt 2 2000)) (evenp x)) :concl (and (minus-is-inverse x) (oddp (1+ x))) :g-bindings `((x ,(g-number (list (mk-number-list 0 1 2001)))))) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Warning: GIFYing undefined function UNARY-/ Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. (ACL2_*1*_GL::G-MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW-CONCL X GL::HYP GL::CLK) took 14,432 microseconds (0.014432 seconds) to run with 2 available CPU cores. During that period, 14,043 microseconds (0.014043 seconds) were spent in user mode 284 microseconds (0.000284 seconds) were spent in system mode 128,496 bytes of memory allocated. 0 minor page faults, 32 major page faults, 0 swaps. Result ok Q.E.D. Q.E.D. Summary Form: ( MAKE-EVENT (QUOTE ...)) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ;;; Starting full GC, 1,514,012,672 bytes allocated. ;;; Finished full GC. 929,530,384 bytes freed in 2.557029 s ;;; 8826 soft faults, 14366 faults, 0 pageins ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. T GL >:pe minus-is-inverse-holds-up-to-2^2000-new 11:x(DEF-G-THM MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW :HYP ...) \ > (DEFTHM MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW (IMPLIES (AND (INTEGERP X) (<= 0 X) (< X (EXPT 2 2000)) (EVENP X)) (AND (MINUS-IS-INVERSE X) (ODDP (1+ X)))) :HINTS (("goal" :USE ((:INSTANCE MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW-G-LEMMA (X (LIST X)))) :IN-THEORY (E/D** (MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW-HYP MINUS-IS-INVERSE-HOLDS-UP-TO-2^2000-NEW-CONCL MINIMAL-THEORY CAR-CONS CDR-CONS))))) GL > ;; Next few events load the MOSTEK model and a multiplication program ;; for it: (in-package "ACL2") "ACL2" ACL2 > (include-book "g-logic/mostek-6502-def" :dir :cbooks) Summary Form: ( INCLUDE-BOOK "g-logic/mostek-6502-def" ...) Rules: NIL Warnings: None Time: 0.12 seconds (prove: 0.00, print: 0.00, other: 0.12) "/Users/sswords/e/cbooks/g-logic/mostek-6502-def.lisp" ACL2 > (defconst *mult* '((LDX 8) ; 1 (LDA 0) ; 2 (CLC) ; 3 ; Added by Hunt (ROR F1) ; 4 (BCC 8) ; 5 (CLC) ; 6 (ADC F2) ; 7 (ROR A) ; 8 (ROR LOW) ; 9 (DEX) ; 10 (BNE 4) ; 11 )) Summary Form: ( DEFCONST *MULT* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *MULT* ACL2 > (defun general-start-state-mult (c a x f1 f2 z f1save) (list 1 ; integer 0 to 255 c ; carry flag a ; accumulator 0 ; low register x ; x - counter ;; operand f1 f1 ;; operand f2 f2 z ; zero flag ;; operand f1 copy f1save *mult*)) Since GENERAL-START-STATE-MULT is non-recursive, its admission is trivial. We observe that the type of GENERAL-START-STATE-MULT is described by the theorem (AND (CONSP (GENERAL-START-STATE-MULT C A X F1 F2 Z F1SAVE)) (TRUE-LISTP (GENERAL-START-STATE-MULT C A X F1 F2 Z F1SAVE))). We used primitive type reasoning. Summary Form: ( DEFUN GENERAL-START-STATE-MULT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) GENERAL-START-STATE-MULT ACL2 > ;; Prove by symbolic execution that the multiplication program works: (def-g-thm mult-is-correct :hyp (and (bitsp f1 nil 8) (bitsp f2 nil 8)) :concl (let* ((start-state (general-start-state-mult c a x f1 f2 z f1save)) (last-state (run-it 67 start-state))) (equal (* f1 f2) (+ (* 256 (a last-state)) (low last-state)))) :g-bindings `((f1 ,(gl::g-number (list (mk-number-list 0 1 9)))) (f2 ,(gl::g-number (list (mk-number-list 9 1 9))))) :local nil) Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Warning: GIFYing undefined function UNARY-/ Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. ;;; Starting full GC, 1,658,978,304 bytes allocated. ;;; Finished full GC. 1,058,865,216 bytes freed in 2.501318 s ;;; 0 soft faults, 6043 faults, 0 pageins ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. ; set-and-reset-gc-thresholds: Setting (lisp-heap-gc-threshold) to 1,073,741,824 bytes. Q.E.D. Q.E.D. Q.E.D. Q.E.D. Q.E.D. (ACL2_*1*_GL::G-MULT-IS-CORRECT-CONCL X GL::HYP GL::CLK) took 2,857,987 microseconds (2.857987 seconds) to run with 2 available CPU cores. During that period, 2,723,113 microseconds (2.723113 seconds) were spent in user mode 59,230 microseconds (0.059230 seconds) were spent in system mode 193,167,072 bytes of memory allocated. 1,866 minor page faults, 1,881 major page faults, 0 swaps. Result ok Q.E.D. Q.E.D. Summary Form: ( MAKE-EVENT (QUOTE ...)) Rules: NIL Warnings: None Time: 4.12 seconds (prove: 4.10, print: 0.00, other: 0.02) ACL2 > :pe mult-is-correct d 15:x(DEF-G-THM MULT-IS-CORRECT :HYP ...) \ > (DEFTHM MULT-IS-CORRECT (IMPLIES (AND (BITSP F1 NIL 8) (BITSP F2 NIL 8)) (LET* ((START-STATE (GENERAL-START-STATE-MULT C A X F1 F2 Z F1SAVE)) (LAST-STATE (RUN-IT 67 START-STATE))) (EQUAL (* F1 F2) (+ (* 256 (A LAST-STATE)) (LOW LAST-STATE))))) :HINTS (("goal" :USE ((:INSTANCE MULT-IS-CORRECT-G-LEMMA (X (LIST F1SAVE Z X A C F1 F2)))) :IN-THEORY (E/D** (MULT-IS-CORRECT-HYP MULT-IS-CORRECT-CONCL MINIMAL-THEORY CAR-CONS CDR-CONS))))) ACL2 >