WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 3881 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 1063 ms] (6) BEST (7) proven lower bound (8) LowerBoundPropagationProof [FINISHED, 0 ms] (9) BOUNDS(n^1, INF) (10) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #ABS(#0) -> c85 #ABS(#neg(z0)) -> c86 #ABS(#pos(z0)) -> c87 #ABS(#s(z0)) -> c88 #EQUAL(z0, z1) -> c89(#EQ'(z0, z1)) #GREATER(z0, z1) -> c90(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) #LESS(z0, z1) -> c91(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) *'(z0, z1) -> c92(#MULT(z0, z1)) +'(z0, z1) -> c93(#ADD(z0, z1)) -'(z0, z1) -> c94(#SUB(z0, z1)) ADD(z0, z1) -> c95(ADD'(z0, z1, #abs(#0)), #ABS(#0)) ADD'(z0, z1, z2) -> c96(ADD'#1(z0, z1, z2)) ADD'#1(::(z0, z1), z2, z3) -> c97(ADD'#2(z2, z3, z0, z1)) ADD'#1(nil, z0, z1) -> c98 ADD'#2(::(z0, z1), z2, z3, z4) -> c99(ADD'#3(sum(z3, z0, z2), z4, z1), SUM(z3, z0, z2)) ADD'#2(nil, z0, z1, z2) -> c100 ADD'#3(tuple#2(z0, z1), z2, z3) -> c101(ADD'(z2, z3, z1)) BITTOINT(z0) -> c102(BITTOINT'(z0, #abs(#pos(#s(#0)))), #ABS(#pos(#s(#0)))) BITTOINT'(z0, z1) -> c103(BITTOINT'#1(z0, z1)) BITTOINT'#1(::(z0, z1), z2) -> c104(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), *'(z0, z2)) BITTOINT'#1(::(z0, z1), z2) -> c105(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), BITTOINT'(z1, *(z2, #pos(#s(#s(#0))))), *'(z2, #pos(#s(#s(#0))))) BITTOINT'#1(nil, z0) -> c106(#ABS(#0)) COMPARE(z0, z1) -> c107(COMPARE#1(z0, z1)) COMPARE#1(::(z0, z1), z2) -> c108(COMPARE#2(z2, z0, z1)) COMPARE#1(nil, z0) -> c109(#ABS(#0)) COMPARE#2(::(z0, z1), z2, z3) -> c110(COMPARE#3(compare(z3, z1), z2, z0), COMPARE(z3, z1)) COMPARE#2(nil, z0, z1) -> c111(#ABS(#0)) COMPARE#3(z0, z1, z2) -> c112(COMPARE#4(#equal(z0, #0), z0, z1, z2), #EQUAL(z0, #0)) COMPARE#4(#false, z0, z1, z2) -> c113 COMPARE#4(#true, z0, z1, z2) -> c114(COMPARE#5(#less(z1, z2), z1, z2), #LESS(z1, z2)) COMPARE#5(#false, z0, z1) -> c115(COMPARE#6(#greater(z0, z1)), #GREATER(z0, z1)) COMPARE#5(#true, z0, z1) -> c116(-'(#0, #pos(#s(#0)))) COMPARE#6(#false) -> c117(#ABS(#0)) COMPARE#6(#true) -> c118(#ABS(#pos(#s(#0)))) DIFF(z0, z1, z2) -> c119(MOD(+(+(z0, z1), z2), #pos(#s(#s(#0)))), +'(+(z0, z1), z2), +'(z0, z1)) DIFF(z0, z1, z2) -> c120(DIFF#1(#less(-(-(z0, z1), z2), #0)), #LESS(-(-(z0, z1), z2), #0), -'(-(z0, z1), z2), -'(z0, z1)) DIFF#1(#false) -> c121(#ABS(#0)) DIFF#1(#true) -> c122(#ABS(#pos(#s(#0)))) DIV(z0, z1) -> c123(#DIV(z0, z1)) LEQ(z0, z1) -> c124(#LESS(compare(z0, z1), #pos(#s(#0))), COMPARE(z0, z1)) MOD(z0, z1) -> c125(-'(z0, *(z0, div(z0, z1))), *'(z0, div(z0, z1)), DIV(z0, z1)) MULT(z0, z1) -> c126(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c127(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), #ABS(#0)) MULT#1(::(z0, z1), z2) -> c128(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), MULT(z1, z2)) MULT#1(nil, z0) -> c129 MULT#2(z0, z1, z2) -> c130(MULT#3(#equal(z2, #pos(#s(#0))), z1, z0), #EQUAL(z2, #pos(#s(#0)))) MULT#3(#false, z0, z1) -> c131 MULT#3(#true, z0, z1) -> c132(ADD(z0, z1)) MULT3(z0, z1, z2) -> c133(MULT(mult(z0, z1), z1), MULT(z0, z1)) SUB(z0, z1) -> c134(SUB#1(sub'(z0, z1, #abs(#0))), SUB'(z0, z1, #abs(#0)), #ABS(#0)) SUB#1(tuple#2(z0, z1)) -> c135 SUB'(z0, z1, z2) -> c136(SUB'#1(z0, z1, z2)) SUB'#1(::(z0, z1), z2, z3) -> c137(SUB'#2(z2, z3, z0, z1)) SUB'#1(nil, z0, z1) -> c138 SUB'#2(::(z0, z1), z2, z3, z4) -> c139(SUB'#3(diff(z3, z0, z2), z4, z1), DIFF(z3, z0, z2)) SUB'#2(nil, z0, z1, z2) -> c140 SUB'#3(tuple#2(z0, z1), z2, z3) -> c141(SUB'#4(sub'(z2, z3, z1), z0), SUB'(z2, z3, z1)) SUB'#4(tuple#2(z0, z1), z2) -> c142(SUB'#5(#equal(z1, #pos(#s(#0))), z2, z0), #EQUAL(z1, #pos(#s(#0)))) SUB'#5(#false, z0, z1) -> c143 SUB'#5(#true, z0, z1) -> c144(#ABS(#0)) SUM(z0, z1, z2) -> c145(SUM#1(+(+(z0, z1), z2)), +'(+(z0, z1), z2), +'(z0, z1)) SUM#1(z0) -> c146(SUM#2(#equal(z0, #0), z0), #EQUAL(z0, #0)) SUM#2(#false, z0) -> c147(SUM#3(#equal(z0, #pos(#s(#0))), z0), #EQUAL(z0, #pos(#s(#0)))) SUM#2(#true, z0) -> c148(#ABS(#0)) SUM#2(#true, z0) -> c149(#ABS(#0)) SUM#3(#false, z0) -> c150(SUM#4(#equal(z0, #pos(#s(#s(#0))))), #EQUAL(z0, #pos(#s(#s(#0))))) SUM#3(#true, z0) -> c151(#ABS(#pos(#s(#0)))) SUM#3(#true, z0) -> c152(#ABS(#0)) SUM#4(#false) -> c153(#ABS(#pos(#s(#0)))) SUM#4(#false) -> c154(#ABS(#pos(#s(#0)))) SUM#4(#true) -> c155(#ABS(#0)) SUM#4(#true) -> c156(#ABS(#pos(#s(#0)))) The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #AND(#false, #false) -> c5 #AND(#false, #true) -> c6 #AND(#true, #false) -> c7 #AND(#true, #true) -> c8 #CKGT(#EQ) -> c9 #CKGT(#GT) -> c10 #CKGT(#LT) -> c11 #CKLT(#EQ) -> c12 #CKLT(#GT) -> c13 #CKLT(#LT) -> c14 #COMPARE(#0, #0) -> c15 #COMPARE(#0, #neg(z0)) -> c16 #COMPARE(#0, #pos(z0)) -> c17 #COMPARE(#0, #s(z0)) -> c18 #COMPARE(#neg(z0), #0) -> c19 #COMPARE(#neg(z0), #neg(z1)) -> c20(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c21 #COMPARE(#pos(z0), #0) -> c22 #COMPARE(#pos(z0), #neg(z1)) -> c23 #COMPARE(#pos(z0), #pos(z1)) -> c24(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c25 #COMPARE(#s(z0), #s(z1)) -> c26(#COMPARE(z0, z1)) #DIV(#0, #0) -> c27 #DIV(#0, #neg(z0)) -> c28 #DIV(#0, #pos(z0)) -> c29 #DIV(#neg(z0), #0) -> c30 #DIV(#neg(z0), #neg(z1)) -> c31(#NATDIV(z0, z1)) #DIV(#neg(z0), #pos(z1)) -> c32(#NATDIV(z0, z1)) #DIV(#pos(z0), #0) -> c33 #DIV(#pos(z0), #neg(z1)) -> c34(#NATDIV(z0, z1)) #DIV(#pos(z0), #pos(z1)) -> c35(#NATDIV(z0, z1)) #EQ'(#0, #0) -> c36 #EQ'(#0, #neg(z0)) -> c37 #EQ'(#0, #pos(z0)) -> c38 #EQ'(#0, #s(z0)) -> c39 #EQ'(#neg(z0), #0) -> c40 #EQ'(#neg(z0), #neg(z1)) -> c41(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c42 #EQ'(#pos(z0), #0) -> c43 #EQ'(#pos(z0), #neg(z1)) -> c44 #EQ'(#pos(z0), #pos(z1)) -> c45(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c46 #EQ'(#s(z0), #s(z1)) -> c47(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c48(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c49(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c50 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c51 #EQ'(nil, ::(z0, z1)) -> c52 #EQ'(nil, nil) -> c53 #EQ'(nil, tuple#2(z0, z1)) -> c54 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c55 #EQ'(tuple#2(z0, z1), nil) -> c56 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c57(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c58(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #MULT(#0, #0) -> c59 #MULT(#0, #neg(z0)) -> c60 #MULT(#0, #pos(z0)) -> c61 #MULT(#neg(z0), #0) -> c62 #MULT(#neg(z0), #neg(z1)) -> c63(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c64(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c65 #MULT(#pos(z0), #neg(z1)) -> c66(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c67(#NATMULT(z0, z1)) #NATDIV(#0, #0) -> c68 #NATDIV(#s(z0), #s(z1)) -> c69(#NATDIV(#natsub(z0, z1), #s(z1)), #NATSUB(z0, z1)) #NATMULT(#0, z0) -> c70 #NATMULT(#s(z0), z1) -> c71(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #NATSUB(z0, #0) -> c72 #NATSUB(#s(z0), #s(z1)) -> c73(#NATSUB(z0, z1)) #PRED(#0) -> c74 #PRED(#neg(#s(z0))) -> c75 #PRED(#pos(#s(#0))) -> c76 #PRED(#pos(#s(#s(z0)))) -> c77 #SUB(z0, #0) -> c78 #SUB(z0, #neg(z1)) -> c79(#ADD(z0, #pos(z1))) #SUB(z0, #pos(z1)) -> c80(#ADD(z0, #neg(z1))) #SUCC(#0) -> c81 #SUCC(#neg(#s(#0))) -> c82 #SUCC(#neg(#s(#s(z0)))) -> c83 #SUCC(#pos(#s(z0))) -> c84 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(z0, z1) #div(#0, #0) -> #divByZero #div(#0, #neg(z0)) -> #0 #div(#0, #pos(z0)) -> #0 #div(#neg(z0), #0) -> #divByZero #div(#neg(z0), #neg(z1)) -> #pos(#natdiv(z0, z1)) #div(#neg(z0), #pos(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #0) -> #divByZero #div(#pos(z0), #neg(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #pos(z1)) -> #pos(#natdiv(z0, z1)) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natdiv(#0, #0) -> #divByZero #natdiv(#s(z0), #s(z1)) -> #s(#natdiv(#natsub(z0, z1), #s(z1))) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #natsub(z0, #0) -> z0 #natsub(#s(z0), #s(z1)) -> #natsub(z0, z1) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #sub(z0, #0) -> z0 #sub(z0, #neg(z1)) -> #add(z0, #pos(z1)) #sub(z0, #pos(z1)) -> #add(z0, #neg(z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) #less(z0, z1) -> #cklt(#compare(z0, z1)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) -(z0, z1) -> #sub(z0, z1) add(z0, z1) -> add'(z0, z1, #abs(#0)) add'(z0, z1, z2) -> add'#1(z0, z1, z2) add'#1(::(z0, z1), z2, z3) -> add'#2(z2, z3, z0, z1) add'#1(nil, z0, z1) -> nil add'#2(::(z0, z1), z2, z3, z4) -> add'#3(sum(z3, z0, z2), z4, z1) add'#2(nil, z0, z1, z2) -> nil add'#3(tuple#2(z0, z1), z2, z3) -> ::(z0, add'(z2, z3, z1)) bitToInt(z0) -> bitToInt'(z0, #abs(#pos(#s(#0)))) bitToInt'(z0, z1) -> bitToInt'#1(z0, z1) bitToInt'#1(::(z0, z1), z2) -> +(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))) bitToInt'#1(nil, z0) -> #abs(#0) compare(z0, z1) -> compare#1(z0, z1) compare#1(::(z0, z1), z2) -> compare#2(z2, z0, z1) compare#1(nil, z0) -> #abs(#0) compare#2(::(z0, z1), z2, z3) -> compare#3(compare(z3, z1), z2, z0) compare#2(nil, z0, z1) -> #abs(#0) compare#3(z0, z1, z2) -> compare#4(#equal(z0, #0), z0, z1, z2) compare#4(#false, z0, z1, z2) -> z0 compare#4(#true, z0, z1, z2) -> compare#5(#less(z1, z2), z1, z2) compare#5(#false, z0, z1) -> compare#6(#greater(z0, z1)) compare#5(#true, z0, z1) -> -(#0, #pos(#s(#0))) compare#6(#false) -> #abs(#0) compare#6(#true) -> #abs(#pos(#s(#0))) diff(z0, z1, z2) -> tuple#2(mod(+(+(z0, z1), z2), #pos(#s(#s(#0)))), diff#1(#less(-(-(z0, z1), z2), #0))) diff#1(#false) -> #abs(#0) diff#1(#true) -> #abs(#pos(#s(#0))) div(z0, z1) -> #div(z0, z1) leq(z0, z1) -> #less(compare(z0, z1), #pos(#s(#0))) mod(z0, z1) -> -(z0, *(z0, div(z0, z1))) mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(::(#abs(#0), mult(z1, z2)), z2, z0) mult#1(nil, z0) -> nil mult#2(z0, z1, z2) -> mult#3(#equal(z2, #pos(#s(#0))), z1, z0) mult#3(#false, z0, z1) -> z1 mult#3(#true, z0, z1) -> add(z0, z1) mult3(z0, z1, z2) -> mult(mult(z0, z1), z1) sub(z0, z1) -> sub#1(sub'(z0, z1, #abs(#0))) sub#1(tuple#2(z0, z1)) -> z0 sub'(z0, z1, z2) -> sub'#1(z0, z1, z2) sub'#1(::(z0, z1), z2, z3) -> sub'#2(z2, z3, z0, z1) sub'#1(nil, z0, z1) -> tuple#2(nil, z1) sub'#2(::(z0, z1), z2, z3, z4) -> sub'#3(diff(z3, z0, z2), z4, z1) sub'#2(nil, z0, z1, z2) -> tuple#2(nil, z0) sub'#3(tuple#2(z0, z1), z2, z3) -> sub'#4(sub'(z2, z3, z1), z0) sub'#4(tuple#2(z0, z1), z2) -> tuple#2(sub'#5(#equal(z1, #pos(#s(#0))), z2, z0), z1) sub'#5(#false, z0, z1) -> ::(z0, z1) sub'#5(#true, z0, z1) -> ::(#abs(#0), z1) sum(z0, z1, z2) -> sum#1(+(+(z0, z1), z2)) sum#1(z0) -> sum#2(#equal(z0, #0), z0) sum#2(#false, z0) -> sum#3(#equal(z0, #pos(#s(#0))), z0) sum#2(#true, z0) -> tuple#2(#abs(#0), #abs(#0)) sum#3(#false, z0) -> sum#4(#equal(z0, #pos(#s(#s(#0))))) sum#3(#true, z0) -> tuple#2(#abs(#pos(#s(#0))), #abs(#0)) sum#4(#false) -> tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0)))) sum#4(#true) -> tuple#2(#abs(#0), #abs(#pos(#s(#0)))) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #ABS(#0) -> c85 #ABS(#neg(z0)) -> c86 #ABS(#pos(z0)) -> c87 #ABS(#s(z0)) -> c88 #EQUAL(z0, z1) -> c89(#EQ'(z0, z1)) #GREATER(z0, z1) -> c90(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) #LESS(z0, z1) -> c91(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) *'(z0, z1) -> c92(#MULT(z0, z1)) +'(z0, z1) -> c93(#ADD(z0, z1)) -'(z0, z1) -> c94(#SUB(z0, z1)) ADD(z0, z1) -> c95(ADD'(z0, z1, #abs(#0)), #ABS(#0)) ADD'(z0, z1, z2) -> c96(ADD'#1(z0, z1, z2)) ADD'#1(::(z0, z1), z2, z3) -> c97(ADD'#2(z2, z3, z0, z1)) ADD'#1(nil, z0, z1) -> c98 ADD'#2(::(z0, z1), z2, z3, z4) -> c99(ADD'#3(sum(z3, z0, z2), z4, z1), SUM(z3, z0, z2)) ADD'#2(nil, z0, z1, z2) -> c100 ADD'#3(tuple#2(z0, z1), z2, z3) -> c101(ADD'(z2, z3, z1)) BITTOINT(z0) -> c102(BITTOINT'(z0, #abs(#pos(#s(#0)))), #ABS(#pos(#s(#0)))) BITTOINT'(z0, z1) -> c103(BITTOINT'#1(z0, z1)) BITTOINT'#1(::(z0, z1), z2) -> c104(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), *'(z0, z2)) BITTOINT'#1(::(z0, z1), z2) -> c105(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), BITTOINT'(z1, *(z2, #pos(#s(#s(#0))))), *'(z2, #pos(#s(#s(#0))))) BITTOINT'#1(nil, z0) -> c106(#ABS(#0)) COMPARE(z0, z1) -> c107(COMPARE#1(z0, z1)) COMPARE#1(::(z0, z1), z2) -> c108(COMPARE#2(z2, z0, z1)) COMPARE#1(nil, z0) -> c109(#ABS(#0)) COMPARE#2(::(z0, z1), z2, z3) -> c110(COMPARE#3(compare(z3, z1), z2, z0), COMPARE(z3, z1)) COMPARE#2(nil, z0, z1) -> c111(#ABS(#0)) COMPARE#3(z0, z1, z2) -> c112(COMPARE#4(#equal(z0, #0), z0, z1, z2), #EQUAL(z0, #0)) COMPARE#4(#false, z0, z1, z2) -> c113 COMPARE#4(#true, z0, z1, z2) -> c114(COMPARE#5(#less(z1, z2), z1, z2), #LESS(z1, z2)) COMPARE#5(#false, z0, z1) -> c115(COMPARE#6(#greater(z0, z1)), #GREATER(z0, z1)) COMPARE#5(#true, z0, z1) -> c116(-'(#0, #pos(#s(#0)))) COMPARE#6(#false) -> c117(#ABS(#0)) COMPARE#6(#true) -> c118(#ABS(#pos(#s(#0)))) DIFF(z0, z1, z2) -> c119(MOD(+(+(z0, z1), z2), #pos(#s(#s(#0)))), +'(+(z0, z1), z2), +'(z0, z1)) DIFF(z0, z1, z2) -> c120(DIFF#1(#less(-(-(z0, z1), z2), #0)), #LESS(-(-(z0, z1), z2), #0), -'(-(z0, z1), z2), -'(z0, z1)) DIFF#1(#false) -> c121(#ABS(#0)) DIFF#1(#true) -> c122(#ABS(#pos(#s(#0)))) DIV(z0, z1) -> c123(#DIV(z0, z1)) LEQ(z0, z1) -> c124(#LESS(compare(z0, z1), #pos(#s(#0))), COMPARE(z0, z1)) MOD(z0, z1) -> c125(-'(z0, *(z0, div(z0, z1))), *'(z0, div(z0, z1)), DIV(z0, z1)) MULT(z0, z1) -> c126(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c127(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), #ABS(#0)) MULT#1(::(z0, z1), z2) -> c128(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), MULT(z1, z2)) MULT#1(nil, z0) -> c129 MULT#2(z0, z1, z2) -> c130(MULT#3(#equal(z2, #pos(#s(#0))), z1, z0), #EQUAL(z2, #pos(#s(#0)))) MULT#3(#false, z0, z1) -> c131 MULT#3(#true, z0, z1) -> c132(ADD(z0, z1)) MULT3(z0, z1, z2) -> c133(MULT(mult(z0, z1), z1), MULT(z0, z1)) SUB(z0, z1) -> c134(SUB#1(sub'(z0, z1, #abs(#0))), SUB'(z0, z1, #abs(#0)), #ABS(#0)) SUB#1(tuple#2(z0, z1)) -> c135 SUB'(z0, z1, z2) -> c136(SUB'#1(z0, z1, z2)) SUB'#1(::(z0, z1), z2, z3) -> c137(SUB'#2(z2, z3, z0, z1)) SUB'#1(nil, z0, z1) -> c138 SUB'#2(::(z0, z1), z2, z3, z4) -> c139(SUB'#3(diff(z3, z0, z2), z4, z1), DIFF(z3, z0, z2)) SUB'#2(nil, z0, z1, z2) -> c140 SUB'#3(tuple#2(z0, z1), z2, z3) -> c141(SUB'#4(sub'(z2, z3, z1), z0), SUB'(z2, z3, z1)) SUB'#4(tuple#2(z0, z1), z2) -> c142(SUB'#5(#equal(z1, #pos(#s(#0))), z2, z0), #EQUAL(z1, #pos(#s(#0)))) SUB'#5(#false, z0, z1) -> c143 SUB'#5(#true, z0, z1) -> c144(#ABS(#0)) SUM(z0, z1, z2) -> c145(SUM#1(+(+(z0, z1), z2)), +'(+(z0, z1), z2), +'(z0, z1)) SUM#1(z0) -> c146(SUM#2(#equal(z0, #0), z0), #EQUAL(z0, #0)) SUM#2(#false, z0) -> c147(SUM#3(#equal(z0, #pos(#s(#0))), z0), #EQUAL(z0, #pos(#s(#0)))) SUM#2(#true, z0) -> c148(#ABS(#0)) SUM#2(#true, z0) -> c149(#ABS(#0)) SUM#3(#false, z0) -> c150(SUM#4(#equal(z0, #pos(#s(#s(#0))))), #EQUAL(z0, #pos(#s(#s(#0))))) SUM#3(#true, z0) -> c151(#ABS(#pos(#s(#0)))) SUM#3(#true, z0) -> c152(#ABS(#0)) SUM#4(#false) -> c153(#ABS(#pos(#s(#0)))) SUM#4(#false) -> c154(#ABS(#pos(#s(#0)))) SUM#4(#true) -> c155(#ABS(#0)) SUM#4(#true) -> c156(#ABS(#pos(#s(#0)))) The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #AND(#false, #false) -> c5 #AND(#false, #true) -> c6 #AND(#true, #false) -> c7 #AND(#true, #true) -> c8 #CKGT(#EQ) -> c9 #CKGT(#GT) -> c10 #CKGT(#LT) -> c11 #CKLT(#EQ) -> c12 #CKLT(#GT) -> c13 #CKLT(#LT) -> c14 #COMPARE(#0, #0) -> c15 #COMPARE(#0, #neg(z0)) -> c16 #COMPARE(#0, #pos(z0)) -> c17 #COMPARE(#0, #s(z0)) -> c18 #COMPARE(#neg(z0), #0) -> c19 #COMPARE(#neg(z0), #neg(z1)) -> c20(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c21 #COMPARE(#pos(z0), #0) -> c22 #COMPARE(#pos(z0), #neg(z1)) -> c23 #COMPARE(#pos(z0), #pos(z1)) -> c24(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c25 #COMPARE(#s(z0), #s(z1)) -> c26(#COMPARE(z0, z1)) #DIV(#0, #0) -> c27 #DIV(#0, #neg(z0)) -> c28 #DIV(#0, #pos(z0)) -> c29 #DIV(#neg(z0), #0) -> c30 #DIV(#neg(z0), #neg(z1)) -> c31(#NATDIV(z0, z1)) #DIV(#neg(z0), #pos(z1)) -> c32(#NATDIV(z0, z1)) #DIV(#pos(z0), #0) -> c33 #DIV(#pos(z0), #neg(z1)) -> c34(#NATDIV(z0, z1)) #DIV(#pos(z0), #pos(z1)) -> c35(#NATDIV(z0, z1)) #EQ'(#0, #0) -> c36 #EQ'(#0, #neg(z0)) -> c37 #EQ'(#0, #pos(z0)) -> c38 #EQ'(#0, #s(z0)) -> c39 #EQ'(#neg(z0), #0) -> c40 #EQ'(#neg(z0), #neg(z1)) -> c41(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c42 #EQ'(#pos(z0), #0) -> c43 #EQ'(#pos(z0), #neg(z1)) -> c44 #EQ'(#pos(z0), #pos(z1)) -> c45(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c46 #EQ'(#s(z0), #s(z1)) -> c47(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c48(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c49(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c50 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c51 #EQ'(nil, ::(z0, z1)) -> c52 #EQ'(nil, nil) -> c53 #EQ'(nil, tuple#2(z0, z1)) -> c54 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c55 #EQ'(tuple#2(z0, z1), nil) -> c56 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c57(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c58(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #MULT(#0, #0) -> c59 #MULT(#0, #neg(z0)) -> c60 #MULT(#0, #pos(z0)) -> c61 #MULT(#neg(z0), #0) -> c62 #MULT(#neg(z0), #neg(z1)) -> c63(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c64(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c65 #MULT(#pos(z0), #neg(z1)) -> c66(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c67(#NATMULT(z0, z1)) #NATDIV(#0, #0) -> c68 #NATDIV(#s(z0), #s(z1)) -> c69(#NATDIV(#natsub(z0, z1), #s(z1)), #NATSUB(z0, z1)) #NATMULT(#0, z0) -> c70 #NATMULT(#s(z0), z1) -> c71(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #NATSUB(z0, #0) -> c72 #NATSUB(#s(z0), #s(z1)) -> c73(#NATSUB(z0, z1)) #PRED(#0) -> c74 #PRED(#neg(#s(z0))) -> c75 #PRED(#pos(#s(#0))) -> c76 #PRED(#pos(#s(#s(z0)))) -> c77 #SUB(z0, #0) -> c78 #SUB(z0, #neg(z1)) -> c79(#ADD(z0, #pos(z1))) #SUB(z0, #pos(z1)) -> c80(#ADD(z0, #neg(z1))) #SUCC(#0) -> c81 #SUCC(#neg(#s(#0))) -> c82 #SUCC(#neg(#s(#s(z0)))) -> c83 #SUCC(#pos(#s(z0))) -> c84 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(z0, z1) #div(#0, #0) -> #divByZero #div(#0, #neg(z0)) -> #0 #div(#0, #pos(z0)) -> #0 #div(#neg(z0), #0) -> #divByZero #div(#neg(z0), #neg(z1)) -> #pos(#natdiv(z0, z1)) #div(#neg(z0), #pos(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #0) -> #divByZero #div(#pos(z0), #neg(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #pos(z1)) -> #pos(#natdiv(z0, z1)) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natdiv(#0, #0) -> #divByZero #natdiv(#s(z0), #s(z1)) -> #s(#natdiv(#natsub(z0, z1), #s(z1))) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #natsub(z0, #0) -> z0 #natsub(#s(z0), #s(z1)) -> #natsub(z0, z1) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #sub(z0, #0) -> z0 #sub(z0, #neg(z1)) -> #add(z0, #pos(z1)) #sub(z0, #pos(z1)) -> #add(z0, #neg(z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) #less(z0, z1) -> #cklt(#compare(z0, z1)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) -(z0, z1) -> #sub(z0, z1) add(z0, z1) -> add'(z0, z1, #abs(#0)) add'(z0, z1, z2) -> add'#1(z0, z1, z2) add'#1(::(z0, z1), z2, z3) -> add'#2(z2, z3, z0, z1) add'#1(nil, z0, z1) -> nil add'#2(::(z0, z1), z2, z3, z4) -> add'#3(sum(z3, z0, z2), z4, z1) add'#2(nil, z0, z1, z2) -> nil add'#3(tuple#2(z0, z1), z2, z3) -> ::(z0, add'(z2, z3, z1)) bitToInt(z0) -> bitToInt'(z0, #abs(#pos(#s(#0)))) bitToInt'(z0, z1) -> bitToInt'#1(z0, z1) bitToInt'#1(::(z0, z1), z2) -> +(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))) bitToInt'#1(nil, z0) -> #abs(#0) compare(z0, z1) -> compare#1(z0, z1) compare#1(::(z0, z1), z2) -> compare#2(z2, z0, z1) compare#1(nil, z0) -> #abs(#0) compare#2(::(z0, z1), z2, z3) -> compare#3(compare(z3, z1), z2, z0) compare#2(nil, z0, z1) -> #abs(#0) compare#3(z0, z1, z2) -> compare#4(#equal(z0, #0), z0, z1, z2) compare#4(#false, z0, z1, z2) -> z0 compare#4(#true, z0, z1, z2) -> compare#5(#less(z1, z2), z1, z2) compare#5(#false, z0, z1) -> compare#6(#greater(z0, z1)) compare#5(#true, z0, z1) -> -(#0, #pos(#s(#0))) compare#6(#false) -> #abs(#0) compare#6(#true) -> #abs(#pos(#s(#0))) diff(z0, z1, z2) -> tuple#2(mod(+(+(z0, z1), z2), #pos(#s(#s(#0)))), diff#1(#less(-(-(z0, z1), z2), #0))) diff#1(#false) -> #abs(#0) diff#1(#true) -> #abs(#pos(#s(#0))) div(z0, z1) -> #div(z0, z1) leq(z0, z1) -> #less(compare(z0, z1), #pos(#s(#0))) mod(z0, z1) -> -(z0, *(z0, div(z0, z1))) mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(::(#abs(#0), mult(z1, z2)), z2, z0) mult#1(nil, z0) -> nil mult#2(z0, z1, z2) -> mult#3(#equal(z2, #pos(#s(#0))), z1, z0) mult#3(#false, z0, z1) -> z1 mult#3(#true, z0, z1) -> add(z0, z1) mult3(z0, z1, z2) -> mult(mult(z0, z1), z1) sub(z0, z1) -> sub#1(sub'(z0, z1, #abs(#0))) sub#1(tuple#2(z0, z1)) -> z0 sub'(z0, z1, z2) -> sub'#1(z0, z1, z2) sub'#1(::(z0, z1), z2, z3) -> sub'#2(z2, z3, z0, z1) sub'#1(nil, z0, z1) -> tuple#2(nil, z1) sub'#2(::(z0, z1), z2, z3, z4) -> sub'#3(diff(z3, z0, z2), z4, z1) sub'#2(nil, z0, z1, z2) -> tuple#2(nil, z0) sub'#3(tuple#2(z0, z1), z2, z3) -> sub'#4(sub'(z2, z3, z1), z0) sub'#4(tuple#2(z0, z1), z2) -> tuple#2(sub'#5(#equal(z1, #pos(#s(#0))), z2, z0), z1) sub'#5(#false, z0, z1) -> ::(z0, z1) sub'#5(#true, z0, z1) -> ::(#abs(#0), z1) sum(z0, z1, z2) -> sum#1(+(+(z0, z1), z2)) sum#1(z0) -> sum#2(#equal(z0, #0), z0) sum#2(#false, z0) -> sum#3(#equal(z0, #pos(#s(#0))), z0) sum#2(#true, z0) -> tuple#2(#abs(#0), #abs(#0)) sum#3(#false, z0) -> sum#4(#equal(z0, #pos(#s(#s(#0))))) sum#3(#true, z0) -> tuple#2(#abs(#pos(#s(#0))), #abs(#0)) sum#4(#false) -> tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0)))) sum#4(#true) -> tuple#2(#abs(#0), #abs(#pos(#s(#0)))) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (4) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #ABS(#0) -> c85 #ABS(#neg(z0)) -> c86 #ABS(#pos(z0)) -> c87 #ABS(#s(z0)) -> c88 #EQUAL(z0, z1) -> c89(#EQ'(z0, z1)) #GREATER(z0, z1) -> c90(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) #LESS(z0, z1) -> c91(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) *'(z0, z1) -> c92(#MULT(z0, z1)) +'(z0, z1) -> c93(#ADD(z0, z1)) -'(z0, z1) -> c94(#SUB(z0, z1)) ADD(z0, z1) -> c95(ADD'(z0, z1, #abs(#0)), #ABS(#0)) ADD'(z0, z1, z2) -> c96(ADD'#1(z0, z1, z2)) ADD'#1(::(z0, z1), z2, z3) -> c97(ADD'#2(z2, z3, z0, z1)) ADD'#1(nil, z0, z1) -> c98 ADD'#2(::(z0, z1), z2, z3, z4) -> c99(ADD'#3(sum(z3, z0, z2), z4, z1), SUM(z3, z0, z2)) ADD'#2(nil, z0, z1, z2) -> c100 ADD'#3(tuple#2(z0, z1), z2, z3) -> c101(ADD'(z2, z3, z1)) BITTOINT(z0) -> c102(BITTOINT'(z0, #abs(#pos(#s(#0)))), #ABS(#pos(#s(#0)))) BITTOINT'(z0, z1) -> c103(BITTOINT'#1(z0, z1)) BITTOINT'#1(::(z0, z1), z2) -> c104(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), *'(z0, z2)) BITTOINT'#1(::(z0, z1), z2) -> c105(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), BITTOINT'(z1, *(z2, #pos(#s(#s(#0))))), *'(z2, #pos(#s(#s(#0))))) BITTOINT'#1(nil, z0) -> c106(#ABS(#0)) COMPARE(z0, z1) -> c107(COMPARE#1(z0, z1)) COMPARE#1(::(z0, z1), z2) -> c108(COMPARE#2(z2, z0, z1)) COMPARE#1(nil, z0) -> c109(#ABS(#0)) COMPARE#2(::(z0, z1), z2, z3) -> c110(COMPARE#3(compare(z3, z1), z2, z0), COMPARE(z3, z1)) COMPARE#2(nil, z0, z1) -> c111(#ABS(#0)) COMPARE#3(z0, z1, z2) -> c112(COMPARE#4(#equal(z0, #0), z0, z1, z2), #EQUAL(z0, #0)) COMPARE#4(#false, z0, z1, z2) -> c113 COMPARE#4(#true, z0, z1, z2) -> c114(COMPARE#5(#less(z1, z2), z1, z2), #LESS(z1, z2)) COMPARE#5(#false, z0, z1) -> c115(COMPARE#6(#greater(z0, z1)), #GREATER(z0, z1)) COMPARE#5(#true, z0, z1) -> c116(-'(#0, #pos(#s(#0)))) COMPARE#6(#false) -> c117(#ABS(#0)) COMPARE#6(#true) -> c118(#ABS(#pos(#s(#0)))) DIFF(z0, z1, z2) -> c119(MOD(+(+(z0, z1), z2), #pos(#s(#s(#0)))), +'(+(z0, z1), z2), +'(z0, z1)) DIFF(z0, z1, z2) -> c120(DIFF#1(#less(-(-(z0, z1), z2), #0)), #LESS(-(-(z0, z1), z2), #0), -'(-(z0, z1), z2), -'(z0, z1)) DIFF#1(#false) -> c121(#ABS(#0)) DIFF#1(#true) -> c122(#ABS(#pos(#s(#0)))) DIV(z0, z1) -> c123(#DIV(z0, z1)) LEQ(z0, z1) -> c124(#LESS(compare(z0, z1), #pos(#s(#0))), COMPARE(z0, z1)) MOD(z0, z1) -> c125(-'(z0, *(z0, div(z0, z1))), *'(z0, div(z0, z1)), DIV(z0, z1)) MULT(z0, z1) -> c126(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c127(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), #ABS(#0)) MULT#1(::(z0, z1), z2) -> c128(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), MULT(z1, z2)) MULT#1(nil, z0) -> c129 MULT#2(z0, z1, z2) -> c130(MULT#3(#equal(z2, #pos(#s(#0))), z1, z0), #EQUAL(z2, #pos(#s(#0)))) MULT#3(#false, z0, z1) -> c131 MULT#3(#true, z0, z1) -> c132(ADD(z0, z1)) MULT3(z0, z1, z2) -> c133(MULT(mult(z0, z1), z1), MULT(z0, z1)) SUB(z0, z1) -> c134(SUB#1(sub'(z0, z1, #abs(#0))), SUB'(z0, z1, #abs(#0)), #ABS(#0)) SUB#1(tuple#2(z0, z1)) -> c135 SUB'(z0, z1, z2) -> c136(SUB'#1(z0, z1, z2)) SUB'#1(::(z0, z1), z2, z3) -> c137(SUB'#2(z2, z3, z0, z1)) SUB'#1(nil, z0, z1) -> c138 SUB'#2(::(z0, z1), z2, z3, z4) -> c139(SUB'#3(diff(z3, z0, z2), z4, z1), DIFF(z3, z0, z2)) SUB'#2(nil, z0, z1, z2) -> c140 SUB'#3(tuple#2(z0, z1), z2, z3) -> c141(SUB'#4(sub'(z2, z3, z1), z0), SUB'(z2, z3, z1)) SUB'#4(tuple#2(z0, z1), z2) -> c142(SUB'#5(#equal(z1, #pos(#s(#0))), z2, z0), #EQUAL(z1, #pos(#s(#0)))) SUB'#5(#false, z0, z1) -> c143 SUB'#5(#true, z0, z1) -> c144(#ABS(#0)) SUM(z0, z1, z2) -> c145(SUM#1(+(+(z0, z1), z2)), +'(+(z0, z1), z2), +'(z0, z1)) SUM#1(z0) -> c146(SUM#2(#equal(z0, #0), z0), #EQUAL(z0, #0)) SUM#2(#false, z0) -> c147(SUM#3(#equal(z0, #pos(#s(#0))), z0), #EQUAL(z0, #pos(#s(#0)))) SUM#2(#true, z0) -> c148(#ABS(#0)) SUM#2(#true, z0) -> c149(#ABS(#0)) SUM#3(#false, z0) -> c150(SUM#4(#equal(z0, #pos(#s(#s(#0))))), #EQUAL(z0, #pos(#s(#s(#0))))) SUM#3(#true, z0) -> c151(#ABS(#pos(#s(#0)))) SUM#3(#true, z0) -> c152(#ABS(#0)) SUM#4(#false) -> c153(#ABS(#pos(#s(#0)))) SUM#4(#false) -> c154(#ABS(#pos(#s(#0)))) SUM#4(#true) -> c155(#ABS(#0)) SUM#4(#true) -> c156(#ABS(#pos(#s(#0)))) The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #AND(#false, #false) -> c5 #AND(#false, #true) -> c6 #AND(#true, #false) -> c7 #AND(#true, #true) -> c8 #CKGT(#EQ) -> c9 #CKGT(#GT) -> c10 #CKGT(#LT) -> c11 #CKLT(#EQ) -> c12 #CKLT(#GT) -> c13 #CKLT(#LT) -> c14 #COMPARE(#0, #0) -> c15 #COMPARE(#0, #neg(z0)) -> c16 #COMPARE(#0, #pos(z0)) -> c17 #COMPARE(#0, #s(z0)) -> c18 #COMPARE(#neg(z0), #0) -> c19 #COMPARE(#neg(z0), #neg(z1)) -> c20(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c21 #COMPARE(#pos(z0), #0) -> c22 #COMPARE(#pos(z0), #neg(z1)) -> c23 #COMPARE(#pos(z0), #pos(z1)) -> c24(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c25 #COMPARE(#s(z0), #s(z1)) -> c26(#COMPARE(z0, z1)) #DIV(#0, #0) -> c27 #DIV(#0, #neg(z0)) -> c28 #DIV(#0, #pos(z0)) -> c29 #DIV(#neg(z0), #0) -> c30 #DIV(#neg(z0), #neg(z1)) -> c31(#NATDIV(z0, z1)) #DIV(#neg(z0), #pos(z1)) -> c32(#NATDIV(z0, z1)) #DIV(#pos(z0), #0) -> c33 #DIV(#pos(z0), #neg(z1)) -> c34(#NATDIV(z0, z1)) #DIV(#pos(z0), #pos(z1)) -> c35(#NATDIV(z0, z1)) #EQ'(#0, #0) -> c36 #EQ'(#0, #neg(z0)) -> c37 #EQ'(#0, #pos(z0)) -> c38 #EQ'(#0, #s(z0)) -> c39 #EQ'(#neg(z0), #0) -> c40 #EQ'(#neg(z0), #neg(z1)) -> c41(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c42 #EQ'(#pos(z0), #0) -> c43 #EQ'(#pos(z0), #neg(z1)) -> c44 #EQ'(#pos(z0), #pos(z1)) -> c45(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c46 #EQ'(#s(z0), #s(z1)) -> c47(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c48(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c49(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c50 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c51 #EQ'(nil, ::(z0, z1)) -> c52 #EQ'(nil, nil) -> c53 #EQ'(nil, tuple#2(z0, z1)) -> c54 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c55 #EQ'(tuple#2(z0, z1), nil) -> c56 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c57(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c58(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #MULT(#0, #0) -> c59 #MULT(#0, #neg(z0)) -> c60 #MULT(#0, #pos(z0)) -> c61 #MULT(#neg(z0), #0) -> c62 #MULT(#neg(z0), #neg(z1)) -> c63(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c64(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c65 #MULT(#pos(z0), #neg(z1)) -> c66(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c67(#NATMULT(z0, z1)) #NATDIV(#0, #0) -> c68 #NATDIV(#s(z0), #s(z1)) -> c69(#NATDIV(#natsub(z0, z1), #s(z1)), #NATSUB(z0, z1)) #NATMULT(#0, z0) -> c70 #NATMULT(#s(z0), z1) -> c71(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #NATSUB(z0, #0) -> c72 #NATSUB(#s(z0), #s(z1)) -> c73(#NATSUB(z0, z1)) #PRED(#0) -> c74 #PRED(#neg(#s(z0))) -> c75 #PRED(#pos(#s(#0))) -> c76 #PRED(#pos(#s(#s(z0)))) -> c77 #SUB(z0, #0) -> c78 #SUB(z0, #neg(z1)) -> c79(#ADD(z0, #pos(z1))) #SUB(z0, #pos(z1)) -> c80(#ADD(z0, #neg(z1))) #SUCC(#0) -> c81 #SUCC(#neg(#s(#0))) -> c82 #SUCC(#neg(#s(#s(z0)))) -> c83 #SUCC(#pos(#s(z0))) -> c84 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(z0, z1) #div(#0, #0) -> #divByZero #div(#0, #neg(z0)) -> #0 #div(#0, #pos(z0)) -> #0 #div(#neg(z0), #0) -> #divByZero #div(#neg(z0), #neg(z1)) -> #pos(#natdiv(z0, z1)) #div(#neg(z0), #pos(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #0) -> #divByZero #div(#pos(z0), #neg(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #pos(z1)) -> #pos(#natdiv(z0, z1)) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natdiv(#0, #0) -> #divByZero #natdiv(#s(z0), #s(z1)) -> #s(#natdiv(#natsub(z0, z1), #s(z1))) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #natsub(z0, #0) -> z0 #natsub(#s(z0), #s(z1)) -> #natsub(z0, z1) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #sub(z0, #0) -> z0 #sub(z0, #neg(z1)) -> #add(z0, #pos(z1)) #sub(z0, #pos(z1)) -> #add(z0, #neg(z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) #less(z0, z1) -> #cklt(#compare(z0, z1)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) -(z0, z1) -> #sub(z0, z1) add(z0, z1) -> add'(z0, z1, #abs(#0)) add'(z0, z1, z2) -> add'#1(z0, z1, z2) add'#1(::(z0, z1), z2, z3) -> add'#2(z2, z3, z0, z1) add'#1(nil, z0, z1) -> nil add'#2(::(z0, z1), z2, z3, z4) -> add'#3(sum(z3, z0, z2), z4, z1) add'#2(nil, z0, z1, z2) -> nil add'#3(tuple#2(z0, z1), z2, z3) -> ::(z0, add'(z2, z3, z1)) bitToInt(z0) -> bitToInt'(z0, #abs(#pos(#s(#0)))) bitToInt'(z0, z1) -> bitToInt'#1(z0, z1) bitToInt'#1(::(z0, z1), z2) -> +(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))) bitToInt'#1(nil, z0) -> #abs(#0) compare(z0, z1) -> compare#1(z0, z1) compare#1(::(z0, z1), z2) -> compare#2(z2, z0, z1) compare#1(nil, z0) -> #abs(#0) compare#2(::(z0, z1), z2, z3) -> compare#3(compare(z3, z1), z2, z0) compare#2(nil, z0, z1) -> #abs(#0) compare#3(z0, z1, z2) -> compare#4(#equal(z0, #0), z0, z1, z2) compare#4(#false, z0, z1, z2) -> z0 compare#4(#true, z0, z1, z2) -> compare#5(#less(z1, z2), z1, z2) compare#5(#false, z0, z1) -> compare#6(#greater(z0, z1)) compare#5(#true, z0, z1) -> -(#0, #pos(#s(#0))) compare#6(#false) -> #abs(#0) compare#6(#true) -> #abs(#pos(#s(#0))) diff(z0, z1, z2) -> tuple#2(mod(+(+(z0, z1), z2), #pos(#s(#s(#0)))), diff#1(#less(-(-(z0, z1), z2), #0))) diff#1(#false) -> #abs(#0) diff#1(#true) -> #abs(#pos(#s(#0))) div(z0, z1) -> #div(z0, z1) leq(z0, z1) -> #less(compare(z0, z1), #pos(#s(#0))) mod(z0, z1) -> -(z0, *(z0, div(z0, z1))) mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(::(#abs(#0), mult(z1, z2)), z2, z0) mult#1(nil, z0) -> nil mult#2(z0, z1, z2) -> mult#3(#equal(z2, #pos(#s(#0))), z1, z0) mult#3(#false, z0, z1) -> z1 mult#3(#true, z0, z1) -> add(z0, z1) mult3(z0, z1, z2) -> mult(mult(z0, z1), z1) sub(z0, z1) -> sub#1(sub'(z0, z1, #abs(#0))) sub#1(tuple#2(z0, z1)) -> z0 sub'(z0, z1, z2) -> sub'#1(z0, z1, z2) sub'#1(::(z0, z1), z2, z3) -> sub'#2(z2, z3, z0, z1) sub'#1(nil, z0, z1) -> tuple#2(nil, z1) sub'#2(::(z0, z1), z2, z3, z4) -> sub'#3(diff(z3, z0, z2), z4, z1) sub'#2(nil, z0, z1, z2) -> tuple#2(nil, z0) sub'#3(tuple#2(z0, z1), z2, z3) -> sub'#4(sub'(z2, z3, z1), z0) sub'#4(tuple#2(z0, z1), z2) -> tuple#2(sub'#5(#equal(z1, #pos(#s(#0))), z2, z0), z1) sub'#5(#false, z0, z1) -> ::(z0, z1) sub'#5(#true, z0, z1) -> ::(#abs(#0), z1) sum(z0, z1, z2) -> sum#1(+(+(z0, z1), z2)) sum#1(z0) -> sum#2(#equal(z0, #0), z0) sum#2(#false, z0) -> sum#3(#equal(z0, #pos(#s(#0))), z0) sum#2(#true, z0) -> tuple#2(#abs(#0), #abs(#0)) sum#3(#false, z0) -> sum#4(#equal(z0, #pos(#s(#s(#0))))) sum#3(#true, z0) -> tuple#2(#abs(#pos(#s(#0))), #abs(#0)) sum#4(#false) -> tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0)))) sum#4(#true) -> tuple#2(#abs(#0), #abs(#pos(#s(#0)))) Rewrite Strategy: INNERMOST ---------------------------------------- (5) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence MULT#1(::(z0, z1), z2) ->^+ c128(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), c126(MULT#1(z1, z2))) gives rise to a decreasing loop by considering the right hand sides subterm at position [1,0]. The pumping substitution is [z1 / ::(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (6) Complex Obligation (BEST) ---------------------------------------- (7) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #ABS(#0) -> c85 #ABS(#neg(z0)) -> c86 #ABS(#pos(z0)) -> c87 #ABS(#s(z0)) -> c88 #EQUAL(z0, z1) -> c89(#EQ'(z0, z1)) #GREATER(z0, z1) -> c90(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) #LESS(z0, z1) -> c91(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) *'(z0, z1) -> c92(#MULT(z0, z1)) +'(z0, z1) -> c93(#ADD(z0, z1)) -'(z0, z1) -> c94(#SUB(z0, z1)) ADD(z0, z1) -> c95(ADD'(z0, z1, #abs(#0)), #ABS(#0)) ADD'(z0, z1, z2) -> c96(ADD'#1(z0, z1, z2)) ADD'#1(::(z0, z1), z2, z3) -> c97(ADD'#2(z2, z3, z0, z1)) ADD'#1(nil, z0, z1) -> c98 ADD'#2(::(z0, z1), z2, z3, z4) -> c99(ADD'#3(sum(z3, z0, z2), z4, z1), SUM(z3, z0, z2)) ADD'#2(nil, z0, z1, z2) -> c100 ADD'#3(tuple#2(z0, z1), z2, z3) -> c101(ADD'(z2, z3, z1)) BITTOINT(z0) -> c102(BITTOINT'(z0, #abs(#pos(#s(#0)))), #ABS(#pos(#s(#0)))) BITTOINT'(z0, z1) -> c103(BITTOINT'#1(z0, z1)) BITTOINT'#1(::(z0, z1), z2) -> c104(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), *'(z0, z2)) BITTOINT'#1(::(z0, z1), z2) -> c105(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), BITTOINT'(z1, *(z2, #pos(#s(#s(#0))))), *'(z2, #pos(#s(#s(#0))))) BITTOINT'#1(nil, z0) -> c106(#ABS(#0)) COMPARE(z0, z1) -> c107(COMPARE#1(z0, z1)) COMPARE#1(::(z0, z1), z2) -> c108(COMPARE#2(z2, z0, z1)) COMPARE#1(nil, z0) -> c109(#ABS(#0)) COMPARE#2(::(z0, z1), z2, z3) -> c110(COMPARE#3(compare(z3, z1), z2, z0), COMPARE(z3, z1)) COMPARE#2(nil, z0, z1) -> c111(#ABS(#0)) COMPARE#3(z0, z1, z2) -> c112(COMPARE#4(#equal(z0, #0), z0, z1, z2), #EQUAL(z0, #0)) COMPARE#4(#false, z0, z1, z2) -> c113 COMPARE#4(#true, z0, z1, z2) -> c114(COMPARE#5(#less(z1, z2), z1, z2), #LESS(z1, z2)) COMPARE#5(#false, z0, z1) -> c115(COMPARE#6(#greater(z0, z1)), #GREATER(z0, z1)) COMPARE#5(#true, z0, z1) -> c116(-'(#0, #pos(#s(#0)))) COMPARE#6(#false) -> c117(#ABS(#0)) COMPARE#6(#true) -> c118(#ABS(#pos(#s(#0)))) DIFF(z0, z1, z2) -> c119(MOD(+(+(z0, z1), z2), #pos(#s(#s(#0)))), +'(+(z0, z1), z2), +'(z0, z1)) DIFF(z0, z1, z2) -> c120(DIFF#1(#less(-(-(z0, z1), z2), #0)), #LESS(-(-(z0, z1), z2), #0), -'(-(z0, z1), z2), -'(z0, z1)) DIFF#1(#false) -> c121(#ABS(#0)) DIFF#1(#true) -> c122(#ABS(#pos(#s(#0)))) DIV(z0, z1) -> c123(#DIV(z0, z1)) LEQ(z0, z1) -> c124(#LESS(compare(z0, z1), #pos(#s(#0))), COMPARE(z0, z1)) MOD(z0, z1) -> c125(-'(z0, *(z0, div(z0, z1))), *'(z0, div(z0, z1)), DIV(z0, z1)) MULT(z0, z1) -> c126(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c127(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), #ABS(#0)) MULT#1(::(z0, z1), z2) -> c128(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), MULT(z1, z2)) MULT#1(nil, z0) -> c129 MULT#2(z0, z1, z2) -> c130(MULT#3(#equal(z2, #pos(#s(#0))), z1, z0), #EQUAL(z2, #pos(#s(#0)))) MULT#3(#false, z0, z1) -> c131 MULT#3(#true, z0, z1) -> c132(ADD(z0, z1)) MULT3(z0, z1, z2) -> c133(MULT(mult(z0, z1), z1), MULT(z0, z1)) SUB(z0, z1) -> c134(SUB#1(sub'(z0, z1, #abs(#0))), SUB'(z0, z1, #abs(#0)), #ABS(#0)) SUB#1(tuple#2(z0, z1)) -> c135 SUB'(z0, z1, z2) -> c136(SUB'#1(z0, z1, z2)) SUB'#1(::(z0, z1), z2, z3) -> c137(SUB'#2(z2, z3, z0, z1)) SUB'#1(nil, z0, z1) -> c138 SUB'#2(::(z0, z1), z2, z3, z4) -> c139(SUB'#3(diff(z3, z0, z2), z4, z1), DIFF(z3, z0, z2)) SUB'#2(nil, z0, z1, z2) -> c140 SUB'#3(tuple#2(z0, z1), z2, z3) -> c141(SUB'#4(sub'(z2, z3, z1), z0), SUB'(z2, z3, z1)) SUB'#4(tuple#2(z0, z1), z2) -> c142(SUB'#5(#equal(z1, #pos(#s(#0))), z2, z0), #EQUAL(z1, #pos(#s(#0)))) SUB'#5(#false, z0, z1) -> c143 SUB'#5(#true, z0, z1) -> c144(#ABS(#0)) SUM(z0, z1, z2) -> c145(SUM#1(+(+(z0, z1), z2)), +'(+(z0, z1), z2), +'(z0, z1)) SUM#1(z0) -> c146(SUM#2(#equal(z0, #0), z0), #EQUAL(z0, #0)) SUM#2(#false, z0) -> c147(SUM#3(#equal(z0, #pos(#s(#0))), z0), #EQUAL(z0, #pos(#s(#0)))) SUM#2(#true, z0) -> c148(#ABS(#0)) SUM#2(#true, z0) -> c149(#ABS(#0)) SUM#3(#false, z0) -> c150(SUM#4(#equal(z0, #pos(#s(#s(#0))))), #EQUAL(z0, #pos(#s(#s(#0))))) SUM#3(#true, z0) -> c151(#ABS(#pos(#s(#0)))) SUM#3(#true, z0) -> c152(#ABS(#0)) SUM#4(#false) -> c153(#ABS(#pos(#s(#0)))) SUM#4(#false) -> c154(#ABS(#pos(#s(#0)))) SUM#4(#true) -> c155(#ABS(#0)) SUM#4(#true) -> c156(#ABS(#pos(#s(#0)))) The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #AND(#false, #false) -> c5 #AND(#false, #true) -> c6 #AND(#true, #false) -> c7 #AND(#true, #true) -> c8 #CKGT(#EQ) -> c9 #CKGT(#GT) -> c10 #CKGT(#LT) -> c11 #CKLT(#EQ) -> c12 #CKLT(#GT) -> c13 #CKLT(#LT) -> c14 #COMPARE(#0, #0) -> c15 #COMPARE(#0, #neg(z0)) -> c16 #COMPARE(#0, #pos(z0)) -> c17 #COMPARE(#0, #s(z0)) -> c18 #COMPARE(#neg(z0), #0) -> c19 #COMPARE(#neg(z0), #neg(z1)) -> c20(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c21 #COMPARE(#pos(z0), #0) -> c22 #COMPARE(#pos(z0), #neg(z1)) -> c23 #COMPARE(#pos(z0), #pos(z1)) -> c24(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c25 #COMPARE(#s(z0), #s(z1)) -> c26(#COMPARE(z0, z1)) #DIV(#0, #0) -> c27 #DIV(#0, #neg(z0)) -> c28 #DIV(#0, #pos(z0)) -> c29 #DIV(#neg(z0), #0) -> c30 #DIV(#neg(z0), #neg(z1)) -> c31(#NATDIV(z0, z1)) #DIV(#neg(z0), #pos(z1)) -> c32(#NATDIV(z0, z1)) #DIV(#pos(z0), #0) -> c33 #DIV(#pos(z0), #neg(z1)) -> c34(#NATDIV(z0, z1)) #DIV(#pos(z0), #pos(z1)) -> c35(#NATDIV(z0, z1)) #EQ'(#0, #0) -> c36 #EQ'(#0, #neg(z0)) -> c37 #EQ'(#0, #pos(z0)) -> c38 #EQ'(#0, #s(z0)) -> c39 #EQ'(#neg(z0), #0) -> c40 #EQ'(#neg(z0), #neg(z1)) -> c41(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c42 #EQ'(#pos(z0), #0) -> c43 #EQ'(#pos(z0), #neg(z1)) -> c44 #EQ'(#pos(z0), #pos(z1)) -> c45(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c46 #EQ'(#s(z0), #s(z1)) -> c47(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c48(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c49(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c50 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c51 #EQ'(nil, ::(z0, z1)) -> c52 #EQ'(nil, nil) -> c53 #EQ'(nil, tuple#2(z0, z1)) -> c54 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c55 #EQ'(tuple#2(z0, z1), nil) -> c56 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c57(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c58(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #MULT(#0, #0) -> c59 #MULT(#0, #neg(z0)) -> c60 #MULT(#0, #pos(z0)) -> c61 #MULT(#neg(z0), #0) -> c62 #MULT(#neg(z0), #neg(z1)) -> c63(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c64(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c65 #MULT(#pos(z0), #neg(z1)) -> c66(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c67(#NATMULT(z0, z1)) #NATDIV(#0, #0) -> c68 #NATDIV(#s(z0), #s(z1)) -> c69(#NATDIV(#natsub(z0, z1), #s(z1)), #NATSUB(z0, z1)) #NATMULT(#0, z0) -> c70 #NATMULT(#s(z0), z1) -> c71(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #NATSUB(z0, #0) -> c72 #NATSUB(#s(z0), #s(z1)) -> c73(#NATSUB(z0, z1)) #PRED(#0) -> c74 #PRED(#neg(#s(z0))) -> c75 #PRED(#pos(#s(#0))) -> c76 #PRED(#pos(#s(#s(z0)))) -> c77 #SUB(z0, #0) -> c78 #SUB(z0, #neg(z1)) -> c79(#ADD(z0, #pos(z1))) #SUB(z0, #pos(z1)) -> c80(#ADD(z0, #neg(z1))) #SUCC(#0) -> c81 #SUCC(#neg(#s(#0))) -> c82 #SUCC(#neg(#s(#s(z0)))) -> c83 #SUCC(#pos(#s(z0))) -> c84 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(z0, z1) #div(#0, #0) -> #divByZero #div(#0, #neg(z0)) -> #0 #div(#0, #pos(z0)) -> #0 #div(#neg(z0), #0) -> #divByZero #div(#neg(z0), #neg(z1)) -> #pos(#natdiv(z0, z1)) #div(#neg(z0), #pos(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #0) -> #divByZero #div(#pos(z0), #neg(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #pos(z1)) -> #pos(#natdiv(z0, z1)) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natdiv(#0, #0) -> #divByZero #natdiv(#s(z0), #s(z1)) -> #s(#natdiv(#natsub(z0, z1), #s(z1))) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #natsub(z0, #0) -> z0 #natsub(#s(z0), #s(z1)) -> #natsub(z0, z1) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #sub(z0, #0) -> z0 #sub(z0, #neg(z1)) -> #add(z0, #pos(z1)) #sub(z0, #pos(z1)) -> #add(z0, #neg(z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) #less(z0, z1) -> #cklt(#compare(z0, z1)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) -(z0, z1) -> #sub(z0, z1) add(z0, z1) -> add'(z0, z1, #abs(#0)) add'(z0, z1, z2) -> add'#1(z0, z1, z2) add'#1(::(z0, z1), z2, z3) -> add'#2(z2, z3, z0, z1) add'#1(nil, z0, z1) -> nil add'#2(::(z0, z1), z2, z3, z4) -> add'#3(sum(z3, z0, z2), z4, z1) add'#2(nil, z0, z1, z2) -> nil add'#3(tuple#2(z0, z1), z2, z3) -> ::(z0, add'(z2, z3, z1)) bitToInt(z0) -> bitToInt'(z0, #abs(#pos(#s(#0)))) bitToInt'(z0, z1) -> bitToInt'#1(z0, z1) bitToInt'#1(::(z0, z1), z2) -> +(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))) bitToInt'#1(nil, z0) -> #abs(#0) compare(z0, z1) -> compare#1(z0, z1) compare#1(::(z0, z1), z2) -> compare#2(z2, z0, z1) compare#1(nil, z0) -> #abs(#0) compare#2(::(z0, z1), z2, z3) -> compare#3(compare(z3, z1), z2, z0) compare#2(nil, z0, z1) -> #abs(#0) compare#3(z0, z1, z2) -> compare#4(#equal(z0, #0), z0, z1, z2) compare#4(#false, z0, z1, z2) -> z0 compare#4(#true, z0, z1, z2) -> compare#5(#less(z1, z2), z1, z2) compare#5(#false, z0, z1) -> compare#6(#greater(z0, z1)) compare#5(#true, z0, z1) -> -(#0, #pos(#s(#0))) compare#6(#false) -> #abs(#0) compare#6(#true) -> #abs(#pos(#s(#0))) diff(z0, z1, z2) -> tuple#2(mod(+(+(z0, z1), z2), #pos(#s(#s(#0)))), diff#1(#less(-(-(z0, z1), z2), #0))) diff#1(#false) -> #abs(#0) diff#1(#true) -> #abs(#pos(#s(#0))) div(z0, z1) -> #div(z0, z1) leq(z0, z1) -> #less(compare(z0, z1), #pos(#s(#0))) mod(z0, z1) -> -(z0, *(z0, div(z0, z1))) mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(::(#abs(#0), mult(z1, z2)), z2, z0) mult#1(nil, z0) -> nil mult#2(z0, z1, z2) -> mult#3(#equal(z2, #pos(#s(#0))), z1, z0) mult#3(#false, z0, z1) -> z1 mult#3(#true, z0, z1) -> add(z0, z1) mult3(z0, z1, z2) -> mult(mult(z0, z1), z1) sub(z0, z1) -> sub#1(sub'(z0, z1, #abs(#0))) sub#1(tuple#2(z0, z1)) -> z0 sub'(z0, z1, z2) -> sub'#1(z0, z1, z2) sub'#1(::(z0, z1), z2, z3) -> sub'#2(z2, z3, z0, z1) sub'#1(nil, z0, z1) -> tuple#2(nil, z1) sub'#2(::(z0, z1), z2, z3, z4) -> sub'#3(diff(z3, z0, z2), z4, z1) sub'#2(nil, z0, z1, z2) -> tuple#2(nil, z0) sub'#3(tuple#2(z0, z1), z2, z3) -> sub'#4(sub'(z2, z3, z1), z0) sub'#4(tuple#2(z0, z1), z2) -> tuple#2(sub'#5(#equal(z1, #pos(#s(#0))), z2, z0), z1) sub'#5(#false, z0, z1) -> ::(z0, z1) sub'#5(#true, z0, z1) -> ::(#abs(#0), z1) sum(z0, z1, z2) -> sum#1(+(+(z0, z1), z2)) sum#1(z0) -> sum#2(#equal(z0, #0), z0) sum#2(#false, z0) -> sum#3(#equal(z0, #pos(#s(#0))), z0) sum#2(#true, z0) -> tuple#2(#abs(#0), #abs(#0)) sum#3(#false, z0) -> sum#4(#equal(z0, #pos(#s(#s(#0))))) sum#3(#true, z0) -> tuple#2(#abs(#pos(#s(#0))), #abs(#0)) sum#4(#false) -> tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0)))) sum#4(#true) -> tuple#2(#abs(#0), #abs(#pos(#s(#0)))) Rewrite Strategy: INNERMOST ---------------------------------------- (8) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (9) BOUNDS(n^1, INF) ---------------------------------------- (10) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #ABS(#0) -> c85 #ABS(#neg(z0)) -> c86 #ABS(#pos(z0)) -> c87 #ABS(#s(z0)) -> c88 #EQUAL(z0, z1) -> c89(#EQ'(z0, z1)) #GREATER(z0, z1) -> c90(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) #LESS(z0, z1) -> c91(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) *'(z0, z1) -> c92(#MULT(z0, z1)) +'(z0, z1) -> c93(#ADD(z0, z1)) -'(z0, z1) -> c94(#SUB(z0, z1)) ADD(z0, z1) -> c95(ADD'(z0, z1, #abs(#0)), #ABS(#0)) ADD'(z0, z1, z2) -> c96(ADD'#1(z0, z1, z2)) ADD'#1(::(z0, z1), z2, z3) -> c97(ADD'#2(z2, z3, z0, z1)) ADD'#1(nil, z0, z1) -> c98 ADD'#2(::(z0, z1), z2, z3, z4) -> c99(ADD'#3(sum(z3, z0, z2), z4, z1), SUM(z3, z0, z2)) ADD'#2(nil, z0, z1, z2) -> c100 ADD'#3(tuple#2(z0, z1), z2, z3) -> c101(ADD'(z2, z3, z1)) BITTOINT(z0) -> c102(BITTOINT'(z0, #abs(#pos(#s(#0)))), #ABS(#pos(#s(#0)))) BITTOINT'(z0, z1) -> c103(BITTOINT'#1(z0, z1)) BITTOINT'#1(::(z0, z1), z2) -> c104(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), *'(z0, z2)) BITTOINT'#1(::(z0, z1), z2) -> c105(+'(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))), BITTOINT'(z1, *(z2, #pos(#s(#s(#0))))), *'(z2, #pos(#s(#s(#0))))) BITTOINT'#1(nil, z0) -> c106(#ABS(#0)) COMPARE(z0, z1) -> c107(COMPARE#1(z0, z1)) COMPARE#1(::(z0, z1), z2) -> c108(COMPARE#2(z2, z0, z1)) COMPARE#1(nil, z0) -> c109(#ABS(#0)) COMPARE#2(::(z0, z1), z2, z3) -> c110(COMPARE#3(compare(z3, z1), z2, z0), COMPARE(z3, z1)) COMPARE#2(nil, z0, z1) -> c111(#ABS(#0)) COMPARE#3(z0, z1, z2) -> c112(COMPARE#4(#equal(z0, #0), z0, z1, z2), #EQUAL(z0, #0)) COMPARE#4(#false, z0, z1, z2) -> c113 COMPARE#4(#true, z0, z1, z2) -> c114(COMPARE#5(#less(z1, z2), z1, z2), #LESS(z1, z2)) COMPARE#5(#false, z0, z1) -> c115(COMPARE#6(#greater(z0, z1)), #GREATER(z0, z1)) COMPARE#5(#true, z0, z1) -> c116(-'(#0, #pos(#s(#0)))) COMPARE#6(#false) -> c117(#ABS(#0)) COMPARE#6(#true) -> c118(#ABS(#pos(#s(#0)))) DIFF(z0, z1, z2) -> c119(MOD(+(+(z0, z1), z2), #pos(#s(#s(#0)))), +'(+(z0, z1), z2), +'(z0, z1)) DIFF(z0, z1, z2) -> c120(DIFF#1(#less(-(-(z0, z1), z2), #0)), #LESS(-(-(z0, z1), z2), #0), -'(-(z0, z1), z2), -'(z0, z1)) DIFF#1(#false) -> c121(#ABS(#0)) DIFF#1(#true) -> c122(#ABS(#pos(#s(#0)))) DIV(z0, z1) -> c123(#DIV(z0, z1)) LEQ(z0, z1) -> c124(#LESS(compare(z0, z1), #pos(#s(#0))), COMPARE(z0, z1)) MOD(z0, z1) -> c125(-'(z0, *(z0, div(z0, z1))), *'(z0, div(z0, z1)), DIV(z0, z1)) MULT(z0, z1) -> c126(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c127(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), #ABS(#0)) MULT#1(::(z0, z1), z2) -> c128(MULT#2(::(#abs(#0), mult(z1, z2)), z2, z0), MULT(z1, z2)) MULT#1(nil, z0) -> c129 MULT#2(z0, z1, z2) -> c130(MULT#3(#equal(z2, #pos(#s(#0))), z1, z0), #EQUAL(z2, #pos(#s(#0)))) MULT#3(#false, z0, z1) -> c131 MULT#3(#true, z0, z1) -> c132(ADD(z0, z1)) MULT3(z0, z1, z2) -> c133(MULT(mult(z0, z1), z1), MULT(z0, z1)) SUB(z0, z1) -> c134(SUB#1(sub'(z0, z1, #abs(#0))), SUB'(z0, z1, #abs(#0)), #ABS(#0)) SUB#1(tuple#2(z0, z1)) -> c135 SUB'(z0, z1, z2) -> c136(SUB'#1(z0, z1, z2)) SUB'#1(::(z0, z1), z2, z3) -> c137(SUB'#2(z2, z3, z0, z1)) SUB'#1(nil, z0, z1) -> c138 SUB'#2(::(z0, z1), z2, z3, z4) -> c139(SUB'#3(diff(z3, z0, z2), z4, z1), DIFF(z3, z0, z2)) SUB'#2(nil, z0, z1, z2) -> c140 SUB'#3(tuple#2(z0, z1), z2, z3) -> c141(SUB'#4(sub'(z2, z3, z1), z0), SUB'(z2, z3, z1)) SUB'#4(tuple#2(z0, z1), z2) -> c142(SUB'#5(#equal(z1, #pos(#s(#0))), z2, z0), #EQUAL(z1, #pos(#s(#0)))) SUB'#5(#false, z0, z1) -> c143 SUB'#5(#true, z0, z1) -> c144(#ABS(#0)) SUM(z0, z1, z2) -> c145(SUM#1(+(+(z0, z1), z2)), +'(+(z0, z1), z2), +'(z0, z1)) SUM#1(z0) -> c146(SUM#2(#equal(z0, #0), z0), #EQUAL(z0, #0)) SUM#2(#false, z0) -> c147(SUM#3(#equal(z0, #pos(#s(#0))), z0), #EQUAL(z0, #pos(#s(#0)))) SUM#2(#true, z0) -> c148(#ABS(#0)) SUM#2(#true, z0) -> c149(#ABS(#0)) SUM#3(#false, z0) -> c150(SUM#4(#equal(z0, #pos(#s(#s(#0))))), #EQUAL(z0, #pos(#s(#s(#0))))) SUM#3(#true, z0) -> c151(#ABS(#pos(#s(#0)))) SUM#3(#true, z0) -> c152(#ABS(#0)) SUM#4(#false) -> c153(#ABS(#pos(#s(#0)))) SUM#4(#false) -> c154(#ABS(#pos(#s(#0)))) SUM#4(#true) -> c155(#ABS(#0)) SUM#4(#true) -> c156(#ABS(#pos(#s(#0)))) The (relative) TRS S consists of the following rules: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #AND(#false, #false) -> c5 #AND(#false, #true) -> c6 #AND(#true, #false) -> c7 #AND(#true, #true) -> c8 #CKGT(#EQ) -> c9 #CKGT(#GT) -> c10 #CKGT(#LT) -> c11 #CKLT(#EQ) -> c12 #CKLT(#GT) -> c13 #CKLT(#LT) -> c14 #COMPARE(#0, #0) -> c15 #COMPARE(#0, #neg(z0)) -> c16 #COMPARE(#0, #pos(z0)) -> c17 #COMPARE(#0, #s(z0)) -> c18 #COMPARE(#neg(z0), #0) -> c19 #COMPARE(#neg(z0), #neg(z1)) -> c20(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c21 #COMPARE(#pos(z0), #0) -> c22 #COMPARE(#pos(z0), #neg(z1)) -> c23 #COMPARE(#pos(z0), #pos(z1)) -> c24(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c25 #COMPARE(#s(z0), #s(z1)) -> c26(#COMPARE(z0, z1)) #DIV(#0, #0) -> c27 #DIV(#0, #neg(z0)) -> c28 #DIV(#0, #pos(z0)) -> c29 #DIV(#neg(z0), #0) -> c30 #DIV(#neg(z0), #neg(z1)) -> c31(#NATDIV(z0, z1)) #DIV(#neg(z0), #pos(z1)) -> c32(#NATDIV(z0, z1)) #DIV(#pos(z0), #0) -> c33 #DIV(#pos(z0), #neg(z1)) -> c34(#NATDIV(z0, z1)) #DIV(#pos(z0), #pos(z1)) -> c35(#NATDIV(z0, z1)) #EQ'(#0, #0) -> c36 #EQ'(#0, #neg(z0)) -> c37 #EQ'(#0, #pos(z0)) -> c38 #EQ'(#0, #s(z0)) -> c39 #EQ'(#neg(z0), #0) -> c40 #EQ'(#neg(z0), #neg(z1)) -> c41(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c42 #EQ'(#pos(z0), #0) -> c43 #EQ'(#pos(z0), #neg(z1)) -> c44 #EQ'(#pos(z0), #pos(z1)) -> c45(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c46 #EQ'(#s(z0), #s(z1)) -> c47(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c48(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c49(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c50 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c51 #EQ'(nil, ::(z0, z1)) -> c52 #EQ'(nil, nil) -> c53 #EQ'(nil, tuple#2(z0, z1)) -> c54 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c55 #EQ'(tuple#2(z0, z1), nil) -> c56 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c57(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c58(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #MULT(#0, #0) -> c59 #MULT(#0, #neg(z0)) -> c60 #MULT(#0, #pos(z0)) -> c61 #MULT(#neg(z0), #0) -> c62 #MULT(#neg(z0), #neg(z1)) -> c63(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c64(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c65 #MULT(#pos(z0), #neg(z1)) -> c66(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c67(#NATMULT(z0, z1)) #NATDIV(#0, #0) -> c68 #NATDIV(#s(z0), #s(z1)) -> c69(#NATDIV(#natsub(z0, z1), #s(z1)), #NATSUB(z0, z1)) #NATMULT(#0, z0) -> c70 #NATMULT(#s(z0), z1) -> c71(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #NATSUB(z0, #0) -> c72 #NATSUB(#s(z0), #s(z1)) -> c73(#NATSUB(z0, z1)) #PRED(#0) -> c74 #PRED(#neg(#s(z0))) -> c75 #PRED(#pos(#s(#0))) -> c76 #PRED(#pos(#s(#s(z0)))) -> c77 #SUB(z0, #0) -> c78 #SUB(z0, #neg(z1)) -> c79(#ADD(z0, #pos(z1))) #SUB(z0, #pos(z1)) -> c80(#ADD(z0, #neg(z1))) #SUCC(#0) -> c81 #SUCC(#neg(#s(#0))) -> c82 #SUCC(#neg(#s(#s(z0)))) -> c83 #SUCC(#pos(#s(z0))) -> c84 #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(z0, z1) #div(#0, #0) -> #divByZero #div(#0, #neg(z0)) -> #0 #div(#0, #pos(z0)) -> #0 #div(#neg(z0), #0) -> #divByZero #div(#neg(z0), #neg(z1)) -> #pos(#natdiv(z0, z1)) #div(#neg(z0), #pos(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #0) -> #divByZero #div(#pos(z0), #neg(z1)) -> #neg(#natdiv(z0, z1)) #div(#pos(z0), #pos(z1)) -> #pos(#natdiv(z0, z1)) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natdiv(#0, #0) -> #divByZero #natdiv(#s(z0), #s(z1)) -> #s(#natdiv(#natsub(z0, z1), #s(z1))) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #natsub(z0, #0) -> z0 #natsub(#s(z0), #s(z1)) -> #natsub(z0, z1) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #sub(z0, #0) -> z0 #sub(z0, #neg(z1)) -> #add(z0, #pos(z1)) #sub(z0, #pos(z1)) -> #add(z0, #neg(z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) #less(z0, z1) -> #cklt(#compare(z0, z1)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) -(z0, z1) -> #sub(z0, z1) add(z0, z1) -> add'(z0, z1, #abs(#0)) add'(z0, z1, z2) -> add'#1(z0, z1, z2) add'#1(::(z0, z1), z2, z3) -> add'#2(z2, z3, z0, z1) add'#1(nil, z0, z1) -> nil add'#2(::(z0, z1), z2, z3, z4) -> add'#3(sum(z3, z0, z2), z4, z1) add'#2(nil, z0, z1, z2) -> nil add'#3(tuple#2(z0, z1), z2, z3) -> ::(z0, add'(z2, z3, z1)) bitToInt(z0) -> bitToInt'(z0, #abs(#pos(#s(#0)))) bitToInt'(z0, z1) -> bitToInt'#1(z0, z1) bitToInt'#1(::(z0, z1), z2) -> +(*(z0, z2), bitToInt'(z1, *(z2, #pos(#s(#s(#0)))))) bitToInt'#1(nil, z0) -> #abs(#0) compare(z0, z1) -> compare#1(z0, z1) compare#1(::(z0, z1), z2) -> compare#2(z2, z0, z1) compare#1(nil, z0) -> #abs(#0) compare#2(::(z0, z1), z2, z3) -> compare#3(compare(z3, z1), z2, z0) compare#2(nil, z0, z1) -> #abs(#0) compare#3(z0, z1, z2) -> compare#4(#equal(z0, #0), z0, z1, z2) compare#4(#false, z0, z1, z2) -> z0 compare#4(#true, z0, z1, z2) -> compare#5(#less(z1, z2), z1, z2) compare#5(#false, z0, z1) -> compare#6(#greater(z0, z1)) compare#5(#true, z0, z1) -> -(#0, #pos(#s(#0))) compare#6(#false) -> #abs(#0) compare#6(#true) -> #abs(#pos(#s(#0))) diff(z0, z1, z2) -> tuple#2(mod(+(+(z0, z1), z2), #pos(#s(#s(#0)))), diff#1(#less(-(-(z0, z1), z2), #0))) diff#1(#false) -> #abs(#0) diff#1(#true) -> #abs(#pos(#s(#0))) div(z0, z1) -> #div(z0, z1) leq(z0, z1) -> #less(compare(z0, z1), #pos(#s(#0))) mod(z0, z1) -> -(z0, *(z0, div(z0, z1))) mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(::(#abs(#0), mult(z1, z2)), z2, z0) mult#1(nil, z0) -> nil mult#2(z0, z1, z2) -> mult#3(#equal(z2, #pos(#s(#0))), z1, z0) mult#3(#false, z0, z1) -> z1 mult#3(#true, z0, z1) -> add(z0, z1) mult3(z0, z1, z2) -> mult(mult(z0, z1), z1) sub(z0, z1) -> sub#1(sub'(z0, z1, #abs(#0))) sub#1(tuple#2(z0, z1)) -> z0 sub'(z0, z1, z2) -> sub'#1(z0, z1, z2) sub'#1(::(z0, z1), z2, z3) -> sub'#2(z2, z3, z0, z1) sub'#1(nil, z0, z1) -> tuple#2(nil, z1) sub'#2(::(z0, z1), z2, z3, z4) -> sub'#3(diff(z3, z0, z2), z4, z1) sub'#2(nil, z0, z1, z2) -> tuple#2(nil, z0) sub'#3(tuple#2(z0, z1), z2, z3) -> sub'#4(sub'(z2, z3, z1), z0) sub'#4(tuple#2(z0, z1), z2) -> tuple#2(sub'#5(#equal(z1, #pos(#s(#0))), z2, z0), z1) sub'#5(#false, z0, z1) -> ::(z0, z1) sub'#5(#true, z0, z1) -> ::(#abs(#0), z1) sum(z0, z1, z2) -> sum#1(+(+(z0, z1), z2)) sum#1(z0) -> sum#2(#equal(z0, #0), z0) sum#2(#false, z0) -> sum#3(#equal(z0, #pos(#s(#0))), z0) sum#2(#true, z0) -> tuple#2(#abs(#0), #abs(#0)) sum#3(#false, z0) -> sum#4(#equal(z0, #pos(#s(#s(#0))))) sum#3(#true, z0) -> tuple#2(#abs(#pos(#s(#0))), #abs(#0)) sum#4(#false) -> tuple#2(#abs(#pos(#s(#0))), #abs(#pos(#s(#0)))) sum#4(#true) -> tuple#2(#abs(#0), #abs(#pos(#s(#0)))) Rewrite Strategy: INNERMOST