Term Rewriting System R:
[z, x, y]
+(a, b) -> +(b, a)
+(a, +(b, z)) -> +(b, +(a, z))
+(+(x, y), z) -> +(x, +(y, z))
f(a, y) -> a
f(b, y) -> b
f(+(x, y), z) -> +(f(x, z), f(y, z))
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
+'(a, b) -> +'(b, a)
+'(a, +(b, z)) -> +'(b, +(a, z))
+'(a, +(b, z)) -> +'(a, z)
+'(+(x, y), z) -> +'(x, +(y, z))
+'(+(x, y), z) -> +'(y, z)
F(+(x, y), z) -> +'(f(x, z), f(y, z))
F(+(x, y), z) -> F(x, z)
F(+(x, y), z) -> F(y, z)
Furthermore, R contains three SCCs.
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
Dependency Pair:
+'(a, +(b, z)) -> +'(a, z)
Rules:
+(a, b) -> +(b, a)
+(a, +(b, z)) -> +(b, +(a, z))
+(+(x, y), z) -> +(x, +(y, z))
f(a, y) -> a
f(b, y) -> b
f(+(x, y), z) -> +(f(x, z), f(y, z))
Strategy:
innermost
As we are in the innermost case, we can delete all 6 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳A-Transformation
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
Dependency Pair:
+'(a, +(b, z)) -> +'(a, z)
Rule:
none
Strategy:
innermost
We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳ATrans
...
→DP Problem 5
↳Size-Change Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
Dependency Pair:
A(b(z)) -> A(z)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
- A(b(z)) -> A(z)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
b(x1) -> b(x1)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
Dependency Pair:
+'(+(x, y), z) -> +'(y, z)
Rules:
+(a, b) -> +(b, a)
+(a, +(b, z)) -> +(b, +(a, z))
+(+(x, y), z) -> +(x, +(y, z))
f(a, y) -> a
f(b, y) -> b
f(+(x, y), z) -> +(f(x, z), f(y, z))
Strategy:
innermost
As we are in the innermost case, we can delete all 6 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 6
↳Size-Change Principle
→DP Problem 3
↳UsableRules
Dependency Pair:
+'(+(x, y), z) -> +'(y, z)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
- +'(+(x, y), z) -> +'(y, z)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
+(x1, x2) -> +(x1, x2)
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
Dependency Pair:
F(+(x, y), z) -> F(y, z)
Rules:
+(a, b) -> +(b, a)
+(a, +(b, z)) -> +(b, +(a, z))
+(+(x, y), z) -> +(x, +(y, z))
f(a, y) -> a
f(b, y) -> b
f(+(x, y), z) -> +(f(x, z), f(y, z))
Strategy:
innermost
As we are in the innermost case, we can delete all 6 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 7
↳Size-Change Principle
Dependency Pair:
F(+(x, y), z) -> F(y, z)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
- F(+(x, y), z) -> F(y, z)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
+(x1, x2) -> +(x1, x2)
We obtain no new DP problems.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes