resolveRedundancy
public static ImmutableList<Term> resolveRedundancy(Term t1,
Term t2)
resolves term redundancy (used by Sequent to avoid duplicate formulas).
In case of t2 being unlabeled a list with t1 as single element is
returned. Otherwise if t1 is unlabeled (and t2 labeled), then a list with t2 as single element
is returned. If both terms are labeled a list of terms is returned which is not redundant.
The terms t1 and t2 may only differ in their attached labels. Otherwise they have to be
structural identical
This method should be used in case to implement more complex redundancy checks.
- Parameters:
t1
- the Term t1 which is structural equivalent to t2 (except maybe labels)
t2
- the Term t2
- Returns:
- a list which represents a redundancy free result of merging labels in t1 and t2