(exec-proof-tree-list ptrees defs p) → outcome
Theorem:
(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)))))