Term Rewriting System R:
[x, y, z]
and(x, or(y, z)) -> or(and(x, y), and(x, z))
and(x, and(y, y)) -> and(x, y)
and(x, true) -> x
and(false, y) -> false
and(x, x) -> x
or(or(x, y), and(y, z)) -> or(x, y)
or(x, and(x, y)) -> x
or(true, y) -> true
or(x, false) -> x
or(x, x) -> x
or(x, or(y, y)) -> or(x, y)
Innermost Termination of R to be shown.
R
↳Removing Redundant Rules for Innermost Termination
Removing the following rules from R which left hand sides contain non normal subterms
and(x, and(y, y)) -> and(x, y)
or(x, or(y, y)) -> or(x, y)
R
↳RRRI
→TRS2
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
AND(x, or(y, z)) -> OR(and(x, y), and(x, z))
AND(x, or(y, z)) -> AND(x, y)
AND(x, or(y, z)) -> AND(x, z)
Furthermore, R contains one SCC.
R
↳RRRI
→TRS2
↳DPs
→DP Problem 1
↳Size-Change Principle
Dependency Pairs:
AND(x, or(y, z)) -> AND(x, z)
AND(x, or(y, z)) -> AND(x, y)
Rules:
and(x, or(y, z)) -> or(and(x, y), and(x, z))
and(x, true) -> x
and(false, y) -> false
and(x, x) -> x
or(or(x, y), and(y, z)) -> or(x, y)
or(x, and(x, y)) -> x
or(true, y) -> true
or(x, false) -> x
or(x, x) -> x
We number the DPs as follows:
- AND(x, or(y, z)) -> AND(x, z)
- AND(x, or(y, z)) -> AND(x, y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
or(x_{1}, x_{2}) -> or(x_{1}, x_{2})
We obtain no new DP problems.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes