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