NAT-ETREE : MEXPR

NAT-ETREE is a top-level command.
Translates a natural deduction proof, (which must be the current dproof
-- use RECONSIDER to return to an old proof in memory), into an
expansion proof. This will not work on all proofs: in particular,
proofs containing ASSERT of anything but REFL= and SYM=, proofs
using rewrite rules and proofs containing SUBST= or SUB= cannot be
translated at present. However, the user is given the option of
removing lines justified by SUBST= or SUB= and replacing the justification
with a subproof. This permanently modifies the proof. (AUTO-SUGGEST
also gives such an option.)
The command format for NAT-ETREE is:

 <n>NAT-ETREE  PREFIX 
"SYMBOL"


The arguments have the following meaning:
PREFIX : Name of the Proof

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage