YES
0 QTRS
↳1 QTRSRRRProof (⇔, 71 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 19 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 QDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QDPSizeChangeProof (⇔, 0 ms)
↳18 YES
↳19 QDP
↳20 UsableRulesProof (⇔, 0 ms)
↳21 QDP
↳22 MRRProof (⇔, 0 ms)
↳23 QDP
↳24 PisEmptyProof (⇔, 0 ms)
↳25 YES
↳26 QDP
↳27 UsableRulesProof (⇔, 0 ms)
↳28 QDP
↳29 MRRProof (⇔, 0 ms)
↳30 QDP
↳31 PisEmptyProof (⇔, 0 ms)
↳32 YES
↳33 QDP
↳34 UsableRulesProof (⇔, 0 ms)
↳35 QDP
↳36 QDPSizeChangeProof (⇔, 0 ms)
↳37 YES
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(#)), #)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(#) = 0
POL(+(x1, x2)) = x1 + x2
POL(-(x1, x2)) = x1 + x2
POL(0(x1)) = 2·x1
POL(1(x1)) = 2·x1
POL(false) = 0
POL(ge(x1, x2)) = 2·x1 + x2
POL(if(x1, x2, x3)) = x1 + x2 + x3
POL(log(x1)) = 1 + 2·x1
POL(log'(x1)) = 1 + 2·x1
POL(not(x1)) = x1
POL(true) = 0
log'(#) → #
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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(#) = 0
POL(+(x1, x2)) = x1 + x2
POL(-(x1, x2)) = x1 + x2
POL(0(x1)) = 2·x1
POL(1(x1)) = 2·x1
POL(false) = 0
POL(ge(x1, x2)) = x1 + x2
POL(if(x1, x2, x3)) = 2·x1 + x2 + x3
POL(log(x1)) = 2 + 2·x1
POL(log'(x1)) = 1 + 2·x1
POL(not(x1)) = 2·x1
POL(true) = 0
log(x) → -(log'(x), 1(#))
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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
+1(0(x), 0(y)) → 01(+(x, y))
+1(0(x), 0(y)) → +1(x, y)
+1(0(x), 1(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → 01(+(+(x, y), 1(#)))
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)
-1(0(x), 0(y)) → 01(-(x, y))
-1(0(x), 0(y)) → -1(x, y)
-1(0(x), 1(y)) → -1(-(x, y), 1(#))
-1(0(x), 1(y)) → -1(x, y)
-1(1(x), 0(y)) → -1(x, y)
-1(1(x), 1(y)) → 01(-(x, y))
-1(1(x), 1(y)) → -1(x, y)
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), 0(y)) → GE(x, y)
GE(1(x), 1(y)) → GE(x, y)
GE(#, 0(x)) → GE(#, x)
LOG'(1(x)) → +1(log'(x), 1(#))
LOG'(1(x)) → LOG'(x)
LOG'(0(x)) → IF(ge(x, 1(#)), +(log'(x), 1(#)), #)
LOG'(0(x)) → GE(x, 1(#))
LOG'(0(x)) → +1(log'(x), 1(#))
LOG'(0(x)) → LOG'(x)
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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
GE(#, 0(x)) → GE(#, x)
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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
GE(#, 0(x)) → GE(#, x)
From the DPs we obtained the following set of size-change graphs:
GE(0(x), 1(y)) → GE(y, x)
GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)
GE(1(x), 1(y)) → GE(x, y)
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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
GE(0(x), 1(y)) → GE(y, x)
GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)
GE(1(x), 1(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
-1(0(x), 1(y)) → -1(-(x, y), 1(#))
-1(0(x), 1(y)) → -1(x, y)
-1(0(x), 0(y)) → -1(x, y)
-1(1(x), 0(y)) → -1(x, y)
-1(1(x), 1(y)) → -1(x, y)
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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
-1(0(x), 1(y)) → -1(-(x, y), 1(#))
-1(0(x), 1(y)) → -1(x, y)
-1(0(x), 0(y)) → -1(x, y)
-1(1(x), 0(y)) → -1(x, y)
-1(1(x), 1(y)) → -1(x, y)
-(#, 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))
0(#) → #
-1(0(x), 1(y)) → -1(-(x, y), 1(#))
-1(0(x), 1(y)) → -1(x, y)
-1(0(x), 0(y)) → -1(x, y)
-1(1(x), 0(y)) → -1(x, y)
-1(1(x), 1(y)) → -1(x, y)
-(#, 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))
0(#) → #
-2 > -^12 > 01 > 11 > #
#=2
0_1=5
1_1=3
-_2=0
-^1_2=0
+1(0(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
+1(0(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)
+(#, 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))
0(#) → #
+1(0(x), 1(y)) → +1(x, y)
+1(0(x), 0(y)) → +1(x, y)
+1(1(x), 0(y)) → +1(x, y)
+1(1(x), 1(y)) → +1(+(x, y), 1(#))
+1(1(x), 1(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)
+(#, 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))
0(#) → #
# > +2 > 11 > 01 > +^12
#=2
0_1=1
1_1=3
+_2=0
+^1_2=0
LOG'(0(x)) → LOG'(x)
LOG'(1(x)) → LOG'(x)
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'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
LOG'(0(x)) → LOG'(x)
LOG'(1(x)) → LOG'(x)
From the DPs we obtained the following set of size-change graphs: