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