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