public static class Provers.UseWhenPossible extends Prover.HypProver
It does not use work variables in the substitution; thus applying the theorem addcni "( A + B ) e. CC" to "( ( 1 + 1 ) + &C2 ) e. CC" will succeed (with A = ( 1 + 1 ) and B = &C2), but will fail against "&C1 e. CC" even though unification is possible.
Prover.AssrtProver, Prover.HypProver, Prover.HypProverResult, Prover.ProverResult
Modifier and Type | Field and Description |
---|---|
protected VarHyp[] |
varHypArray |
assrt
Constructor and Description |
---|
UseWhenPossible(Assrt assrt) |
UseWhenPossible(Assrt assrt,
Provers.UseWhenPossibleListener f) |
Modifier and Type | Method and Description |
---|---|
Prover.HypProverResult |
hypProve(mmj.transforms.WorksheetInfo info,
ParseNode root)
Similar to
Prover.prove(WorksheetInfo, ParseNode) . |
prove
toString
protected VarHyp[] varHypArray
public UseWhenPossible(Assrt assrt)
public UseWhenPossible(Assrt assrt, Provers.UseWhenPossibleListener f)
public Prover.HypProverResult hypProve(mmj.transforms.WorksheetInfo info, ParseNode root)
Prover.HypProver
Prover.prove(WorksheetInfo, ParseNode)
. Prove a
goal expression, producing an Assrt and a list of substitutions to
variables. The list of variables must be exhaustive in all VarHyps
used in the conclusion and its hypotheses; failure to do so will
cause an IllegalArgumentException
.hypProve
in class Prover.HypProver
info
- The contextroot
- The goal expression