MAYBE 1122.73/297.07 MAYBE 1122.73/297.07 1122.73/297.07 We are left with following problem, upon which TcT provides the 1122.73/297.07 certificate MAYBE. 1122.73/297.07 1122.73/297.07 Strict Trs: 1122.73/297.07 { active(from(X)) -> from(active(X)) 1122.73/297.07 , active(from(X)) -> mark(cons(X, from(s(X)))) 1122.73/297.07 , active(cons(X1, X2)) -> cons(active(X1), X2) 1122.73/297.07 , active(s(X)) -> s(active(X)) 1122.73/297.07 , active(2ndspos(X1, X2)) -> 2ndspos(X1, active(X2)) 1122.73/297.07 , active(2ndspos(X1, X2)) -> 2ndspos(active(X1), X2) 1122.73/297.07 , active(2ndspos(s(N), cons(X, Z))) -> 1122.73/297.07 mark(2ndspos(s(N), cons2(X, Z))) 1122.73/297.07 , active(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.07 mark(rcons(posrecip(Y), 2ndsneg(N, Z))) 1122.73/297.07 , active(2ndspos(0(), Z)) -> mark(rnil()) 1122.73/297.07 , active(cons2(X1, X2)) -> cons2(X1, active(X2)) 1122.73/297.07 , active(rcons(X1, X2)) -> rcons(X1, active(X2)) 1122.73/297.07 , active(rcons(X1, X2)) -> rcons(active(X1), X2) 1122.73/297.07 , active(posrecip(X)) -> posrecip(active(X)) 1122.73/297.07 , active(2ndsneg(X1, X2)) -> 2ndsneg(X1, active(X2)) 1122.73/297.07 , active(2ndsneg(X1, X2)) -> 2ndsneg(active(X1), X2) 1122.73/297.07 , active(2ndsneg(s(N), cons(X, Z))) -> 1122.73/297.07 mark(2ndsneg(s(N), cons2(X, Z))) 1122.73/297.07 , active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.07 mark(rcons(negrecip(Y), 2ndspos(N, Z))) 1122.73/297.07 , active(2ndsneg(0(), Z)) -> mark(rnil()) 1122.73/297.07 , active(negrecip(X)) -> negrecip(active(X)) 1122.73/297.07 , active(pi(X)) -> mark(2ndspos(X, from(0()))) 1122.73/297.07 , active(pi(X)) -> pi(active(X)) 1122.73/297.07 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1122.73/297.07 , active(plus(X1, X2)) -> plus(active(X1), X2) 1122.73/297.07 , active(plus(s(X), Y)) -> mark(s(plus(X, Y))) 1122.73/297.07 , active(plus(0(), Y)) -> mark(Y) 1122.73/297.07 , active(times(X1, X2)) -> times(X1, active(X2)) 1122.73/297.07 , active(times(X1, X2)) -> times(active(X1), X2) 1122.73/297.07 , active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) 1122.73/297.07 , active(times(0(), Y)) -> mark(0()) 1122.73/297.07 , active(square(X)) -> mark(times(X, X)) 1122.73/297.07 , active(square(X)) -> square(active(X)) 1122.73/297.07 , from(mark(X)) -> mark(from(X)) 1122.73/297.07 , from(ok(X)) -> ok(from(X)) 1122.73/297.07 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1122.73/297.07 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1122.73/297.07 , s(mark(X)) -> mark(s(X)) 1122.73/297.07 , s(ok(X)) -> ok(s(X)) 1122.73/297.07 , 2ndspos(X1, mark(X2)) -> mark(2ndspos(X1, X2)) 1122.73/297.07 , 2ndspos(mark(X1), X2) -> mark(2ndspos(X1, X2)) 1122.73/297.07 , 2ndspos(ok(X1), ok(X2)) -> ok(2ndspos(X1, X2)) 1122.73/297.07 , cons2(X1, mark(X2)) -> mark(cons2(X1, X2)) 1122.73/297.07 , cons2(ok(X1), ok(X2)) -> ok(cons2(X1, X2)) 1122.73/297.07 , rcons(X1, mark(X2)) -> mark(rcons(X1, X2)) 1122.73/297.07 , rcons(mark(X1), X2) -> mark(rcons(X1, X2)) 1122.73/297.07 , rcons(ok(X1), ok(X2)) -> ok(rcons(X1, X2)) 1122.73/297.07 , posrecip(mark(X)) -> mark(posrecip(X)) 1122.73/297.07 , posrecip(ok(X)) -> ok(posrecip(X)) 1122.73/297.07 , 2ndsneg(X1, mark(X2)) -> mark(2ndsneg(X1, X2)) 1122.73/297.07 , 2ndsneg(mark(X1), X2) -> mark(2ndsneg(X1, X2)) 1122.73/297.07 , 2ndsneg(ok(X1), ok(X2)) -> ok(2ndsneg(X1, X2)) 1122.73/297.07 , negrecip(mark(X)) -> mark(negrecip(X)) 1122.73/297.07 , negrecip(ok(X)) -> ok(negrecip(X)) 1122.73/297.07 , pi(mark(X)) -> mark(pi(X)) 1122.73/297.07 , pi(ok(X)) -> ok(pi(X)) 1122.73/297.07 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1122.73/297.07 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1122.73/297.07 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1122.73/297.07 , times(X1, mark(X2)) -> mark(times(X1, X2)) 1122.73/297.07 , times(mark(X1), X2) -> mark(times(X1, X2)) 1122.73/297.07 , times(ok(X1), ok(X2)) -> ok(times(X1, X2)) 1122.73/297.07 , square(mark(X)) -> mark(square(X)) 1122.73/297.07 , square(ok(X)) -> ok(square(X)) 1122.73/297.07 , proper(from(X)) -> from(proper(X)) 1122.73/297.07 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1122.73/297.07 , proper(s(X)) -> s(proper(X)) 1122.73/297.07 , proper(2ndspos(X1, X2)) -> 2ndspos(proper(X1), proper(X2)) 1122.73/297.07 , proper(0()) -> ok(0()) 1122.73/297.07 , proper(rnil()) -> ok(rnil()) 1122.73/297.07 , proper(cons2(X1, X2)) -> cons2(proper(X1), proper(X2)) 1122.73/297.07 , proper(rcons(X1, X2)) -> rcons(proper(X1), proper(X2)) 1122.73/297.07 , proper(posrecip(X)) -> posrecip(proper(X)) 1122.73/297.07 , proper(2ndsneg(X1, X2)) -> 2ndsneg(proper(X1), proper(X2)) 1122.73/297.07 , proper(negrecip(X)) -> negrecip(proper(X)) 1122.73/297.07 , proper(pi(X)) -> pi(proper(X)) 1122.73/297.07 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1122.73/297.07 , proper(times(X1, X2)) -> times(proper(X1), proper(X2)) 1122.73/297.07 , proper(square(X)) -> square(proper(X)) 1122.73/297.07 , proper(nil()) -> ok(nil()) 1122.73/297.07 , top(mark(X)) -> top(proper(X)) 1122.73/297.07 , top(ok(X)) -> top(active(X)) } 1122.73/297.07 Obligation: 1122.73/297.07 runtime complexity 1122.73/297.07 Answer: 1122.73/297.07 MAYBE 1122.73/297.07 1122.73/297.07 None of the processors succeeded. 1122.73/297.07 1122.73/297.07 Details of failed attempt(s): 1122.73/297.07 ----------------------------- 1122.73/297.07 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1122.73/297.07 following reason: 1122.73/297.07 1122.73/297.07 Computation stopped due to timeout after 297.0 seconds. 1122.73/297.07 1122.73/297.07 2) 'Best' failed due to the following reason: 1122.73/297.07 1122.73/297.07 None of the processors succeeded. 1122.73/297.07 1122.73/297.07 Details of failed attempt(s): 1122.73/297.07 ----------------------------- 1122.73/297.07 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1122.73/297.07 seconds)' failed due to the following reason: 1122.73/297.07 1122.73/297.07 Computation stopped due to timeout after 148.0 seconds. 1122.73/297.07 1122.73/297.07 2) 'Best' failed due to the following reason: 1122.73/297.07 1122.73/297.07 None of the processors succeeded. 1122.73/297.07 1122.73/297.07 Details of failed attempt(s): 1122.73/297.07 ----------------------------- 1122.73/297.07 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1122.73/297.07 to the following reason: 1122.73/297.07 1122.73/297.07 The processor is inapplicable, reason: 1122.73/297.07 Processor only applicable for innermost runtime complexity analysis 1122.73/297.07 1122.73/297.07 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1122.73/297.07 following reason: 1122.73/297.07 1122.73/297.07 The processor is inapplicable, reason: 1122.73/297.07 Processor only applicable for innermost runtime complexity analysis 1122.73/297.07 1122.73/297.07 1122.73/297.07 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1122.73/297.07 failed due to the following reason: 1122.73/297.07 1122.73/297.07 None of the processors succeeded. 1122.73/297.07 1122.73/297.07 Details of failed attempt(s): 1122.73/297.07 ----------------------------- 1122.73/297.07 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1122.73/297.07 failed due to the following reason: 1122.73/297.07 1122.73/297.07 match-boundness of the problem could not be verified. 1122.73/297.07 1122.73/297.07 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1122.73/297.07 failed due to the following reason: 1122.73/297.07 1122.73/297.07 match-boundness of the problem could not be verified. 1122.73/297.07 1122.73/297.07 1122.73/297.07 1122.73/297.07 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1122.73/297.07 the following reason: 1122.73/297.07 1122.73/297.07 We add the following weak dependency pairs: 1122.73/297.07 1122.73/297.07 Strict DPs: 1122.73/297.07 { active^#(from(X)) -> c_1(from^#(active(X))) 1122.73/297.07 , active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1122.73/297.07 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1122.73/297.07 , active^#(s(X)) -> c_4(s^#(active(X))) 1122.73/297.07 , active^#(2ndspos(X1, X2)) -> c_5(2ndspos^#(X1, active(X2))) 1122.73/297.07 , active^#(2ndspos(X1, X2)) -> c_6(2ndspos^#(active(X1), X2)) 1122.73/297.07 , active^#(2ndspos(s(N), cons(X, Z))) -> 1122.73/297.07 c_7(2ndspos^#(s(N), cons2(X, Z))) 1122.73/297.07 , active^#(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.07 c_8(rcons^#(posrecip(Y), 2ndsneg(N, Z))) 1122.73/297.07 , active^#(2ndspos(0(), Z)) -> c_9() 1122.73/297.07 , active^#(cons2(X1, X2)) -> c_10(cons2^#(X1, active(X2))) 1122.73/297.07 , active^#(rcons(X1, X2)) -> c_11(rcons^#(X1, active(X2))) 1122.73/297.07 , active^#(rcons(X1, X2)) -> c_12(rcons^#(active(X1), X2)) 1122.73/297.07 , active^#(posrecip(X)) -> c_13(posrecip^#(active(X))) 1122.73/297.07 , active^#(2ndsneg(X1, X2)) -> c_14(2ndsneg^#(X1, active(X2))) 1122.73/297.07 , active^#(2ndsneg(X1, X2)) -> c_15(2ndsneg^#(active(X1), X2)) 1122.73/297.07 , active^#(2ndsneg(s(N), cons(X, Z))) -> 1122.73/297.07 c_16(2ndsneg^#(s(N), cons2(X, Z))) 1122.73/297.07 , active^#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.07 c_17(rcons^#(negrecip(Y), 2ndspos(N, Z))) 1122.73/297.07 , active^#(2ndsneg(0(), Z)) -> c_18() 1122.73/297.07 , active^#(negrecip(X)) -> c_19(negrecip^#(active(X))) 1122.73/297.07 , active^#(pi(X)) -> c_20(2ndspos^#(X, from(0()))) 1122.73/297.07 , active^#(pi(X)) -> c_21(pi^#(active(X))) 1122.73/297.07 , active^#(plus(X1, X2)) -> c_22(plus^#(X1, active(X2))) 1122.73/297.07 , active^#(plus(X1, X2)) -> c_23(plus^#(active(X1), X2)) 1122.73/297.07 , active^#(plus(s(X), Y)) -> c_24(s^#(plus(X, Y))) 1122.73/297.07 , active^#(plus(0(), Y)) -> c_25(Y) 1122.73/297.07 , active^#(times(X1, X2)) -> c_26(times^#(X1, active(X2))) 1122.73/297.07 , active^#(times(X1, X2)) -> c_27(times^#(active(X1), X2)) 1122.73/297.07 , active^#(times(s(X), Y)) -> c_28(plus^#(Y, times(X, Y))) 1122.73/297.07 , active^#(times(0(), Y)) -> c_29() 1122.73/297.07 , active^#(square(X)) -> c_30(times^#(X, X)) 1122.73/297.07 , active^#(square(X)) -> c_31(square^#(active(X))) 1122.73/297.07 , from^#(mark(X)) -> c_32(from^#(X)) 1122.73/297.07 , from^#(ok(X)) -> c_33(from^#(X)) 1122.73/297.07 , cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) 1122.73/297.07 , cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) 1122.73/297.07 , s^#(mark(X)) -> c_36(s^#(X)) 1122.73/297.07 , s^#(ok(X)) -> c_37(s^#(X)) 1122.73/297.07 , 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) 1122.73/297.07 , 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) 1122.73/297.07 , 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) 1122.73/297.07 , rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) 1122.73/297.07 , rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) 1122.73/297.07 , rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) 1122.73/297.07 , cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) 1122.73/297.07 , cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) 1122.73/297.07 , posrecip^#(mark(X)) -> c_46(posrecip^#(X)) 1122.73/297.07 , posrecip^#(ok(X)) -> c_47(posrecip^#(X)) 1122.73/297.07 , 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) 1122.73/297.07 , 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) 1122.73/297.07 , 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) 1122.73/297.07 , negrecip^#(mark(X)) -> c_51(negrecip^#(X)) 1122.73/297.07 , negrecip^#(ok(X)) -> c_52(negrecip^#(X)) 1122.73/297.07 , pi^#(mark(X)) -> c_53(pi^#(X)) 1122.73/297.07 , pi^#(ok(X)) -> c_54(pi^#(X)) 1122.73/297.07 , plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) 1122.73/297.07 , plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) 1122.73/297.07 , plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) 1122.73/297.07 , times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) 1122.73/297.07 , times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) 1122.73/297.07 , times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) 1122.73/297.07 , square^#(mark(X)) -> c_61(square^#(X)) 1122.73/297.07 , square^#(ok(X)) -> c_62(square^#(X)) 1122.73/297.07 , proper^#(from(X)) -> c_63(from^#(proper(X))) 1122.73/297.07 , proper^#(cons(X1, X2)) -> c_64(cons^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(s(X)) -> c_65(s^#(proper(X))) 1122.73/297.07 , proper^#(2ndspos(X1, X2)) -> 1122.73/297.07 c_66(2ndspos^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(0()) -> c_67() 1122.73/297.07 , proper^#(rnil()) -> c_68() 1122.73/297.07 , proper^#(cons2(X1, X2)) -> c_69(cons2^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(rcons(X1, X2)) -> c_70(rcons^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(posrecip(X)) -> c_71(posrecip^#(proper(X))) 1122.73/297.07 , proper^#(2ndsneg(X1, X2)) -> 1122.73/297.07 c_72(2ndsneg^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(negrecip(X)) -> c_73(negrecip^#(proper(X))) 1122.73/297.07 , proper^#(pi(X)) -> c_74(pi^#(proper(X))) 1122.73/297.07 , proper^#(plus(X1, X2)) -> c_75(plus^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(times(X1, X2)) -> c_76(times^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(square(X)) -> c_77(square^#(proper(X))) 1122.73/297.07 , proper^#(nil()) -> c_78() 1122.73/297.07 , top^#(mark(X)) -> c_79(top^#(proper(X))) 1122.73/297.07 , top^#(ok(X)) -> c_80(top^#(active(X))) } 1122.73/297.07 1122.73/297.07 and mark the set of starting terms. 1122.73/297.07 1122.73/297.07 We are left with following problem, upon which TcT provides the 1122.73/297.07 certificate MAYBE. 1122.73/297.07 1122.73/297.07 Strict DPs: 1122.73/297.07 { active^#(from(X)) -> c_1(from^#(active(X))) 1122.73/297.07 , active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1122.73/297.07 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1122.73/297.07 , active^#(s(X)) -> c_4(s^#(active(X))) 1122.73/297.07 , active^#(2ndspos(X1, X2)) -> c_5(2ndspos^#(X1, active(X2))) 1122.73/297.07 , active^#(2ndspos(X1, X2)) -> c_6(2ndspos^#(active(X1), X2)) 1122.73/297.07 , active^#(2ndspos(s(N), cons(X, Z))) -> 1122.73/297.07 c_7(2ndspos^#(s(N), cons2(X, Z))) 1122.73/297.07 , active^#(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.07 c_8(rcons^#(posrecip(Y), 2ndsneg(N, Z))) 1122.73/297.07 , active^#(2ndspos(0(), Z)) -> c_9() 1122.73/297.07 , active^#(cons2(X1, X2)) -> c_10(cons2^#(X1, active(X2))) 1122.73/297.07 , active^#(rcons(X1, X2)) -> c_11(rcons^#(X1, active(X2))) 1122.73/297.07 , active^#(rcons(X1, X2)) -> c_12(rcons^#(active(X1), X2)) 1122.73/297.07 , active^#(posrecip(X)) -> c_13(posrecip^#(active(X))) 1122.73/297.07 , active^#(2ndsneg(X1, X2)) -> c_14(2ndsneg^#(X1, active(X2))) 1122.73/297.07 , active^#(2ndsneg(X1, X2)) -> c_15(2ndsneg^#(active(X1), X2)) 1122.73/297.07 , active^#(2ndsneg(s(N), cons(X, Z))) -> 1122.73/297.07 c_16(2ndsneg^#(s(N), cons2(X, Z))) 1122.73/297.07 , active^#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.07 c_17(rcons^#(negrecip(Y), 2ndspos(N, Z))) 1122.73/297.07 , active^#(2ndsneg(0(), Z)) -> c_18() 1122.73/297.07 , active^#(negrecip(X)) -> c_19(negrecip^#(active(X))) 1122.73/297.07 , active^#(pi(X)) -> c_20(2ndspos^#(X, from(0()))) 1122.73/297.07 , active^#(pi(X)) -> c_21(pi^#(active(X))) 1122.73/297.07 , active^#(plus(X1, X2)) -> c_22(plus^#(X1, active(X2))) 1122.73/297.07 , active^#(plus(X1, X2)) -> c_23(plus^#(active(X1), X2)) 1122.73/297.07 , active^#(plus(s(X), Y)) -> c_24(s^#(plus(X, Y))) 1122.73/297.07 , active^#(plus(0(), Y)) -> c_25(Y) 1122.73/297.07 , active^#(times(X1, X2)) -> c_26(times^#(X1, active(X2))) 1122.73/297.07 , active^#(times(X1, X2)) -> c_27(times^#(active(X1), X2)) 1122.73/297.07 , active^#(times(s(X), Y)) -> c_28(plus^#(Y, times(X, Y))) 1122.73/297.07 , active^#(times(0(), Y)) -> c_29() 1122.73/297.07 , active^#(square(X)) -> c_30(times^#(X, X)) 1122.73/297.07 , active^#(square(X)) -> c_31(square^#(active(X))) 1122.73/297.07 , from^#(mark(X)) -> c_32(from^#(X)) 1122.73/297.07 , from^#(ok(X)) -> c_33(from^#(X)) 1122.73/297.07 , cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) 1122.73/297.07 , cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) 1122.73/297.07 , s^#(mark(X)) -> c_36(s^#(X)) 1122.73/297.07 , s^#(ok(X)) -> c_37(s^#(X)) 1122.73/297.07 , 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) 1122.73/297.07 , 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) 1122.73/297.07 , 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) 1122.73/297.07 , rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) 1122.73/297.07 , rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) 1122.73/297.07 , rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) 1122.73/297.07 , cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) 1122.73/297.07 , cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) 1122.73/297.07 , posrecip^#(mark(X)) -> c_46(posrecip^#(X)) 1122.73/297.07 , posrecip^#(ok(X)) -> c_47(posrecip^#(X)) 1122.73/297.07 , 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) 1122.73/297.07 , 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) 1122.73/297.07 , 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) 1122.73/297.07 , negrecip^#(mark(X)) -> c_51(negrecip^#(X)) 1122.73/297.07 , negrecip^#(ok(X)) -> c_52(negrecip^#(X)) 1122.73/297.07 , pi^#(mark(X)) -> c_53(pi^#(X)) 1122.73/297.07 , pi^#(ok(X)) -> c_54(pi^#(X)) 1122.73/297.07 , plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) 1122.73/297.07 , plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) 1122.73/297.07 , plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) 1122.73/297.07 , times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) 1122.73/297.07 , times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) 1122.73/297.07 , times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) 1122.73/297.07 , square^#(mark(X)) -> c_61(square^#(X)) 1122.73/297.07 , square^#(ok(X)) -> c_62(square^#(X)) 1122.73/297.07 , proper^#(from(X)) -> c_63(from^#(proper(X))) 1122.73/297.07 , proper^#(cons(X1, X2)) -> c_64(cons^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(s(X)) -> c_65(s^#(proper(X))) 1122.73/297.07 , proper^#(2ndspos(X1, X2)) -> 1122.73/297.07 c_66(2ndspos^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(0()) -> c_67() 1122.73/297.07 , proper^#(rnil()) -> c_68() 1122.73/297.07 , proper^#(cons2(X1, X2)) -> c_69(cons2^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(rcons(X1, X2)) -> c_70(rcons^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(posrecip(X)) -> c_71(posrecip^#(proper(X))) 1122.73/297.07 , proper^#(2ndsneg(X1, X2)) -> 1122.73/297.07 c_72(2ndsneg^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(negrecip(X)) -> c_73(negrecip^#(proper(X))) 1122.73/297.07 , proper^#(pi(X)) -> c_74(pi^#(proper(X))) 1122.73/297.07 , proper^#(plus(X1, X2)) -> c_75(plus^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(times(X1, X2)) -> c_76(times^#(proper(X1), proper(X2))) 1122.73/297.07 , proper^#(square(X)) -> c_77(square^#(proper(X))) 1122.73/297.07 , proper^#(nil()) -> c_78() 1122.73/297.07 , top^#(mark(X)) -> c_79(top^#(proper(X))) 1122.73/297.07 , top^#(ok(X)) -> c_80(top^#(active(X))) } 1122.73/297.07 Strict Trs: 1122.73/297.07 { active(from(X)) -> from(active(X)) 1122.73/297.07 , active(from(X)) -> mark(cons(X, from(s(X)))) 1122.73/297.07 , active(cons(X1, X2)) -> cons(active(X1), X2) 1122.73/297.07 , active(s(X)) -> s(active(X)) 1122.73/297.07 , active(2ndspos(X1, X2)) -> 2ndspos(X1, active(X2)) 1122.73/297.07 , active(2ndspos(X1, X2)) -> 2ndspos(active(X1), X2) 1122.73/297.07 , active(2ndspos(s(N), cons(X, Z))) -> 1122.73/297.07 mark(2ndspos(s(N), cons2(X, Z))) 1122.73/297.07 , active(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.07 mark(rcons(posrecip(Y), 2ndsneg(N, Z))) 1122.73/297.07 , active(2ndspos(0(), Z)) -> mark(rnil()) 1122.73/297.07 , active(cons2(X1, X2)) -> cons2(X1, active(X2)) 1122.73/297.07 , active(rcons(X1, X2)) -> rcons(X1, active(X2)) 1122.73/297.07 , active(rcons(X1, X2)) -> rcons(active(X1), X2) 1122.73/297.07 , active(posrecip(X)) -> posrecip(active(X)) 1122.73/297.07 , active(2ndsneg(X1, X2)) -> 2ndsneg(X1, active(X2)) 1122.73/297.07 , active(2ndsneg(X1, X2)) -> 2ndsneg(active(X1), X2) 1122.73/297.07 , active(2ndsneg(s(N), cons(X, Z))) -> 1122.73/297.07 mark(2ndsneg(s(N), cons2(X, Z))) 1122.73/297.07 , active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.08 mark(rcons(negrecip(Y), 2ndspos(N, Z))) 1122.73/297.08 , active(2ndsneg(0(), Z)) -> mark(rnil()) 1122.73/297.08 , active(negrecip(X)) -> negrecip(active(X)) 1122.73/297.08 , active(pi(X)) -> mark(2ndspos(X, from(0()))) 1122.73/297.08 , active(pi(X)) -> pi(active(X)) 1122.73/297.08 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1122.73/297.08 , active(plus(X1, X2)) -> plus(active(X1), X2) 1122.73/297.08 , active(plus(s(X), Y)) -> mark(s(plus(X, Y))) 1122.73/297.08 , active(plus(0(), Y)) -> mark(Y) 1122.73/297.08 , active(times(X1, X2)) -> times(X1, active(X2)) 1122.73/297.08 , active(times(X1, X2)) -> times(active(X1), X2) 1122.73/297.08 , active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) 1122.73/297.08 , active(times(0(), Y)) -> mark(0()) 1122.73/297.08 , active(square(X)) -> mark(times(X, X)) 1122.73/297.08 , active(square(X)) -> square(active(X)) 1122.73/297.08 , from(mark(X)) -> mark(from(X)) 1122.73/297.08 , from(ok(X)) -> ok(from(X)) 1122.73/297.08 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1122.73/297.08 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1122.73/297.08 , s(mark(X)) -> mark(s(X)) 1122.73/297.08 , s(ok(X)) -> ok(s(X)) 1122.73/297.08 , 2ndspos(X1, mark(X2)) -> mark(2ndspos(X1, X2)) 1122.73/297.08 , 2ndspos(mark(X1), X2) -> mark(2ndspos(X1, X2)) 1122.73/297.08 , 2ndspos(ok(X1), ok(X2)) -> ok(2ndspos(X1, X2)) 1122.73/297.08 , cons2(X1, mark(X2)) -> mark(cons2(X1, X2)) 1122.73/297.08 , cons2(ok(X1), ok(X2)) -> ok(cons2(X1, X2)) 1122.73/297.08 , rcons(X1, mark(X2)) -> mark(rcons(X1, X2)) 1122.73/297.08 , rcons(mark(X1), X2) -> mark(rcons(X1, X2)) 1122.73/297.08 , rcons(ok(X1), ok(X2)) -> ok(rcons(X1, X2)) 1122.73/297.08 , posrecip(mark(X)) -> mark(posrecip(X)) 1122.73/297.08 , posrecip(ok(X)) -> ok(posrecip(X)) 1122.73/297.08 , 2ndsneg(X1, mark(X2)) -> mark(2ndsneg(X1, X2)) 1122.73/297.08 , 2ndsneg(mark(X1), X2) -> mark(2ndsneg(X1, X2)) 1122.73/297.08 , 2ndsneg(ok(X1), ok(X2)) -> ok(2ndsneg(X1, X2)) 1122.73/297.08 , negrecip(mark(X)) -> mark(negrecip(X)) 1122.73/297.08 , negrecip(ok(X)) -> ok(negrecip(X)) 1122.73/297.08 , pi(mark(X)) -> mark(pi(X)) 1122.73/297.08 , pi(ok(X)) -> ok(pi(X)) 1122.73/297.08 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1122.73/297.08 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1122.73/297.08 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1122.73/297.08 , times(X1, mark(X2)) -> mark(times(X1, X2)) 1122.73/297.08 , times(mark(X1), X2) -> mark(times(X1, X2)) 1122.73/297.08 , times(ok(X1), ok(X2)) -> ok(times(X1, X2)) 1122.73/297.08 , square(mark(X)) -> mark(square(X)) 1122.73/297.08 , square(ok(X)) -> ok(square(X)) 1122.73/297.08 , proper(from(X)) -> from(proper(X)) 1122.73/297.08 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1122.73/297.08 , proper(s(X)) -> s(proper(X)) 1122.73/297.08 , proper(2ndspos(X1, X2)) -> 2ndspos(proper(X1), proper(X2)) 1122.73/297.08 , proper(0()) -> ok(0()) 1122.73/297.08 , proper(rnil()) -> ok(rnil()) 1122.73/297.08 , proper(cons2(X1, X2)) -> cons2(proper(X1), proper(X2)) 1122.73/297.08 , proper(rcons(X1, X2)) -> rcons(proper(X1), proper(X2)) 1122.73/297.08 , proper(posrecip(X)) -> posrecip(proper(X)) 1122.73/297.08 , proper(2ndsneg(X1, X2)) -> 2ndsneg(proper(X1), proper(X2)) 1122.73/297.08 , proper(negrecip(X)) -> negrecip(proper(X)) 1122.73/297.08 , proper(pi(X)) -> pi(proper(X)) 1122.73/297.08 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1122.73/297.08 , proper(times(X1, X2)) -> times(proper(X1), proper(X2)) 1122.73/297.08 , proper(square(X)) -> square(proper(X)) 1122.73/297.08 , proper(nil()) -> ok(nil()) 1122.73/297.08 , top(mark(X)) -> top(proper(X)) 1122.73/297.08 , top(ok(X)) -> top(active(X)) } 1122.73/297.08 Obligation: 1122.73/297.08 runtime complexity 1122.73/297.08 Answer: 1122.73/297.08 MAYBE 1122.73/297.08 1122.73/297.08 Consider the dependency graph: 1122.73/297.08 1122.73/297.08 1: active^#(from(X)) -> c_1(from^#(active(X))) 1122.73/297.08 -->_1 from^#(ok(X)) -> c_33(from^#(X)) :33 1122.73/297.08 -->_1 from^#(mark(X)) -> c_32(from^#(X)) :32 1122.73/297.08 1122.73/297.08 2: active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1122.73/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) :35 1122.73/297.08 -->_1 cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) :34 1122.73/297.08 1122.73/297.08 3: active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1122.73/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) :35 1122.73/297.08 -->_1 cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) :34 1122.73/297.08 1122.73/297.08 4: active^#(s(X)) -> c_4(s^#(active(X))) 1122.73/297.08 -->_1 s^#(ok(X)) -> c_37(s^#(X)) :37 1122.73/297.08 -->_1 s^#(mark(X)) -> c_36(s^#(X)) :36 1122.73/297.08 1122.73/297.08 5: active^#(2ndspos(X1, X2)) -> c_5(2ndspos^#(X1, active(X2))) 1122.73/297.08 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.08 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.08 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.08 1122.73/297.08 6: active^#(2ndspos(X1, X2)) -> c_6(2ndspos^#(active(X1), X2)) 1122.73/297.08 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.08 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.08 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.08 1122.73/297.08 7: active^#(2ndspos(s(N), cons(X, Z))) -> 1122.73/297.08 c_7(2ndspos^#(s(N), cons2(X, Z))) 1122.73/297.08 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.08 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.08 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.08 1122.73/297.08 8: active^#(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.08 c_8(rcons^#(posrecip(Y), 2ndsneg(N, Z))) 1122.73/297.08 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.08 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.08 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.08 1122.73/297.08 9: active^#(2ndspos(0(), Z)) -> c_9() 1122.73/297.08 1122.73/297.08 10: active^#(cons2(X1, X2)) -> c_10(cons2^#(X1, active(X2))) 1122.73/297.08 -->_1 cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) :45 1122.73/297.08 -->_1 cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) :44 1122.73/297.08 1122.73/297.08 11: active^#(rcons(X1, X2)) -> c_11(rcons^#(X1, active(X2))) 1122.73/297.08 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.08 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.08 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.08 1122.73/297.08 12: active^#(rcons(X1, X2)) -> c_12(rcons^#(active(X1), X2)) 1122.73/297.08 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.08 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.08 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.08 1122.73/297.08 13: active^#(posrecip(X)) -> c_13(posrecip^#(active(X))) 1122.73/297.08 -->_1 posrecip^#(ok(X)) -> c_47(posrecip^#(X)) :47 1122.73/297.08 -->_1 posrecip^#(mark(X)) -> c_46(posrecip^#(X)) :46 1122.73/297.08 1122.73/297.08 14: active^#(2ndsneg(X1, X2)) -> c_14(2ndsneg^#(X1, active(X2))) 1122.73/297.08 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.08 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.08 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.08 1122.73/297.08 15: active^#(2ndsneg(X1, X2)) -> c_15(2ndsneg^#(active(X1), X2)) 1122.73/297.08 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.08 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.08 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.08 1122.73/297.08 16: active^#(2ndsneg(s(N), cons(X, Z))) -> 1122.73/297.08 c_16(2ndsneg^#(s(N), cons2(X, Z))) 1122.73/297.08 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.08 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.08 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.08 1122.73/297.08 17: active^#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.08 c_17(rcons^#(negrecip(Y), 2ndspos(N, Z))) 1122.73/297.08 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.08 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.08 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.08 1122.73/297.08 18: active^#(2ndsneg(0(), Z)) -> c_18() 1122.73/297.08 1122.73/297.08 19: active^#(negrecip(X)) -> c_19(negrecip^#(active(X))) 1122.73/297.08 -->_1 negrecip^#(ok(X)) -> c_52(negrecip^#(X)) :52 1122.73/297.08 -->_1 negrecip^#(mark(X)) -> c_51(negrecip^#(X)) :51 1122.73/297.08 1122.73/297.08 20: active^#(pi(X)) -> c_20(2ndspos^#(X, from(0()))) 1122.73/297.08 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.08 1122.73/297.08 21: active^#(pi(X)) -> c_21(pi^#(active(X))) 1122.73/297.08 -->_1 pi^#(ok(X)) -> c_54(pi^#(X)) :54 1122.73/297.08 -->_1 pi^#(mark(X)) -> c_53(pi^#(X)) :53 1122.73/297.08 1122.73/297.08 22: active^#(plus(X1, X2)) -> c_22(plus^#(X1, active(X2))) 1122.73/297.08 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.08 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.08 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.08 1122.73/297.08 23: active^#(plus(X1, X2)) -> c_23(plus^#(active(X1), X2)) 1122.73/297.08 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.08 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.08 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.08 1122.73/297.08 24: active^#(plus(s(X), Y)) -> c_24(s^#(plus(X, Y))) 1122.73/297.08 -->_1 s^#(ok(X)) -> c_37(s^#(X)) :37 1122.73/297.08 -->_1 s^#(mark(X)) -> c_36(s^#(X)) :36 1122.73/297.08 1122.73/297.08 25: active^#(plus(0(), Y)) -> c_25(Y) 1122.73/297.08 -->_1 top^#(ok(X)) -> c_80(top^#(active(X))) :80 1122.73/297.08 -->_1 top^#(mark(X)) -> c_79(top^#(proper(X))) :79 1122.73/297.08 -->_1 proper^#(square(X)) -> c_77(square^#(proper(X))) :77 1122.73/297.08 -->_1 proper^#(times(X1, X2)) -> 1122.73/297.08 c_76(times^#(proper(X1), proper(X2))) :76 1122.73/297.08 -->_1 proper^#(plus(X1, X2)) -> 1122.73/297.08 c_75(plus^#(proper(X1), proper(X2))) :75 1122.73/297.08 -->_1 proper^#(pi(X)) -> c_74(pi^#(proper(X))) :74 1122.73/297.08 -->_1 proper^#(negrecip(X)) -> c_73(negrecip^#(proper(X))) :73 1122.73/297.08 -->_1 proper^#(2ndsneg(X1, X2)) -> 1122.73/297.08 c_72(2ndsneg^#(proper(X1), proper(X2))) :72 1122.73/297.08 -->_1 proper^#(posrecip(X)) -> c_71(posrecip^#(proper(X))) :71 1122.73/297.08 -->_1 proper^#(rcons(X1, X2)) -> 1122.73/297.08 c_70(rcons^#(proper(X1), proper(X2))) :70 1122.73/297.08 -->_1 proper^#(cons2(X1, X2)) -> 1122.73/297.08 c_69(cons2^#(proper(X1), proper(X2))) :69 1122.73/297.08 -->_1 proper^#(2ndspos(X1, X2)) -> 1122.73/297.08 c_66(2ndspos^#(proper(X1), proper(X2))) :66 1122.73/297.08 -->_1 proper^#(s(X)) -> c_65(s^#(proper(X))) :65 1122.73/297.08 -->_1 proper^#(cons(X1, X2)) -> 1122.73/297.08 c_64(cons^#(proper(X1), proper(X2))) :64 1122.73/297.08 -->_1 proper^#(from(X)) -> c_63(from^#(proper(X))) :63 1122.73/297.08 -->_1 square^#(ok(X)) -> c_62(square^#(X)) :62 1122.73/297.08 -->_1 square^#(mark(X)) -> c_61(square^#(X)) :61 1122.73/297.08 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.08 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.08 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.08 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.08 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.08 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.08 -->_1 pi^#(ok(X)) -> c_54(pi^#(X)) :54 1122.73/297.08 -->_1 pi^#(mark(X)) -> c_53(pi^#(X)) :53 1122.73/297.08 -->_1 negrecip^#(ok(X)) -> c_52(negrecip^#(X)) :52 1122.73/297.08 -->_1 negrecip^#(mark(X)) -> c_51(negrecip^#(X)) :51 1122.73/297.08 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.08 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.08 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.08 -->_1 posrecip^#(ok(X)) -> c_47(posrecip^#(X)) :47 1122.73/297.08 -->_1 posrecip^#(mark(X)) -> c_46(posrecip^#(X)) :46 1122.73/297.08 -->_1 cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) :45 1122.73/297.08 -->_1 cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) :44 1122.73/297.08 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.08 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.08 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.08 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.08 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.08 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.08 -->_1 s^#(ok(X)) -> c_37(s^#(X)) :37 1122.73/297.08 -->_1 s^#(mark(X)) -> c_36(s^#(X)) :36 1122.73/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) :35 1122.73/297.08 -->_1 cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) :34 1122.73/297.08 -->_1 from^#(ok(X)) -> c_33(from^#(X)) :33 1122.73/297.08 -->_1 from^#(mark(X)) -> c_32(from^#(X)) :32 1122.73/297.08 -->_1 active^#(square(X)) -> c_31(square^#(active(X))) :31 1122.73/297.08 -->_1 active^#(square(X)) -> c_30(times^#(X, X)) :30 1122.73/297.08 -->_1 active^#(times(s(X), Y)) -> c_28(plus^#(Y, times(X, Y))) :28 1122.73/297.08 -->_1 active^#(times(X1, X2)) -> c_27(times^#(active(X1), X2)) :27 1122.73/297.08 -->_1 active^#(times(X1, X2)) -> c_26(times^#(X1, active(X2))) :26 1122.73/297.08 -->_1 proper^#(nil()) -> c_78() :78 1122.73/297.08 -->_1 proper^#(rnil()) -> c_68() :68 1122.73/297.08 -->_1 proper^#(0()) -> c_67() :67 1122.73/297.08 -->_1 active^#(times(0(), Y)) -> c_29() :29 1122.73/297.08 -->_1 active^#(plus(0(), Y)) -> c_25(Y) :25 1122.73/297.08 -->_1 active^#(plus(s(X), Y)) -> c_24(s^#(plus(X, Y))) :24 1122.73/297.08 -->_1 active^#(plus(X1, X2)) -> c_23(plus^#(active(X1), X2)) :23 1122.73/297.08 -->_1 active^#(plus(X1, X2)) -> c_22(plus^#(X1, active(X2))) :22 1122.73/297.08 -->_1 active^#(pi(X)) -> c_21(pi^#(active(X))) :21 1122.73/297.08 -->_1 active^#(pi(X)) -> c_20(2ndspos^#(X, from(0()))) :20 1122.73/297.08 -->_1 active^#(negrecip(X)) -> c_19(negrecip^#(active(X))) :19 1122.73/297.08 -->_1 active^#(2ndsneg(0(), Z)) -> c_18() :18 1122.73/297.08 -->_1 active^#(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.08 c_17(rcons^#(negrecip(Y), 2ndspos(N, Z))) :17 1122.73/297.08 -->_1 active^#(2ndsneg(s(N), cons(X, Z))) -> 1122.73/297.08 c_16(2ndsneg^#(s(N), cons2(X, Z))) :16 1122.73/297.08 -->_1 active^#(2ndsneg(X1, X2)) -> 1122.73/297.08 c_15(2ndsneg^#(active(X1), X2)) :15 1122.73/297.08 -->_1 active^#(2ndsneg(X1, X2)) -> 1122.73/297.08 c_14(2ndsneg^#(X1, active(X2))) :14 1122.73/297.08 -->_1 active^#(posrecip(X)) -> c_13(posrecip^#(active(X))) :13 1122.73/297.08 -->_1 active^#(rcons(X1, X2)) -> c_12(rcons^#(active(X1), X2)) :12 1122.73/297.08 -->_1 active^#(rcons(X1, X2)) -> c_11(rcons^#(X1, active(X2))) :11 1122.73/297.08 -->_1 active^#(cons2(X1, X2)) -> c_10(cons2^#(X1, active(X2))) :10 1122.73/297.08 -->_1 active^#(2ndspos(0(), Z)) -> c_9() :9 1122.73/297.08 -->_1 active^#(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.08 c_8(rcons^#(posrecip(Y), 2ndsneg(N, Z))) :8 1122.73/297.08 -->_1 active^#(2ndspos(s(N), cons(X, Z))) -> 1122.73/297.08 c_7(2ndspos^#(s(N), cons2(X, Z))) :7 1122.73/297.08 -->_1 active^#(2ndspos(X1, X2)) -> 1122.73/297.08 c_6(2ndspos^#(active(X1), X2)) :6 1122.73/297.08 -->_1 active^#(2ndspos(X1, X2)) -> 1122.73/297.08 c_5(2ndspos^#(X1, active(X2))) :5 1122.73/297.08 -->_1 active^#(s(X)) -> c_4(s^#(active(X))) :4 1122.73/297.08 -->_1 active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) :3 1122.73/297.08 -->_1 active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) :2 1122.73/297.08 -->_1 active^#(from(X)) -> c_1(from^#(active(X))) :1 1122.73/297.08 1122.73/297.08 26: active^#(times(X1, X2)) -> c_26(times^#(X1, active(X2))) 1122.73/297.08 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.08 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.08 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.08 1122.73/297.08 27: active^#(times(X1, X2)) -> c_27(times^#(active(X1), X2)) 1122.73/297.08 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.08 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.08 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.08 1122.73/297.08 28: active^#(times(s(X), Y)) -> c_28(plus^#(Y, times(X, Y))) 1122.73/297.08 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.08 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.08 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.08 1122.73/297.08 29: active^#(times(0(), Y)) -> c_29() 1122.73/297.08 1122.73/297.08 30: active^#(square(X)) -> c_30(times^#(X, X)) 1122.73/297.08 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.08 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.08 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.08 1122.73/297.08 31: active^#(square(X)) -> c_31(square^#(active(X))) 1122.73/297.08 -->_1 square^#(ok(X)) -> c_62(square^#(X)) :62 1122.73/297.08 -->_1 square^#(mark(X)) -> c_61(square^#(X)) :61 1122.73/297.08 1122.73/297.08 32: from^#(mark(X)) -> c_32(from^#(X)) 1122.73/297.08 -->_1 from^#(ok(X)) -> c_33(from^#(X)) :33 1122.73/297.08 -->_1 from^#(mark(X)) -> c_32(from^#(X)) :32 1122.73/297.08 1122.73/297.08 33: from^#(ok(X)) -> c_33(from^#(X)) 1122.73/297.08 -->_1 from^#(ok(X)) -> c_33(from^#(X)) :33 1122.73/297.08 -->_1 from^#(mark(X)) -> c_32(from^#(X)) :32 1122.73/297.08 1122.73/297.08 34: cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) 1122.73/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) :35 1122.73/297.08 -->_1 cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) :34 1122.73/297.08 1122.73/297.08 35: cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) 1122.73/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) :35 1122.73/297.08 -->_1 cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) :34 1122.73/297.08 1122.73/297.08 36: s^#(mark(X)) -> c_36(s^#(X)) 1122.73/297.08 -->_1 s^#(ok(X)) -> c_37(s^#(X)) :37 1122.73/297.08 -->_1 s^#(mark(X)) -> c_36(s^#(X)) :36 1122.73/297.08 1122.73/297.08 37: s^#(ok(X)) -> c_37(s^#(X)) 1122.73/297.08 -->_1 s^#(ok(X)) -> c_37(s^#(X)) :37 1122.73/297.08 -->_1 s^#(mark(X)) -> c_36(s^#(X)) :36 1122.73/297.09 1122.73/297.09 38: 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) 1122.73/297.09 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.09 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.09 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.09 1122.73/297.09 39: 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) 1122.73/297.09 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.09 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.09 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.09 1122.73/297.09 40: 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) 1122.73/297.09 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.09 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.09 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.09 1122.73/297.09 41: rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) 1122.73/297.09 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.09 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.09 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.09 1122.73/297.09 42: rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) 1122.73/297.09 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.09 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.09 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.09 1122.73/297.09 43: rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) 1122.73/297.09 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.09 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.09 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.09 1122.73/297.09 44: cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) 1122.73/297.09 -->_1 cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) :45 1122.73/297.09 -->_1 cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) :44 1122.73/297.09 1122.73/297.09 45: cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) 1122.73/297.09 -->_1 cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) :45 1122.73/297.09 -->_1 cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) :44 1122.73/297.09 1122.73/297.09 46: posrecip^#(mark(X)) -> c_46(posrecip^#(X)) 1122.73/297.09 -->_1 posrecip^#(ok(X)) -> c_47(posrecip^#(X)) :47 1122.73/297.09 -->_1 posrecip^#(mark(X)) -> c_46(posrecip^#(X)) :46 1122.73/297.09 1122.73/297.09 47: posrecip^#(ok(X)) -> c_47(posrecip^#(X)) 1122.73/297.09 -->_1 posrecip^#(ok(X)) -> c_47(posrecip^#(X)) :47 1122.73/297.09 -->_1 posrecip^#(mark(X)) -> c_46(posrecip^#(X)) :46 1122.73/297.09 1122.73/297.09 48: 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) 1122.73/297.09 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.09 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.09 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.09 1122.73/297.09 49: 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) 1122.73/297.09 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.09 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.09 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.09 1122.73/297.09 50: 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) 1122.73/297.09 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.09 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.09 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.09 1122.73/297.09 51: negrecip^#(mark(X)) -> c_51(negrecip^#(X)) 1122.73/297.09 -->_1 negrecip^#(ok(X)) -> c_52(negrecip^#(X)) :52 1122.73/297.09 -->_1 negrecip^#(mark(X)) -> c_51(negrecip^#(X)) :51 1122.73/297.09 1122.73/297.09 52: negrecip^#(ok(X)) -> c_52(negrecip^#(X)) 1122.73/297.09 -->_1 negrecip^#(ok(X)) -> c_52(negrecip^#(X)) :52 1122.73/297.09 -->_1 negrecip^#(mark(X)) -> c_51(negrecip^#(X)) :51 1122.73/297.09 1122.73/297.09 53: pi^#(mark(X)) -> c_53(pi^#(X)) 1122.73/297.09 -->_1 pi^#(ok(X)) -> c_54(pi^#(X)) :54 1122.73/297.09 -->_1 pi^#(mark(X)) -> c_53(pi^#(X)) :53 1122.73/297.09 1122.73/297.09 54: pi^#(ok(X)) -> c_54(pi^#(X)) 1122.73/297.09 -->_1 pi^#(ok(X)) -> c_54(pi^#(X)) :54 1122.73/297.09 -->_1 pi^#(mark(X)) -> c_53(pi^#(X)) :53 1122.73/297.09 1122.73/297.09 55: plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) 1122.73/297.09 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.09 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.09 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.09 1122.73/297.09 56: plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) 1122.73/297.09 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.09 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.09 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.09 1122.73/297.09 57: plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) 1122.73/297.09 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.09 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.09 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.09 1122.73/297.09 58: times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) 1122.73/297.09 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.09 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.09 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.09 1122.73/297.09 59: times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) 1122.73/297.09 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.09 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.09 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.09 1122.73/297.09 60: times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) 1122.73/297.09 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.09 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.09 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.09 1122.73/297.09 61: square^#(mark(X)) -> c_61(square^#(X)) 1122.73/297.09 -->_1 square^#(ok(X)) -> c_62(square^#(X)) :62 1122.73/297.09 -->_1 square^#(mark(X)) -> c_61(square^#(X)) :61 1122.73/297.09 1122.73/297.09 62: square^#(ok(X)) -> c_62(square^#(X)) 1122.73/297.09 -->_1 square^#(ok(X)) -> c_62(square^#(X)) :62 1122.73/297.09 -->_1 square^#(mark(X)) -> c_61(square^#(X)) :61 1122.73/297.09 1122.73/297.09 63: proper^#(from(X)) -> c_63(from^#(proper(X))) 1122.73/297.09 -->_1 from^#(ok(X)) -> c_33(from^#(X)) :33 1122.73/297.09 -->_1 from^#(mark(X)) -> c_32(from^#(X)) :32 1122.73/297.09 1122.73/297.09 64: proper^#(cons(X1, X2)) -> c_64(cons^#(proper(X1), proper(X2))) 1122.73/297.09 -->_1 cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) :35 1122.73/297.09 -->_1 cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) :34 1122.73/297.09 1122.73/297.09 65: proper^#(s(X)) -> c_65(s^#(proper(X))) 1122.73/297.09 -->_1 s^#(ok(X)) -> c_37(s^#(X)) :37 1122.73/297.09 -->_1 s^#(mark(X)) -> c_36(s^#(X)) :36 1122.73/297.09 1122.73/297.09 66: proper^#(2ndspos(X1, X2)) -> 1122.73/297.09 c_66(2ndspos^#(proper(X1), proper(X2))) 1122.73/297.09 -->_1 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) :40 1122.73/297.09 -->_1 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) :39 1122.73/297.09 -->_1 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) :38 1122.73/297.09 1122.73/297.09 67: proper^#(0()) -> c_67() 1122.73/297.09 1122.73/297.09 68: proper^#(rnil()) -> c_68() 1122.73/297.09 1122.73/297.09 69: proper^#(cons2(X1, X2)) -> 1122.73/297.09 c_69(cons2^#(proper(X1), proper(X2))) 1122.73/297.09 -->_1 cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) :45 1122.73/297.09 -->_1 cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) :44 1122.73/297.09 1122.73/297.09 70: proper^#(rcons(X1, X2)) -> 1122.73/297.09 c_70(rcons^#(proper(X1), proper(X2))) 1122.73/297.09 -->_1 rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) :43 1122.73/297.09 -->_1 rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) :42 1122.73/297.09 -->_1 rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) :41 1122.73/297.09 1122.73/297.09 71: proper^#(posrecip(X)) -> c_71(posrecip^#(proper(X))) 1122.73/297.09 -->_1 posrecip^#(ok(X)) -> c_47(posrecip^#(X)) :47 1122.73/297.09 -->_1 posrecip^#(mark(X)) -> c_46(posrecip^#(X)) :46 1122.73/297.09 1122.73/297.09 72: proper^#(2ndsneg(X1, X2)) -> 1122.73/297.09 c_72(2ndsneg^#(proper(X1), proper(X2))) 1122.73/297.09 -->_1 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) :50 1122.73/297.09 -->_1 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) :49 1122.73/297.09 -->_1 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) :48 1122.73/297.09 1122.73/297.09 73: proper^#(negrecip(X)) -> c_73(negrecip^#(proper(X))) 1122.73/297.09 -->_1 negrecip^#(ok(X)) -> c_52(negrecip^#(X)) :52 1122.73/297.09 -->_1 negrecip^#(mark(X)) -> c_51(negrecip^#(X)) :51 1122.73/297.09 1122.73/297.09 74: proper^#(pi(X)) -> c_74(pi^#(proper(X))) 1122.73/297.09 -->_1 pi^#(ok(X)) -> c_54(pi^#(X)) :54 1122.73/297.09 -->_1 pi^#(mark(X)) -> c_53(pi^#(X)) :53 1122.73/297.09 1122.73/297.09 75: proper^#(plus(X1, X2)) -> c_75(plus^#(proper(X1), proper(X2))) 1122.73/297.09 -->_1 plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) :57 1122.73/297.09 -->_1 plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) :56 1122.73/297.09 -->_1 plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) :55 1122.73/297.09 1122.73/297.09 76: proper^#(times(X1, X2)) -> 1122.73/297.09 c_76(times^#(proper(X1), proper(X2))) 1122.73/297.09 -->_1 times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) :60 1122.73/297.09 -->_1 times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) :59 1122.73/297.09 -->_1 times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) :58 1122.73/297.09 1122.73/297.09 77: proper^#(square(X)) -> c_77(square^#(proper(X))) 1122.73/297.09 -->_1 square^#(ok(X)) -> c_62(square^#(X)) :62 1122.73/297.09 -->_1 square^#(mark(X)) -> c_61(square^#(X)) :61 1122.73/297.09 1122.73/297.09 78: proper^#(nil()) -> c_78() 1122.73/297.09 1122.73/297.09 79: top^#(mark(X)) -> c_79(top^#(proper(X))) 1122.73/297.09 -->_1 top^#(ok(X)) -> c_80(top^#(active(X))) :80 1122.73/297.09 -->_1 top^#(mark(X)) -> c_79(top^#(proper(X))) :79 1122.73/297.09 1122.73/297.09 80: top^#(ok(X)) -> c_80(top^#(active(X))) 1122.73/297.09 -->_1 top^#(ok(X)) -> c_80(top^#(active(X))) :80 1122.73/297.09 -->_1 top^#(mark(X)) -> c_79(top^#(proper(X))) :79 1122.73/297.09 1122.73/297.09 1122.73/297.09 Only the nodes 1122.73/297.09 {32,33,34,35,36,37,38,40,39,41,43,42,44,45,46,47,48,50,49,51,52,53,54,55,57,56,58,60,59,61,62,67,68,78,79,80} 1122.73/297.09 are reachable from nodes 1122.73/297.09 {32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,67,68,78,79,80} 1122.73/297.09 that start derivation from marked basic terms. The nodes not 1122.73/297.09 reachable are removed from the problem. 1122.73/297.09 1122.73/297.09 We are left with following problem, upon which TcT provides the 1122.73/297.09 certificate MAYBE. 1122.73/297.09 1122.73/297.09 Strict DPs: 1122.73/297.09 { from^#(mark(X)) -> c_32(from^#(X)) 1122.73/297.09 , from^#(ok(X)) -> c_33(from^#(X)) 1122.73/297.09 , cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) 1122.73/297.09 , cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) 1122.73/297.09 , s^#(mark(X)) -> c_36(s^#(X)) 1122.73/297.09 , s^#(ok(X)) -> c_37(s^#(X)) 1122.73/297.09 , 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) 1122.73/297.09 , 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) 1122.73/297.09 , 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) 1122.73/297.09 , rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) 1122.73/297.09 , rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) 1122.73/297.09 , rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) 1122.73/297.09 , cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) 1122.73/297.09 , cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) 1122.73/297.09 , posrecip^#(mark(X)) -> c_46(posrecip^#(X)) 1122.73/297.09 , posrecip^#(ok(X)) -> c_47(posrecip^#(X)) 1122.73/297.09 , 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) 1122.73/297.09 , 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) 1122.73/297.09 , 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) 1122.73/297.09 , negrecip^#(mark(X)) -> c_51(negrecip^#(X)) 1122.73/297.09 , negrecip^#(ok(X)) -> c_52(negrecip^#(X)) 1122.73/297.09 , pi^#(mark(X)) -> c_53(pi^#(X)) 1122.73/297.09 , pi^#(ok(X)) -> c_54(pi^#(X)) 1122.73/297.09 , plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) 1122.73/297.09 , plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) 1122.73/297.09 , plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) 1122.73/297.09 , times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) 1122.73/297.09 , times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) 1122.73/297.09 , times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) 1122.73/297.09 , square^#(mark(X)) -> c_61(square^#(X)) 1122.73/297.09 , square^#(ok(X)) -> c_62(square^#(X)) 1122.73/297.09 , proper^#(0()) -> c_67() 1122.73/297.09 , proper^#(rnil()) -> c_68() 1122.73/297.10 , proper^#(nil()) -> c_78() 1122.73/297.10 , top^#(mark(X)) -> c_79(top^#(proper(X))) 1122.73/297.10 , top^#(ok(X)) -> c_80(top^#(active(X))) } 1122.73/297.10 Strict Trs: 1122.73/297.10 { active(from(X)) -> from(active(X)) 1122.73/297.10 , active(from(X)) -> mark(cons(X, from(s(X)))) 1122.73/297.10 , active(cons(X1, X2)) -> cons(active(X1), X2) 1122.73/297.10 , active(s(X)) -> s(active(X)) 1122.73/297.10 , active(2ndspos(X1, X2)) -> 2ndspos(X1, active(X2)) 1122.73/297.10 , active(2ndspos(X1, X2)) -> 2ndspos(active(X1), X2) 1122.73/297.10 , active(2ndspos(s(N), cons(X, Z))) -> 1122.73/297.10 mark(2ndspos(s(N), cons2(X, Z))) 1122.73/297.10 , active(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.10 mark(rcons(posrecip(Y), 2ndsneg(N, Z))) 1122.73/297.10 , active(2ndspos(0(), Z)) -> mark(rnil()) 1122.73/297.10 , active(cons2(X1, X2)) -> cons2(X1, active(X2)) 1122.73/297.10 , active(rcons(X1, X2)) -> rcons(X1, active(X2)) 1122.73/297.10 , active(rcons(X1, X2)) -> rcons(active(X1), X2) 1122.73/297.10 , active(posrecip(X)) -> posrecip(active(X)) 1122.73/297.10 , active(2ndsneg(X1, X2)) -> 2ndsneg(X1, active(X2)) 1122.73/297.10 , active(2ndsneg(X1, X2)) -> 2ndsneg(active(X1), X2) 1122.73/297.10 , active(2ndsneg(s(N), cons(X, Z))) -> 1122.73/297.10 mark(2ndsneg(s(N), cons2(X, Z))) 1122.73/297.10 , active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1122.73/297.10 mark(rcons(negrecip(Y), 2ndspos(N, Z))) 1122.73/297.10 , active(2ndsneg(0(), Z)) -> mark(rnil()) 1122.73/297.10 , active(negrecip(X)) -> negrecip(active(X)) 1122.73/297.10 , active(pi(X)) -> mark(2ndspos(X, from(0()))) 1122.73/297.10 , active(pi(X)) -> pi(active(X)) 1122.73/297.10 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1122.73/297.10 , active(plus(X1, X2)) -> plus(active(X1), X2) 1122.73/297.10 , active(plus(s(X), Y)) -> mark(s(plus(X, Y))) 1122.73/297.10 , active(plus(0(), Y)) -> mark(Y) 1122.73/297.10 , active(times(X1, X2)) -> times(X1, active(X2)) 1122.73/297.10 , active(times(X1, X2)) -> times(active(X1), X2) 1122.73/297.10 , active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) 1122.73/297.10 , active(times(0(), Y)) -> mark(0()) 1122.73/297.10 , active(square(X)) -> mark(times(X, X)) 1122.73/297.10 , active(square(X)) -> square(active(X)) 1122.73/297.10 , from(mark(X)) -> mark(from(X)) 1122.73/297.10 , from(ok(X)) -> ok(from(X)) 1122.73/297.10 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1122.73/297.10 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1122.73/297.10 , s(mark(X)) -> mark(s(X)) 1122.73/297.10 , s(ok(X)) -> ok(s(X)) 1122.73/297.10 , 2ndspos(X1, mark(X2)) -> mark(2ndspos(X1, X2)) 1122.73/297.10 , 2ndspos(mark(X1), X2) -> mark(2ndspos(X1, X2)) 1122.73/297.10 , 2ndspos(ok(X1), ok(X2)) -> ok(2ndspos(X1, X2)) 1122.73/297.10 , cons2(X1, mark(X2)) -> mark(cons2(X1, X2)) 1122.73/297.10 , cons2(ok(X1), ok(X2)) -> ok(cons2(X1, X2)) 1122.73/297.10 , rcons(X1, mark(X2)) -> mark(rcons(X1, X2)) 1122.73/297.10 , rcons(mark(X1), X2) -> mark(rcons(X1, X2)) 1122.73/297.10 , rcons(ok(X1), ok(X2)) -> ok(rcons(X1, X2)) 1122.73/297.10 , posrecip(mark(X)) -> mark(posrecip(X)) 1122.73/297.10 , posrecip(ok(X)) -> ok(posrecip(X)) 1122.73/297.10 , 2ndsneg(X1, mark(X2)) -> mark(2ndsneg(X1, X2)) 1122.73/297.10 , 2ndsneg(mark(X1), X2) -> mark(2ndsneg(X1, X2)) 1122.73/297.10 , 2ndsneg(ok(X1), ok(X2)) -> ok(2ndsneg(X1, X2)) 1122.73/297.10 , negrecip(mark(X)) -> mark(negrecip(X)) 1122.73/297.10 , negrecip(ok(X)) -> ok(negrecip(X)) 1122.73/297.10 , pi(mark(X)) -> mark(pi(X)) 1122.73/297.10 , pi(ok(X)) -> ok(pi(X)) 1122.73/297.10 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1122.73/297.10 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1122.73/297.10 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1122.73/297.10 , times(X1, mark(X2)) -> mark(times(X1, X2)) 1122.73/297.10 , times(mark(X1), X2) -> mark(times(X1, X2)) 1122.73/297.10 , times(ok(X1), ok(X2)) -> ok(times(X1, X2)) 1122.73/297.10 , square(mark(X)) -> mark(square(X)) 1122.73/297.10 , square(ok(X)) -> ok(square(X)) 1122.73/297.10 , proper(from(X)) -> from(proper(X)) 1122.73/297.10 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1122.73/297.10 , proper(s(X)) -> s(proper(X)) 1122.73/297.10 , proper(2ndspos(X1, X2)) -> 2ndspos(proper(X1), proper(X2)) 1122.73/297.10 , proper(0()) -> ok(0()) 1122.73/297.10 , proper(rnil()) -> ok(rnil()) 1122.73/297.10 , proper(cons2(X1, X2)) -> cons2(proper(X1), proper(X2)) 1122.73/297.10 , proper(rcons(X1, X2)) -> rcons(proper(X1), proper(X2)) 1122.73/297.10 , proper(posrecip(X)) -> posrecip(proper(X)) 1122.73/297.10 , proper(2ndsneg(X1, X2)) -> 2ndsneg(proper(X1), proper(X2)) 1122.73/297.10 , proper(negrecip(X)) -> negrecip(proper(X)) 1122.73/297.10 , proper(pi(X)) -> pi(proper(X)) 1122.73/297.10 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1122.73/297.10 , proper(times(X1, X2)) -> times(proper(X1), proper(X2)) 1122.73/297.10 , proper(square(X)) -> square(proper(X)) 1122.73/297.10 , proper(nil()) -> ok(nil()) 1122.73/297.10 , top(mark(X)) -> top(proper(X)) 1122.73/297.10 , top(ok(X)) -> top(active(X)) } 1122.73/297.10 Obligation: 1122.73/297.10 runtime complexity 1122.73/297.10 Answer: 1122.73/297.10 MAYBE 1122.73/297.10 1122.73/297.10 We estimate the number of application of {32,33,34} by applications 1122.73/297.10 of Pre({32,33,34}) = {}. Here rules are labeled as follows: 1122.73/297.10 1122.73/297.10 DPs: 1122.73/297.10 { 1: from^#(mark(X)) -> c_32(from^#(X)) 1122.73/297.10 , 2: from^#(ok(X)) -> c_33(from^#(X)) 1122.73/297.10 , 3: cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) 1122.73/297.10 , 4: cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) 1122.73/297.10 , 5: s^#(mark(X)) -> c_36(s^#(X)) 1122.73/297.10 , 6: s^#(ok(X)) -> c_37(s^#(X)) 1122.73/297.10 , 7: 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) 1122.73/297.10 , 8: 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) 1122.73/297.10 , 9: 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) 1122.73/297.10 , 10: rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) 1122.73/297.10 , 11: rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) 1122.73/297.10 , 12: rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) 1123.01/297.10 , 13: cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) 1123.01/297.10 , 14: cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) 1123.01/297.10 , 15: posrecip^#(mark(X)) -> c_46(posrecip^#(X)) 1123.01/297.10 , 16: posrecip^#(ok(X)) -> c_47(posrecip^#(X)) 1123.01/297.10 , 17: 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) 1123.01/297.10 , 18: 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) 1123.01/297.10 , 19: 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) 1123.01/297.10 , 20: negrecip^#(mark(X)) -> c_51(negrecip^#(X)) 1123.01/297.10 , 21: negrecip^#(ok(X)) -> c_52(negrecip^#(X)) 1123.01/297.10 , 22: pi^#(mark(X)) -> c_53(pi^#(X)) 1123.01/297.10 , 23: pi^#(ok(X)) -> c_54(pi^#(X)) 1123.01/297.10 , 24: plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) 1123.01/297.10 , 25: plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) 1123.01/297.10 , 26: plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) 1123.01/297.10 , 27: times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) 1123.01/297.10 , 28: times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) 1123.01/297.10 , 29: times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) 1123.01/297.10 , 30: square^#(mark(X)) -> c_61(square^#(X)) 1123.01/297.10 , 31: square^#(ok(X)) -> c_62(square^#(X)) 1123.01/297.10 , 32: proper^#(0()) -> c_67() 1123.01/297.10 , 33: proper^#(rnil()) -> c_68() 1123.01/297.10 , 34: proper^#(nil()) -> c_78() 1123.01/297.10 , 35: top^#(mark(X)) -> c_79(top^#(proper(X))) 1123.01/297.10 , 36: top^#(ok(X)) -> c_80(top^#(active(X))) } 1123.01/297.10 1123.01/297.10 We are left with following problem, upon which TcT provides the 1123.01/297.10 certificate MAYBE. 1123.01/297.10 1123.01/297.10 Strict DPs: 1123.01/297.10 { from^#(mark(X)) -> c_32(from^#(X)) 1123.01/297.10 , from^#(ok(X)) -> c_33(from^#(X)) 1123.01/297.10 , cons^#(mark(X1), X2) -> c_34(cons^#(X1, X2)) 1123.01/297.10 , cons^#(ok(X1), ok(X2)) -> c_35(cons^#(X1, X2)) 1123.01/297.10 , s^#(mark(X)) -> c_36(s^#(X)) 1123.01/297.10 , s^#(ok(X)) -> c_37(s^#(X)) 1123.01/297.10 , 2ndspos^#(X1, mark(X2)) -> c_38(2ndspos^#(X1, X2)) 1123.01/297.10 , 2ndspos^#(mark(X1), X2) -> c_39(2ndspos^#(X1, X2)) 1123.01/297.10 , 2ndspos^#(ok(X1), ok(X2)) -> c_40(2ndspos^#(X1, X2)) 1123.01/297.10 , rcons^#(X1, mark(X2)) -> c_43(rcons^#(X1, X2)) 1123.01/297.10 , rcons^#(mark(X1), X2) -> c_44(rcons^#(X1, X2)) 1123.01/297.10 , rcons^#(ok(X1), ok(X2)) -> c_45(rcons^#(X1, X2)) 1123.01/297.10 , cons2^#(X1, mark(X2)) -> c_41(cons2^#(X1, X2)) 1123.01/297.10 , cons2^#(ok(X1), ok(X2)) -> c_42(cons2^#(X1, X2)) 1123.01/297.10 , posrecip^#(mark(X)) -> c_46(posrecip^#(X)) 1123.01/297.10 , posrecip^#(ok(X)) -> c_47(posrecip^#(X)) 1123.01/297.10 , 2ndsneg^#(X1, mark(X2)) -> c_48(2ndsneg^#(X1, X2)) 1123.01/297.10 , 2ndsneg^#(mark(X1), X2) -> c_49(2ndsneg^#(X1, X2)) 1123.01/297.10 , 2ndsneg^#(ok(X1), ok(X2)) -> c_50(2ndsneg^#(X1, X2)) 1123.01/297.10 , negrecip^#(mark(X)) -> c_51(negrecip^#(X)) 1123.01/297.10 , negrecip^#(ok(X)) -> c_52(negrecip^#(X)) 1123.01/297.10 , pi^#(mark(X)) -> c_53(pi^#(X)) 1123.01/297.10 , pi^#(ok(X)) -> c_54(pi^#(X)) 1123.01/297.10 , plus^#(X1, mark(X2)) -> c_55(plus^#(X1, X2)) 1123.01/297.10 , plus^#(mark(X1), X2) -> c_56(plus^#(X1, X2)) 1123.01/297.10 , plus^#(ok(X1), ok(X2)) -> c_57(plus^#(X1, X2)) 1123.01/297.10 , times^#(X1, mark(X2)) -> c_58(times^#(X1, X2)) 1123.01/297.10 , times^#(mark(X1), X2) -> c_59(times^#(X1, X2)) 1123.01/297.10 , times^#(ok(X1), ok(X2)) -> c_60(times^#(X1, X2)) 1123.01/297.10 , square^#(mark(X)) -> c_61(square^#(X)) 1123.01/297.10 , square^#(ok(X)) -> c_62(square^#(X)) 1123.01/297.10 , top^#(mark(X)) -> c_79(top^#(proper(X))) 1123.01/297.10 , top^#(ok(X)) -> c_80(top^#(active(X))) } 1123.01/297.10 Strict Trs: 1123.01/297.10 { active(from(X)) -> from(active(X)) 1123.01/297.10 , active(from(X)) -> mark(cons(X, from(s(X)))) 1123.01/297.10 , active(cons(X1, X2)) -> cons(active(X1), X2) 1123.01/297.10 , active(s(X)) -> s(active(X)) 1123.01/297.10 , active(2ndspos(X1, X2)) -> 2ndspos(X1, active(X2)) 1123.01/297.10 , active(2ndspos(X1, X2)) -> 2ndspos(active(X1), X2) 1123.01/297.10 , active(2ndspos(s(N), cons(X, Z))) -> 1123.01/297.10 mark(2ndspos(s(N), cons2(X, Z))) 1123.01/297.10 , active(2ndspos(s(N), cons2(X, cons(Y, Z)))) -> 1123.01/297.10 mark(rcons(posrecip(Y), 2ndsneg(N, Z))) 1123.01/297.10 , active(2ndspos(0(), Z)) -> mark(rnil()) 1123.01/297.10 , active(cons2(X1, X2)) -> cons2(X1, active(X2)) 1123.01/297.10 , active(rcons(X1, X2)) -> rcons(X1, active(X2)) 1123.01/297.10 , active(rcons(X1, X2)) -> rcons(active(X1), X2) 1123.01/297.10 , active(posrecip(X)) -> posrecip(active(X)) 1123.01/297.10 , active(2ndsneg(X1, X2)) -> 2ndsneg(X1, active(X2)) 1123.01/297.10 , active(2ndsneg(X1, X2)) -> 2ndsneg(active(X1), X2) 1123.01/297.10 , active(2ndsneg(s(N), cons(X, Z))) -> 1123.01/297.10 mark(2ndsneg(s(N), cons2(X, Z))) 1123.01/297.10 , active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) -> 1123.01/297.10 mark(rcons(negrecip(Y), 2ndspos(N, Z))) 1123.01/297.10 , active(2ndsneg(0(), Z)) -> mark(rnil()) 1123.01/297.10 , active(negrecip(X)) -> negrecip(active(X)) 1123.01/297.10 , active(pi(X)) -> mark(2ndspos(X, from(0()))) 1123.01/297.10 , active(pi(X)) -> pi(active(X)) 1123.01/297.10 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1123.01/297.10 , active(plus(X1, X2)) -> plus(active(X1), X2) 1123.01/297.10 , active(plus(s(X), Y)) -> mark(s(plus(X, Y))) 1123.01/297.10 , active(plus(0(), Y)) -> mark(Y) 1123.01/297.10 , active(times(X1, X2)) -> times(X1, active(X2)) 1123.01/297.10 , active(times(X1, X2)) -> times(active(X1), X2) 1123.01/297.10 , active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))) 1123.01/297.10 , active(times(0(), Y)) -> mark(0()) 1123.01/297.10 , active(square(X)) -> mark(times(X, X)) 1123.01/297.10 , active(square(X)) -> square(active(X)) 1123.01/297.10 , from(mark(X)) -> mark(from(X)) 1123.01/297.10 , from(ok(X)) -> ok(from(X)) 1123.01/297.10 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1123.01/297.10 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1123.01/297.10 , s(mark(X)) -> mark(s(X)) 1123.01/297.10 , s(ok(X)) -> ok(s(X)) 1123.01/297.10 , 2ndspos(X1, mark(X2)) -> mark(2ndspos(X1, X2)) 1123.01/297.10 , 2ndspos(mark(X1), X2) -> mark(2ndspos(X1, X2)) 1123.01/297.10 , 2ndspos(ok(X1), ok(X2)) -> ok(2ndspos(X1, X2)) 1123.01/297.10 , cons2(X1, mark(X2)) -> mark(cons2(X1, X2)) 1123.01/297.10 , cons2(ok(X1), ok(X2)) -> ok(cons2(X1, X2)) 1123.01/297.10 , rcons(X1, mark(X2)) -> mark(rcons(X1, X2)) 1123.01/297.10 , rcons(mark(X1), X2) -> mark(rcons(X1, X2)) 1123.01/297.10 , rcons(ok(X1), ok(X2)) -> ok(rcons(X1, X2)) 1123.01/297.10 , posrecip(mark(X)) -> mark(posrecip(X)) 1123.01/297.10 , posrecip(ok(X)) -> ok(posrecip(X)) 1123.01/297.10 , 2ndsneg(X1, mark(X2)) -> mark(2ndsneg(X1, X2)) 1123.01/297.10 , 2ndsneg(mark(X1), X2) -> mark(2ndsneg(X1, X2)) 1123.01/297.10 , 2ndsneg(ok(X1), ok(X2)) -> ok(2ndsneg(X1, X2)) 1123.01/297.10 , negrecip(mark(X)) -> mark(negrecip(X)) 1123.01/297.10 , negrecip(ok(X)) -> ok(negrecip(X)) 1123.01/297.10 , pi(mark(X)) -> mark(pi(X)) 1123.01/297.10 , pi(ok(X)) -> ok(pi(X)) 1123.01/297.10 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1123.01/297.10 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1123.01/297.10 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1123.01/297.10 , times(X1, mark(X2)) -> mark(times(X1, X2)) 1123.01/297.10 , times(mark(X1), X2) -> mark(times(X1, X2)) 1123.01/297.10 , times(ok(X1), ok(X2)) -> ok(times(X1, X2)) 1123.01/297.10 , square(mark(X)) -> mark(square(X)) 1123.01/297.10 , square(ok(X)) -> ok(square(X)) 1123.01/297.10 , proper(from(X)) -> from(proper(X)) 1123.01/297.10 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1123.01/297.10 , proper(s(X)) -> s(proper(X)) 1123.01/297.10 , proper(2ndspos(X1, X2)) -> 2ndspos(proper(X1), proper(X2)) 1123.01/297.10 , proper(0()) -> ok(0()) 1123.01/297.10 , proper(rnil()) -> ok(rnil()) 1123.01/297.10 , proper(cons2(X1, X2)) -> cons2(proper(X1), proper(X2)) 1123.01/297.10 , proper(rcons(X1, X2)) -> rcons(proper(X1), proper(X2)) 1123.01/297.10 , proper(posrecip(X)) -> posrecip(proper(X)) 1123.01/297.10 , proper(2ndsneg(X1, X2)) -> 2ndsneg(proper(X1), proper(X2)) 1123.01/297.10 , proper(negrecip(X)) -> negrecip(proper(X)) 1123.01/297.10 , proper(pi(X)) -> pi(proper(X)) 1123.01/297.10 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1123.01/297.10 , proper(times(X1, X2)) -> times(proper(X1), proper(X2)) 1123.01/297.10 , proper(square(X)) -> square(proper(X)) 1123.01/297.10 , proper(nil()) -> ok(nil()) 1123.01/297.10 , top(mark(X)) -> top(proper(X)) 1123.01/297.10 , top(ok(X)) -> top(active(X)) } 1123.01/297.10 Weak DPs: 1123.01/297.10 { proper^#(0()) -> c_67() 1123.01/297.10 , proper^#(rnil()) -> c_68() 1123.01/297.10 , proper^#(nil()) -> c_78() } 1123.01/297.10 Obligation: 1123.01/297.10 runtime complexity 1123.01/297.10 Answer: 1123.01/297.10 MAYBE 1123.01/297.10 1123.01/297.10 Empty strict component of the problem is NOT empty. 1123.01/297.10 1123.01/297.10 1123.01/297.10 Arrrr.. 1123.91/298.04 EOF