0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPOrderProof (⇔)
↳20 QDP
↳21 DependencyGraphProof (⇔)
↳22 TRUE
↳23 QDP
↳24 UsableRulesProof (⇔)
↳25 QDP
↳26 QReductionProof (⇔)
↳27 QDP
↳28 QDPOrderProof (⇔)
↳29 QDP
↳30 DependencyGraphProof (⇔)
↳31 TRUE
↳32 QDP
↳33 UsableRulesProof (⇔)
↳34 QDP
↳35 QReductionProof (⇔)
↳36 QDP
↳37 Instantiation (⇔)
↳38 QDP
↳39 Rewriting (⇔)
↳40 QDP
↳41 Instantiation (⇔)
↳42 QDP
↳43 Narrowing (⇔)
↳44 QDP
↳45 DependencyGraphProof (⇔)
↳46 QDP
↳47 Rewriting (⇔)
↳48 QDP
↳49 UsableRulesProof (⇔)
↳50 QDP
↳51 Instantiation (⇔)
↳52 QDP
↳53 Instantiation (⇔)
↳54 QDP
↳55 UsableRulesProof (⇔)
↳56 QDP
↳57 Rewriting (⇔)
↳58 QDP
↳59 Rewriting (⇔)
↳60 QDP
↳61 UsableRulesProof (⇔)
↳62 QDP
↳63 QReductionProof (⇔)
↳64 QDP
↳65 ForwardInstantiation (⇔)
↳66 QDP
↳67 Narrowing (⇔)
↳68 QDP
↳69 DependencyGraphProof (⇔)
↳70 QDP
↳71 UsableRulesProof (⇔)
↳72 QDP
↳73 QReductionProof (⇔)
↳74 QDP
↳75 Narrowing (⇔)
↳76 QDP
↳77 DependencyGraphProof (⇔)
↳78 QDP
↳79 UsableRulesProof (⇔)
↳80 QDP
↳81 QReductionProof (⇔)
↳82 QDP
↳83 Rewriting (⇔)
↳84 QDP
↳85 UsableRulesProof (⇔)
↳86 QDP
↳87 QReductionProof (⇔)
↳88 QDP
↳89 Instantiation (⇔)
↳90 QDP
↳91 QDPOrderProof (⇔)
↳92 QDP
↳93 DependencyGraphProof (⇔)
↳94 TRUE
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
PLUS(x, y) → IFPLUS(isZero(x), x, y)
PLUS(x, y) → ISZERO(x)
IFPLUS(false, x, y) → PLUS(p(x), y)
IFPLUS(false, x, y) → P(x)
TIMES(x, y) → IFTIMES(isZero(x), x, y)
TIMES(x, y) → ISZERO(x)
IFTIMES(false, x, y) → PLUS(y, times(p(x), y))
IFTIMES(false, x, y) → TIMES(p(x), y)
IFTIMES(false, x, y) → P(x)
SHORTER(cons(x, l), s(y)) → SHORTER(l, y)
PROD(l) → IF(shorter(l, 0), shorter(l, s(0)), l)
PROD(l) → SHORTER(l, 0)
PROD(l) → SHORTER(l, s(0))
IF(false, b, l) → IF2(b, l)
IF2(true, l) → CAR(l)
IF2(false, l) → PROD(cons(times(car(l), cadr(l)), cddr(l)))
IF2(false, l) → TIMES(car(l), cadr(l))
IF2(false, l) → CAR(l)
IF2(false, l) → CADR(l)
IF2(false, l) → CDDR(l)
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
SHORTER(cons(x, l), s(y)) → SHORTER(l, y)
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
SHORTER(cons(x, l), s(y)) → SHORTER(l, y)
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
SHORTER(cons(x, l), s(y)) → SHORTER(l, y)
From the DPs we obtained the following set of size-change graphs:
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(x, y) → IFPLUS(isZero(x), x, y)
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(x, y) → IFPLUS(isZero(x), x, y)
isZero(0) → true
isZero(s(x)) → false
p(s(x)) → x
p(0) → 0
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
IFPLUS(false, x, y) → PLUS(p(x), y)
PLUS(x, y) → IFPLUS(isZero(x), x, y)
isZero(0) → true
isZero(s(x)) → false
p(s(x)) → x
p(0) → 0
isZero(0)
isZero(s(x0))
p(s(x0))
p(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFPLUS(false, x, y) → PLUS(p(x), y)
The value of delta used in the strict ordering is 3/8.
POL(IFPLUS(x1, x2, x3)) = 1 + (3/2)x1 + (1/4)x2
POL(false) = 1/4
POL(PLUS(x1, x2)) = 1 + x1
POL(p(x1)) = (1/4)x1
POL(isZero(x1)) = (1/2)x1
POL(s(x1)) = 3 + (4)x1
POL(0) = 0
POL(true) = 0
isZero(s(x)) → false
isZero(0) → true
p(0) → 0
p(s(x)) → x
PLUS(x, y) → IFPLUS(isZero(x), x, y)
isZero(0) → true
isZero(s(x)) → false
p(s(x)) → x
p(0) → 0
isZero(0)
isZero(s(x0))
p(s(x0))
p(0)
IFTIMES(false, x, y) → TIMES(p(x), y)
TIMES(x, y) → IFTIMES(isZero(x), x, y)
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
IFTIMES(false, x, y) → TIMES(p(x), y)
TIMES(x, y) → IFTIMES(isZero(x), x, y)
isZero(0) → true
isZero(s(x)) → false
p(s(x)) → x
p(0) → 0
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
IFTIMES(false, x, y) → TIMES(p(x), y)
TIMES(x, y) → IFTIMES(isZero(x), x, y)
isZero(0) → true
isZero(s(x)) → false
p(s(x)) → x
p(0) → 0
isZero(0)
isZero(s(x0))
p(s(x0))
p(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(x, y) → IFTIMES(isZero(x), x, y)
The value of delta used in the strict ordering is 7/8.
POL(IFTIMES(x1, x2, x3)) = (1/2)x1 + (1/2)x2
POL(false) = 2
POL(TIMES(x1, x2)) = 1 + x1
POL(p(x1)) = (1/2)x1
POL(isZero(x1)) = 1/4 + (1/2)x1
POL(0) = 0
POL(s(x1)) = 4 + (4)x1
POL(true) = 1/4
p(0) → 0
p(s(x)) → x
isZero(s(x)) → false
isZero(0) → true
IFTIMES(false, x, y) → TIMES(p(x), y)
isZero(0) → true
isZero(s(x)) → false
p(s(x)) → x
p(0) → 0
isZero(0)
isZero(s(x0))
p(s(x0))
p(0)
IF2(false, l) → PROD(cons(times(car(l), cadr(l)), cddr(l)))
PROD(l) → IF(shorter(l, 0), shorter(l, s(0)), l)
IF(false, b, l) → IF2(b, l)
car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
IF2(false, l) → PROD(cons(times(car(l), cadr(l)), cddr(l)))
PROD(l) → IF(shorter(l, 0), shorter(l, s(0)), l)
IF(false, b, l) → IF2(b, l)
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
prod(x0)
if(true, x0, x1)
if(false, x0, x1)
if2(true, x0)
if2(false, x0)
IF2(false, l) → PROD(cons(times(car(l), cadr(l)), cddr(l)))
PROD(l) → IF(shorter(l, 0), shorter(l, s(0)), l)
IF(false, b, l) → IF2(b, l)
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(y_2, y_3)) → IF(shorter(cons(y_2, y_3), 0), shorter(cons(y_2, y_3), s(0)), cons(y_2, y_3))
IF2(false, l) → PROD(cons(times(car(l), cadr(l)), cddr(l)))
IF(false, b, l) → IF2(b, l)
PROD(cons(y_2, y_3)) → IF(shorter(cons(y_2, y_3), 0), shorter(cons(y_2, y_3), s(0)), cons(y_2, y_3))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
PROD(l) → IF(shorter(l, 0), shorter(l, s(0)), l)
IF(false, b, l) → IF2(b, l)
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(y_4, y_5)) → IF(shorter(cons(y_4, y_5), 0), shorter(cons(y_4, y_5), s(0)), cons(y_4, y_5))
IF(false, b, l) → IF2(b, l)
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
PROD(cons(y_4, y_5)) → IF(shorter(cons(y_4, y_5), 0), shorter(cons(y_4, y_5), s(0)), cons(y_4, y_5))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(nil) → IF(true, shorter(nil, s(0)), nil)
PROD(cons(x0, x1)) → IF(false, shorter(cons(x0, x1), s(0)), cons(x0, x1))
IF(false, b, l) → IF2(b, l)
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
PROD(nil) → IF(true, shorter(nil, s(0)), nil)
PROD(cons(x0, x1)) → IF(false, shorter(cons(x0, x1), s(0)), cons(x0, x1))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
PROD(cons(x0, x1)) → IF(false, shorter(cons(x0, x1), s(0)), cons(x0, x1))
IF(false, b, l) → IF2(b, l)
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
IF(false, b, l) → IF2(b, l)
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
car(cons(x, l)) → x
cadr(cons(x, cons(y, l))) → y
times(x, y) → iftimes(isZero(x), x, y)
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
IF(false, b, l) → IF2(b, l)
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
car(cons(x, l)) → x
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
IF2(false, l) → PROD(cons(iftimes(isZero(car(l)), car(l), cadr(l)), cddr(l)))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
car(cons(x, l)) → x
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(car(cons(z1, z2))), car(cons(z1, z2)), cadr(cons(z1, z2))), cddr(cons(z1, z2))))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(car(cons(z1, z2))), car(cons(z1, z2)), cadr(cons(z1, z2))), cddr(cons(z1, z2))))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
car(cons(x, l)) → x
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(car(cons(z1, z2))), car(cons(z1, z2)), cadr(cons(z1, z2))), cddr(cons(z1, z2))))
car(cons(x, l)) → x
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), car(cons(z1, z2)), cadr(cons(z1, z2))), cddr(cons(z1, z2))))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), car(cons(z1, z2)), cadr(cons(z1, z2))), cddr(cons(z1, z2))))
car(cons(x, l)) → x
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
car(cons(x, l)) → x
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
car(cons(x0, x1))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
car(cons(x0, x1))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF(false, y_0, cons(z0, z1)) → IF2(y_0, cons(z0, z1))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
PROD(cons(x0, x1)) → IF(false, shorter(x1, 0), cons(x0, x1))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(y0, nil)) → IF(false, true, cons(y0, nil))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
PROD(cons(y0, nil)) → IF(false, true, cons(y0, nil))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
shorter(nil, x0)
shorter(cons(x0, x1), 0)
shorter(cons(x0, x1), s(x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
IF2(false, cons(z1, z2)) → PROD(cons(iftimes(isZero(z1), z1, cadr(cons(z1, z2))), cddr(cons(z1, z2))))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
IF2(false, cons(x0, nil)) → PROD(cons(iftimes(isZero(x0), x0, cadr(cons(x0, nil))), nil))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, cadr(cons(x0, cons(x1, x2)))), x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
IF2(false, cons(x0, nil)) → PROD(cons(iftimes(isZero(x0), x0, cadr(cons(x0, nil))), nil))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, cadr(cons(x0, cons(x1, x2)))), x2))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, cadr(cons(x0, cons(x1, x2)))), x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, cadr(cons(x0, cons(x1, x2)))), x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
cddr(nil)
cddr(cons(x0, nil))
cddr(cons(x0, cons(x1, x2)))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, cadr(cons(x0, cons(x1, x2)))), x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, x1), x2))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, x1), x2))
isZero(0) → true
isZero(s(x)) → false
cadr(cons(x, cons(y, l))) → y
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, x1), x2))
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
cadr(cons(x0, cons(x1, x2)))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
cadr(cons(x0, cons(x1, x2)))
IF(false, false, cons(x1, x2)) → IF2(false, cons(x1, x2))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, x1), x2))
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
IF(false, false, cons(z0, cons(z1, z2))) → IF2(false, cons(z0, cons(z1, z2)))
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, x1), x2))
IF(false, false, cons(z0, cons(z1, z2))) → IF2(false, cons(z0, cons(z1, z2)))
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF2(false, cons(x0, cons(x1, x2))) → PROD(cons(iftimes(isZero(x0), x0, x1), x2))
POL(0) = 0
POL(IF(x1, x2, x3)) = 1 + x3
POL(IF2(x1, x2)) = 1 + x2
POL(PROD(x1)) = 1 + x1
POL(cons(x1, x2)) = 1 + x2
POL(false) = 0
POL(ifplus(x1, x2, x3)) = 0
POL(iftimes(x1, x2, x3)) = 0
POL(isZero(x1)) = 0
POL(p(x1)) = 0
POL(plus(x1, x2)) = 0
POL(s(x1)) = 0
POL(times(x1, x2)) = 0
POL(true) = 0
PROD(cons(y0, cons(x0, x1))) → IF(false, false, cons(y0, cons(x0, x1)))
IF(false, false, cons(z0, cons(z1, z2))) → IF2(false, cons(z0, cons(z1, z2)))
isZero(0) → true
isZero(s(x)) → false
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
times(x, y) → iftimes(isZero(x), x, y)
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
isZero(0)
isZero(s(x0))
plus(x0, x1)
ifplus(true, x0, x1)
ifplus(false, x0, x1)
times(x0, x1)
iftimes(true, x0, x1)
iftimes(false, x0, x1)
p(s(x0))
p(0)