MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: #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())))) - Weak TRS: #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() #abs(#0()) -> #0() #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) #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)) #equal(z0,z1) -> #eq(z0,z1) #greater(z0,z1) -> #ckgt(#compare(z0,z1)) #less(z0,z1) -> #cklt(#compare(z0,z1)) #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))) *(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())))) - Signature: {#ABS/1,#ADD/2,#AND/2,#CKGT/1,#CKLT/1,#COMPARE/2,#DIV/2,#EQ'/2,#EQUAL/2,#GREATER/2,#LESS/2,#MULT/2,#NATDIV/2 ,#NATMULT/2,#NATSUB/2,#PRED/1,#SUB/2,#SUCC/1,#abs/1,#add/2,#and/2,#ckgt/1,#cklt/1,#compare/2,#div/2,#eq/2 ,#equal/2,#greater/2,#less/2,#mult/2,#natdiv/2,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,*'/2,+/2,+'/2 ,-/2,-'/2,ADD/2,ADD'/3,ADD'#1/3,ADD'#2/4,ADD'#3/3,BITTOINT/1,BITTOINT'/2,BITTOINT'#1/2,COMPARE/2,COMPARE#1/2 ,COMPARE#2/3,COMPARE#3/3,COMPARE#4/4,COMPARE#5/3,COMPARE#6/1,DIFF/3,DIFF#1/1,DIV/2,LEQ/2,MOD/2,MULT/2 ,MULT#1/2,MULT#2/3,MULT#3/3,MULT3/3,SUB/2,SUB#1/1,SUB'/3,SUB'#1/3,SUB'#2/4,SUB'#3/3,SUB'#4/2,SUB'#5/3,SUM/3 ,SUM#1/1,SUM#2/2,SUM#3/2,SUM#4/1,add/2,add'/3,add'#1/3,add'#2/4,add'#3/3,bitToInt/1,bitToInt'/2 ,bitToInt'#1/2,compare/2,compare#1/2,compare#2/3,compare#3/3,compare#4/4,compare#5/3,compare#6/1,diff/3 ,diff#1/1,div/2,leq/2,mod/2,mult/2,mult#1/2,mult#2/3,mult#3/3,mult3/3,sub/2,sub#1/1,sub'/3,sub'#1/3,sub'#2/4 ,sub'#3/3,sub'#4/2,sub'#5/3,sum/3,sum#1/1,sum#2/2,sum#3/2,sum#4/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#divByZero/0 ,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,c/0,c1/1,c10/0,c100/0,c101/1,c102/2,c103/1,c104/2,c105/3,c106/1 ,c107/1,c108/1,c109/1,c11/0,c110/2,c111/1,c112/2,c113/0,c114/2,c115/2,c116/1,c117/1,c118/1,c119/3,c12/0 ,c120/4,c121/1,c122/1,c123/1,c124/2,c125/3,c126/1,c127/2,c128/2,c129/0,c13/0,c130/2,c131/0,c132/1,c133/2 ,c134/3,c135/0,c136/1,c137/1,c138/0,c139/2,c14/0,c140/0,c141/2,c142/2,c143/0,c144/1,c145/3,c146/2,c147/2 ,c148/1,c149/1,c15/0,c150/2,c151/1,c152/1,c153/1,c154/1,c155/1,c156/1,c16/0,c17/0,c18/0,c19/0,c2/2,c20/1 ,c21/0,c22/0,c23/0,c24/1,c25/0,c26/1,c27/0,c28/0,c29/0,c3/1,c30/0,c31/1,c32/1,c33/0,c34/1,c35/1,c36/0,c37/0 ,c38/0,c39/0,c4/2,c40/0,c41/1,c42/0,c43/0,c44/0,c45/1,c46/0,c47/1,c48/2,c49/2,c5/0,c50/0,c51/0,c52/0,c53/0 ,c54/0,c55/0,c56/0,c57/2,c58/2,c59/0,c6/0,c60/0,c61/0,c62/0,c63/1,c64/1,c65/0,c66/1,c67/1,c68/0,c69/2,c7/0 ,c70/0,c71/2,c72/0,c73/1,c74/0,c75/0,c76/0,c77/0,c78/0,c79/1,c8/0,c80/1,c81/0,c82/0,c83/0,c84/0,c85/0,c86/0 ,c87/0,c88/0,c89/1,c9/0,c90/2,c91/2,c92/1,c93/1,c94/1,c95/2,c96/1,c97/1,c98/0,c99/2,nil/0,tuple#2/2} - Obligation: innermost runtime complexity wrt. defined symbols {#ABS,#ADD,#AND,#CKGT,#CKLT,#COMPARE,#DIV,#EQ',#EQUAL ,#GREATER,#LESS,#MULT,#NATDIV,#NATMULT,#NATSUB,#PRED,#SUB,#SUCC,#abs,#add,#and,#ckgt,#cklt,#compare,#div,#eq ,#equal,#greater,#less,#mult,#natdiv,#natmult,#natsub,#pred,#sub,#succ,*,*',+,+',-,-',ADD,ADD',ADD'#1,ADD'#2 ,ADD'#3,BITTOINT,BITTOINT',BITTOINT'#1,COMPARE,COMPARE#1,COMPARE#2,COMPARE#3,COMPARE#4,COMPARE#5,COMPARE#6 ,DIFF,DIFF#1,DIV,LEQ,MOD,MULT,MULT#1,MULT#2,MULT#3,MULT3,SUB,SUB#1,SUB',SUB'#1,SUB'#2,SUB'#3,SUB'#4,SUB'#5 ,SUM,SUM#1,SUM#2,SUM#3,SUM#4,add,add',add'#1,add'#2,add'#3,bitToInt,bitToInt',bitToInt'#1,compare,compare#1 ,compare#2,compare#3,compare#4,compare#5,compare#6,diff,diff#1,div,leq,mod,mult,mult#1,mult#2,mult#3,mult3 ,sub,sub#1,sub',sub'#1,sub'#2,sub'#3,sub'#4,sub'#5,sum,sum#1,sum#2,sum#3,sum#4} and constructors {#0,#EQ,#GT ,#LT,#divByZero,#false,#neg,#pos,#s,#true,::,c,c1,c10,c100,c101,c102,c103,c104,c105,c106,c107,c108,c109,c11 ,c110,c111,c112,c113,c114,c115,c116,c117,c118,c119,c12,c120,c121,c122,c123,c124,c125,c126,c127,c128,c129,c13 ,c130,c131,c132,c133,c134,c135,c136,c137,c138,c139,c14,c140,c141,c142,c143,c144,c145,c146,c147,c148,c149,c15 ,c150,c151,c152,c153,c154,c155,c156,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31 ,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56 ,c57,c58,c59,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80 ,c81,c82,c83,c84,c85,c86,c87,c88,c89,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,nil,tuple#2} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: None MAYBE