public class ProofDerivationStepEntry
extends java.lang.Object
We use mmj.verify.VerifyProofs to generate the ProofDerivationStepEntry objects for a theorem because VerifyProofs already has the complete mechanism for dealing with a Metamath proof and generating the formula resulting from each derivation step.
Modifier and Type | Field and Description |
---|---|
Formula |
formula
formula is the formula resulting from the derivation using the Ref and
its hypotheses.
|
ParseTree |
formulaParseTree
formulaParseTree is here for use in TMFF, Text Mode Formula Formatting.
|
java.lang.String[] |
hypStep
hypStepNbr contains the stepNbr's of previous steps that are to be used
as hypotheses for the Ref Assrt in the current step.
|
boolean |
isAutoStep |
boolean |
isHyp
isHyp indicates if this step is one of the Theorem's logical hypothesis
steps.
|
int |
proofLevel
Level number of the step within the proof where the qed step has level 0
and each hypothesis is one level higher.
|
java.lang.String |
refLabel
refLabel is the label of the Assrt used to justify the step, and which
creates the derivation of the step's formula.
|
java.lang.String |
step
stepNbr is an integer ranging from 1 through n - 1, where 'n' is the last
derivation step of the proof -- and the final step number is "qed".
|
Constructor and Description |
---|
ProofDerivationStepEntry() |
Modifier and Type | Method and Description |
---|---|
static void |
computeProofLevels(java.util.List<ProofDerivationStepEntry> pList)
Compute proof level numbers for a proof stored in a
ProofDerivationStepEntry ArrayList.
|
static void |
computeProofLevelsSlowly(java.util.List<ProofDerivationStepEntry> pList)
Compute proof level numbers for a proof stored in a
ProofDerivationStepEntry ArrayList.
|
java.lang.String |
toString() |
public boolean isHyp
public java.lang.String step
public java.lang.String[] hypStep
public java.lang.String refLabel
refLabel is always present on hypothesis steps because a Theorem's proof may not refer to the hypotheses in database sequence and so there could be ambiguity about which step is referring to which hypothesis.
public Formula formula
public ParseTree formulaParseTree
formulaParseTree of the formula, or null if either the parse failed or has not yet been attempted (VerifyProofs.getProofDerivationSteps() and VerifyProofs.loadProofDerivStepList() will load the parse tree for the theorem's formula and its logical hypotheses, but the proof step parse trees are not available there -- so ProofWorksheet will fill in the missing parses.)
public int proofLevel
public boolean isAutoStep
public java.lang.String toString()
toString
in class java.lang.Object
public static void computeProofLevels(java.util.List<ProofDerivationStepEntry> pList)
pList
- ProofDerivationStepEntry ArrayListpublic static void computeProofLevelsSlowly(java.util.List<ProofDerivationStepEntry> pList)
This routine is coded because there may be incomplete or invalid proofs that the normal routine cannot handle...and yet, 99.99% of the time we are dealing with complete, valid proofs so it is deemed preferable to try to do the computation the quick way first and see what happens.
pList
- ProofDerivationStepEntry ArrayList