		Search-engine friendly clone of the ACL2 documentation.

Exec-proof-tree

Exec-proof-tree-list

Signature
(exec-proof-tree-list ptrees defs p) → outcome
Arguments: ptrees — Guard (proof-tree-listp ptrees).; defs — Guard (definition-listp defs).; p — Guard (primep p).
Returns: outcome — Type (proof-list-outcomep outcome).

Definitions and Theorems

Theorem: len-of-exec-proof-tree-list

(defthm len-of-exec-proof-tree-list
 (b* ((?outcome (exec-proof-tree-list ptrees defs p)))
  (implies (proof-list-outcome-case outcome :assertions)
           (equal (len (proof-list-outcome-assertions->get outcome))
                  (len ptrees)))))