org.qedeq.kernel.se.base.module
Interface Rename

All Superinterfaces:

Reason

All Known Implementing Classes:

RenameVo

public interface Rename
extends Reason

Rename bound subject variable. This replacement can take place for a certain bound occurrence of the subject variable. For example in this case we replace x by y in at the first occurrence.

   forall x A(x)
  ---------------
   forall y A(y)
 

Author:

Michael Meyling

Method Summary

int	getOccurrence() Get bound occurrence to replace.
Element	getOriginalSubjectVariable() Get original subject variable.
java.lang.String	getReference() Get reference to formula.
Rename	getRename() Get this reason.
Element	getReplacementSubjectVariable() Get replacement subject variable.

Methods inherited from interface org.qedeq.kernel.se.base.module.Reason

getName, getReferences

Method Detail

getRename

Rename getRename()

Get this reason.

Returns:

This reason.

getReference

java.lang.String getReference()

Get reference to formula. Usually this a formula of type A(x)

Returns:

Reference to previously proved formula.

getOriginalSubjectVariable

Element getOriginalSubjectVariable()

Get original subject variable. Something like x.

Returns:

Subject variable.

getReplacementSubjectVariable

Element getReplacementSubjectVariable()

Get replacement subject variable. Something like y.

Returns:

Subject variable.

getOccurrence

int getOccurrence()

Get bound occurrence to replace. Starts with 1. A value of 0 means no specification.

Returns:

Number of occurrence.