MAYBE 1090.42/298.13 MAYBE 1090.42/298.13 1090.42/298.13 We are left with following problem, upon which TcT provides the 1090.42/298.13 certificate MAYBE. 1090.42/298.13 1090.42/298.13 Strict Trs: 1090.42/298.13 { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1090.42/298.13 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1090.42/298.13 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1090.42/298.13 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1090.42/298.13 , active(isNatKind(s(V1))) -> mark(U41(isNatKind(V1))) 1090.42/298.13 , active(isNatKind(plus(V1, V2))) -> mark(U31(isNatKind(V1), V2)) 1090.42/298.13 , active(isNatKind(0())) -> mark(tt()) 1090.42/298.13 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1090.42/298.13 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1090.42/298.13 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1090.42/298.13 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1090.42/298.13 , active(U15(X1, X2)) -> U15(active(X1), X2) 1090.42/298.13 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1090.42/298.13 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1090.42/298.13 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1090.42/298.13 , active(isNat(0())) -> mark(tt()) 1090.42/298.13 , active(U16(X)) -> U16(active(X)) 1090.42/298.13 , active(U16(tt())) -> mark(tt()) 1090.42/298.13 , active(U21(X1, X2)) -> U21(active(X1), X2) 1090.42/298.13 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1090.42/298.13 , active(U22(X1, X2)) -> U22(active(X1), X2) 1090.42/298.13 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1090.42/298.13 , active(U23(X)) -> U23(active(X)) 1090.42/298.13 , active(U23(tt())) -> mark(tt()) 1090.42/298.13 , active(U31(X1, X2)) -> U31(active(X1), X2) 1090.42/298.13 , active(U31(tt(), V2)) -> mark(U32(isNatKind(V2))) 1090.42/298.13 , active(U32(X)) -> U32(active(X)) 1090.42/298.13 , active(U32(tt())) -> mark(tt()) 1090.42/298.13 , active(U41(X)) -> U41(active(X)) 1090.42/298.13 , active(U41(tt())) -> mark(tt()) 1090.42/298.13 , active(U51(X1, X2)) -> U51(active(X1), X2) 1090.42/298.13 , active(U51(tt(), N)) -> mark(U52(isNatKind(N), N)) 1090.42/298.13 , active(U52(X1, X2)) -> U52(active(X1), X2) 1090.42/298.13 , active(U52(tt(), N)) -> mark(N) 1090.42/298.13 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1090.42/298.13 , active(U61(tt(), M, N)) -> mark(U62(isNatKind(M), M, N)) 1090.42/298.13 , active(U62(X1, X2, X3)) -> U62(active(X1), X2, X3) 1090.42/298.13 , active(U62(tt(), M, N)) -> mark(U63(isNat(N), M, N)) 1090.42/298.13 , active(U63(X1, X2, X3)) -> U63(active(X1), X2, X3) 1090.42/298.13 , active(U63(tt(), M, N)) -> mark(U64(isNatKind(N), M, N)) 1090.42/298.13 , active(U64(X1, X2, X3)) -> U64(active(X1), X2, X3) 1090.42/298.13 , active(U64(tt(), M, N)) -> mark(s(plus(N, M))) 1090.42/298.13 , active(s(X)) -> s(active(X)) 1090.42/298.13 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1090.42/298.13 , active(plus(X1, X2)) -> plus(active(X1), X2) 1090.42/298.13 , active(plus(N, s(M))) -> mark(U61(isNat(M), M, N)) 1090.42/298.13 , active(plus(N, 0())) -> mark(U51(isNat(N), N)) 1090.42/298.13 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1090.42/298.13 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1090.42/298.13 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1090.42/298.13 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1090.42/298.13 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1090.42/298.13 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1090.42/298.13 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1090.42/298.13 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1090.42/298.13 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1090.42/298.13 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1090.42/298.13 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1090.42/298.13 , isNat(ok(X)) -> ok(isNat(X)) 1090.42/298.13 , U16(mark(X)) -> mark(U16(X)) 1090.42/298.13 , U16(ok(X)) -> ok(U16(X)) 1090.42/298.13 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1090.42/298.13 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1090.42/298.13 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1090.42/298.13 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1090.42/298.13 , U23(mark(X)) -> mark(U23(X)) 1090.42/298.13 , U23(ok(X)) -> ok(U23(X)) 1090.42/298.13 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1090.42/298.13 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1090.42/298.13 , U32(mark(X)) -> mark(U32(X)) 1090.42/298.13 , U32(ok(X)) -> ok(U32(X)) 1090.42/298.13 , U41(mark(X)) -> mark(U41(X)) 1090.42/298.13 , U41(ok(X)) -> ok(U41(X)) 1090.42/298.13 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 1090.42/298.13 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 1090.42/298.13 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1090.42/298.13 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1090.42/298.13 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1090.42/298.13 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1090.42/298.13 , U62(mark(X1), X2, X3) -> mark(U62(X1, X2, X3)) 1090.42/298.13 , U62(ok(X1), ok(X2), ok(X3)) -> ok(U62(X1, X2, X3)) 1090.42/298.13 , U63(mark(X1), X2, X3) -> mark(U63(X1, X2, X3)) 1090.42/298.13 , U63(ok(X1), ok(X2), ok(X3)) -> ok(U63(X1, X2, X3)) 1090.42/298.13 , U64(mark(X1), X2, X3) -> mark(U64(X1, X2, X3)) 1090.42/298.13 , U64(ok(X1), ok(X2), ok(X3)) -> ok(U64(X1, X2, X3)) 1090.42/298.13 , s(mark(X)) -> mark(s(X)) 1090.42/298.13 , s(ok(X)) -> ok(s(X)) 1090.42/298.13 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1090.42/298.13 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1090.42/298.13 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1090.42/298.13 , proper(U11(X1, X2, X3)) -> 1090.42/298.13 U11(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(tt()) -> ok(tt()) 1090.42/298.13 , proper(U12(X1, X2, X3)) -> 1090.42/298.13 U12(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1090.42/298.13 , proper(U13(X1, X2, X3)) -> 1090.42/298.13 U13(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(U14(X1, X2, X3)) -> 1090.42/298.13 U14(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1090.42/298.13 , proper(isNat(X)) -> isNat(proper(X)) 1090.42/298.13 , proper(U16(X)) -> U16(proper(X)) 1090.42/298.13 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1090.42/298.13 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1090.42/298.13 , proper(U23(X)) -> U23(proper(X)) 1090.42/298.13 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1090.42/298.13 , proper(U32(X)) -> U32(proper(X)) 1090.42/298.13 , proper(U41(X)) -> U41(proper(X)) 1090.42/298.13 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 1090.42/298.13 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1090.42/298.13 , proper(U61(X1, X2, X3)) -> 1090.42/298.13 U61(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(U62(X1, X2, X3)) -> 1090.42/298.13 U62(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(U63(X1, X2, X3)) -> 1090.42/298.13 U63(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(U64(X1, X2, X3)) -> 1090.42/298.13 U64(proper(X1), proper(X2), proper(X3)) 1090.42/298.13 , proper(s(X)) -> s(proper(X)) 1090.42/298.13 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1090.42/298.13 , proper(0()) -> ok(0()) 1090.42/298.13 , top(mark(X)) -> top(proper(X)) 1090.42/298.13 , top(ok(X)) -> top(active(X)) } 1090.42/298.13 Obligation: 1090.42/298.13 runtime complexity 1090.42/298.13 Answer: 1090.42/298.13 MAYBE 1090.42/298.13 1090.42/298.13 None of the processors succeeded. 1090.42/298.13 1090.42/298.13 Details of failed attempt(s): 1090.42/298.13 ----------------------------- 1090.42/298.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1090.42/298.13 following reason: 1090.42/298.13 1090.42/298.13 Computation stopped due to timeout after 297.0 seconds. 1090.42/298.13 1090.42/298.13 2) 'Best' failed due to the following reason: 1090.42/298.13 1090.42/298.13 None of the processors succeeded. 1090.42/298.13 1090.42/298.13 Details of failed attempt(s): 1090.42/298.13 ----------------------------- 1090.42/298.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1090.42/298.13 seconds)' failed due to the following reason: 1090.42/298.13 1090.42/298.13 Computation stopped due to timeout after 148.0 seconds. 1090.42/298.13 1090.42/298.13 2) 'Best' failed due to the following reason: 1090.42/298.13 1090.42/298.13 None of the processors succeeded. 1090.42/298.13 1090.42/298.13 Details of failed attempt(s): 1090.42/298.13 ----------------------------- 1090.42/298.13 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1090.42/298.13 following reason: 1090.42/298.13 1090.42/298.13 The processor is inapplicable, reason: 1090.42/298.13 Processor only applicable for innermost runtime complexity analysis 1090.42/298.13 1090.42/298.13 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1090.42/298.13 to the following reason: 1090.42/298.13 1090.42/298.13 The processor is inapplicable, reason: 1090.42/298.13 Processor only applicable for innermost runtime complexity analysis 1090.42/298.13 1090.42/298.13 1090.42/298.13 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1090.42/298.13 failed due to the following reason: 1090.42/298.13 1090.42/298.13 None of the processors succeeded. 1090.42/298.13 1090.42/298.13 Details of failed attempt(s): 1090.42/298.13 ----------------------------- 1090.42/298.13 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1090.42/298.13 failed due to the following reason: 1090.42/298.13 1090.42/298.13 match-boundness of the problem could not be verified. 1090.42/298.13 1090.42/298.13 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1090.42/298.13 failed due to the following reason: 1090.42/298.13 1090.42/298.13 match-boundness of the problem could not be verified. 1090.42/298.13 1090.42/298.13 1090.42/298.13 1090.42/298.13 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1090.42/298.13 the following reason: 1090.42/298.13 1090.42/298.13 We add the following weak dependency pairs: 1090.42/298.13 1090.42/298.13 Strict DPs: 1090.42/298.13 { active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNatKind(V1), V1, V2)) 1090.42/298.13 , active^#(U12(X1, X2, X3)) -> c_3(U12^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U12(tt(), V1, V2)) -> c_4(U13^#(isNatKind(V2), V1, V2)) 1090.42/298.13 , active^#(isNatKind(s(V1))) -> c_5(U41^#(isNatKind(V1))) 1090.42/298.13 , active^#(isNatKind(plus(V1, V2))) -> 1090.42/298.13 c_6(U31^#(isNatKind(V1), V2)) 1090.42/298.13 , active^#(isNatKind(0())) -> c_7() 1090.42/298.13 , active^#(U13(X1, X2, X3)) -> c_8(U13^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U13(tt(), V1, V2)) -> c_9(U14^#(isNatKind(V2), V1, V2)) 1090.42/298.13 , active^#(U14(X1, X2, X3)) -> c_10(U14^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U14(tt(), V1, V2)) -> c_11(U15^#(isNat(V1), V2)) 1090.42/298.13 , active^#(U15(X1, X2)) -> c_12(U15^#(active(X1), X2)) 1090.42/298.13 , active^#(U15(tt(), V2)) -> c_13(U16^#(isNat(V2))) 1090.42/298.13 , active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1)) 1090.42/298.13 , active^#(isNat(plus(V1, V2))) -> 1090.42/298.13 c_15(U11^#(isNatKind(V1), V1, V2)) 1090.42/298.13 , active^#(isNat(0())) -> c_16() 1090.42/298.13 , active^#(U16(X)) -> c_17(U16^#(active(X))) 1090.42/298.13 , active^#(U16(tt())) -> c_18() 1090.42/298.13 , active^#(U21(X1, X2)) -> c_19(U21^#(active(X1), X2)) 1090.42/298.13 , active^#(U21(tt(), V1)) -> c_20(U22^#(isNatKind(V1), V1)) 1090.42/298.13 , active^#(U22(X1, X2)) -> c_21(U22^#(active(X1), X2)) 1090.42/298.13 , active^#(U22(tt(), V1)) -> c_22(U23^#(isNat(V1))) 1090.42/298.13 , active^#(U23(X)) -> c_23(U23^#(active(X))) 1090.42/298.13 , active^#(U23(tt())) -> c_24() 1090.42/298.13 , active^#(U31(X1, X2)) -> c_25(U31^#(active(X1), X2)) 1090.42/298.13 , active^#(U31(tt(), V2)) -> c_26(U32^#(isNatKind(V2))) 1090.42/298.13 , active^#(U32(X)) -> c_27(U32^#(active(X))) 1090.42/298.13 , active^#(U32(tt())) -> c_28() 1090.42/298.13 , active^#(U41(X)) -> c_29(U41^#(active(X))) 1090.42/298.13 , active^#(U41(tt())) -> c_30() 1090.42/298.13 , active^#(U51(X1, X2)) -> c_31(U51^#(active(X1), X2)) 1090.42/298.13 , active^#(U51(tt(), N)) -> c_32(U52^#(isNatKind(N), N)) 1090.42/298.13 , active^#(U52(X1, X2)) -> c_33(U52^#(active(X1), X2)) 1090.42/298.13 , active^#(U52(tt(), N)) -> c_34(N) 1090.42/298.13 , active^#(U61(X1, X2, X3)) -> c_35(U61^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U61(tt(), M, N)) -> c_36(U62^#(isNatKind(M), M, N)) 1090.42/298.13 , active^#(U62(X1, X2, X3)) -> c_37(U62^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U62(tt(), M, N)) -> c_38(U63^#(isNat(N), M, N)) 1090.42/298.13 , active^#(U63(X1, X2, X3)) -> c_39(U63^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U63(tt(), M, N)) -> c_40(U64^#(isNatKind(N), M, N)) 1090.42/298.13 , active^#(U64(X1, X2, X3)) -> c_41(U64^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U64(tt(), M, N)) -> c_42(s^#(plus(N, M))) 1090.42/298.13 , active^#(s(X)) -> c_43(s^#(active(X))) 1090.42/298.13 , active^#(plus(X1, X2)) -> c_44(plus^#(X1, active(X2))) 1090.42/298.13 , active^#(plus(X1, X2)) -> c_45(plus^#(active(X1), X2)) 1090.42/298.13 , active^#(plus(N, s(M))) -> c_46(U61^#(isNat(M), M, N)) 1090.42/298.13 , active^#(plus(N, 0())) -> c_47(U51^#(isNat(N), N)) 1090.42/298.13 , U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) 1090.42/298.13 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) 1090.42/298.13 , U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) 1090.42/298.13 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) 1090.42/298.13 , U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) 1090.42/298.13 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) 1090.42/298.13 , U41^#(mark(X)) -> c_72(U41^#(X)) 1090.42/298.13 , U41^#(ok(X)) -> c_73(U41^#(X)) 1090.42/298.13 , U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) 1090.42/298.13 , U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) 1090.42/298.13 , U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) 1090.42/298.13 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) 1090.42/298.13 , U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) 1090.42/298.13 , U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) 1090.42/298.13 , U16^#(mark(X)) -> c_60(U16^#(X)) 1090.42/298.13 , U16^#(ok(X)) -> c_61(U16^#(X)) 1090.42/298.13 , U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) 1090.42/298.13 , U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) 1090.42/298.13 , U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) 1090.42/298.13 , U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) 1090.42/298.13 , U23^#(mark(X)) -> c_66(U23^#(X)) 1090.42/298.13 , U23^#(ok(X)) -> c_67(U23^#(X)) 1090.42/298.13 , U32^#(mark(X)) -> c_70(U32^#(X)) 1090.42/298.13 , U32^#(ok(X)) -> c_71(U32^#(X)) 1090.42/298.13 , U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) 1090.42/298.13 , U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) 1090.42/298.13 , U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) 1090.42/298.13 , U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) 1090.42/298.13 , U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) 1090.42/298.13 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) 1090.42/298.13 , U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) 1090.42/298.13 , U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) 1090.42/298.13 , U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) 1090.42/298.13 , U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) 1090.42/298.13 , U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) 1090.42/298.13 , U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) 1090.42/298.13 , s^#(mark(X)) -> c_86(s^#(X)) 1090.42/298.13 , s^#(ok(X)) -> c_87(s^#(X)) 1090.42/298.13 , plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) 1090.42/298.13 , plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) 1090.42/298.13 , plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) 1090.42/298.13 , isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) 1090.42/298.13 , isNat^#(ok(X)) -> c_59(isNat^#(X)) 1090.42/298.13 , proper^#(U11(X1, X2, X3)) -> 1090.42/298.13 c_91(U11^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(tt()) -> c_92() 1090.42/298.13 , proper^#(U12(X1, X2, X3)) -> 1090.42/298.13 c_93(U12^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(isNatKind(X)) -> c_94(isNatKind^#(proper(X))) 1090.42/298.13 , proper^#(U13(X1, X2, X3)) -> 1090.42/298.13 c_95(U13^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(U14(X1, X2, X3)) -> 1090.42/298.13 c_96(U14^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(U15(X1, X2)) -> c_97(U15^#(proper(X1), proper(X2))) 1090.42/298.13 , proper^#(isNat(X)) -> c_98(isNat^#(proper(X))) 1090.42/298.13 , proper^#(U16(X)) -> c_99(U16^#(proper(X))) 1090.42/298.13 , proper^#(U21(X1, X2)) -> c_100(U21^#(proper(X1), proper(X2))) 1090.42/298.13 , proper^#(U22(X1, X2)) -> c_101(U22^#(proper(X1), proper(X2))) 1090.42/298.13 , proper^#(U23(X)) -> c_102(U23^#(proper(X))) 1090.42/298.13 , proper^#(U31(X1, X2)) -> c_103(U31^#(proper(X1), proper(X2))) 1090.42/298.13 , proper^#(U32(X)) -> c_104(U32^#(proper(X))) 1090.42/298.13 , proper^#(U41(X)) -> c_105(U41^#(proper(X))) 1090.42/298.13 , proper^#(U51(X1, X2)) -> c_106(U51^#(proper(X1), proper(X2))) 1090.42/298.13 , proper^#(U52(X1, X2)) -> c_107(U52^#(proper(X1), proper(X2))) 1090.42/298.13 , proper^#(U61(X1, X2, X3)) -> 1090.42/298.13 c_108(U61^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(U62(X1, X2, X3)) -> 1090.42/298.13 c_109(U62^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(U63(X1, X2, X3)) -> 1090.42/298.13 c_110(U63^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(U64(X1, X2, X3)) -> 1090.42/298.13 c_111(U64^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.13 , proper^#(s(X)) -> c_112(s^#(proper(X))) 1090.42/298.13 , proper^#(plus(X1, X2)) -> c_113(plus^#(proper(X1), proper(X2))) 1090.42/298.13 , proper^#(0()) -> c_114() 1090.42/298.13 , top^#(mark(X)) -> c_115(top^#(proper(X))) 1090.42/298.13 , top^#(ok(X)) -> c_116(top^#(active(X))) } 1090.42/298.13 1090.42/298.13 and mark the set of starting terms. 1090.42/298.13 1090.42/298.13 We are left with following problem, upon which TcT provides the 1090.42/298.13 certificate MAYBE. 1090.42/298.13 1090.42/298.13 Strict DPs: 1090.42/298.13 { active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNatKind(V1), V1, V2)) 1090.42/298.13 , active^#(U12(X1, X2, X3)) -> c_3(U12^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U12(tt(), V1, V2)) -> c_4(U13^#(isNatKind(V2), V1, V2)) 1090.42/298.13 , active^#(isNatKind(s(V1))) -> c_5(U41^#(isNatKind(V1))) 1090.42/298.13 , active^#(isNatKind(plus(V1, V2))) -> 1090.42/298.13 c_6(U31^#(isNatKind(V1), V2)) 1090.42/298.13 , active^#(isNatKind(0())) -> c_7() 1090.42/298.13 , active^#(U13(X1, X2, X3)) -> c_8(U13^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U13(tt(), V1, V2)) -> c_9(U14^#(isNatKind(V2), V1, V2)) 1090.42/298.13 , active^#(U14(X1, X2, X3)) -> c_10(U14^#(active(X1), X2, X3)) 1090.42/298.13 , active^#(U14(tt(), V1, V2)) -> c_11(U15^#(isNat(V1), V2)) 1090.42/298.13 , active^#(U15(X1, X2)) -> c_12(U15^#(active(X1), X2)) 1090.42/298.13 , active^#(U15(tt(), V2)) -> c_13(U16^#(isNat(V2))) 1090.42/298.13 , active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1)) 1090.42/298.13 , active^#(isNat(plus(V1, V2))) -> 1090.42/298.13 c_15(U11^#(isNatKind(V1), V1, V2)) 1090.42/298.13 , active^#(isNat(0())) -> c_16() 1090.42/298.13 , active^#(U16(X)) -> c_17(U16^#(active(X))) 1090.42/298.13 , active^#(U16(tt())) -> c_18() 1090.42/298.13 , active^#(U21(X1, X2)) -> c_19(U21^#(active(X1), X2)) 1090.42/298.13 , active^#(U21(tt(), V1)) -> c_20(U22^#(isNatKind(V1), V1)) 1090.42/298.13 , active^#(U22(X1, X2)) -> c_21(U22^#(active(X1), X2)) 1090.42/298.13 , active^#(U22(tt(), V1)) -> c_22(U23^#(isNat(V1))) 1090.42/298.13 , active^#(U23(X)) -> c_23(U23^#(active(X))) 1090.42/298.13 , active^#(U23(tt())) -> c_24() 1090.42/298.14 , active^#(U31(X1, X2)) -> c_25(U31^#(active(X1), X2)) 1090.42/298.14 , active^#(U31(tt(), V2)) -> c_26(U32^#(isNatKind(V2))) 1090.42/298.14 , active^#(U32(X)) -> c_27(U32^#(active(X))) 1090.42/298.14 , active^#(U32(tt())) -> c_28() 1090.42/298.14 , active^#(U41(X)) -> c_29(U41^#(active(X))) 1090.42/298.14 , active^#(U41(tt())) -> c_30() 1090.42/298.14 , active^#(U51(X1, X2)) -> c_31(U51^#(active(X1), X2)) 1090.42/298.14 , active^#(U51(tt(), N)) -> c_32(U52^#(isNatKind(N), N)) 1090.42/298.14 , active^#(U52(X1, X2)) -> c_33(U52^#(active(X1), X2)) 1090.42/298.14 , active^#(U52(tt(), N)) -> c_34(N) 1090.42/298.14 , active^#(U61(X1, X2, X3)) -> c_35(U61^#(active(X1), X2, X3)) 1090.42/298.14 , active^#(U61(tt(), M, N)) -> c_36(U62^#(isNatKind(M), M, N)) 1090.42/298.14 , active^#(U62(X1, X2, X3)) -> c_37(U62^#(active(X1), X2, X3)) 1090.42/298.14 , active^#(U62(tt(), M, N)) -> c_38(U63^#(isNat(N), M, N)) 1090.42/298.14 , active^#(U63(X1, X2, X3)) -> c_39(U63^#(active(X1), X2, X3)) 1090.42/298.14 , active^#(U63(tt(), M, N)) -> c_40(U64^#(isNatKind(N), M, N)) 1090.42/298.14 , active^#(U64(X1, X2, X3)) -> c_41(U64^#(active(X1), X2, X3)) 1090.42/298.14 , active^#(U64(tt(), M, N)) -> c_42(s^#(plus(N, M))) 1090.42/298.14 , active^#(s(X)) -> c_43(s^#(active(X))) 1090.42/298.14 , active^#(plus(X1, X2)) -> c_44(plus^#(X1, active(X2))) 1090.42/298.14 , active^#(plus(X1, X2)) -> c_45(plus^#(active(X1), X2)) 1090.42/298.14 , active^#(plus(N, s(M))) -> c_46(U61^#(isNat(M), M, N)) 1090.42/298.14 , active^#(plus(N, 0())) -> c_47(U51^#(isNat(N), N)) 1090.42/298.14 , U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) 1090.42/298.14 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) 1090.42/298.14 , U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) 1090.42/298.14 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) 1090.42/298.14 , U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) 1090.42/298.14 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) 1090.42/298.14 , U41^#(mark(X)) -> c_72(U41^#(X)) 1090.42/298.14 , U41^#(ok(X)) -> c_73(U41^#(X)) 1090.42/298.14 , U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) 1090.42/298.14 , U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) 1090.42/298.14 , U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) 1090.42/298.14 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) 1090.42/298.14 , U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) 1090.42/298.14 , U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) 1090.42/298.14 , U16^#(mark(X)) -> c_60(U16^#(X)) 1090.42/298.14 , U16^#(ok(X)) -> c_61(U16^#(X)) 1090.42/298.14 , U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) 1090.42/298.14 , U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) 1090.42/298.14 , U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) 1090.42/298.14 , U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) 1090.42/298.14 , U23^#(mark(X)) -> c_66(U23^#(X)) 1090.42/298.14 , U23^#(ok(X)) -> c_67(U23^#(X)) 1090.42/298.14 , U32^#(mark(X)) -> c_70(U32^#(X)) 1090.42/298.14 , U32^#(ok(X)) -> c_71(U32^#(X)) 1090.42/298.14 , U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) 1090.42/298.14 , U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) 1090.42/298.14 , U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) 1090.42/298.14 , U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) 1090.42/298.14 , U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) 1090.42/298.14 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) 1090.42/298.14 , U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) 1090.42/298.14 , U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) 1090.42/298.14 , U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) 1090.42/298.14 , U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) 1090.42/298.14 , U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) 1090.42/298.14 , U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) 1090.42/298.14 , s^#(mark(X)) -> c_86(s^#(X)) 1090.42/298.14 , s^#(ok(X)) -> c_87(s^#(X)) 1090.42/298.14 , plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) 1090.42/298.14 , plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) 1090.42/298.14 , plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) 1090.42/298.14 , isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) 1090.42/298.14 , isNat^#(ok(X)) -> c_59(isNat^#(X)) 1090.42/298.14 , proper^#(U11(X1, X2, X3)) -> 1090.42/298.14 c_91(U11^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(tt()) -> c_92() 1090.42/298.14 , proper^#(U12(X1, X2, X3)) -> 1090.42/298.14 c_93(U12^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(isNatKind(X)) -> c_94(isNatKind^#(proper(X))) 1090.42/298.14 , proper^#(U13(X1, X2, X3)) -> 1090.42/298.14 c_95(U13^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(U14(X1, X2, X3)) -> 1090.42/298.14 c_96(U14^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(U15(X1, X2)) -> c_97(U15^#(proper(X1), proper(X2))) 1090.42/298.14 , proper^#(isNat(X)) -> c_98(isNat^#(proper(X))) 1090.42/298.14 , proper^#(U16(X)) -> c_99(U16^#(proper(X))) 1090.42/298.14 , proper^#(U21(X1, X2)) -> c_100(U21^#(proper(X1), proper(X2))) 1090.42/298.14 , proper^#(U22(X1, X2)) -> c_101(U22^#(proper(X1), proper(X2))) 1090.42/298.14 , proper^#(U23(X)) -> c_102(U23^#(proper(X))) 1090.42/298.14 , proper^#(U31(X1, X2)) -> c_103(U31^#(proper(X1), proper(X2))) 1090.42/298.14 , proper^#(U32(X)) -> c_104(U32^#(proper(X))) 1090.42/298.14 , proper^#(U41(X)) -> c_105(U41^#(proper(X))) 1090.42/298.14 , proper^#(U51(X1, X2)) -> c_106(U51^#(proper(X1), proper(X2))) 1090.42/298.14 , proper^#(U52(X1, X2)) -> c_107(U52^#(proper(X1), proper(X2))) 1090.42/298.14 , proper^#(U61(X1, X2, X3)) -> 1090.42/298.14 c_108(U61^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(U62(X1, X2, X3)) -> 1090.42/298.14 c_109(U62^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(U63(X1, X2, X3)) -> 1090.42/298.14 c_110(U63^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(U64(X1, X2, X3)) -> 1090.42/298.14 c_111(U64^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.14 , proper^#(s(X)) -> c_112(s^#(proper(X))) 1090.42/298.14 , proper^#(plus(X1, X2)) -> c_113(plus^#(proper(X1), proper(X2))) 1090.42/298.14 , proper^#(0()) -> c_114() 1090.42/298.14 , top^#(mark(X)) -> c_115(top^#(proper(X))) 1090.42/298.14 , top^#(ok(X)) -> c_116(top^#(active(X))) } 1090.42/298.14 Strict Trs: 1090.42/298.14 { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1090.42/298.14 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1090.42/298.14 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1090.42/298.14 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1090.42/298.14 , active(isNatKind(s(V1))) -> mark(U41(isNatKind(V1))) 1090.42/298.14 , active(isNatKind(plus(V1, V2))) -> mark(U31(isNatKind(V1), V2)) 1090.42/298.14 , active(isNatKind(0())) -> mark(tt()) 1090.42/298.14 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1090.42/298.14 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1090.42/298.14 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1090.42/298.14 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1090.42/298.14 , active(U15(X1, X2)) -> U15(active(X1), X2) 1090.42/298.14 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1090.42/298.14 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1090.42/298.14 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1090.42/298.14 , active(isNat(0())) -> mark(tt()) 1090.42/298.14 , active(U16(X)) -> U16(active(X)) 1090.42/298.14 , active(U16(tt())) -> mark(tt()) 1090.42/298.14 , active(U21(X1, X2)) -> U21(active(X1), X2) 1090.42/298.14 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1090.42/298.14 , active(U22(X1, X2)) -> U22(active(X1), X2) 1090.42/298.14 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1090.42/298.14 , active(U23(X)) -> U23(active(X)) 1090.42/298.14 , active(U23(tt())) -> mark(tt()) 1090.42/298.14 , active(U31(X1, X2)) -> U31(active(X1), X2) 1090.42/298.14 , active(U31(tt(), V2)) -> mark(U32(isNatKind(V2))) 1090.42/298.14 , active(U32(X)) -> U32(active(X)) 1090.42/298.14 , active(U32(tt())) -> mark(tt()) 1090.42/298.14 , active(U41(X)) -> U41(active(X)) 1090.42/298.14 , active(U41(tt())) -> mark(tt()) 1090.42/298.14 , active(U51(X1, X2)) -> U51(active(X1), X2) 1090.42/298.14 , active(U51(tt(), N)) -> mark(U52(isNatKind(N), N)) 1090.42/298.14 , active(U52(X1, X2)) -> U52(active(X1), X2) 1090.42/298.14 , active(U52(tt(), N)) -> mark(N) 1090.42/298.14 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1090.42/298.14 , active(U61(tt(), M, N)) -> mark(U62(isNatKind(M), M, N)) 1090.42/298.14 , active(U62(X1, X2, X3)) -> U62(active(X1), X2, X3) 1090.42/298.14 , active(U62(tt(), M, N)) -> mark(U63(isNat(N), M, N)) 1090.42/298.14 , active(U63(X1, X2, X3)) -> U63(active(X1), X2, X3) 1090.42/298.14 , active(U63(tt(), M, N)) -> mark(U64(isNatKind(N), M, N)) 1090.42/298.14 , active(U64(X1, X2, X3)) -> U64(active(X1), X2, X3) 1090.42/298.14 , active(U64(tt(), M, N)) -> mark(s(plus(N, M))) 1090.42/298.14 , active(s(X)) -> s(active(X)) 1090.42/298.14 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1090.42/298.14 , active(plus(X1, X2)) -> plus(active(X1), X2) 1090.42/298.14 , active(plus(N, s(M))) -> mark(U61(isNat(M), M, N)) 1090.42/298.14 , active(plus(N, 0())) -> mark(U51(isNat(N), N)) 1090.42/298.14 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1090.42/298.14 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1090.42/298.14 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1090.42/298.14 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1090.42/298.14 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1090.42/298.14 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1090.42/298.14 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1090.42/298.14 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1090.42/298.14 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1090.42/298.14 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1090.42/298.14 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1090.42/298.14 , isNat(ok(X)) -> ok(isNat(X)) 1090.42/298.14 , U16(mark(X)) -> mark(U16(X)) 1090.42/298.14 , U16(ok(X)) -> ok(U16(X)) 1090.42/298.14 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1090.42/298.14 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1090.42/298.14 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1090.42/298.14 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1090.42/298.14 , U23(mark(X)) -> mark(U23(X)) 1090.42/298.14 , U23(ok(X)) -> ok(U23(X)) 1090.42/298.14 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1090.42/298.14 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1090.42/298.14 , U32(mark(X)) -> mark(U32(X)) 1090.42/298.14 , U32(ok(X)) -> ok(U32(X)) 1090.42/298.14 , U41(mark(X)) -> mark(U41(X)) 1090.42/298.14 , U41(ok(X)) -> ok(U41(X)) 1090.42/298.14 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 1090.42/298.14 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 1090.42/298.14 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1090.42/298.14 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1090.42/298.14 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1090.42/298.14 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1090.42/298.14 , U62(mark(X1), X2, X3) -> mark(U62(X1, X2, X3)) 1090.42/298.14 , U62(ok(X1), ok(X2), ok(X3)) -> ok(U62(X1, X2, X3)) 1090.42/298.14 , U63(mark(X1), X2, X3) -> mark(U63(X1, X2, X3)) 1090.42/298.14 , U63(ok(X1), ok(X2), ok(X3)) -> ok(U63(X1, X2, X3)) 1090.42/298.14 , U64(mark(X1), X2, X3) -> mark(U64(X1, X2, X3)) 1090.42/298.14 , U64(ok(X1), ok(X2), ok(X3)) -> ok(U64(X1, X2, X3)) 1090.42/298.14 , s(mark(X)) -> mark(s(X)) 1090.42/298.14 , s(ok(X)) -> ok(s(X)) 1090.42/298.14 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1090.42/298.14 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1090.42/298.14 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1090.42/298.14 , proper(U11(X1, X2, X3)) -> 1090.42/298.14 U11(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(tt()) -> ok(tt()) 1090.42/298.14 , proper(U12(X1, X2, X3)) -> 1090.42/298.14 U12(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1090.42/298.14 , proper(U13(X1, X2, X3)) -> 1090.42/298.14 U13(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(U14(X1, X2, X3)) -> 1090.42/298.14 U14(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1090.42/298.14 , proper(isNat(X)) -> isNat(proper(X)) 1090.42/298.14 , proper(U16(X)) -> U16(proper(X)) 1090.42/298.14 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1090.42/298.14 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1090.42/298.14 , proper(U23(X)) -> U23(proper(X)) 1090.42/298.14 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1090.42/298.14 , proper(U32(X)) -> U32(proper(X)) 1090.42/298.14 , proper(U41(X)) -> U41(proper(X)) 1090.42/298.14 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 1090.42/298.14 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1090.42/298.14 , proper(U61(X1, X2, X3)) -> 1090.42/298.14 U61(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(U62(X1, X2, X3)) -> 1090.42/298.14 U62(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(U63(X1, X2, X3)) -> 1090.42/298.14 U63(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(U64(X1, X2, X3)) -> 1090.42/298.14 U64(proper(X1), proper(X2), proper(X3)) 1090.42/298.14 , proper(s(X)) -> s(proper(X)) 1090.42/298.14 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1090.42/298.14 , proper(0()) -> ok(0()) 1090.42/298.14 , top(mark(X)) -> top(proper(X)) 1090.42/298.14 , top(ok(X)) -> top(active(X)) } 1090.42/298.14 Obligation: 1090.42/298.14 runtime complexity 1090.42/298.14 Answer: 1090.42/298.14 MAYBE 1090.42/298.14 1090.42/298.14 Consider the dependency graph: 1090.42/298.14 1090.42/298.14 1: active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) 1090.42/298.14 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) :49 1090.42/298.14 -->_1 U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) :48 1090.42/298.14 1090.42/298.14 2: active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNatKind(V1), V1, V2)) 1090.42/298.14 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) :51 1090.42/298.14 -->_1 U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) :50 1090.42/298.14 1090.42/298.14 3: active^#(U12(X1, X2, X3)) -> c_3(U12^#(active(X1), X2, X3)) 1090.42/298.14 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) :51 1090.42/298.14 -->_1 U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) :50 1090.42/298.14 1090.42/298.14 4: active^#(U12(tt(), V1, V2)) -> c_4(U13^#(isNatKind(V2), V1, V2)) 1090.42/298.14 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) :53 1090.42/298.14 -->_1 U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) :52 1090.42/298.14 1090.42/298.14 5: active^#(isNatKind(s(V1))) -> c_5(U41^#(isNatKind(V1))) 1090.42/298.14 -->_1 U41^#(ok(X)) -> c_73(U41^#(X)) :55 1090.42/298.14 -->_1 U41^#(mark(X)) -> c_72(U41^#(X)) :54 1090.42/298.14 1090.42/298.14 6: active^#(isNatKind(plus(V1, V2))) -> 1090.42/298.14 c_6(U31^#(isNatKind(V1), V2)) 1090.42/298.14 -->_1 U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) :57 1090.42/298.14 -->_1 U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) :56 1090.42/298.14 1090.42/298.14 7: active^#(isNatKind(0())) -> c_7() 1090.42/298.14 1090.42/298.14 8: active^#(U13(X1, X2, X3)) -> c_8(U13^#(active(X1), X2, X3)) 1090.42/298.14 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) :53 1090.42/298.14 -->_1 U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) :52 1090.42/298.14 1090.42/298.14 9: active^#(U13(tt(), V1, V2)) -> c_9(U14^#(isNatKind(V2), V1, V2)) 1090.42/298.14 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) :59 1090.42/298.14 -->_1 U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) :58 1090.42/298.14 1090.42/298.14 10: active^#(U14(X1, X2, X3)) -> c_10(U14^#(active(X1), X2, X3)) 1090.42/298.14 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) :59 1090.42/298.14 -->_1 U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) :58 1090.42/298.14 1090.42/298.14 11: active^#(U14(tt(), V1, V2)) -> c_11(U15^#(isNat(V1), V2)) 1090.42/298.14 -->_1 U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) :61 1090.42/298.14 -->_1 U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) :60 1090.42/298.14 1090.42/298.14 12: active^#(U15(X1, X2)) -> c_12(U15^#(active(X1), X2)) 1090.42/298.14 -->_1 U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) :61 1090.42/298.14 -->_1 U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) :60 1090.42/298.14 1090.42/298.14 13: active^#(U15(tt(), V2)) -> c_13(U16^#(isNat(V2))) 1090.42/298.14 -->_1 U16^#(ok(X)) -> c_61(U16^#(X)) :63 1090.42/298.14 -->_1 U16^#(mark(X)) -> c_60(U16^#(X)) :62 1090.42/298.14 1090.42/298.14 14: active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1)) 1090.42/298.14 -->_1 U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) :65 1090.42/298.14 -->_1 U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) :64 1090.42/298.14 1090.42/298.14 15: active^#(isNat(plus(V1, V2))) -> 1090.42/298.14 c_15(U11^#(isNatKind(V1), V1, V2)) 1090.42/298.14 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) :49 1090.42/298.14 -->_1 U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) :48 1090.42/298.14 1090.42/298.14 16: active^#(isNat(0())) -> c_16() 1090.42/298.14 1090.42/298.14 17: active^#(U16(X)) -> c_17(U16^#(active(X))) 1090.42/298.14 -->_1 U16^#(ok(X)) -> c_61(U16^#(X)) :63 1090.42/298.14 -->_1 U16^#(mark(X)) -> c_60(U16^#(X)) :62 1090.42/298.14 1090.42/298.14 18: active^#(U16(tt())) -> c_18() 1090.42/298.14 1090.42/298.14 19: active^#(U21(X1, X2)) -> c_19(U21^#(active(X1), X2)) 1090.42/298.14 -->_1 U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) :65 1090.42/298.14 -->_1 U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) :64 1090.42/298.14 1090.42/298.14 20: active^#(U21(tt(), V1)) -> c_20(U22^#(isNatKind(V1), V1)) 1090.42/298.14 -->_1 U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) :67 1090.42/298.14 -->_1 U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) :66 1090.42/298.14 1090.42/298.14 21: active^#(U22(X1, X2)) -> c_21(U22^#(active(X1), X2)) 1090.42/298.14 -->_1 U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) :67 1090.42/298.14 -->_1 U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) :66 1090.42/298.14 1090.42/298.14 22: active^#(U22(tt(), V1)) -> c_22(U23^#(isNat(V1))) 1090.42/298.14 -->_1 U23^#(ok(X)) -> c_67(U23^#(X)) :69 1090.42/298.14 -->_1 U23^#(mark(X)) -> c_66(U23^#(X)) :68 1090.42/298.14 1090.42/298.14 23: active^#(U23(X)) -> c_23(U23^#(active(X))) 1090.42/298.14 -->_1 U23^#(ok(X)) -> c_67(U23^#(X)) :69 1090.42/298.14 -->_1 U23^#(mark(X)) -> c_66(U23^#(X)) :68 1090.42/298.14 1090.42/298.14 24: active^#(U23(tt())) -> c_24() 1090.42/298.14 1090.42/298.14 25: active^#(U31(X1, X2)) -> c_25(U31^#(active(X1), X2)) 1090.42/298.14 -->_1 U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) :57 1090.42/298.14 -->_1 U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) :56 1090.42/298.14 1090.42/298.14 26: active^#(U31(tt(), V2)) -> c_26(U32^#(isNatKind(V2))) 1090.42/298.14 -->_1 U32^#(ok(X)) -> c_71(U32^#(X)) :71 1090.42/298.14 -->_1 U32^#(mark(X)) -> c_70(U32^#(X)) :70 1090.42/298.14 1090.42/298.14 27: active^#(U32(X)) -> c_27(U32^#(active(X))) 1090.42/298.14 -->_1 U32^#(ok(X)) -> c_71(U32^#(X)) :71 1090.42/298.14 -->_1 U32^#(mark(X)) -> c_70(U32^#(X)) :70 1090.42/298.14 1090.42/298.14 28: active^#(U32(tt())) -> c_28() 1090.42/298.14 1090.42/298.14 29: active^#(U41(X)) -> c_29(U41^#(active(X))) 1090.42/298.15 -->_1 U41^#(ok(X)) -> c_73(U41^#(X)) :55 1090.42/298.15 -->_1 U41^#(mark(X)) -> c_72(U41^#(X)) :54 1090.42/298.15 1090.42/298.15 30: active^#(U41(tt())) -> c_30() 1090.42/298.15 1090.42/298.15 31: active^#(U51(X1, X2)) -> c_31(U51^#(active(X1), X2)) 1090.42/298.15 -->_1 U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) :73 1090.42/298.15 -->_1 U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) :72 1090.42/298.15 1090.42/298.15 32: active^#(U51(tt(), N)) -> c_32(U52^#(isNatKind(N), N)) 1090.42/298.15 -->_1 U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) :75 1090.42/298.15 -->_1 U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) :74 1090.42/298.15 1090.42/298.15 33: active^#(U52(X1, X2)) -> c_33(U52^#(active(X1), X2)) 1090.42/298.15 -->_1 U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) :75 1090.42/298.15 -->_1 U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) :74 1090.42/298.15 1090.42/298.15 34: active^#(U52(tt(), N)) -> c_34(N) 1090.42/298.15 -->_1 top^#(ok(X)) -> c_116(top^#(active(X))) :116 1090.42/298.15 -->_1 top^#(mark(X)) -> c_115(top^#(proper(X))) :115 1090.42/298.15 -->_1 proper^#(plus(X1, X2)) -> 1090.42/298.15 c_113(plus^#(proper(X1), proper(X2))) :113 1090.42/298.15 -->_1 proper^#(s(X)) -> c_112(s^#(proper(X))) :112 1090.42/298.15 -->_1 proper^#(U64(X1, X2, X3)) -> 1090.42/298.15 c_111(U64^#(proper(X1), proper(X2), proper(X3))) :111 1090.42/298.15 -->_1 proper^#(U63(X1, X2, X3)) -> 1090.42/298.15 c_110(U63^#(proper(X1), proper(X2), proper(X3))) :110 1090.42/298.15 -->_1 proper^#(U62(X1, X2, X3)) -> 1090.42/298.15 c_109(U62^#(proper(X1), proper(X2), proper(X3))) :109 1090.42/298.15 -->_1 proper^#(U61(X1, X2, X3)) -> 1090.42/298.15 c_108(U61^#(proper(X1), proper(X2), proper(X3))) :108 1090.42/298.15 -->_1 proper^#(U52(X1, X2)) -> 1090.42/298.15 c_107(U52^#(proper(X1), proper(X2))) :107 1090.42/298.15 -->_1 proper^#(U51(X1, X2)) -> 1090.42/298.15 c_106(U51^#(proper(X1), proper(X2))) :106 1090.42/298.15 -->_1 proper^#(U41(X)) -> c_105(U41^#(proper(X))) :105 1090.42/298.15 -->_1 proper^#(U32(X)) -> c_104(U32^#(proper(X))) :104 1090.42/298.15 -->_1 proper^#(U31(X1, X2)) -> 1090.42/298.15 c_103(U31^#(proper(X1), proper(X2))) :103 1090.42/298.15 -->_1 proper^#(U23(X)) -> c_102(U23^#(proper(X))) :102 1090.42/298.15 -->_1 proper^#(U22(X1, X2)) -> 1090.42/298.15 c_101(U22^#(proper(X1), proper(X2))) :101 1090.42/298.15 -->_1 proper^#(U21(X1, X2)) -> 1090.42/298.15 c_100(U21^#(proper(X1), proper(X2))) :100 1090.42/298.15 -->_1 proper^#(U16(X)) -> c_99(U16^#(proper(X))) :99 1090.42/298.15 -->_1 proper^#(isNat(X)) -> c_98(isNat^#(proper(X))) :98 1090.42/298.15 -->_1 proper^#(U15(X1, X2)) -> 1090.42/298.15 c_97(U15^#(proper(X1), proper(X2))) :97 1090.42/298.15 -->_1 proper^#(U14(X1, X2, X3)) -> 1090.42/298.15 c_96(U14^#(proper(X1), proper(X2), proper(X3))) :96 1090.42/298.15 -->_1 proper^#(U13(X1, X2, X3)) -> 1090.42/298.15 c_95(U13^#(proper(X1), proper(X2), proper(X3))) :95 1090.42/298.15 -->_1 proper^#(isNatKind(X)) -> c_94(isNatKind^#(proper(X))) :94 1090.42/298.15 -->_1 proper^#(U12(X1, X2, X3)) -> 1090.42/298.15 c_93(U12^#(proper(X1), proper(X2), proper(X3))) :93 1090.42/298.15 -->_1 proper^#(U11(X1, X2, X3)) -> 1090.42/298.15 c_91(U11^#(proper(X1), proper(X2), proper(X3))) :91 1090.42/298.15 -->_1 isNat^#(ok(X)) -> c_59(isNat^#(X)) :90 1090.42/298.15 -->_1 isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) :89 1090.42/298.15 -->_1 plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) :88 1090.42/298.15 -->_1 plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) :87 1090.42/298.15 -->_1 plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) :86 1090.42/298.15 -->_1 s^#(ok(X)) -> c_87(s^#(X)) :85 1090.42/298.15 -->_1 s^#(mark(X)) -> c_86(s^#(X)) :84 1090.42/298.15 -->_1 U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) :83 1090.42/298.15 -->_1 U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) :82 1090.42/298.15 -->_1 U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) :81 1090.42/298.15 -->_1 U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) :80 1090.42/298.15 -->_1 U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) :79 1090.42/298.15 -->_1 U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) :78 1090.42/298.15 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) :77 1090.42/298.15 -->_1 U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) :76 1090.42/298.15 -->_1 U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) :75 1090.42/298.15 -->_1 U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) :74 1090.42/298.15 -->_1 U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) :73 1090.42/298.15 -->_1 U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) :72 1090.42/298.15 -->_1 U32^#(ok(X)) -> c_71(U32^#(X)) :71 1090.42/298.15 -->_1 U32^#(mark(X)) -> c_70(U32^#(X)) :70 1090.42/298.15 -->_1 U23^#(ok(X)) -> c_67(U23^#(X)) :69 1090.42/298.15 -->_1 U23^#(mark(X)) -> c_66(U23^#(X)) :68 1090.42/298.15 -->_1 U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) :67 1090.42/298.15 -->_1 U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) :66 1090.42/298.15 -->_1 U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) :65 1090.42/298.15 -->_1 U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) :64 1090.42/298.15 -->_1 U16^#(ok(X)) -> c_61(U16^#(X)) :63 1090.42/298.15 -->_1 U16^#(mark(X)) -> c_60(U16^#(X)) :62 1090.42/298.15 -->_1 U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) :61 1090.42/298.15 -->_1 U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) :60 1090.42/298.15 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) :59 1090.42/298.15 -->_1 U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) :58 1090.42/298.15 -->_1 U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) :57 1090.42/298.15 -->_1 U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) :56 1090.42/298.15 -->_1 U41^#(ok(X)) -> c_73(U41^#(X)) :55 1090.42/298.15 -->_1 U41^#(mark(X)) -> c_72(U41^#(X)) :54 1090.42/298.15 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) :53 1090.42/298.15 -->_1 U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) :52 1090.42/298.15 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) :51 1090.42/298.15 -->_1 U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) :50 1090.42/298.15 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) :49 1090.42/298.15 -->_1 U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) :48 1090.42/298.15 -->_1 active^#(plus(N, 0())) -> c_47(U51^#(isNat(N), N)) :47 1090.42/298.15 -->_1 active^#(plus(N, s(M))) -> c_46(U61^#(isNat(M), M, N)) :46 1090.42/298.15 -->_1 active^#(plus(X1, X2)) -> c_45(plus^#(active(X1), X2)) :45 1090.42/298.15 -->_1 active^#(plus(X1, X2)) -> c_44(plus^#(X1, active(X2))) :44 1090.42/298.15 -->_1 active^#(s(X)) -> c_43(s^#(active(X))) :43 1090.42/298.15 -->_1 active^#(U64(tt(), M, N)) -> c_42(s^#(plus(N, M))) :42 1090.42/298.15 -->_1 active^#(U64(X1, X2, X3)) -> 1090.42/298.15 c_41(U64^#(active(X1), X2, X3)) :41 1090.42/298.15 -->_1 active^#(U63(tt(), M, N)) -> 1090.42/298.15 c_40(U64^#(isNatKind(N), M, N)) :40 1090.42/298.15 -->_1 active^#(U63(X1, X2, X3)) -> 1090.42/298.15 c_39(U63^#(active(X1), X2, X3)) :39 1090.42/298.15 -->_1 active^#(U62(tt(), M, N)) -> c_38(U63^#(isNat(N), M, N)) :38 1090.42/298.15 -->_1 active^#(U62(X1, X2, X3)) -> 1090.42/298.15 c_37(U62^#(active(X1), X2, X3)) :37 1090.42/298.15 -->_1 active^#(U61(tt(), M, N)) -> 1090.42/298.15 c_36(U62^#(isNatKind(M), M, N)) :36 1090.42/298.15 -->_1 active^#(U61(X1, X2, X3)) -> 1090.42/298.15 c_35(U61^#(active(X1), X2, X3)) :35 1090.42/298.15 -->_1 proper^#(0()) -> c_114() :114 1090.42/298.15 -->_1 proper^#(tt()) -> c_92() :92 1090.42/298.15 -->_1 active^#(U52(tt(), N)) -> c_34(N) :34 1090.42/298.15 -->_1 active^#(U52(X1, X2)) -> c_33(U52^#(active(X1), X2)) :33 1090.42/298.15 -->_1 active^#(U51(tt(), N)) -> c_32(U52^#(isNatKind(N), N)) :32 1090.42/298.15 -->_1 active^#(U51(X1, X2)) -> c_31(U51^#(active(X1), X2)) :31 1090.42/298.15 -->_1 active^#(U41(tt())) -> c_30() :30 1090.42/298.15 -->_1 active^#(U41(X)) -> c_29(U41^#(active(X))) :29 1090.42/298.15 -->_1 active^#(U32(tt())) -> c_28() :28 1090.42/298.15 -->_1 active^#(U32(X)) -> c_27(U32^#(active(X))) :27 1090.42/298.15 -->_1 active^#(U31(tt(), V2)) -> c_26(U32^#(isNatKind(V2))) :26 1090.42/298.15 -->_1 active^#(U31(X1, X2)) -> c_25(U31^#(active(X1), X2)) :25 1090.42/298.15 -->_1 active^#(U23(tt())) -> c_24() :24 1090.42/298.15 -->_1 active^#(U23(X)) -> c_23(U23^#(active(X))) :23 1090.42/298.15 -->_1 active^#(U22(tt(), V1)) -> c_22(U23^#(isNat(V1))) :22 1090.42/298.15 -->_1 active^#(U22(X1, X2)) -> c_21(U22^#(active(X1), X2)) :21 1090.42/298.15 -->_1 active^#(U21(tt(), V1)) -> c_20(U22^#(isNatKind(V1), V1)) :20 1090.42/298.15 -->_1 active^#(U21(X1, X2)) -> c_19(U21^#(active(X1), X2)) :19 1090.42/298.15 -->_1 active^#(U16(tt())) -> c_18() :18 1090.42/298.15 -->_1 active^#(U16(X)) -> c_17(U16^#(active(X))) :17 1090.42/298.15 -->_1 active^#(isNat(0())) -> c_16() :16 1090.42/298.15 -->_1 active^#(isNat(plus(V1, V2))) -> 1090.42/298.15 c_15(U11^#(isNatKind(V1), V1, V2)) :15 1090.42/298.15 -->_1 active^#(isNat(s(V1))) -> c_14(U21^#(isNatKind(V1), V1)) :14 1090.42/298.15 -->_1 active^#(U15(tt(), V2)) -> c_13(U16^#(isNat(V2))) :13 1090.42/298.15 -->_1 active^#(U15(X1, X2)) -> c_12(U15^#(active(X1), X2)) :12 1090.42/298.15 -->_1 active^#(U14(tt(), V1, V2)) -> c_11(U15^#(isNat(V1), V2)) :11 1090.42/298.15 -->_1 active^#(U14(X1, X2, X3)) -> 1090.42/298.15 c_10(U14^#(active(X1), X2, X3)) :10 1090.42/298.15 -->_1 active^#(U13(tt(), V1, V2)) -> 1090.42/298.15 c_9(U14^#(isNatKind(V2), V1, V2)) :9 1090.42/298.15 -->_1 active^#(U13(X1, X2, X3)) -> 1090.42/298.15 c_8(U13^#(active(X1), X2, X3)) :8 1090.42/298.15 -->_1 active^#(isNatKind(0())) -> c_7() :7 1090.42/298.15 -->_1 active^#(isNatKind(plus(V1, V2))) -> 1090.42/298.15 c_6(U31^#(isNatKind(V1), V2)) :6 1090.42/298.15 -->_1 active^#(isNatKind(s(V1))) -> c_5(U41^#(isNatKind(V1))) :5 1090.42/298.15 -->_1 active^#(U12(tt(), V1, V2)) -> 1090.42/298.15 c_4(U13^#(isNatKind(V2), V1, V2)) :4 1090.42/298.15 -->_1 active^#(U12(X1, X2, X3)) -> 1090.42/298.15 c_3(U12^#(active(X1), X2, X3)) :3 1090.42/298.15 -->_1 active^#(U11(tt(), V1, V2)) -> 1090.42/298.15 c_2(U12^#(isNatKind(V1), V1, V2)) :2 1090.42/298.15 -->_1 active^#(U11(X1, X2, X3)) -> 1090.42/298.15 c_1(U11^#(active(X1), X2, X3)) :1 1090.42/298.15 1090.42/298.15 35: active^#(U61(X1, X2, X3)) -> c_35(U61^#(active(X1), X2, X3)) 1090.42/298.15 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) :77 1090.42/298.15 -->_1 U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) :76 1090.42/298.15 1090.42/298.15 36: active^#(U61(tt(), M, N)) -> c_36(U62^#(isNatKind(M), M, N)) 1090.42/298.15 -->_1 U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) :79 1090.42/298.15 -->_1 U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) :78 1090.42/298.15 1090.42/298.15 37: active^#(U62(X1, X2, X3)) -> c_37(U62^#(active(X1), X2, X3)) 1090.42/298.15 -->_1 U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) :79 1090.42/298.15 -->_1 U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) :78 1090.42/298.15 1090.42/298.15 38: active^#(U62(tt(), M, N)) -> c_38(U63^#(isNat(N), M, N)) 1090.42/298.15 -->_1 U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) :81 1090.42/298.15 -->_1 U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) :80 1090.42/298.15 1090.42/298.15 39: active^#(U63(X1, X2, X3)) -> c_39(U63^#(active(X1), X2, X3)) 1090.42/298.15 -->_1 U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) :81 1090.42/298.15 -->_1 U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) :80 1090.42/298.15 1090.42/298.15 40: active^#(U63(tt(), M, N)) -> c_40(U64^#(isNatKind(N), M, N)) 1090.42/298.15 -->_1 U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) :83 1090.42/298.15 -->_1 U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) :82 1090.42/298.15 1090.42/298.15 41: active^#(U64(X1, X2, X3)) -> c_41(U64^#(active(X1), X2, X3)) 1090.42/298.15 -->_1 U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) :83 1090.42/298.15 -->_1 U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) :82 1090.42/298.15 1090.42/298.15 42: active^#(U64(tt(), M, N)) -> c_42(s^#(plus(N, M))) 1090.42/298.15 -->_1 s^#(ok(X)) -> c_87(s^#(X)) :85 1090.42/298.15 -->_1 s^#(mark(X)) -> c_86(s^#(X)) :84 1090.42/298.15 1090.42/298.15 43: active^#(s(X)) -> c_43(s^#(active(X))) 1090.42/298.15 -->_1 s^#(ok(X)) -> c_87(s^#(X)) :85 1090.42/298.15 -->_1 s^#(mark(X)) -> c_86(s^#(X)) :84 1090.42/298.15 1090.42/298.15 44: active^#(plus(X1, X2)) -> c_44(plus^#(X1, active(X2))) 1090.42/298.15 -->_1 plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) :88 1090.42/298.15 -->_1 plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) :87 1090.42/298.15 -->_1 plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) :86 1090.42/298.15 1090.42/298.15 45: active^#(plus(X1, X2)) -> c_45(plus^#(active(X1), X2)) 1090.42/298.15 -->_1 plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) :88 1090.42/298.15 -->_1 plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) :87 1090.42/298.15 -->_1 plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) :86 1090.42/298.15 1090.42/298.15 46: active^#(plus(N, s(M))) -> c_46(U61^#(isNat(M), M, N)) 1090.42/298.15 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) :77 1090.42/298.15 -->_1 U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) :76 1090.42/298.15 1090.42/298.15 47: active^#(plus(N, 0())) -> c_47(U51^#(isNat(N), N)) 1090.42/298.15 -->_1 U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) :73 1090.42/298.15 -->_1 U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) :72 1090.42/298.15 1090.42/298.15 48: U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) 1090.42/298.15 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) :49 1090.42/298.15 -->_1 U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) :48 1090.42/298.15 1090.42/298.15 49: U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) 1090.42/298.15 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) :49 1090.42/298.15 -->_1 U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) :48 1090.42/298.15 1090.42/298.15 50: U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) 1090.42/298.15 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) :51 1090.42/298.15 -->_1 U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) :50 1090.42/298.15 1090.42/298.15 51: U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) 1090.42/298.15 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) :51 1090.42/298.15 -->_1 U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) :50 1090.42/298.15 1090.42/298.15 52: U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) 1090.42/298.15 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) :53 1090.42/298.15 -->_1 U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) :52 1090.42/298.15 1090.42/298.15 53: U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) 1090.42/298.15 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) :53 1090.42/298.15 -->_1 U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) :52 1090.42/298.15 1090.42/298.15 54: U41^#(mark(X)) -> c_72(U41^#(X)) 1090.42/298.15 -->_1 U41^#(ok(X)) -> c_73(U41^#(X)) :55 1090.42/298.15 -->_1 U41^#(mark(X)) -> c_72(U41^#(X)) :54 1090.42/298.15 1090.42/298.15 55: U41^#(ok(X)) -> c_73(U41^#(X)) 1090.42/298.15 -->_1 U41^#(ok(X)) -> c_73(U41^#(X)) :55 1090.42/298.15 -->_1 U41^#(mark(X)) -> c_72(U41^#(X)) :54 1090.42/298.15 1090.42/298.15 56: U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) 1090.42/298.15 -->_1 U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) :57 1090.42/298.15 -->_1 U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) :56 1090.42/298.15 1090.42/298.15 57: U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) 1090.42/298.15 -->_1 U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) :57 1090.42/298.15 -->_1 U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) :56 1090.42/298.15 1090.42/298.15 58: U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) 1090.42/298.15 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) :59 1090.42/298.15 -->_1 U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) :58 1090.42/298.15 1090.42/298.15 59: U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) 1090.42/298.15 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) :59 1090.42/298.15 -->_1 U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) :58 1090.42/298.15 1090.42/298.15 60: U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) 1090.42/298.15 -->_1 U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) :61 1090.42/298.15 -->_1 U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) :60 1090.42/298.15 1090.42/298.15 61: U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) 1090.42/298.15 -->_1 U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) :61 1090.42/298.15 -->_1 U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) :60 1090.42/298.15 1090.42/298.15 62: U16^#(mark(X)) -> c_60(U16^#(X)) 1090.42/298.15 -->_1 U16^#(ok(X)) -> c_61(U16^#(X)) :63 1090.42/298.15 -->_1 U16^#(mark(X)) -> c_60(U16^#(X)) :62 1090.42/298.15 1090.42/298.15 63: U16^#(ok(X)) -> c_61(U16^#(X)) 1090.42/298.15 -->_1 U16^#(ok(X)) -> c_61(U16^#(X)) :63 1090.42/298.15 -->_1 U16^#(mark(X)) -> c_60(U16^#(X)) :62 1090.42/298.15 1090.42/298.15 64: U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) 1090.42/298.15 -->_1 U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) :65 1090.42/298.15 -->_1 U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) :64 1090.42/298.15 1090.42/298.15 65: U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) 1090.42/298.15 -->_1 U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) :65 1090.42/298.15 -->_1 U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) :64 1090.42/298.15 1090.42/298.15 66: U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) 1090.42/298.15 -->_1 U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) :67 1090.42/298.15 -->_1 U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) :66 1090.42/298.15 1090.42/298.15 67: U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) 1090.42/298.15 -->_1 U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) :67 1090.42/298.15 -->_1 U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) :66 1090.42/298.15 1090.42/298.15 68: U23^#(mark(X)) -> c_66(U23^#(X)) 1090.42/298.15 -->_1 U23^#(ok(X)) -> c_67(U23^#(X)) :69 1090.42/298.15 -->_1 U23^#(mark(X)) -> c_66(U23^#(X)) :68 1090.42/298.15 1090.42/298.15 69: U23^#(ok(X)) -> c_67(U23^#(X)) 1090.42/298.15 -->_1 U23^#(ok(X)) -> c_67(U23^#(X)) :69 1090.42/298.15 -->_1 U23^#(mark(X)) -> c_66(U23^#(X)) :68 1090.42/298.15 1090.42/298.15 70: U32^#(mark(X)) -> c_70(U32^#(X)) 1090.42/298.15 -->_1 U32^#(ok(X)) -> c_71(U32^#(X)) :71 1090.42/298.15 -->_1 U32^#(mark(X)) -> c_70(U32^#(X)) :70 1090.42/298.15 1090.42/298.15 71: U32^#(ok(X)) -> c_71(U32^#(X)) 1090.42/298.15 -->_1 U32^#(ok(X)) -> c_71(U32^#(X)) :71 1090.42/298.16 -->_1 U32^#(mark(X)) -> c_70(U32^#(X)) :70 1090.42/298.16 1090.42/298.16 72: U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) 1090.42/298.16 -->_1 U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) :73 1090.42/298.16 -->_1 U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) :72 1090.42/298.16 1090.42/298.16 73: U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) 1090.42/298.16 -->_1 U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) :73 1090.42/298.16 -->_1 U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) :72 1090.42/298.16 1090.42/298.16 74: U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) 1090.42/298.16 -->_1 U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) :75 1090.42/298.16 -->_1 U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) :74 1090.42/298.16 1090.42/298.16 75: U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) 1090.42/298.16 -->_1 U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) :75 1090.42/298.16 -->_1 U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) :74 1090.42/298.16 1090.42/298.16 76: U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) 1090.42/298.16 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) :77 1090.42/298.16 -->_1 U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) :76 1090.42/298.16 1090.42/298.16 77: U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) 1090.42/298.16 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) :77 1090.42/298.16 -->_1 U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) :76 1090.42/298.16 1090.42/298.16 78: U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) 1090.42/298.16 -->_1 U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) :79 1090.42/298.16 -->_1 U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) :78 1090.42/298.16 1090.42/298.16 79: U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) 1090.42/298.16 -->_1 U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) :79 1090.42/298.16 -->_1 U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) :78 1090.42/298.16 1090.42/298.16 80: U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) 1090.42/298.16 -->_1 U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) :81 1090.42/298.16 -->_1 U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) :80 1090.42/298.16 1090.42/298.16 81: U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) 1090.42/298.16 -->_1 U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) :81 1090.42/298.16 -->_1 U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) :80 1090.42/298.16 1090.42/298.16 82: U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) 1090.42/298.16 -->_1 U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) :83 1090.42/298.16 -->_1 U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) :82 1090.42/298.16 1090.42/298.16 83: U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) 1090.42/298.16 -->_1 U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) :83 1090.42/298.16 -->_1 U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) :82 1090.42/298.16 1090.42/298.16 84: s^#(mark(X)) -> c_86(s^#(X)) 1090.42/298.16 -->_1 s^#(ok(X)) -> c_87(s^#(X)) :85 1090.42/298.16 -->_1 s^#(mark(X)) -> c_86(s^#(X)) :84 1090.42/298.16 1090.42/298.16 85: s^#(ok(X)) -> c_87(s^#(X)) 1090.42/298.16 -->_1 s^#(ok(X)) -> c_87(s^#(X)) :85 1090.42/298.16 -->_1 s^#(mark(X)) -> c_86(s^#(X)) :84 1090.42/298.16 1090.42/298.16 86: plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) 1090.42/298.16 -->_1 plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) :88 1090.42/298.16 -->_1 plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) :87 1090.42/298.16 -->_1 plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) :86 1090.42/298.16 1090.42/298.16 87: plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) 1090.42/298.16 -->_1 plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) :88 1090.42/298.16 -->_1 plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) :87 1090.42/298.16 -->_1 plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) :86 1090.42/298.16 1090.42/298.16 88: plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) 1090.42/298.16 -->_1 plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) :88 1090.42/298.16 -->_1 plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) :87 1090.42/298.16 -->_1 plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) :86 1090.42/298.16 1090.42/298.16 89: isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) 1090.42/298.16 -->_1 isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) :89 1090.42/298.16 1090.42/298.16 90: isNat^#(ok(X)) -> c_59(isNat^#(X)) 1090.42/298.16 -->_1 isNat^#(ok(X)) -> c_59(isNat^#(X)) :90 1090.42/298.16 1090.42/298.16 91: proper^#(U11(X1, X2, X3)) -> 1090.42/298.16 c_91(U11^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) :49 1090.42/298.16 -->_1 U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) :48 1090.42/298.16 1090.42/298.16 92: proper^#(tt()) -> c_92() 1090.42/298.16 1090.42/298.16 93: proper^#(U12(X1, X2, X3)) -> 1090.42/298.16 c_93(U12^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) :51 1090.42/298.16 -->_1 U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) :50 1090.42/298.16 1090.42/298.16 94: proper^#(isNatKind(X)) -> c_94(isNatKind^#(proper(X))) 1090.42/298.16 -->_1 isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) :89 1090.42/298.16 1090.42/298.16 95: proper^#(U13(X1, X2, X3)) -> 1090.42/298.16 c_95(U13^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) :53 1090.42/298.16 -->_1 U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) :52 1090.42/298.16 1090.42/298.16 96: proper^#(U14(X1, X2, X3)) -> 1090.42/298.16 c_96(U14^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) :59 1090.42/298.16 -->_1 U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) :58 1090.42/298.16 1090.42/298.16 97: proper^#(U15(X1, X2)) -> c_97(U15^#(proper(X1), proper(X2))) 1090.42/298.16 -->_1 U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) :61 1090.42/298.16 -->_1 U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) :60 1090.42/298.16 1090.42/298.16 98: proper^#(isNat(X)) -> c_98(isNat^#(proper(X))) 1090.42/298.16 -->_1 isNat^#(ok(X)) -> c_59(isNat^#(X)) :90 1090.42/298.16 1090.42/298.16 99: proper^#(U16(X)) -> c_99(U16^#(proper(X))) 1090.42/298.16 -->_1 U16^#(ok(X)) -> c_61(U16^#(X)) :63 1090.42/298.16 -->_1 U16^#(mark(X)) -> c_60(U16^#(X)) :62 1090.42/298.16 1090.42/298.16 100: proper^#(U21(X1, X2)) -> c_100(U21^#(proper(X1), proper(X2))) 1090.42/298.16 -->_1 U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) :65 1090.42/298.16 -->_1 U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) :64 1090.42/298.16 1090.42/298.16 101: proper^#(U22(X1, X2)) -> c_101(U22^#(proper(X1), proper(X2))) 1090.42/298.16 -->_1 U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) :67 1090.42/298.16 -->_1 U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) :66 1090.42/298.16 1090.42/298.16 102: proper^#(U23(X)) -> c_102(U23^#(proper(X))) 1090.42/298.16 -->_1 U23^#(ok(X)) -> c_67(U23^#(X)) :69 1090.42/298.16 -->_1 U23^#(mark(X)) -> c_66(U23^#(X)) :68 1090.42/298.16 1090.42/298.16 103: proper^#(U31(X1, X2)) -> c_103(U31^#(proper(X1), proper(X2))) 1090.42/298.16 -->_1 U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) :57 1090.42/298.16 -->_1 U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) :56 1090.42/298.16 1090.42/298.16 104: proper^#(U32(X)) -> c_104(U32^#(proper(X))) 1090.42/298.16 -->_1 U32^#(ok(X)) -> c_71(U32^#(X)) :71 1090.42/298.16 -->_1 U32^#(mark(X)) -> c_70(U32^#(X)) :70 1090.42/298.16 1090.42/298.16 105: proper^#(U41(X)) -> c_105(U41^#(proper(X))) 1090.42/298.16 -->_1 U41^#(ok(X)) -> c_73(U41^#(X)) :55 1090.42/298.16 -->_1 U41^#(mark(X)) -> c_72(U41^#(X)) :54 1090.42/298.16 1090.42/298.16 106: proper^#(U51(X1, X2)) -> c_106(U51^#(proper(X1), proper(X2))) 1090.42/298.16 -->_1 U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) :73 1090.42/298.16 -->_1 U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) :72 1090.42/298.16 1090.42/298.16 107: proper^#(U52(X1, X2)) -> c_107(U52^#(proper(X1), proper(X2))) 1090.42/298.16 -->_1 U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) :75 1090.42/298.16 -->_1 U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) :74 1090.42/298.16 1090.42/298.16 108: proper^#(U61(X1, X2, X3)) -> 1090.42/298.16 c_108(U61^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) :77 1090.42/298.16 -->_1 U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) :76 1090.42/298.16 1090.42/298.16 109: proper^#(U62(X1, X2, X3)) -> 1090.42/298.16 c_109(U62^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) :79 1090.42/298.16 -->_1 U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) :78 1090.42/298.16 1090.42/298.16 110: proper^#(U63(X1, X2, X3)) -> 1090.42/298.16 c_110(U63^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) :81 1090.42/298.16 -->_1 U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) :80 1090.42/298.16 1090.42/298.16 111: proper^#(U64(X1, X2, X3)) -> 1090.42/298.16 c_111(U64^#(proper(X1), proper(X2), proper(X3))) 1090.42/298.16 -->_1 U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) :83 1090.42/298.16 -->_1 U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) :82 1090.42/298.16 1090.42/298.16 112: proper^#(s(X)) -> c_112(s^#(proper(X))) 1090.42/298.16 -->_1 s^#(ok(X)) -> c_87(s^#(X)) :85 1090.42/298.16 -->_1 s^#(mark(X)) -> c_86(s^#(X)) :84 1090.42/298.16 1090.42/298.16 113: proper^#(plus(X1, X2)) -> 1090.42/298.16 c_113(plus^#(proper(X1), proper(X2))) 1090.42/298.16 -->_1 plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) :88 1090.42/298.16 -->_1 plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) :87 1090.42/298.16 -->_1 plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) :86 1090.42/298.16 1090.42/298.16 114: proper^#(0()) -> c_114() 1090.42/298.16 1090.42/298.16 115: top^#(mark(X)) -> c_115(top^#(proper(X))) 1090.42/298.16 -->_1 top^#(ok(X)) -> c_116(top^#(active(X))) :116 1090.42/298.16 -->_1 top^#(mark(X)) -> c_115(top^#(proper(X))) :115 1090.42/298.16 1090.42/298.16 116: top^#(ok(X)) -> c_116(top^#(active(X))) 1090.42/298.16 -->_1 top^#(ok(X)) -> c_116(top^#(active(X))) :116 1090.42/298.16 -->_1 top^#(mark(X)) -> c_115(top^#(proper(X))) :115 1090.42/298.16 1090.42/298.16 1090.42/298.16 Only the nodes 1090.42/298.16 {48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,88,87,89,90,92,114,115,116} 1090.42/298.16 are reachable from nodes 1090.42/298.16 {48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,92,114,115,116} 1090.42/298.16 that start derivation from marked basic terms. The nodes not 1090.42/298.16 reachable are removed from the problem. 1090.42/298.16 1090.42/298.16 We are left with following problem, upon which TcT provides the 1090.42/298.16 certificate MAYBE. 1090.42/298.16 1090.42/298.16 Strict DPs: 1090.42/298.16 { U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) 1090.42/298.16 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) 1090.42/298.16 , U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) 1090.42/298.16 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) 1090.42/298.16 , U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) 1090.42/298.16 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) 1090.42/298.16 , U41^#(mark(X)) -> c_72(U41^#(X)) 1090.42/298.16 , U41^#(ok(X)) -> c_73(U41^#(X)) 1090.42/298.16 , U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) 1090.42/298.16 , U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) 1090.42/298.16 , U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) 1090.42/298.16 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) 1090.42/298.16 , U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) 1090.42/298.16 , U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) 1090.42/298.16 , U16^#(mark(X)) -> c_60(U16^#(X)) 1090.42/298.16 , U16^#(ok(X)) -> c_61(U16^#(X)) 1090.42/298.16 , U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) 1090.42/298.16 , U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) 1090.42/298.16 , U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) 1090.42/298.16 , U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) 1090.42/298.16 , U23^#(mark(X)) -> c_66(U23^#(X)) 1090.42/298.16 , U23^#(ok(X)) -> c_67(U23^#(X)) 1090.42/298.16 , U32^#(mark(X)) -> c_70(U32^#(X)) 1090.42/298.16 , U32^#(ok(X)) -> c_71(U32^#(X)) 1090.42/298.16 , U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) 1090.42/298.16 , U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) 1090.42/298.16 , U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) 1090.42/298.16 , U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) 1090.42/298.16 , U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) 1090.42/298.16 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) 1090.42/298.16 , U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) 1090.42/298.16 , U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) 1090.42/298.16 , U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) 1090.42/298.16 , U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) 1090.42/298.16 , U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) 1090.42/298.16 , U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) 1090.42/298.16 , s^#(mark(X)) -> c_86(s^#(X)) 1090.42/298.16 , s^#(ok(X)) -> c_87(s^#(X)) 1090.42/298.16 , plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) 1090.42/298.16 , plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) 1090.42/298.16 , plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) 1090.42/298.16 , isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) 1090.42/298.16 , isNat^#(ok(X)) -> c_59(isNat^#(X)) 1090.42/298.16 , proper^#(tt()) -> c_92() 1090.42/298.16 , proper^#(0()) -> c_114() 1090.42/298.16 , top^#(mark(X)) -> c_115(top^#(proper(X))) 1090.42/298.16 , top^#(ok(X)) -> c_116(top^#(active(X))) } 1090.42/298.16 Strict Trs: 1090.42/298.16 { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1090.42/298.16 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1090.42/298.16 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1090.42/298.16 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1090.42/298.16 , active(isNatKind(s(V1))) -> mark(U41(isNatKind(V1))) 1090.42/298.16 , active(isNatKind(plus(V1, V2))) -> mark(U31(isNatKind(V1), V2)) 1090.42/298.16 , active(isNatKind(0())) -> mark(tt()) 1090.42/298.16 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1090.42/298.16 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1090.42/298.16 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1090.42/298.16 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1090.42/298.16 , active(U15(X1, X2)) -> U15(active(X1), X2) 1090.42/298.16 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1090.42/298.16 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1090.42/298.16 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1090.42/298.16 , active(isNat(0())) -> mark(tt()) 1090.42/298.16 , active(U16(X)) -> U16(active(X)) 1090.42/298.16 , active(U16(tt())) -> mark(tt()) 1090.42/298.16 , active(U21(X1, X2)) -> U21(active(X1), X2) 1090.42/298.16 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1090.42/298.16 , active(U22(X1, X2)) -> U22(active(X1), X2) 1090.42/298.16 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1090.42/298.16 , active(U23(X)) -> U23(active(X)) 1090.42/298.16 , active(U23(tt())) -> mark(tt()) 1090.42/298.16 , active(U31(X1, X2)) -> U31(active(X1), X2) 1090.42/298.16 , active(U31(tt(), V2)) -> mark(U32(isNatKind(V2))) 1090.42/298.16 , active(U32(X)) -> U32(active(X)) 1090.42/298.16 , active(U32(tt())) -> mark(tt()) 1090.42/298.16 , active(U41(X)) -> U41(active(X)) 1090.42/298.16 , active(U41(tt())) -> mark(tt()) 1090.42/298.16 , active(U51(X1, X2)) -> U51(active(X1), X2) 1090.42/298.16 , active(U51(tt(), N)) -> mark(U52(isNatKind(N), N)) 1090.42/298.16 , active(U52(X1, X2)) -> U52(active(X1), X2) 1090.42/298.16 , active(U52(tt(), N)) -> mark(N) 1090.42/298.16 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1090.42/298.16 , active(U61(tt(), M, N)) -> mark(U62(isNatKind(M), M, N)) 1090.42/298.16 , active(U62(X1, X2, X3)) -> U62(active(X1), X2, X3) 1090.42/298.16 , active(U62(tt(), M, N)) -> mark(U63(isNat(N), M, N)) 1090.42/298.16 , active(U63(X1, X2, X3)) -> U63(active(X1), X2, X3) 1090.42/298.16 , active(U63(tt(), M, N)) -> mark(U64(isNatKind(N), M, N)) 1090.42/298.16 , active(U64(X1, X2, X3)) -> U64(active(X1), X2, X3) 1090.42/298.16 , active(U64(tt(), M, N)) -> mark(s(plus(N, M))) 1090.42/298.16 , active(s(X)) -> s(active(X)) 1090.42/298.16 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1090.42/298.16 , active(plus(X1, X2)) -> plus(active(X1), X2) 1090.42/298.16 , active(plus(N, s(M))) -> mark(U61(isNat(M), M, N)) 1090.42/298.16 , active(plus(N, 0())) -> mark(U51(isNat(N), N)) 1090.42/298.16 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1090.42/298.16 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1090.42/298.16 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1090.42/298.16 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1090.42/298.16 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1090.42/298.16 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1090.42/298.16 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1090.42/298.16 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1090.42/298.16 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1090.42/298.16 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1090.42/298.16 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1090.42/298.16 , isNat(ok(X)) -> ok(isNat(X)) 1090.42/298.16 , U16(mark(X)) -> mark(U16(X)) 1090.42/298.16 , U16(ok(X)) -> ok(U16(X)) 1090.42/298.16 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1090.42/298.16 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1090.42/298.16 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1090.42/298.16 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1090.42/298.16 , U23(mark(X)) -> mark(U23(X)) 1090.42/298.16 , U23(ok(X)) -> ok(U23(X)) 1090.42/298.16 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1090.42/298.16 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1090.42/298.16 , U32(mark(X)) -> mark(U32(X)) 1090.42/298.16 , U32(ok(X)) -> ok(U32(X)) 1090.42/298.16 , U41(mark(X)) -> mark(U41(X)) 1090.42/298.16 , U41(ok(X)) -> ok(U41(X)) 1090.42/298.16 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 1090.42/298.16 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 1090.42/298.16 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1090.42/298.16 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1090.42/298.16 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1090.42/298.16 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1090.42/298.16 , U62(mark(X1), X2, X3) -> mark(U62(X1, X2, X3)) 1090.42/298.16 , U62(ok(X1), ok(X2), ok(X3)) -> ok(U62(X1, X2, X3)) 1090.42/298.16 , U63(mark(X1), X2, X3) -> mark(U63(X1, X2, X3)) 1090.42/298.16 , U63(ok(X1), ok(X2), ok(X3)) -> ok(U63(X1, X2, X3)) 1090.42/298.16 , U64(mark(X1), X2, X3) -> mark(U64(X1, X2, X3)) 1090.42/298.16 , U64(ok(X1), ok(X2), ok(X3)) -> ok(U64(X1, X2, X3)) 1090.42/298.16 , s(mark(X)) -> mark(s(X)) 1090.42/298.16 , s(ok(X)) -> ok(s(X)) 1090.42/298.16 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1090.42/298.16 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1090.42/298.16 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1090.42/298.16 , proper(U11(X1, X2, X3)) -> 1090.42/298.17 U11(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(tt()) -> ok(tt()) 1090.42/298.17 , proper(U12(X1, X2, X3)) -> 1090.42/298.17 U12(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1090.42/298.17 , proper(U13(X1, X2, X3)) -> 1090.42/298.17 U13(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U14(X1, X2, X3)) -> 1090.42/298.17 U14(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1090.42/298.17 , proper(isNat(X)) -> isNat(proper(X)) 1090.42/298.17 , proper(U16(X)) -> U16(proper(X)) 1090.42/298.17 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1090.42/298.17 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1090.42/298.17 , proper(U23(X)) -> U23(proper(X)) 1090.42/298.17 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1090.42/298.17 , proper(U32(X)) -> U32(proper(X)) 1090.42/298.17 , proper(U41(X)) -> U41(proper(X)) 1090.42/298.17 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 1090.42/298.17 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1090.42/298.17 , proper(U61(X1, X2, X3)) -> 1090.42/298.17 U61(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U62(X1, X2, X3)) -> 1090.42/298.17 U62(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U63(X1, X2, X3)) -> 1090.42/298.17 U63(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U64(X1, X2, X3)) -> 1090.42/298.17 U64(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(s(X)) -> s(proper(X)) 1090.42/298.17 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1090.42/298.17 , proper(0()) -> ok(0()) 1090.42/298.17 , top(mark(X)) -> top(proper(X)) 1090.42/298.17 , top(ok(X)) -> top(active(X)) } 1090.42/298.17 Obligation: 1090.42/298.17 runtime complexity 1090.42/298.17 Answer: 1090.42/298.17 MAYBE 1090.42/298.17 1090.42/298.17 We estimate the number of application of {44,45} by applications of 1090.42/298.17 Pre({44,45}) = {}. Here rules are labeled as follows: 1090.42/298.17 1090.42/298.17 DPs: 1090.42/298.17 { 1: U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) 1090.42/298.17 , 2: U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) 1090.42/298.17 , 3: U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) 1090.42/298.17 , 4: U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) 1090.42/298.17 , 5: U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) 1090.42/298.17 , 6: U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) 1090.42/298.17 , 7: U41^#(mark(X)) -> c_72(U41^#(X)) 1090.42/298.17 , 8: U41^#(ok(X)) -> c_73(U41^#(X)) 1090.42/298.17 , 9: U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) 1090.42/298.17 , 10: U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) 1090.42/298.17 , 11: U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) 1090.42/298.17 , 12: U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) 1090.42/298.17 , 13: U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) 1090.42/298.17 , 14: U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) 1090.42/298.17 , 15: U16^#(mark(X)) -> c_60(U16^#(X)) 1090.42/298.17 , 16: U16^#(ok(X)) -> c_61(U16^#(X)) 1090.42/298.17 , 17: U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) 1090.42/298.17 , 18: U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) 1090.42/298.17 , 19: U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) 1090.42/298.17 , 20: U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) 1090.42/298.17 , 21: U23^#(mark(X)) -> c_66(U23^#(X)) 1090.42/298.17 , 22: U23^#(ok(X)) -> c_67(U23^#(X)) 1090.42/298.17 , 23: U32^#(mark(X)) -> c_70(U32^#(X)) 1090.42/298.17 , 24: U32^#(ok(X)) -> c_71(U32^#(X)) 1090.42/298.17 , 25: U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) 1090.42/298.17 , 26: U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) 1090.42/298.17 , 27: U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) 1090.42/298.17 , 28: U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) 1090.42/298.17 , 29: U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) 1090.42/298.17 , 30: U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) 1090.42/298.17 , 31: U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) 1090.42/298.17 , 32: U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) 1090.42/298.17 , 33: U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) 1090.42/298.17 , 34: U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) 1090.42/298.17 , 35: U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) 1090.42/298.17 , 36: U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) 1090.42/298.17 , 37: s^#(mark(X)) -> c_86(s^#(X)) 1090.42/298.17 , 38: s^#(ok(X)) -> c_87(s^#(X)) 1090.42/298.17 , 39: plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) 1090.42/298.17 , 40: plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) 1090.42/298.17 , 41: plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) 1090.42/298.17 , 42: isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) 1090.42/298.17 , 43: isNat^#(ok(X)) -> c_59(isNat^#(X)) 1090.42/298.17 , 44: proper^#(tt()) -> c_92() 1090.42/298.17 , 45: proper^#(0()) -> c_114() 1090.42/298.17 , 46: top^#(mark(X)) -> c_115(top^#(proper(X))) 1090.42/298.17 , 47: top^#(ok(X)) -> c_116(top^#(active(X))) } 1090.42/298.17 1090.42/298.17 We are left with following problem, upon which TcT provides the 1090.42/298.17 certificate MAYBE. 1090.42/298.17 1090.42/298.17 Strict DPs: 1090.42/298.17 { U11^#(mark(X1), X2, X3) -> c_48(U11^#(X1, X2, X3)) 1090.42/298.17 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_49(U11^#(X1, X2, X3)) 1090.42/298.17 , U12^#(mark(X1), X2, X3) -> c_50(U12^#(X1, X2, X3)) 1090.42/298.17 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_51(U12^#(X1, X2, X3)) 1090.42/298.17 , U13^#(mark(X1), X2, X3) -> c_53(U13^#(X1, X2, X3)) 1090.42/298.17 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_54(U13^#(X1, X2, X3)) 1090.42/298.17 , U41^#(mark(X)) -> c_72(U41^#(X)) 1090.42/298.17 , U41^#(ok(X)) -> c_73(U41^#(X)) 1090.42/298.17 , U31^#(mark(X1), X2) -> c_68(U31^#(X1, X2)) 1090.42/298.17 , U31^#(ok(X1), ok(X2)) -> c_69(U31^#(X1, X2)) 1090.42/298.17 , U14^#(mark(X1), X2, X3) -> c_55(U14^#(X1, X2, X3)) 1090.42/298.17 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_56(U14^#(X1, X2, X3)) 1090.42/298.17 , U15^#(mark(X1), X2) -> c_57(U15^#(X1, X2)) 1090.42/298.17 , U15^#(ok(X1), ok(X2)) -> c_58(U15^#(X1, X2)) 1090.42/298.17 , U16^#(mark(X)) -> c_60(U16^#(X)) 1090.42/298.17 , U16^#(ok(X)) -> c_61(U16^#(X)) 1090.42/298.17 , U21^#(mark(X1), X2) -> c_62(U21^#(X1, X2)) 1090.42/298.17 , U21^#(ok(X1), ok(X2)) -> c_63(U21^#(X1, X2)) 1090.42/298.17 , U22^#(mark(X1), X2) -> c_64(U22^#(X1, X2)) 1090.42/298.17 , U22^#(ok(X1), ok(X2)) -> c_65(U22^#(X1, X2)) 1090.42/298.17 , U23^#(mark(X)) -> c_66(U23^#(X)) 1090.42/298.17 , U23^#(ok(X)) -> c_67(U23^#(X)) 1090.42/298.17 , U32^#(mark(X)) -> c_70(U32^#(X)) 1090.42/298.17 , U32^#(ok(X)) -> c_71(U32^#(X)) 1090.42/298.17 , U51^#(mark(X1), X2) -> c_74(U51^#(X1, X2)) 1090.42/298.17 , U51^#(ok(X1), ok(X2)) -> c_75(U51^#(X1, X2)) 1090.42/298.17 , U52^#(mark(X1), X2) -> c_76(U52^#(X1, X2)) 1090.42/298.17 , U52^#(ok(X1), ok(X2)) -> c_77(U52^#(X1, X2)) 1090.42/298.17 , U61^#(mark(X1), X2, X3) -> c_78(U61^#(X1, X2, X3)) 1090.42/298.17 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_79(U61^#(X1, X2, X3)) 1090.42/298.17 , U62^#(mark(X1), X2, X3) -> c_80(U62^#(X1, X2, X3)) 1090.42/298.17 , U62^#(ok(X1), ok(X2), ok(X3)) -> c_81(U62^#(X1, X2, X3)) 1090.42/298.17 , U63^#(mark(X1), X2, X3) -> c_82(U63^#(X1, X2, X3)) 1090.42/298.17 , U63^#(ok(X1), ok(X2), ok(X3)) -> c_83(U63^#(X1, X2, X3)) 1090.42/298.17 , U64^#(mark(X1), X2, X3) -> c_84(U64^#(X1, X2, X3)) 1090.42/298.17 , U64^#(ok(X1), ok(X2), ok(X3)) -> c_85(U64^#(X1, X2, X3)) 1090.42/298.17 , s^#(mark(X)) -> c_86(s^#(X)) 1090.42/298.17 , s^#(ok(X)) -> c_87(s^#(X)) 1090.42/298.17 , plus^#(X1, mark(X2)) -> c_88(plus^#(X1, X2)) 1090.42/298.17 , plus^#(mark(X1), X2) -> c_89(plus^#(X1, X2)) 1090.42/298.17 , plus^#(ok(X1), ok(X2)) -> c_90(plus^#(X1, X2)) 1090.42/298.17 , isNatKind^#(ok(X)) -> c_52(isNatKind^#(X)) 1090.42/298.17 , isNat^#(ok(X)) -> c_59(isNat^#(X)) 1090.42/298.17 , top^#(mark(X)) -> c_115(top^#(proper(X))) 1090.42/298.17 , top^#(ok(X)) -> c_116(top^#(active(X))) } 1090.42/298.17 Strict Trs: 1090.42/298.17 { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1090.42/298.17 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1090.42/298.17 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1090.42/298.17 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1090.42/298.17 , active(isNatKind(s(V1))) -> mark(U41(isNatKind(V1))) 1090.42/298.17 , active(isNatKind(plus(V1, V2))) -> mark(U31(isNatKind(V1), V2)) 1090.42/298.17 , active(isNatKind(0())) -> mark(tt()) 1090.42/298.17 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1090.42/298.17 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1090.42/298.17 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1090.42/298.17 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1090.42/298.17 , active(U15(X1, X2)) -> U15(active(X1), X2) 1090.42/298.17 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1090.42/298.17 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1090.42/298.17 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1090.42/298.17 , active(isNat(0())) -> mark(tt()) 1090.42/298.17 , active(U16(X)) -> U16(active(X)) 1090.42/298.17 , active(U16(tt())) -> mark(tt()) 1090.42/298.17 , active(U21(X1, X2)) -> U21(active(X1), X2) 1090.42/298.17 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1090.42/298.17 , active(U22(X1, X2)) -> U22(active(X1), X2) 1090.42/298.17 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1090.42/298.17 , active(U23(X)) -> U23(active(X)) 1090.42/298.17 , active(U23(tt())) -> mark(tt()) 1090.42/298.17 , active(U31(X1, X2)) -> U31(active(X1), X2) 1090.42/298.17 , active(U31(tt(), V2)) -> mark(U32(isNatKind(V2))) 1090.42/298.17 , active(U32(X)) -> U32(active(X)) 1090.42/298.17 , active(U32(tt())) -> mark(tt()) 1090.42/298.17 , active(U41(X)) -> U41(active(X)) 1090.42/298.17 , active(U41(tt())) -> mark(tt()) 1090.42/298.17 , active(U51(X1, X2)) -> U51(active(X1), X2) 1090.42/298.17 , active(U51(tt(), N)) -> mark(U52(isNatKind(N), N)) 1090.42/298.17 , active(U52(X1, X2)) -> U52(active(X1), X2) 1090.42/298.17 , active(U52(tt(), N)) -> mark(N) 1090.42/298.17 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1090.42/298.17 , active(U61(tt(), M, N)) -> mark(U62(isNatKind(M), M, N)) 1090.42/298.17 , active(U62(X1, X2, X3)) -> U62(active(X1), X2, X3) 1090.42/298.17 , active(U62(tt(), M, N)) -> mark(U63(isNat(N), M, N)) 1090.42/298.17 , active(U63(X1, X2, X3)) -> U63(active(X1), X2, X3) 1090.42/298.17 , active(U63(tt(), M, N)) -> mark(U64(isNatKind(N), M, N)) 1090.42/298.17 , active(U64(X1, X2, X3)) -> U64(active(X1), X2, X3) 1090.42/298.17 , active(U64(tt(), M, N)) -> mark(s(plus(N, M))) 1090.42/298.17 , active(s(X)) -> s(active(X)) 1090.42/298.17 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1090.42/298.17 , active(plus(X1, X2)) -> plus(active(X1), X2) 1090.42/298.17 , active(plus(N, s(M))) -> mark(U61(isNat(M), M, N)) 1090.42/298.17 , active(plus(N, 0())) -> mark(U51(isNat(N), N)) 1090.42/298.17 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1090.42/298.17 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1090.42/298.17 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1090.42/298.17 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1090.42/298.17 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1090.42/298.17 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1090.42/298.17 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1090.42/298.17 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1090.42/298.17 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1090.42/298.17 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1090.42/298.17 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1090.42/298.17 , isNat(ok(X)) -> ok(isNat(X)) 1090.42/298.17 , U16(mark(X)) -> mark(U16(X)) 1090.42/298.17 , U16(ok(X)) -> ok(U16(X)) 1090.42/298.17 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1090.42/298.17 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1090.42/298.17 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1090.42/298.17 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1090.42/298.17 , U23(mark(X)) -> mark(U23(X)) 1090.42/298.17 , U23(ok(X)) -> ok(U23(X)) 1090.42/298.17 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1090.42/298.17 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1090.42/298.17 , U32(mark(X)) -> mark(U32(X)) 1090.42/298.17 , U32(ok(X)) -> ok(U32(X)) 1090.42/298.17 , U41(mark(X)) -> mark(U41(X)) 1090.42/298.17 , U41(ok(X)) -> ok(U41(X)) 1090.42/298.17 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 1090.42/298.17 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 1090.42/298.17 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1090.42/298.17 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1090.42/298.17 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1090.42/298.17 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1090.42/298.17 , U62(mark(X1), X2, X3) -> mark(U62(X1, X2, X3)) 1090.42/298.17 , U62(ok(X1), ok(X2), ok(X3)) -> ok(U62(X1, X2, X3)) 1090.42/298.17 , U63(mark(X1), X2, X3) -> mark(U63(X1, X2, X3)) 1090.42/298.17 , U63(ok(X1), ok(X2), ok(X3)) -> ok(U63(X1, X2, X3)) 1090.42/298.17 , U64(mark(X1), X2, X3) -> mark(U64(X1, X2, X3)) 1090.42/298.17 , U64(ok(X1), ok(X2), ok(X3)) -> ok(U64(X1, X2, X3)) 1090.42/298.17 , s(mark(X)) -> mark(s(X)) 1090.42/298.17 , s(ok(X)) -> ok(s(X)) 1090.42/298.17 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1090.42/298.17 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1090.42/298.17 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1090.42/298.17 , proper(U11(X1, X2, X3)) -> 1090.42/298.17 U11(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(tt()) -> ok(tt()) 1090.42/298.17 , proper(U12(X1, X2, X3)) -> 1090.42/298.17 U12(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1090.42/298.17 , proper(U13(X1, X2, X3)) -> 1090.42/298.17 U13(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U14(X1, X2, X3)) -> 1090.42/298.17 U14(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1090.42/298.17 , proper(isNat(X)) -> isNat(proper(X)) 1090.42/298.17 , proper(U16(X)) -> U16(proper(X)) 1090.42/298.17 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1090.42/298.17 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1090.42/298.17 , proper(U23(X)) -> U23(proper(X)) 1090.42/298.17 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1090.42/298.17 , proper(U32(X)) -> U32(proper(X)) 1090.42/298.17 , proper(U41(X)) -> U41(proper(X)) 1090.42/298.17 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 1090.42/298.17 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1090.42/298.17 , proper(U61(X1, X2, X3)) -> 1090.42/298.17 U61(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U62(X1, X2, X3)) -> 1090.42/298.17 U62(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U63(X1, X2, X3)) -> 1090.42/298.17 U63(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(U64(X1, X2, X3)) -> 1090.42/298.17 U64(proper(X1), proper(X2), proper(X3)) 1090.42/298.17 , proper(s(X)) -> s(proper(X)) 1090.42/298.17 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1090.42/298.17 , proper(0()) -> ok(0()) 1090.42/298.17 , top(mark(X)) -> top(proper(X)) 1090.42/298.17 , top(ok(X)) -> top(active(X)) } 1090.42/298.17 Weak DPs: 1090.42/298.17 { proper^#(tt()) -> c_92() 1090.42/298.17 , proper^#(0()) -> c_114() } 1090.42/298.17 Obligation: 1090.42/298.17 runtime complexity 1090.42/298.17 Answer: 1090.42/298.17 MAYBE 1090.42/298.17 1090.42/298.17 Empty strict component of the problem is NOT empty. 1090.42/298.17 1090.42/298.17 1090.42/298.17 Arrrr.. 1090.74/298.31 EOF