File: GUARD-EVALUATION-EXAMPLES-LOG.html

package info (click to toggle)
acl2 3.1-1
links: PTS
area: main
in suites: etch, etch-m68k
size: 36,712 kB
ctags: 38,396
sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (787 lines) | stat: -rw-r--r-- 22,068 bytes
<html>
<head><title>GUARD-EVALUATION-EXAMPLES-LOG.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>GUARD-EVALUATION-EXAMPLES-LOG</h3>log showing combinations of <a href="DEFUN-MODE.html">defun-mode</a>s and <a href="GUARD.html">guard</a>-checking
<pre>Major Section:  <a href="GUARD.html">GUARD</a>
</pre><p>

See <a href="GUARD-EVALUATION-EXAMPLES-SCRIPT.html">guard-evaluation-examples-script</a> for a script that shows the interaction
of <a href="DEFUN-MODE.html">defun-mode</a>s with the value set by <code><a href="SET-GUARD-CHECKING.html">set-guard-checking</a></code>.  Here, we
present a log resulting from running this script (using ACL2 Version  3.0,
built on Allegro Common Lisp).
<p>
See <a href="SET-GUARD-CHECKING.html">set-guard-checking</a> for discussion of the interaction between
<a href="DEFUN-MODE.html">defun-mode</a>s and <a href="GUARD.html">guard</a>-checking that is illustrated by this script.
Also see <a href="GUARD-EVALUATION-TABLE.html">guard-evaluation-table</a> for a succinct table, with associated
discussion, that covers in detail the interactions illustrated here.<p>


<pre>
ACL2 !&gt;(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :mode :program))
         (if (posp x)
             (* x (fact (1- x)))
           1))<p>

Summary
Form:  ( DEFUN FACT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 !&gt;(trace$ fact)
NIL
ACL2 !&gt;:set-guard-checking t<p>

Guard-checking-on already has value T.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
FACT, which is (INTEGERP X), is violated by the arguments in the call
(FACT T).  See :DOC wet for how you might be able to get an error backtrace.
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :all<p>

Leaving guard checking on, but changing value to :ALL.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (ACL2_*1*_ACL2::FACT 1)
    3&gt; (ACL2_*1*_ACL2::FACT 0)
    &lt;3 (ACL2_*1*_ACL2::FACT 1)
  &lt;2 (ACL2_*1*_ACL2::FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
FACT, which is (INTEGERP X), is violated by the arguments in the call
(FACT T).  See :DOC wet for how you might be able to get an error backtrace.
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :none<p>

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (ACL2_*1*_ACL2::FACT 1)
    3&gt; (ACL2_*1*_ACL2::FACT 0)
    &lt;3 (ACL2_*1*_ACL2::FACT 1)
  &lt;2 (ACL2_*1*_ACL2::FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:set-guard-checking nil<p>

Masking guard violations but still checking guards.  To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
  2&gt; (FACT T)
  &lt;2 (FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:u<p>

          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 &gt;(defun fact (x)
         (declare (xargs :guard t
                         :mode :program))
         (if (posp x)
             (* x (fact (1- x)))
           1))<p>

Summary
Form:  ( DEFUN FACT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 &gt;(trace$ fact)
NIL
ACL2 &gt;:set-guard-checking t<p>

Turning guard checking on, value T.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
  2&gt; (FACT T)
  &lt;2 (FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !&gt;:set-guard-checking :all<p>

Leaving guard checking on, but changing value to :ALL.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (ACL2_*1*_ACL2::FACT 1)
    3&gt; (ACL2_*1*_ACL2::FACT 0)
    &lt;3 (ACL2_*1*_ACL2::FACT 1)
  &lt;2 (ACL2_*1*_ACL2::FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !&gt;:set-guard-checking :none<p>

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (ACL2_*1*_ACL2::FACT 1)
    3&gt; (ACL2_*1*_ACL2::FACT 0)
    &lt;3 (ACL2_*1*_ACL2::FACT 1)
  &lt;2 (ACL2_*1*_ACL2::FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:set-guard-checking nil<p>

Masking guard violations but still checking guards.  To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
  2&gt; (FACT T)
  &lt;2 (FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:u<p>

          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 &gt;(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :verify-guards nil
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))<p>

For the admission of FACT we will use the relation O&lt; (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is<p>

Goal
(IMPLIES (POSP X)
         (O&lt; (ACL2-COUNT (+ -1 X))
             (ACL2-COUNT X))).<p>

By the simple :definition POSP we reduce the conjecture to<p>

Goal'
(IMPLIES (AND (INTEGERP X) (&lt; 0 X))
         (O&lt; (ACL2-COUNT (+ -1 X))
             (ACL2-COUNT X))).<p>

But we reduce the conjecture to T, by case analysis.<p>

Q.E.D.<p>

That completes the proof of the measure theorem for FACT.  Thus, we
admit this function under the principle of definition. We observe that
the type of FACT is described by the theorem 
(AND (INTEGERP (FACT X)) (&lt; 0 (FACT X))).  We used the :compound-recognizer
rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.<p>

Summary
Form:  ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION NOT)
        (:DEFINITION POSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
 FACT
ACL2 &gt;(trace$ fact)
NIL
ACL2 &gt;:set-guard-checking t<p>

Turning guard checking on, value T.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)<p>

ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
on recursive calls of the executable counterpart (i.e., in the ACL2
logic) of FACT.  To check guards on all recursive calls:
  (set-guard-checking :all)
To leave behavior unchanged except for inhibiting this message:
  (set-guard-checking :nowarn)<p>

&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC wet for how you might be able to get an error backtrace. 
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :all<p>

Leaving guard checking on, but changing value to :ALL.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (ACL2_*1*_ACL2::FACT 1)
    3&gt; (ACL2_*1*_ACL2::FACT 0)
    &lt;3 (ACL2_*1*_ACL2::FACT 1)
  &lt;2 (ACL2_*1*_ACL2::FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC wet for how you might be able to get an error backtrace. 
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :none<p>

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:set-guard-checking nil<p>

Masking guard violations but still checking guards.  To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;(verify-guards fact)<p>

Computing the guard conjecture for FACT....<p>

The guard conjecture for FACT is trivial to prove, given the :compound-
recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning
and the :type-prescription rule FACT.  FACT is compliant with Common
Lisp.<p>

Summary
Form:  ( VERIFY-GUARDS FACT)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FACT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 &gt;(trace$ fact)
NIL
ACL2 &gt;:set-guard-checking t<p>

Turning guard checking on, value T.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC wet for how you might be able to get an error backtrace. 
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :all<p>

Leaving guard checking on, but changing value to :ALL.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC wet for how you might be able to get an error backtrace. 
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :none<p>

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:set-guard-checking nil<p>

Masking guard violations but still checking guards.  To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:u
 L        1:x(DEFUN FACT (X) ...)
ACL2 &gt;:u
          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 &gt;(defun fact (x)
         (declare (xargs :guard (integerp x)
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))<p>

For the admission of FACT we will use the relation O&lt; (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is<p>

Goal
(IMPLIES (POSP X)
         (O&lt; (ACL2-COUNT (+ -1 X))
             (ACL2-COUNT X))).<p>

By the simple :definition POSP we reduce the conjecture to<p>

Goal'
(IMPLIES (AND (INTEGERP X) (&lt; 0 X))
         (O&lt; (ACL2-COUNT (+ -1 X))
             (ACL2-COUNT X))).<p>

But we reduce the conjecture to T, by case analysis.<p>

Q.E.D.<p>

That completes the proof of the measure theorem for FACT.  Thus, we
admit this function under the principle of definition. We observe that
the type of FACT is described by the theorem 
(AND (INTEGERP (FACT X)) (&lt; 0 (FACT X))).  We used the :compound-recognizer
rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.<p>

Computing the guard conjecture for FACT....<p>

The guard conjecture for FACT is trivial to prove, given the :compound-
recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning
and the :type-prescription rule FACT.  FACT is compliant with Common
Lisp.<p>

Summary
Form:  ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION NOT)
        (:DEFINITION POSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FACT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 &gt;(trace$ fact)
NIL
ACL2 &gt;:set-guard-checking t<p>

Turning guard checking on, value T.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC wet for how you might be able to get an error backtrace. 
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :all<p>

Leaving guard checking on, but changing value to :ALL.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)<p>


ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
is (INTEGERP X), is violated by the arguments in the call (FACT T).
See :DOC wet for how you might be able to get an error backtrace. 
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.<p>

ACL2 !&gt;:set-guard-checking :none<p>

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:set-guard-checking nil<p>

Masking guard violations but still checking guards.  To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:u
          0:x(EXIT-BOOT-STRAP-MODE)
ACL2 &gt;(defun fact (x)
         (declare (xargs :guard t
                         :verify-guards nil
                         :mode :logic))
         (if (posp x)
             (* x (fact (1- x)))
           1))<p>

For the admission of FACT we will use the relation O&lt; (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X).  The non-trivial part of the measure conjecture is<p>

Goal
(IMPLIES (POSP X)
         (O&lt; (ACL2-COUNT (+ -1 X))
             (ACL2-COUNT X))).<p>

By the simple :definition POSP we reduce the conjecture to<p>

Goal'
(IMPLIES (AND (INTEGERP X) (&lt; 0 X))
         (O&lt; (ACL2-COUNT (+ -1 X))
             (ACL2-COUNT X))).<p>

But we reduce the conjecture to T, by case analysis.<p>

Q.E.D.<p>

That completes the proof of the measure theorem for FACT.  Thus, we
admit this function under the principle of definition. We observe that
the type of FACT is described by the theorem 
(AND (INTEGERP (FACT X)) (&lt; 0 (FACT X))).  We used the :compound-recognizer
rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.<p>

Summary
Form:  ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:DEFINITION NOT)
        (:DEFINITION POSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 &gt;(trace$ fact)
NIL
ACL2 &gt;:set-guard-checking t<p>

Turning guard checking on, value T.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !&gt;:set-guard-checking :all<p>

Leaving guard checking on, but changing value to :ALL.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (ACL2_*1*_ACL2::FACT 1)
    3&gt; (ACL2_*1*_ACL2::FACT 0)
    &lt;3 (ACL2_*1*_ACL2::FACT 1)
  &lt;2 (ACL2_*1*_ACL2::FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !&gt;:set-guard-checking :none<p>

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:set-guard-checking nil<p>

Masking guard violations but still checking guards.  To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;(verify-guards fact)<p>

Computing the guard conjecture for FACT....<p>

The guard conjecture for FACT is trivial to prove, given the :compound-
recognizer rule POSP-COMPOUND-RECOGNIZER and the :type-prescription
rule FACT.  FACT is compliant with Common Lisp.<p>

Summary
Form:  ( VERIFY-GUARDS FACT)
Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
        (:TYPE-PRESCRIPTION FACT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 &gt;(trace$ fact)
NIL
ACL2 &gt;:set-guard-checking t<p>

Turning guard checking on, value T.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
  2&gt; (FACT T)
  &lt;2 (FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !&gt;:set-guard-checking :all<p>

Leaving guard checking on, but changing value to :ALL.<p>

ACL2 !&gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 !&gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
  2&gt; (FACT T)
  &lt;2 (FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 !&gt;:set-guard-checking :none<p>

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
  2&gt; (FACT T)
  &lt;2 (FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;:set-guard-checking nil<p>

Masking guard violations but still checking guards.  To avoid guard
checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
checking.<p>

ACL2 &gt;(fact 2)
1&gt; (ACL2_*1*_ACL2::FACT 2)
  2&gt; (FACT 2)
    3&gt; (FACT 1)
      4&gt; (FACT 0)
      &lt;4 (FACT 1)
    &lt;3 (FACT 1)
  &lt;2 (FACT 2)
&lt;1 (ACL2_*1*_ACL2::FACT 2)
2
ACL2 &gt;(fact t)
1&gt; (ACL2_*1*_ACL2::FACT T)
  2&gt; (FACT T)
  &lt;2 (FACT 1)
&lt;1 (ACL2_*1*_ACL2::FACT 1)
1
ACL2 &gt;
</pre>

<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>