| java.lang.Object
 de.uka.ilkd.key.logic.Term
de.uka.ilkd.key.logic.SubstitutionTerm
| SubstitutionTerm | | class SubstitutionTerm extends Term (Code) | | A SubstitutionTerm is an object that contains an Operator two subterms.
and one variable
Instances should never be accessed via
this interface, use the interface of the superclass Term and construct
instances only via
a TermFactory instead.
|
| Method Summary | |
| public int | arity()
| | public int | depth()
| | public Term | sub(int n)
returns the n-th subterm
n-th subterm ( e.g. | | public ArrayOfQuantifiableVariable | varsBoundHere(int n)
the substitution term bound the substituted variable in second
(attention: i.e. |
| SubstitutionTerm | | public SubstitutionTerm(Operator op, QuantifiableVariable substVar, Term[] subs)(Code) | | creates a substitution term
Parameters:
substVar - the Variable to be substituted
Parameters:
substTerm - the Term that replaces substVar
Parameters:
origTerm - the Term that is substituted |
| arity | | public int arity()(Code) | | returns 2 as arity of a substitution term
arity of the substitution term 1 as int |
| depth | | public int depth()(Code) | | returns the longest path from the root to the leaves
depth of the term |
| sub | | public Term sub(int n)(Code) | | returns the n-th subterm
n-th subterm ( e.g. {x s} t (0:s , 1: t) |
| varsBoundHere | | public ArrayOfQuantifiableVariable varsBoundHere(int n)(Code) | | the substitution term bound the substituted variable in second
(attention: i.e. n=1) subterm
the bound variables of the n-th subterm |
|
|