Term Rewriting System R:
[x, y, z]
0(#) > #
+(#, x) > x
+(x, #) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
(#, x) > #
(x, #) > x
(0(x), 0(y)) > 0((x, y))
(0(x), 1(y)) > 1(((x, y), 1(#)))
(1(x), 0(y)) > 1((x, y))
(1(x), 1(y)) > 0((x, y))
not(true) > false
not(false) > true
if(true, x, y) > x
if(false, x, y) > y
ge(0(x), 0(y)) > ge(x, y)
ge(0(x), 1(y)) > not(ge(y, x))
ge(1(x), 0(y)) > ge(x, y)
ge(1(x), 1(y)) > ge(x, y)
ge(x, #) > true
ge(#, 0(x)) > ge(#, x)
ge(#, 1(x)) > false
log(x) > (log'(x), 1(#))
log'(#) > #
log'(1(x)) > +(log'(x), 1(#))
log'(0(x)) > if(ge(x, 1(#)), +(log'(x), 1(#)), #)
Termination of R to be shown.
R
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
log(x) > (log'(x), 1(#))
where the Polynomial interpretation:
_{ }^{ }POL(#)  = 0_{ }^{ } 
_{ }^{ }POL(if(x_{1}, x_{2}, x_{3}))  = x_{1} + x_{2} + x_{3}_{ }^{ } 
_{ }^{ }POL(0(x_{1}))  = 2·x_{1}_{ }^{ } 
_{ }^{ }POL(false)  = 0_{ }^{ } 
_{ }^{ }POL(log'(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL(1(x_{1}))  = 2·x_{1}_{ }^{ } 
_{ }^{ }POL(log(x_{1}))  = 1 + x_{1}_{ }^{ } 
_{ }^{ }POL(true)  = 0_{ }^{ } 
_{ }^{ }POL(ge(x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL((x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(not(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL(+(x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRPolo
→TRS2
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
GE(0(x), 0(y)) > GE(x, y)
GE(0(x), 1(y)) > NOT(ge(y, x))
GE(0(x), 1(y)) > GE(y, x)
GE(1(x), 1(y)) > GE(x, y)
GE(#, 0(x)) > GE(#, x)
GE(1(x), 0(y)) > GE(x, y)
'(0(x), 1(y)) > '((x, y), 1(#))
'(0(x), 1(y)) > '(x, y)
'(0(x), 0(y)) > 0'((x, y))
'(0(x), 0(y)) > '(x, y)
'(1(x), 1(y)) > 0'((x, y))
'(1(x), 1(y)) > '(x, y)
'(1(x), 0(y)) > '(x, y)
+'(0(x), 1(y)) > +'(x, y)
+'(1(x), 0(y)) > +'(x, y)
+'(0(x), 0(y)) > 0'(+(x, y))
+'(0(x), 0(y)) > +'(x, y)
+'(1(x), 1(y)) > 0'(+(+(x, y), 1(#)))
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(1(x), 1(y)) > +'(x, y)
+'(+(x, y), z) > +'(x, +(y, z))
+'(+(x, y), z) > +'(y, z)
LOG'(0(x)) > IF(ge(x, 1(#)), +(log'(x), 1(#)), #)
LOG'(0(x)) > GE(x, 1(#))
LOG'(0(x)) > +'(log'(x), 1(#))
LOG'(0(x)) > LOG'(x)
LOG'(1(x)) > +'(log'(x), 1(#))
LOG'(1(x)) > LOG'(x)
Furthermore, R contains five SCCs.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SizeChange Principle
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pair:
GE(#, 0(x)) > GE(#, x)
Rules:
ge(0(x), 0(y)) > ge(x, y)
ge(0(x), 1(y)) > not(ge(y, x))
ge(1(x), 1(y)) > ge(x, y)
ge(x, #) > true
ge(#, 0(x)) > ge(#, x)
ge(1(x), 0(y)) > ge(x, y)
ge(#, 1(x)) > false
0(#) > #
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
not(true) > false
not(false) > true
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
log'(0(x)) > if(ge(x, 1(#)), +(log'(x), 1(#)), #)
log'(1(x)) > +(log'(x), 1(#))
log'(#) > #
if(false, x, y) > y
if(true, x, y) > x
We number the DPs as follows:
 GE(#, 0(x)) > GE(#, x)
and get the following SizeChange 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 NonStrict Precedence.
trivial
with Argument Filtering System:
0(x_{1}) > 0(x_{1})
We obtain no new DP problems.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Modular Removal of Rules
→DP Problem 3
↳MRR
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pairs:
'(1(x), 0(y)) > '(x, y)
'(1(x), 1(y)) > '(x, y)
'(0(x), 0(y)) > '(x, y)
'(0(x), 1(y)) > '(x, y)
'(0(x), 1(y)) > '((x, y), 1(#))
Rules:
ge(0(x), 0(y)) > ge(x, y)
ge(0(x), 1(y)) > not(ge(y, x))
ge(1(x), 1(y)) > ge(x, y)
ge(x, #) > true
ge(#, 0(x)) > ge(#, x)
ge(1(x), 0(y)) > ge(x, y)
ge(#, 1(x)) > false
0(#) > #
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
not(true) > false
not(false) > true
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
log'(0(x)) > if(ge(x, 1(#)), +(log'(x), 1(#)), #)
log'(1(x)) > +(log'(x), 1(#))
log'(#) > #
if(false, x, y) > y
if(true, x, y) > x
We have the following set of usable rules:
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
0(#) > #
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#)  = 0_{ }^{ } 
_{ }^{ }POL('(x_{1}, x_{2}))  = 1 + x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(0(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL(1(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL((x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
We have the following set D of usable symbols: {#, ', 0, 1, }
No Dependency Pairs can be deleted.
21 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
...
→DP Problem 6
↳Modular Removal of Rules
→DP Problem 3
↳MRR
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pairs:
'(1(x), 0(y)) > '(x, y)
'(1(x), 1(y)) > '(x, y)
'(0(x), 0(y)) > '(x, y)
'(0(x), 1(y)) > '(x, y)
'(0(x), 1(y)) > '((x, y), 1(#))
Rules:
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
0(#) > #
We have the following set of usable rules:
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
0(#) > #
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#)  = 0_{ }^{ } 
_{ }^{ }POL('(x_{1}, x_{2}))  = 1 + x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(0(x_{1}))  = 1 + x_{1}_{ }^{ } 
_{ }^{ }POL(1(x_{1}))  = 1 + x_{1}_{ }^{ } 
_{ }^{ }POL((x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
We have the following set D of usable symbols: {#, ', 0, 1, }
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
'(1(x), 0(y)) > '(x, y)
'(1(x), 1(y)) > '(x, y)
'(0(x), 0(y)) > '(x, y)
'(0(x), 1(y)) > '(x, y)
'(0(x), 1(y)) > '((x, y), 1(#))
No Rules can be deleted.
After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳Modular Removal of Rules
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pairs:
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+'(1(x), 1(y)) > +'(x, y)
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(0(x), 0(y)) > +'(x, y)
+'(1(x), 0(y)) > +'(x, y)
+'(0(x), 1(y)) > +'(x, y)
Rules:
ge(0(x), 0(y)) > ge(x, y)
ge(0(x), 1(y)) > not(ge(y, x))
ge(1(x), 1(y)) > ge(x, y)
ge(x, #) > true
ge(#, 0(x)) > ge(#, x)
ge(1(x), 0(y)) > ge(x, y)
ge(#, 1(x)) > false
0(#) > #
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
not(true) > false
not(false) > true
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
log'(0(x)) > if(ge(x, 1(#)), +(log'(x), 1(#)), #)
log'(1(x)) > +(log'(x), 1(#))
log'(#) > #
if(false, x, y) > y
if(true, x, y) > x
We have the following set of usable rules:
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
0(#) > #
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#)  = 0_{ }^{ } 
_{ }^{ }POL(0(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL(1(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL(+(x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(+'(x_{1}, x_{2}))  = 1 + x_{1} + x_{2}_{ }^{ } 
We have the following set D of usable symbols: {#, 0, 1, +, +'}
No Dependency Pairs can be deleted.
20 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
...
→DP Problem 7
↳Modular Removal of Rules
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pairs:
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+'(1(x), 1(y)) > +'(x, y)
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(0(x), 0(y)) > +'(x, y)
+'(1(x), 0(y)) > +'(x, y)
+'(0(x), 1(y)) > +'(x, y)
Rules:
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
0(#) > #
We have the following set of usable rules:
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
0(#) > #
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#)  = 0_{ }^{ } 
_{ }^{ }POL(0(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL(1(x_{1}))  = 1 + x_{1}_{ }^{ } 
_{ }^{ }POL(+(x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(+'(x_{1}, x_{2}))  = 1 + x_{1} + x_{2}_{ }^{ } 
We have the following set D of usable symbols: {#, 0, 1, +, +'}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
+'(1(x), 1(y)) > +'(x, y)
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(1(x), 0(y)) > +'(x, y)
+'(0(x), 1(y)) > +'(x, y)
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
The result of this processor delivers one new DP problem.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
...
→DP Problem 8
↳Modular Removal of Rules
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pairs:
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+'(0(x), 0(y)) > +'(x, y)
Rules:
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
0(#) > #
We have the following set of usable rules:
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
0(#) > #
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#)  = 0_{ }^{ } 
_{ }^{ }POL(0(x_{1}))  = 1 + x_{1}_{ }^{ } 
_{ }^{ }POL(1(x_{1}))  = x_{1}_{ }^{ } 
_{ }^{ }POL(+(x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(+'(x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
We have the following set D of usable symbols: {#, 0, 1, +, +'}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
+'(0(x), 0(y)) > +'(x, y)
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
0(#) > #
The result of this processor delivers one new DP problem.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
...
→DP Problem 9
↳Modular Removal of Rules
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pairs:
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
Rules:
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
We have the following set of usable rules:
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#)  = 0_{ }^{ } 
_{ }^{ }POL(+(x_{1}, x_{2}))  = x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(+'(x_{1}, x_{2}))  = 1 + x_{1} + x_{2}_{ }^{ } 
We have the following set D of usable symbols: {+, +'}
No Dependency Pairs can be deleted.
The following rules can be deleted as they contain symbols in their lhs which do not occur in D:
+(x, #) > x
+(#, x) > x
The result of this processor delivers one new DP problem.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
...
→DP Problem 10
↳Modular Removal of Rules
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pairs:
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
Rule:
+(+(x, y), z) > +(x, +(y, z))
We have the following set of usable rules:
+(+(x, y), z) > +(x, +(y, z))
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(+(x_{1}, x_{2}))  = 1 + x_{1} + x_{2}_{ }^{ } 
_{ }^{ }POL(+'(x_{1}, x_{2}))  = 1 + x_{1} + x_{2}_{ }^{ } 
We have the following set D of usable symbols: {+, +'}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
+'(+(x, y), z) > +'(y, z)
No Rules can be deleted.
The result of this processor delivers one new DP problem.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
...
→DP Problem 11
↳SizeChange Principle
→DP Problem 4
↳SCP
→DP Problem 5
↳SCP
Dependency Pair:
+'(+(x, y), z) > +'(x, +(y, z))
Rule:
+(+(x, y), z) > +(x, +(y, z))
We number the DPs as follows:
 +'(+(x, y), z) > +'(x, +(y, z))
and get the following SizeChange 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 NonStrict Precedence.
trivial
We obtain no new DP problems.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
→DP Problem 4
↳SizeChange Principle
→DP Problem 5
↳SCP
Dependency Pairs:
GE(1(x), 0(y)) > GE(x, y)
GE(1(x), 1(y)) > GE(x, y)
GE(0(x), 1(y)) > GE(y, x)
GE(0(x), 0(y)) > GE(x, y)
Rules:
ge(0(x), 0(y)) > ge(x, y)
ge(0(x), 1(y)) > not(ge(y, x))
ge(1(x), 1(y)) > ge(x, y)
ge(x, #) > true
ge(#, 0(x)) > ge(#, x)
ge(1(x), 0(y)) > ge(x, y)
ge(#, 1(x)) > false
0(#) > #
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
not(true) > false
not(false) > true
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
log'(0(x)) > if(ge(x, 1(#)), +(log'(x), 1(#)), #)
log'(1(x)) > +(log'(x), 1(#))
log'(#) > #
if(false, x, y) > y
if(true, x, y) > x
We number the DPs as follows:
 GE(1(x), 0(y)) > GE(x, y)
 GE(1(x), 1(y)) > GE(x, y)
 GE(0(x), 1(y)) > GE(y, x)
 GE(0(x), 0(y)) > GE(x, y)
and get the following SizeChange Graph(s): {4, 3, 2, 1}  ,  {4, 3, 2, 1} 

1  >  1 
2  >  2 

{4, 3, 2, 1}  ,  {4, 3, 2, 1} 

1  >  2 
2  >  1 

which lead(s) to this/these maximal multigraph(s): {4, 3, 2, 1}  ,  {4, 3, 2, 1} 

1  >  1 
2  >  2 

D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with NonStrict Precedence.
trivial
with Argument Filtering System:
0(x_{1}) > 0(x_{1})
1(x_{1}) > 1(x_{1})
We obtain no new DP problems.
R
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
→DP Problem 4
↳SCP
→DP Problem 5
↳SizeChange Principle
Dependency Pairs:
LOG'(1(x)) > LOG'(x)
LOG'(0(x)) > LOG'(x)
Rules:
ge(0(x), 0(y)) > ge(x, y)
ge(0(x), 1(y)) > not(ge(y, x))
ge(1(x), 1(y)) > ge(x, y)
ge(x, #) > true
ge(#, 0(x)) > ge(#, x)
ge(1(x), 0(y)) > ge(x, y)
ge(#, 1(x)) > false
0(#) > #
(0(x), 1(y)) > 1(((x, y), 1(#)))
(0(x), 0(y)) > 0((x, y))
(1(x), 1(y)) > 0((x, y))
(1(x), 0(y)) > 1((x, y))
(x, #) > x
(#, x) > #
not(true) > false
not(false) > true
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(0(x), 0(y)) > 0(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
+(x, #) > x
+(#, x) > x
log'(0(x)) > if(ge(x, 1(#)), +(log'(x), 1(#)), #)
log'(1(x)) > +(log'(x), 1(#))
log'(#) > #
if(false, x, y) > y
if(true, x, y) > x
We number the DPs as follows:
 LOG'(1(x)) > LOG'(x)
 LOG'(0(x)) > LOG'(x)
and get the following SizeChange 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 NonStrict Precedence.
trivial
with Argument Filtering System:
0(x_{1}) > 0(x_{1})
1(x_{1}) > 1(x_{1})
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:07 minutes