R
↳Dependency Pair Analysis
+'(O(x), O(y)) > O'(+(x, y))
+'(O(x), O(y)) > +'(x, y)
+'(O(x), I(y)) > +'(x, y)
+'(I(x), O(y)) > +'(x, y)
+'(I(x), I(y)) > O'(+(+(x, y), I(0)))
+'(I(x), I(y)) > +'(+(x, y), I(0))
+'(I(x), I(y)) > +'(x, y)
+'(x, +(y, z)) > +'(+(x, y), z)
+'(x, +(y, z)) > +'(x, y)
'(O(x), O(y)) > O'((x, y))
'(O(x), O(y)) > '(x, y)
'(O(x), I(y)) > '((x, y), I(1))
'(O(x), I(y)) > '(x, y)
'(I(x), O(y)) > '(x, y)
'(I(x), I(y)) > O'((x, y))
'(I(x), I(y)) > '(x, y)
GE(O(x), O(y)) > GE(x, y)
GE(O(x), I(y)) > NOT(ge(y, x))
GE(O(x), I(y)) > GE(y, x)
GE(I(x), O(y)) > GE(x, y)
GE(I(x), I(y)) > GE(x, y)
GE(0, O(x)) > GE(0, x)
LOG'(I(x)) > +'(Log'(x), I(0))
LOG'(I(x)) > LOG'(x)
LOG'(O(x)) > IF(ge(x, I(0)), +(Log'(x), I(0)), 0)
LOG'(O(x)) > GE(x, I(0))
LOG'(O(x)) > +'(Log'(x), I(0))
LOG'(O(x)) > LOG'(x)
LOG(x) > '(Log'(x), I(0))
LOG(x) > LOG'(x)
MIN(N(x, l, r)) > MIN(l)
MAX(N(x, l, r)) > MAX(r)
BS'(N(x, l, r)) > AND(and(ge(x, Max(l)), ge(Min(r), x)), and(BS(l), BS(r)))
BS'(N(x, l, r)) > AND(ge(x, Max(l)), ge(Min(r), x))
BS'(N(x, l, r)) > GE(x, Max(l))
BS'(N(x, l, r)) > MAX(l)
BS'(N(x, l, r)) > GE(Min(r), x)
BS'(N(x, l, r)) > MIN(r)
BS'(N(x, l, r)) > AND(BS(l), BS(r))
BS'(N(x, l, r)) > BS'(l)
BS'(N(x, l, r)) > BS'(r)
SIZE(N(x, l, r)) > +'(+(Size(l), Size(r)), I(1))
SIZE(N(x, l, r)) > +'(Size(l), Size(r))
SIZE(N(x, l, r)) > SIZE(l)
SIZE(N(x, l, r)) > SIZE(r)
WB'(N(x, l, r)) > AND(if(ge(Size(l), Size(r)), ge(I(0), (Size(l), Size(r))), ge(I(0), (Size(r), Size(l)))), and(WB(l), WB(r)))
WB'(N(x, l, r)) > IF(ge(Size(l), Size(r)), ge(I(0), (Size(l), Size(r))), ge(I(0), (Size(r), Size(l))))
WB'(N(x, l, r)) > GE(Size(l), Size(r))
WB'(N(x, l, r)) > SIZE(l)
WB'(N(x, l, r)) > SIZE(r)
WB'(N(x, l, r)) > GE(I(0), (Size(l), Size(r)))
WB'(N(x, l, r)) > '(Size(l), Size(r))
WB'(N(x, l, r)) > GE(I(0), (Size(r), Size(l)))
WB'(N(x, l, r)) > '(Size(r), Size(l))
WB'(N(x, l, r)) > AND(WB(l), WB(r))
WB'(N(x, l, r)) > WB'(l)
WB'(N(x, l, r)) > WB'(r)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
+'(x, +(y, z)) > +'(x, y)
+'(x, +(y, z)) > +'(+(x, y), z)
+'(I(x), I(y)) > +'(x, y)
+'(I(x), I(y)) > +'(+(x, y), I(0))
+'(I(x), O(y)) > +'(x, y)
+'(O(x), I(y)) > +'(x, y)
+'(O(x), O(y)) > +'(x, y)
O(0) > 0
+(0, x) > x
+(x, 0) > x
+(O(x), O(y)) > O(+(x, y))
+(O(x), I(y)) > I(+(x, y))
+(I(x), O(y)) > I(+(x, y))
+(I(x), I(y)) > O(+(+(x, y), I(0)))
+(x, +(y, z)) > +(+(x, y), z)
(x, 0) > x
(0, x) > 0
(O(x), O(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(I(x), O(y)) > I((x, y))
(I(x), I(y)) > O((x, y))
not(true) > false
not(false) > true
and(x, true) > x
and(x, false) > false
if(true, x, y) > x
if(false, x, y) > y
ge(O(x), O(y)) > ge(x, y)
ge(O(x), I(y)) > not(ge(y, x))
ge(I(x), O(y)) > ge(x, y)
ge(I(x), I(y)) > ge(x, y)
ge(x, 0) > true
ge(0, O(x)) > ge(0, x)
ge(0, I(x)) > false
Log'(0) > 0
Log'(I(x)) > +(Log'(x), I(0))
Log'(O(x)) > if(ge(x, I(0)), +(Log'(x), I(0)), 0)
Log(x) > (Log'(x), I(0))
Val(L(x)) > x
Val(N(x, l, r)) > x
Min(L(x)) > x
Min(N(x, l, r)) > Min(l)
Max(L(x)) > x
Max(N(x, l, r)) > Max(r)
BS(L(x)) > true
BS(N(x, l, r)) > and(and(ge(x, Max(l)), ge(Min(r), x)), and(BS(l), BS(r)))
Size(L(x)) > I(0)
Size(N(x, l, r)) > +(+(Size(l), Size(r)), I(1))
WB(L(x)) > true
WB(N(x, l, r)) > and(if(ge(Size(l), Size(r)), ge(I(0), (Size(l), Size(r))), ge(I(0), (Size(r), Size(l)))), and(WB(l), WB(r)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 6
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
+'(x, +(y, z)) > +'(x, y)
+'(x, +(y, z)) > +'(+(x, y), z)
+'(I(x), I(y)) > +'(x, y)
+'(I(x), I(y)) > +'(+(x, y), I(0))
+'(I(x), O(y)) > +'(x, y)
+'(O(x), I(y)) > +'(x, y)
+'(O(x), O(y)) > +'(x, y)
+(I(x), O(y)) > I(+(x, y))
+(x, 0) > x
+(0, x) > x
+(I(x), I(y)) > O(+(+(x, y), I(0)))
+(O(x), O(y)) > O(+(x, y))
+(x, +(y, z)) > +(+(x, y), z)
+(O(x), I(y)) > I(+(x, y))
O(0) > 0
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(I(x), O(y)) > I(+(x, y))
+(x, 0) > x
+(0, x) > x
+(I(x), I(y)) > O(+(+(x, y), I(0)))
+(O(x), O(y)) > O(+(x, y))
+(x, +(y, z)) > +(+(x, y), z)
+(O(x), I(y)) > I(+(x, y))
O(0) > 0
_{ }^{ }POL(I(x_{1})) = 1 + x_{1}_{ }^{ } _{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(O(x_{1})) = x_{1}_{ }^{ } _{ }^{ }POL(+(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ }
+'(I(x), I(y)) > +'(x, y)
+'(I(x), I(y)) > +'(+(x, y), I(0))
+'(I(x), O(y)) > +'(x, y)
+'(O(x), I(y)) > +'(x, y)
+(I(x), I(y)) > O(+(+(x, y), I(0)))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 6
↳MRR
...
→DP Problem 7
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
+'(x, +(y, z)) > +'(x, y)
+'(x, +(y, z)) > +'(+(x, y), z)
+'(O(x), O(y)) > +'(x, y)
+(I(x), O(y)) > I(+(x, y))
+(x, 0) > x
+(0, x) > x
+(O(x), O(y)) > O(+(x, y))
+(x, +(y, z)) > +(+(x, y), z)
+(O(x), I(y)) > I(+(x, y))
O(0) > 0
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(I(x), O(y)) > I(+(x, y))
+(x, 0) > x
+(0, x) > x
+(O(x), O(y)) > O(+(x, y))
+(x, +(y, z)) > +(+(x, y), z)
O(0) > 0
+(O(x), I(y)) > I(+(x, y))
_{ }^{ }POL(I(x_{1})) = x_{1}_{ }^{ } _{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(O(x_{1})) = 1 + x_{1}_{ }^{ } _{ }^{ }POL(+(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ }
+'(O(x), O(y)) > +'(x, y)
+(I(x), O(y)) > I(+(x, y))
+(O(x), O(y)) > O(+(x, y))
O(0) > 0
+(O(x), I(y)) > I(+(x, y))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 6
↳MRR
...
→DP Problem 8
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
+'(x, +(y, z)) > +'(x, y)
+'(x, +(y, z)) > +'(+(x, y), z)
+(x, 0) > x
+(0, x) > x
+(x, +(y, z)) > +(+(x, y), z)
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(x, 0) > x
+(0, x) > x
+(x, +(y, z)) > +(+(x, y), z)
_{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(+(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ }
+(x, 0) > x
+(0, x) > x
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 6
↳MRR
...
→DP Problem 9
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
+'(x, +(y, z)) > +'(x, y)
+'(x, +(y, z)) > +'(+(x, y), z)
+(x, +(y, z)) > +(+(x, y), z)
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(x, +(y, z)) > +(+(x, y), z)
_{ }^{ }POL(+(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ }
+'(x, +(y, z)) > +'(x, y)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 6
↳MRR
...
→DP Problem 10
↳Dependency Graph
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
+'(x, +(y, z)) > +'(+(x, y), z)
+(x, +(y, z)) > +(+(x, y), z)
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
'(I(x), I(y)) > '(x, y)
'(I(x), O(y)) > '(x, y)
'(O(x), I(y)) > '(x, y)
'(O(x), I(y)) > '((x, y), I(1))
'(O(x), O(y)) > '(x, y)
O(0) > 0
+(0, x) > x
+(x, 0) > x
+(O(x), O(y)) > O(+(x, y))
+(O(x), I(y)) > I(+(x, y))
+(I(x), O(y)) > I(+(x, y))
+(I(x), I(y)) > O(+(+(x, y), I(0)))
+(x, +(y, z)) > +(+(x, y), z)
(x, 0) > x
(0, x) > 0
(O(x), O(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(I(x), O(y)) > I((x, y))
(I(x), I(y)) > O((x, y))
not(true) > false
not(false) > true
and(x, true) > x
and(x, false) > false
if(true, x, y) > x
if(false, x, y) > y
ge(O(x), O(y)) > ge(x, y)
ge(O(x), I(y)) > not(ge(y, x))
ge(I(x), O(y)) > ge(x, y)
ge(I(x), I(y)) > ge(x, y)
ge(x, 0) > true
ge(0, O(x)) > ge(0, x)
ge(0, I(x)) > false
Log'(0) > 0
Log'(I(x)) > +(Log'(x), I(0))
Log'(O(x)) > if(ge(x, I(0)), +(Log'(x), I(0)), 0)
Log(x) > (Log'(x), I(0))
Val(L(x)) > x
Val(N(x, l, r)) > x
Min(L(x)) > x
Min(N(x, l, r)) > Min(l)
Max(L(x)) > x
Max(N(x, l, r)) > Max(r)
BS(L(x)) > true
BS(N(x, l, r)) > and(and(ge(x, Max(l)), ge(Min(r), x)), and(BS(l), BS(r)))
Size(L(x)) > I(0)
Size(N(x, l, r)) > +(+(Size(l), Size(r)), I(1))
WB(L(x)) > true
WB(N(x, l, r)) > and(if(ge(Size(l), Size(r)), ge(I(0), (Size(l), Size(r))), ge(I(0), (Size(r), Size(l)))), and(WB(l), WB(r)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 11
↳Modular Removal of Rules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
'(I(x), I(y)) > '(x, y)
'(I(x), O(y)) > '(x, y)
'(O(x), I(y)) > '(x, y)
'(O(x), I(y)) > '((x, y), I(1))
'(O(x), O(y)) > '(x, y)
(I(x), O(y)) > I((x, y))
(x, 0) > x
(I(x), I(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(0, x) > 0
(O(x), O(y)) > O((x, y))
O(0) > 0
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
(I(x), O(y)) > I((x, y))
(x, 0) > x
(I(x), I(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(0, x) > 0
(O(x), O(y)) > O((x, y))
O(0) > 0
_{ }^{ }POL(I(x_{1})) = x_{1}_{ }^{ } _{ }^{ }POL('(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(0) = 1_{ }^{ } _{ }^{ }POL(1) = 0_{ }^{ } _{ }^{ }POL(O(x_{1})) = x_{1}_{ }^{ } _{ }^{ }POL((x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ }
(x, 0) > x
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 11
↳MRR
...
→DP Problem 12
↳Modular Removal of Rules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
'(I(x), I(y)) > '(x, y)
'(I(x), O(y)) > '(x, y)
'(O(x), I(y)) > '(x, y)
'(O(x), I(y)) > '((x, y), I(1))
'(O(x), O(y)) > '(x, y)
(I(x), O(y)) > I((x, y))
(I(x), I(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(0, x) > 0
(O(x), O(y)) > O((x, y))
O(0) > 0
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
(I(x), O(y)) > I((x, y))
(I(x), I(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
O(0) > 0
(0, x) > 0
(O(x), O(y)) > O((x, y))
_{ }^{ }POL(I(x_{1})) = 1 + x_{1}_{ }^{ } _{ }^{ }POL('(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(1) = 0_{ }^{ } _{ }^{ }POL(O(x_{1})) = 1 + x_{1}_{ }^{ } _{ }^{ }POL((x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ }
'(I(x), I(y)) > '(x, y)
'(I(x), O(y)) > '(x, y)
'(O(x), I(y)) > '(x, y)
'(O(x), I(y)) > '((x, y), I(1))
'(O(x), O(y)) > '(x, y)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
GE(0, O(x)) > GE(0, x)
O(0) > 0
+(0, x) > x
+(x, 0) > x
+(O(x), O(y)) > O(+(x, y))
+(O(x), I(y)) > I(+(x, y))
+(I(x), O(y)) > I(+(x, y))
+(I(x), I(y)) > O(+(+(x, y), I(0)))
+(x, +(y, z)) > +(+(x, y), z)
(x, 0) > x
(0, x) > 0
(O(x), O(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(I(x), O(y)) > I((x, y))
(I(x), I(y)) > O((x, y))
not(true) > false
not(false) > true
and(x, true) > x
and(x, false) > false
if(true, x, y) > x
if(false, x, y) > y
ge(O(x), O(y)) > ge(x, y)
ge(O(x), I(y)) > not(ge(y, x))
ge(I(x), O(y)) > ge(x, y)
ge(I(x), I(y)) > ge(x, y)
ge(x, 0) > true
ge(0, O(x)) > ge(0, x)
ge(0, I(x)) > false
Log'(0) > 0
Log'(I(x)) > +(Log'(x), I(0))
Log'(O(x)) > if(ge(x, I(0)), +(Log'(x), I(0)), 0)
Log(x) > (Log'(x), I(0))
Val(L(x)) > x
Val(N(x, l, r)) > x
Min(L(x)) > x
Min(N(x, l, r)) > Min(l)
Max(L(x)) > x
Max(N(x, l, r)) > Max(r)
BS(L(x)) > true
BS(N(x, l, r)) > and(and(ge(x, Max(l)), ge(Min(r), x)), and(BS(l), BS(r)))
Size(L(x)) > I(0)
Size(N(x, l, r)) > +(+(Size(l), Size(r)), I(1))
WB(L(x)) > true
WB(N(x, l, r)) > and(if(ge(Size(l), Size(r)), ge(I(0), (Size(l), Size(r))), ge(I(0), (Size(r), Size(l)))), and(WB(l), WB(r)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 13
↳SizeChange Principle
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
GE(0, O(x)) > GE(0, x)
none
innermost


trivial
O(x_{1}) > O(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳Usable Rules (Innermost)
→DP Problem 5
↳UsableRules
GE(I(x), I(y)) > GE(x, y)
GE(I(x), O(y)) > GE(x, y)
GE(O(x), I(y)) > GE(y, x)
GE(O(x), O(y)) > GE(x, y)
O(0) > 0
+(0, x) > x
+(x, 0) > x
+(O(x), O(y)) > O(+(x, y))
+(O(x), I(y)) > I(+(x, y))
+(I(x), O(y)) > I(+(x, y))
+(I(x), I(y)) > O(+(+(x, y), I(0)))
+(x, +(y, z)) > +(+(x, y), z)
(x, 0) > x
(0, x) > 0
(O(x), O(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(I(x), O(y)) > I((x, y))
(I(x), I(y)) > O((x, y))
not(true) > false
not(false) > true
and(x, true) > x
and(x, false) > false
if(true, x, y) > x
if(false, x, y) > y
ge(O(x), O(y)) > ge(x, y)
ge(O(x), I(y)) > not(ge(y, x))
ge(I(x), O(y)) > ge(x, y)
ge(I(x), I(y)) > ge(x, y)
ge(x, 0) > true
ge(0, O(x)) > ge(0, x)
ge(0, I(x)) > false
Log'(0) > 0
Log'(I(x)) > +(Log'(x), I(0))
Log'(O(x)) > if(ge(x, I(0)), +(Log'(x), I(0)), 0)
Log(x) > (Log'(x), I(0))
Val(L(x)) > x
Val(N(x, l, r)) > x
Min(L(x)) > x
Min(N(x, l, r)) > Min(l)
Max(L(x)) > x
Max(N(x, l, r)) > Max(r)
BS(L(x)) > true
BS(N(x, l, r)) > and(and(ge(x, Max(l)), ge(Min(r), x)), and(BS(l), BS(r)))
Size(L(x)) > I(0)
Size(N(x, l, r)) > +(+(Size(l), Size(r)), I(1))
WB(L(x)) > true
WB(N(x, l, r)) > and(if(ge(Size(l), Size(r)), ge(I(0), (Size(l), Size(r))), ge(I(0), (Size(r), Size(l)))), and(WB(l), WB(r)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 14
↳SizeChange Principle
→DP Problem 5
↳UsableRules
GE(I(x), I(y)) > GE(x, y)
GE(I(x), O(y)) > GE(x, y)
GE(O(x), I(y)) > GE(y, x)
GE(O(x), O(y)) > GE(x, y)
none
innermost



trivial
I(x_{1}) > I(x_{1})
O(x_{1}) > O(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳Usable Rules (Innermost)
LOG'(O(x)) > LOG'(x)
LOG'(I(x)) > LOG'(x)
O(0) > 0
+(0, x) > x
+(x, 0) > x
+(O(x), O(y)) > O(+(x, y))
+(O(x), I(y)) > I(+(x, y))
+(I(x), O(y)) > I(+(x, y))
+(I(x), I(y)) > O(+(+(x, y), I(0)))
+(x, +(y, z)) > +(+(x, y), z)
(x, 0) > x
(0, x) > 0
(O(x), O(y)) > O((x, y))
(O(x), I(y)) > I(((x, y), I(1)))
(I(x), O(y)) > I((x, y))
(I(x), I(y)) > O((x, y))
not(true) > false
not(false) > true
and(x, true) > x
and(x, false) > false
if(true, x, y) > x
if(false, x, y) > y
ge(O(x), O(y)) > ge(x, y)
ge(O(x), I(y)) > not(ge(y, x))
ge(I(x), O(y)) > ge(x, y)
ge(I(x), I(y)) > ge(x, y)
ge(x, 0) > true
ge(0, O(x)) > ge(0, x)
ge(0, I(x)) > false
Log'(0) > 0
Log'(I(x)) > +(Log'(x), I(0))
Log'(O(x)) > if(ge(x, I(0)), +(Log'(x), I(0)), 0)
Log(x) > (Log'(x), I(0))
Val(L(x)) > x
Val(N(x, l, r)) > x
Min(L(x)) > x
Min(N(x, l, r)) > Min(l)
Max(L(x)) > x
Max(N(x, l, r)) > Max(r)
BS(L(x)) > true
BS(N(x, l, r)) > and(and(ge(x, Max(l)), ge(Min(r), x)), and(BS(l), BS(r)))
Size(L(x)) > I(0)
Size(N(x, l, r)) > +(+(Size(l), Size(r)), I(1))
WB(L(x)) > true
WB(N(x, l, r)) > and(if(ge(Size(l), Size(r)), ge(I(0), (Size(l), Size(r))), ge(I(0), (Size(r), Size(l)))), and(WB(l), WB(r)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 15
↳SizeChange Principle
LOG'(O(x)) > LOG'(x)
LOG'(I(x)) > LOG'(x)
none
innermost


trivial
I(x_{1}) > I(x_{1})
O(x_{1}) > O(x_{1})