| java.lang.Object
 de.uka.ilkd.key.logic.DepthTermOrdering
de.uka.ilkd.key.logic.CascadeDepthTermOrdering
| CascadeDepthTermOrdering | | public class CascadeDepthTermOrdering extends DepthTermOrdering (Code) | | Term ordering, comparing the maximum depths of terms and contained
variables; following definition 5.14 in the script "Automatisches
Beweisen", Bernhard Beckert, Reiner Haehnle
This ordering has the possibility to refer to a secundary ordering
upon terms having the same depths (i.e. both the same maximal depth
and maximal variable depths); this guarantees substitutions to stay
monotonic
|
| compare | | public int compare(Term p_a, Term p_b)(Code) | | Compare the two given terms
a number negative, zero or a number positive ifp_a is less than, equal, or greater thanp_b regarding the ordering given by theimplementing class |
|
|