YES(O(1),O(n^2)) 438.23/118.01 YES(O(1),O(n^2)) 438.23/118.01 438.23/118.01 We are left with following problem, upon which TcT provides the 438.23/118.01 certificate YES(O(1),O(n^2)). 438.23/118.01 438.23/118.01 Strict Trs: 438.23/118.01 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.01 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.01 , isNat(n__0()) -> tt() 438.23/118.01 , isNat(n__plus(V1, V2)) -> 438.23/118.01 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 activate(V1), 438.23/118.01 activate(V2)) 438.23/118.01 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.01 , activate(X) -> X 438.23/118.01 , activate(n__0()) -> 0() 438.23/118.01 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.01 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.01 , activate(n__s(X)) -> s(X) 438.23/118.01 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.01 , U13(tt()) -> tt() 438.23/118.01 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.01 , U22(tt()) -> tt() 438.23/118.01 , U31(tt(), N) -> activate(N) 438.23/118.01 , U41(tt(), M, N) -> s(plus(activate(N), activate(M))) 438.23/118.01 , s(X) -> n__s(X) 438.23/118.01 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.01 , plus(N, s(M)) -> 438.23/118.01 U41(and(and(isNat(M), n__isNatKind(M)), 438.23/118.01 n__and(isNat(N), n__isNatKind(N))), 438.23/118.01 M, 438.23/118.01 N) 438.23/118.01 , plus(N, 0()) -> U31(and(isNat(N), n__isNatKind(N)), N) 438.23/118.01 , and(X1, X2) -> n__and(X1, X2) 438.23/118.01 , and(tt(), X) -> activate(X) 438.23/118.01 , isNatKind(X) -> n__isNatKind(X) 438.23/118.01 , isNatKind(n__0()) -> tt() 438.23/118.01 , isNatKind(n__plus(V1, V2)) -> 438.23/118.01 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.01 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.01 , 0() -> n__0() } 438.23/118.01 Obligation: 438.23/118.01 innermost runtime complexity 438.23/118.01 Answer: 438.23/118.01 YES(O(1),O(n^2)) 438.23/118.01 438.23/118.01 Arguments of following rules are not normal-forms: 438.23/118.01 438.23/118.01 { plus(N, s(M)) -> 438.23/118.01 U41(and(and(isNat(M), n__isNatKind(M)), 438.23/118.01 n__and(isNat(N), n__isNatKind(N))), 438.23/118.01 M, 438.23/118.01 N) 438.23/118.01 , plus(N, 0()) -> U31(and(isNat(N), n__isNatKind(N)), N) } 438.23/118.01 438.23/118.01 All above mentioned rules can be savely removed. 438.23/118.01 438.23/118.01 We are left with following problem, upon which TcT provides the 438.23/118.01 certificate YES(O(1),O(n^2)). 438.23/118.01 438.23/118.01 Strict Trs: 438.23/118.01 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.01 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.01 , isNat(n__0()) -> tt() 438.23/118.01 , isNat(n__plus(V1, V2)) -> 438.23/118.01 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 activate(V1), 438.23/118.01 activate(V2)) 438.23/118.01 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.01 , activate(X) -> X 438.23/118.01 , activate(n__0()) -> 0() 438.23/118.01 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.01 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.01 , activate(n__s(X)) -> s(X) 438.23/118.01 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.01 , U13(tt()) -> tt() 438.23/118.01 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.01 , U22(tt()) -> tt() 438.23/118.01 , U31(tt(), N) -> activate(N) 438.23/118.01 , U41(tt(), M, N) -> s(plus(activate(N), activate(M))) 438.23/118.01 , s(X) -> n__s(X) 438.23/118.01 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.01 , and(X1, X2) -> n__and(X1, X2) 438.23/118.01 , and(tt(), X) -> activate(X) 438.23/118.01 , isNatKind(X) -> n__isNatKind(X) 438.23/118.01 , isNatKind(n__0()) -> tt() 438.23/118.01 , isNatKind(n__plus(V1, V2)) -> 438.23/118.01 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.01 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.01 , 0() -> n__0() } 438.23/118.01 Obligation: 438.23/118.01 innermost runtime complexity 438.23/118.01 Answer: 438.23/118.01 YES(O(1),O(n^2)) 438.23/118.01 438.23/118.01 We add the following dependency tuples: 438.23/118.01 438.23/118.01 Strict DPs: 438.23/118.01 { U11^#(tt(), V1, V2) -> 438.23/118.01 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.01 isNat^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2)) 438.23/118.01 , U12^#(tt(), V2) -> 438.23/118.01 c_2(U13^#(isNat(activate(V2))), 438.23/118.01 isNat^#(activate(V2)), 438.23/118.01 activate^#(V2)) 438.23/118.01 , isNat^#(n__0()) -> c_3() 438.23/118.01 , isNat^#(n__plus(V1, V2)) -> 438.23/118.01 c_4(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 activate(V1), 438.23/118.01 activate(V2)), 438.23/118.01 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 isNatKind^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2)) 438.23/118.01 , isNat^#(n__s(V1)) -> 438.23/118.01 c_5(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.01 isNatKind^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V1)) 438.23/118.01 , activate^#(X) -> c_6() 438.23/118.01 , activate^#(n__0()) -> c_7(0^#()) 438.23/118.01 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 438.23/118.01 , activate^#(n__isNatKind(X)) -> c_9(isNatKind^#(X)) 438.23/118.01 , activate^#(n__s(X)) -> c_10(s^#(X)) 438.23/118.01 , activate^#(n__and(X1, X2)) -> c_11(and^#(X1, X2)) 438.23/118.01 , U13^#(tt()) -> c_12() 438.23/118.01 , and^#(X1, X2) -> c_19() 438.23/118.01 , and^#(tt(), X) -> c_20(activate^#(X)) 438.23/118.01 , isNatKind^#(X) -> c_21() 438.23/118.01 , isNatKind^#(n__0()) -> c_22() 438.23/118.01 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.01 c_23(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 isNatKind^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2)) 438.23/118.01 , isNatKind^#(n__s(V1)) -> 438.23/118.01 c_24(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.01 , U21^#(tt(), V1) -> 438.23/118.01 c_13(U22^#(isNat(activate(V1))), 438.23/118.01 isNat^#(activate(V1)), 438.23/118.01 activate^#(V1)) 438.23/118.01 , 0^#() -> c_25() 438.23/118.01 , plus^#(X1, X2) -> c_18() 438.23/118.01 , s^#(X) -> c_17() 438.23/118.01 , U22^#(tt()) -> c_14() 438.23/118.01 , U31^#(tt(), N) -> c_15(activate^#(N)) 438.23/118.01 , U41^#(tt(), M, N) -> 438.23/118.01 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.01 plus^#(activate(N), activate(M)), 438.23/118.01 activate^#(N), 438.23/118.01 activate^#(M)) } 438.23/118.01 438.23/118.01 and mark the set of starting terms. 438.23/118.01 438.23/118.01 We are left with following problem, upon which TcT provides the 438.23/118.01 certificate YES(O(1),O(n^2)). 438.23/118.01 438.23/118.01 Strict DPs: 438.23/118.01 { U11^#(tt(), V1, V2) -> 438.23/118.01 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.01 isNat^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2)) 438.23/118.01 , U12^#(tt(), V2) -> 438.23/118.01 c_2(U13^#(isNat(activate(V2))), 438.23/118.01 isNat^#(activate(V2)), 438.23/118.01 activate^#(V2)) 438.23/118.01 , isNat^#(n__0()) -> c_3() 438.23/118.01 , isNat^#(n__plus(V1, V2)) -> 438.23/118.01 c_4(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 activate(V1), 438.23/118.01 activate(V2)), 438.23/118.01 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 isNatKind^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2)) 438.23/118.01 , isNat^#(n__s(V1)) -> 438.23/118.01 c_5(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.01 isNatKind^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V1)) 438.23/118.01 , activate^#(X) -> c_6() 438.23/118.01 , activate^#(n__0()) -> c_7(0^#()) 438.23/118.01 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 438.23/118.01 , activate^#(n__isNatKind(X)) -> c_9(isNatKind^#(X)) 438.23/118.01 , activate^#(n__s(X)) -> c_10(s^#(X)) 438.23/118.01 , activate^#(n__and(X1, X2)) -> c_11(and^#(X1, X2)) 438.23/118.01 , U13^#(tt()) -> c_12() 438.23/118.01 , and^#(X1, X2) -> c_19() 438.23/118.01 , and^#(tt(), X) -> c_20(activate^#(X)) 438.23/118.01 , isNatKind^#(X) -> c_21() 438.23/118.01 , isNatKind^#(n__0()) -> c_22() 438.23/118.01 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.01 c_23(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 isNatKind^#(activate(V1)), 438.23/118.01 activate^#(V1), 438.23/118.01 activate^#(V2)) 438.23/118.01 , isNatKind^#(n__s(V1)) -> 438.23/118.01 c_24(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.01 , U21^#(tt(), V1) -> 438.23/118.01 c_13(U22^#(isNat(activate(V1))), 438.23/118.01 isNat^#(activate(V1)), 438.23/118.01 activate^#(V1)) 438.23/118.01 , 0^#() -> c_25() 438.23/118.01 , plus^#(X1, X2) -> c_18() 438.23/118.01 , s^#(X) -> c_17() 438.23/118.01 , U22^#(tt()) -> c_14() 438.23/118.01 , U31^#(tt(), N) -> c_15(activate^#(N)) 438.23/118.01 , U41^#(tt(), M, N) -> 438.23/118.01 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.01 plus^#(activate(N), activate(M)), 438.23/118.01 activate^#(N), 438.23/118.01 activate^#(M)) } 438.23/118.01 Weak Trs: 438.23/118.01 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.01 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.01 , isNat(n__0()) -> tt() 438.23/118.01 , isNat(n__plus(V1, V2)) -> 438.23/118.01 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.01 activate(V1), 438.23/118.01 activate(V2)) 438.23/118.01 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.01 , activate(X) -> X 438.23/118.01 , activate(n__0()) -> 0() 438.23/118.01 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.01 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.01 , activate(n__s(X)) -> s(X) 438.23/118.01 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.01 , U13(tt()) -> tt() 438.23/118.01 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.01 , U22(tt()) -> tt() 438.23/118.01 , U31(tt(), N) -> activate(N) 438.23/118.01 , U41(tt(), M, N) -> s(plus(activate(N), activate(M))) 438.23/118.01 , s(X) -> n__s(X) 438.23/118.01 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.01 , and(X1, X2) -> n__and(X1, X2) 438.23/118.01 , and(tt(), X) -> activate(X) 438.23/118.01 , isNatKind(X) -> n__isNatKind(X) 438.23/118.01 , isNatKind(n__0()) -> tt() 438.23/118.01 , isNatKind(n__plus(V1, V2)) -> 438.23/118.01 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.02 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.02 , 0() -> n__0() } 438.23/118.02 Obligation: 438.23/118.02 innermost runtime complexity 438.23/118.02 Answer: 438.23/118.02 YES(O(1),O(n^2)) 438.23/118.02 438.23/118.02 We estimate the number of application of 438.23/118.02 {3,6,12,13,15,16,20,21,22,23} by applications of 438.23/118.02 Pre({3,6,12,13,15,16,20,21,22,23}) = 438.23/118.02 {1,2,4,5,7,8,9,10,11,14,17,18,19,24,25}. Here rules are labeled as 438.23/118.02 follows: 438.23/118.02 438.23/118.02 DPs: 438.23/118.02 { 1: U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 2: U12^#(tt(), V2) -> 438.23/118.02 c_2(U13^#(isNat(activate(V2))), 438.23/118.02 isNat^#(activate(V2)), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 3: isNat^#(n__0()) -> c_3() 438.23/118.02 , 4: isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_4(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 5: isNat^#(n__s(V1)) -> 438.23/118.02 c_5(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) 438.23/118.02 , 6: activate^#(X) -> c_6() 438.23/118.02 , 7: activate^#(n__0()) -> c_7(0^#()) 438.23/118.02 , 8: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 438.23/118.02 , 9: activate^#(n__isNatKind(X)) -> c_9(isNatKind^#(X)) 438.23/118.02 , 10: activate^#(n__s(X)) -> c_10(s^#(X)) 438.23/118.02 , 11: activate^#(n__and(X1, X2)) -> c_11(and^#(X1, X2)) 438.23/118.02 , 12: U13^#(tt()) -> c_12() 438.23/118.02 , 13: and^#(X1, X2) -> c_19() 438.23/118.02 , 14: and^#(tt(), X) -> c_20(activate^#(X)) 438.23/118.02 , 15: isNatKind^#(X) -> c_21() 438.23/118.02 , 16: isNatKind^#(n__0()) -> c_22() 438.23/118.02 , 17: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_23(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 18: isNatKind^#(n__s(V1)) -> 438.23/118.02 c_24(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.02 , 19: U21^#(tt(), V1) -> 438.23/118.02 c_13(U22^#(isNat(activate(V1))), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1)) 438.23/118.02 , 20: 0^#() -> c_25() 438.23/118.02 , 21: plus^#(X1, X2) -> c_18() 438.23/118.02 , 22: s^#(X) -> c_17() 438.23/118.02 , 23: U22^#(tt()) -> c_14() 438.23/118.02 , 24: U31^#(tt(), N) -> c_15(activate^#(N)) 438.23/118.02 , 25: U41^#(tt(), M, N) -> 438.23/118.02 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.02 plus^#(activate(N), activate(M)), 438.23/118.02 activate^#(N), 438.23/118.02 activate^#(M)) } 438.23/118.02 438.23/118.02 We are left with following problem, upon which TcT provides the 438.23/118.02 certificate YES(O(1),O(n^2)). 438.23/118.02 438.23/118.02 Strict DPs: 438.23/118.02 { U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , U12^#(tt(), V2) -> 438.23/118.02 c_2(U13^#(isNat(activate(V2))), 438.23/118.02 isNat^#(activate(V2)), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_4(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__s(V1)) -> 438.23/118.02 c_5(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) 438.23/118.02 , activate^#(n__0()) -> c_7(0^#()) 438.23/118.02 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 438.23/118.02 , activate^#(n__isNatKind(X)) -> c_9(isNatKind^#(X)) 438.23/118.02 , activate^#(n__s(X)) -> c_10(s^#(X)) 438.23/118.02 , activate^#(n__and(X1, X2)) -> c_11(and^#(X1, X2)) 438.23/118.02 , and^#(tt(), X) -> c_20(activate^#(X)) 438.23/118.02 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_23(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNatKind^#(n__s(V1)) -> 438.23/118.02 c_24(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.02 , U21^#(tt(), V1) -> 438.23/118.02 c_13(U22^#(isNat(activate(V1))), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1)) 438.23/118.02 , U31^#(tt(), N) -> c_15(activate^#(N)) 438.23/118.02 , U41^#(tt(), M, N) -> 438.23/118.02 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.02 plus^#(activate(N), activate(M)), 438.23/118.02 activate^#(N), 438.23/118.02 activate^#(M)) } 438.23/118.02 Weak DPs: 438.23/118.02 { isNat^#(n__0()) -> c_3() 438.23/118.02 , activate^#(X) -> c_6() 438.23/118.02 , U13^#(tt()) -> c_12() 438.23/118.02 , and^#(X1, X2) -> c_19() 438.23/118.02 , isNatKind^#(X) -> c_21() 438.23/118.02 , isNatKind^#(n__0()) -> c_22() 438.23/118.02 , 0^#() -> c_25() 438.23/118.02 , plus^#(X1, X2) -> c_18() 438.23/118.02 , s^#(X) -> c_17() 438.23/118.02 , U22^#(tt()) -> c_14() } 438.23/118.02 Weak Trs: 438.23/118.02 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.02 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.02 , isNat(n__0()) -> tt() 438.23/118.02 , isNat(n__plus(V1, V2)) -> 438.23/118.02 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)) 438.23/118.02 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.02 , activate(X) -> X 438.23/118.02 , activate(n__0()) -> 0() 438.23/118.02 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.02 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.02 , activate(n__s(X)) -> s(X) 438.23/118.02 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.02 , U13(tt()) -> tt() 438.23/118.02 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.02 , U22(tt()) -> tt() 438.23/118.02 , U31(tt(), N) -> activate(N) 438.23/118.02 , U41(tt(), M, N) -> s(plus(activate(N), activate(M))) 438.23/118.02 , s(X) -> n__s(X) 438.23/118.02 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.02 , and(X1, X2) -> n__and(X1, X2) 438.23/118.02 , and(tt(), X) -> activate(X) 438.23/118.02 , isNatKind(X) -> n__isNatKind(X) 438.23/118.02 , isNatKind(n__0()) -> tt() 438.23/118.02 , isNatKind(n__plus(V1, V2)) -> 438.23/118.02 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.02 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.02 , 0() -> n__0() } 438.23/118.02 Obligation: 438.23/118.02 innermost runtime complexity 438.23/118.02 Answer: 438.23/118.02 YES(O(1),O(n^2)) 438.23/118.02 438.23/118.02 We estimate the number of application of {5,6,8} by applications of 438.23/118.02 Pre({5,6,8}) = {1,2,3,4,10,11,12,13,14,15}. Here rules are labeled 438.23/118.02 as follows: 438.23/118.02 438.23/118.02 DPs: 438.23/118.02 { 1: U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 2: U12^#(tt(), V2) -> 438.23/118.02 c_2(U13^#(isNat(activate(V2))), 438.23/118.02 isNat^#(activate(V2)), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 3: isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_4(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 4: isNat^#(n__s(V1)) -> 438.23/118.02 c_5(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) 438.23/118.02 , 5: activate^#(n__0()) -> c_7(0^#()) 438.23/118.02 , 6: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 438.23/118.02 , 7: activate^#(n__isNatKind(X)) -> c_9(isNatKind^#(X)) 438.23/118.02 , 8: activate^#(n__s(X)) -> c_10(s^#(X)) 438.23/118.02 , 9: activate^#(n__and(X1, X2)) -> c_11(and^#(X1, X2)) 438.23/118.02 , 10: and^#(tt(), X) -> c_20(activate^#(X)) 438.23/118.02 , 11: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_23(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , 12: isNatKind^#(n__s(V1)) -> 438.23/118.02 c_24(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.02 , 13: U21^#(tt(), V1) -> 438.23/118.02 c_13(U22^#(isNat(activate(V1))), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1)) 438.23/118.02 , 14: U31^#(tt(), N) -> c_15(activate^#(N)) 438.23/118.02 , 15: U41^#(tt(), M, N) -> 438.23/118.02 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.02 plus^#(activate(N), activate(M)), 438.23/118.02 activate^#(N), 438.23/118.02 activate^#(M)) 438.23/118.02 , 16: isNat^#(n__0()) -> c_3() 438.23/118.02 , 17: activate^#(X) -> c_6() 438.23/118.02 , 18: U13^#(tt()) -> c_12() 438.23/118.02 , 19: and^#(X1, X2) -> c_19() 438.23/118.02 , 20: isNatKind^#(X) -> c_21() 438.23/118.02 , 21: isNatKind^#(n__0()) -> c_22() 438.23/118.02 , 22: 0^#() -> c_25() 438.23/118.02 , 23: plus^#(X1, X2) -> c_18() 438.23/118.02 , 24: s^#(X) -> c_17() 438.23/118.02 , 25: U22^#(tt()) -> c_14() } 438.23/118.02 438.23/118.02 We are left with following problem, upon which TcT provides the 438.23/118.02 certificate YES(O(1),O(n^2)). 438.23/118.02 438.23/118.02 Strict DPs: 438.23/118.02 { U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , U12^#(tt(), V2) -> 438.23/118.02 c_2(U13^#(isNat(activate(V2))), 438.23/118.02 isNat^#(activate(V2)), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_4(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__s(V1)) -> 438.23/118.02 c_5(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) 438.23/118.02 , activate^#(n__isNatKind(X)) -> c_9(isNatKind^#(X)) 438.23/118.02 , activate^#(n__and(X1, X2)) -> c_11(and^#(X1, X2)) 438.23/118.02 , and^#(tt(), X) -> c_20(activate^#(X)) 438.23/118.02 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_23(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNatKind^#(n__s(V1)) -> 438.23/118.02 c_24(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.02 , U21^#(tt(), V1) -> 438.23/118.02 c_13(U22^#(isNat(activate(V1))), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1)) 438.23/118.02 , U31^#(tt(), N) -> c_15(activate^#(N)) 438.23/118.02 , U41^#(tt(), M, N) -> 438.23/118.02 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.02 plus^#(activate(N), activate(M)), 438.23/118.02 activate^#(N), 438.23/118.02 activate^#(M)) } 438.23/118.02 Weak DPs: 438.23/118.02 { isNat^#(n__0()) -> c_3() 438.23/118.02 , activate^#(X) -> c_6() 438.23/118.02 , activate^#(n__0()) -> c_7(0^#()) 438.23/118.02 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 438.23/118.02 , activate^#(n__s(X)) -> c_10(s^#(X)) 438.23/118.02 , U13^#(tt()) -> c_12() 438.23/118.02 , and^#(X1, X2) -> c_19() 438.23/118.02 , isNatKind^#(X) -> c_21() 438.23/118.02 , isNatKind^#(n__0()) -> c_22() 438.23/118.02 , 0^#() -> c_25() 438.23/118.02 , plus^#(X1, X2) -> c_18() 438.23/118.02 , s^#(X) -> c_17() 438.23/118.02 , U22^#(tt()) -> c_14() } 438.23/118.02 Weak Trs: 438.23/118.02 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.02 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.02 , isNat(n__0()) -> tt() 438.23/118.02 , isNat(n__plus(V1, V2)) -> 438.23/118.02 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)) 438.23/118.02 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.02 , activate(X) -> X 438.23/118.02 , activate(n__0()) -> 0() 438.23/118.02 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.02 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.02 , activate(n__s(X)) -> s(X) 438.23/118.02 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.02 , U13(tt()) -> tt() 438.23/118.02 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.02 , U22(tt()) -> tt() 438.23/118.02 , U31(tt(), N) -> activate(N) 438.23/118.02 , U41(tt(), M, N) -> s(plus(activate(N), activate(M))) 438.23/118.02 , s(X) -> n__s(X) 438.23/118.02 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.02 , and(X1, X2) -> n__and(X1, X2) 438.23/118.02 , and(tt(), X) -> activate(X) 438.23/118.02 , isNatKind(X) -> n__isNatKind(X) 438.23/118.02 , isNatKind(n__0()) -> tt() 438.23/118.02 , isNatKind(n__plus(V1, V2)) -> 438.23/118.02 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.02 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.02 , 0() -> n__0() } 438.23/118.02 Obligation: 438.23/118.02 innermost runtime complexity 438.23/118.02 Answer: 438.23/118.02 YES(O(1),O(n^2)) 438.23/118.02 438.23/118.02 The following weak DPs constitute a sub-graph of the DG that is 438.23/118.02 closed under successors. The DPs are removed. 438.23/118.02 438.23/118.02 { isNat^#(n__0()) -> c_3() 438.23/118.02 , activate^#(X) -> c_6() 438.23/118.02 , activate^#(n__0()) -> c_7(0^#()) 438.23/118.02 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 438.23/118.02 , activate^#(n__s(X)) -> c_10(s^#(X)) 438.23/118.02 , U13^#(tt()) -> c_12() 438.23/118.02 , and^#(X1, X2) -> c_19() 438.23/118.02 , isNatKind^#(X) -> c_21() 438.23/118.02 , isNatKind^#(n__0()) -> c_22() 438.23/118.02 , 0^#() -> c_25() 438.23/118.02 , plus^#(X1, X2) -> c_18() 438.23/118.02 , s^#(X) -> c_17() 438.23/118.02 , U22^#(tt()) -> c_14() } 438.23/118.02 438.23/118.02 We are left with following problem, upon which TcT provides the 438.23/118.02 certificate YES(O(1),O(n^2)). 438.23/118.02 438.23/118.02 Strict DPs: 438.23/118.02 { U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , U12^#(tt(), V2) -> 438.23/118.02 c_2(U13^#(isNat(activate(V2))), 438.23/118.02 isNat^#(activate(V2)), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_4(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__s(V1)) -> 438.23/118.02 c_5(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) 438.23/118.02 , activate^#(n__isNatKind(X)) -> c_9(isNatKind^#(X)) 438.23/118.02 , activate^#(n__and(X1, X2)) -> c_11(and^#(X1, X2)) 438.23/118.02 , and^#(tt(), X) -> c_20(activate^#(X)) 438.23/118.02 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_23(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNatKind^#(n__s(V1)) -> 438.23/118.02 c_24(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.02 , U21^#(tt(), V1) -> 438.23/118.02 c_13(U22^#(isNat(activate(V1))), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1)) 438.23/118.02 , U31^#(tt(), N) -> c_15(activate^#(N)) 438.23/118.02 , U41^#(tt(), M, N) -> 438.23/118.02 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.02 plus^#(activate(N), activate(M)), 438.23/118.02 activate^#(N), 438.23/118.02 activate^#(M)) } 438.23/118.02 Weak Trs: 438.23/118.02 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.02 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.02 , isNat(n__0()) -> tt() 438.23/118.02 , isNat(n__plus(V1, V2)) -> 438.23/118.02 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)) 438.23/118.02 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.02 , activate(X) -> X 438.23/118.02 , activate(n__0()) -> 0() 438.23/118.02 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.02 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.02 , activate(n__s(X)) -> s(X) 438.23/118.02 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.02 , U13(tt()) -> tt() 438.23/118.02 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.02 , U22(tt()) -> tt() 438.23/118.02 , U31(tt(), N) -> activate(N) 438.23/118.02 , U41(tt(), M, N) -> s(plus(activate(N), activate(M))) 438.23/118.02 , s(X) -> n__s(X) 438.23/118.02 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.02 , and(X1, X2) -> n__and(X1, X2) 438.23/118.02 , and(tt(), X) -> activate(X) 438.23/118.02 , isNatKind(X) -> n__isNatKind(X) 438.23/118.02 , isNatKind(n__0()) -> tt() 438.23/118.02 , isNatKind(n__plus(V1, V2)) -> 438.23/118.02 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.02 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.02 , 0() -> n__0() } 438.23/118.02 Obligation: 438.23/118.02 innermost runtime complexity 438.23/118.02 Answer: 438.23/118.02 YES(O(1),O(n^2)) 438.23/118.02 438.23/118.02 Due to missing edges in the dependency-graph, the right-hand sides 438.23/118.02 of following rules could be simplified: 438.23/118.02 438.23/118.02 { U12^#(tt(), V2) -> 438.23/118.02 c_2(U13^#(isNat(activate(V2))), 438.23/118.02 isNat^#(activate(V2)), 438.23/118.02 activate^#(V2)) 438.23/118.02 , U21^#(tt(), V1) -> 438.23/118.02 c_13(U22^#(isNat(activate(V1))), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1)) 438.23/118.02 , U41^#(tt(), M, N) -> 438.23/118.02 c_16(s^#(plus(activate(N), activate(M))), 438.23/118.02 plus^#(activate(N), activate(M)), 438.23/118.02 activate^#(N), 438.23/118.02 activate^#(M)) } 438.23/118.02 438.23/118.02 We are left with following problem, upon which TcT provides the 438.23/118.02 certificate YES(O(1),O(n^2)). 438.23/118.02 438.23/118.02 Strict DPs: 438.23/118.02 { U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.02 , isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__s(V1)) -> 438.23/118.02 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) 438.23/118.02 , activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.02 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.02 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.02 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNatKind^#(n__s(V1)) -> 438.23/118.02 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.02 , U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) 438.23/118.02 , U31^#(tt(), N) -> c_11(activate^#(N)) 438.23/118.02 , U41^#(tt(), M, N) -> c_12(activate^#(N), activate^#(M)) } 438.23/118.02 Weak Trs: 438.23/118.02 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.02 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.02 , isNat(n__0()) -> tt() 438.23/118.02 , isNat(n__plus(V1, V2)) -> 438.23/118.02 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)) 438.23/118.02 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.02 , activate(X) -> X 438.23/118.02 , activate(n__0()) -> 0() 438.23/118.02 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.02 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.02 , activate(n__s(X)) -> s(X) 438.23/118.02 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.02 , U13(tt()) -> tt() 438.23/118.02 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.02 , U22(tt()) -> tt() 438.23/118.02 , U31(tt(), N) -> activate(N) 438.23/118.02 , U41(tt(), M, N) -> s(plus(activate(N), activate(M))) 438.23/118.02 , s(X) -> n__s(X) 438.23/118.02 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.02 , and(X1, X2) -> n__and(X1, X2) 438.23/118.02 , and(tt(), X) -> activate(X) 438.23/118.02 , isNatKind(X) -> n__isNatKind(X) 438.23/118.02 , isNatKind(n__0()) -> tt() 438.23/118.02 , isNatKind(n__plus(V1, V2)) -> 438.23/118.02 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.02 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.02 , 0() -> n__0() } 438.23/118.02 Obligation: 438.23/118.02 innermost runtime complexity 438.23/118.02 Answer: 438.23/118.02 YES(O(1),O(n^2)) 438.23/118.02 438.23/118.02 We replace rewrite rules by usable rules: 438.23/118.02 438.23/118.02 Weak Usable Rules: 438.23/118.02 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.02 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.02 , isNat(n__0()) -> tt() 438.23/118.02 , isNat(n__plus(V1, V2)) -> 438.23/118.02 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)) 438.23/118.02 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.02 , activate(X) -> X 438.23/118.02 , activate(n__0()) -> 0() 438.23/118.02 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.02 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.02 , activate(n__s(X)) -> s(X) 438.23/118.02 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.02 , U13(tt()) -> tt() 438.23/118.02 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.02 , U22(tt()) -> tt() 438.23/118.02 , s(X) -> n__s(X) 438.23/118.02 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.02 , and(X1, X2) -> n__and(X1, X2) 438.23/118.02 , and(tt(), X) -> activate(X) 438.23/118.02 , isNatKind(X) -> n__isNatKind(X) 438.23/118.02 , isNatKind(n__0()) -> tt() 438.23/118.02 , isNatKind(n__plus(V1, V2)) -> 438.23/118.02 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.02 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.02 , 0() -> n__0() } 438.23/118.02 438.23/118.02 We are left with following problem, upon which TcT provides the 438.23/118.02 certificate YES(O(1),O(n^2)). 438.23/118.02 438.23/118.02 Strict DPs: 438.23/118.02 { U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.02 , isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNat^#(n__s(V1)) -> 438.23/118.02 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) 438.23/118.02 , activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.02 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.02 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.02 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 , isNatKind^#(n__s(V1)) -> 438.23/118.02 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.02 , U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) 438.23/118.02 , U31^#(tt(), N) -> c_11(activate^#(N)) 438.23/118.02 , U41^#(tt(), M, N) -> c_12(activate^#(N), activate^#(M)) } 438.23/118.02 Weak Trs: 438.23/118.02 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.02 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.02 , isNat(n__0()) -> tt() 438.23/118.02 , isNat(n__plus(V1, V2)) -> 438.23/118.02 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)) 438.23/118.02 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.02 , activate(X) -> X 438.23/118.02 , activate(n__0()) -> 0() 438.23/118.02 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.02 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.02 , activate(n__s(X)) -> s(X) 438.23/118.02 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.02 , U13(tt()) -> tt() 438.23/118.02 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.02 , U22(tt()) -> tt() 438.23/118.02 , s(X) -> n__s(X) 438.23/118.02 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.02 , and(X1, X2) -> n__and(X1, X2) 438.23/118.02 , and(tt(), X) -> activate(X) 438.23/118.02 , isNatKind(X) -> n__isNatKind(X) 438.23/118.02 , isNatKind(n__0()) -> tt() 438.23/118.02 , isNatKind(n__plus(V1, V2)) -> 438.23/118.02 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.02 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.02 , 0() -> n__0() } 438.23/118.02 Obligation: 438.23/118.02 innermost runtime complexity 438.23/118.02 Answer: 438.23/118.02 YES(O(1),O(n^2)) 438.23/118.02 438.23/118.02 Consider the dependency graph 438.23/118.02 438.23/118.02 1: U11^#(tt(), V1, V2) -> 438.23/118.02 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.02 isNat^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 -->_4 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.02 -->_3 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.02 -->_4 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.02 -->_3 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.02 -->_2 isNat^#(n__s(V1)) -> 438.23/118.02 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) :4 438.23/118.02 -->_2 isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) :3 438.23/118.02 -->_1 U12^#(tt(), V2) -> 438.23/118.02 c_2(isNat^#(activate(V2)), activate^#(V2)) :2 438.23/118.02 438.23/118.02 2: U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.02 -->_2 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.02 -->_2 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.02 -->_1 isNat^#(n__s(V1)) -> 438.23/118.02 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V1)) :4 438.23/118.02 -->_1 isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) :3 438.23/118.02 438.23/118.02 3: isNat^#(n__plus(V1, V2)) -> 438.23/118.02 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 activate(V1), 438.23/118.02 activate(V2)), 438.23/118.02 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) 438.23/118.02 -->_3 isNatKind^#(n__s(V1)) -> 438.23/118.02 c_9(isNatKind^#(activate(V1)), activate^#(V1)) :9 438.23/118.02 -->_3 isNatKind^#(n__plus(V1, V2)) -> 438.23/118.02 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.02 isNatKind^#(activate(V1)), 438.23/118.02 activate^#(V1), 438.23/118.02 activate^#(V2)) :8 438.23/118.02 -->_2 and^#(tt(), X) -> c_7(activate^#(X)) :7 438.23/118.03 -->_7 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_6 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_5 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_4 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_7 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_6 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_5 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_4 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_1 U11^#(tt(), V1, V2) -> 438.23/118.03 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) :1 438.23/118.03 438.23/118.03 4: isNat^#(n__s(V1)) -> 438.23/118.03 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V1)) 438.23/118.03 -->_1 U21^#(tt(), V1) -> 438.23/118.03 c_10(isNat^#(activate(V1)), activate^#(V1)) :10 438.23/118.03 -->_2 isNatKind^#(n__s(V1)) -> 438.23/118.03 c_9(isNatKind^#(activate(V1)), activate^#(V1)) :9 438.23/118.03 -->_2 isNatKind^#(n__plus(V1, V2)) -> 438.23/118.03 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) :8 438.23/118.03 -->_4 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_3 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_4 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_3 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 438.23/118.03 5: activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.03 -->_1 isNatKind^#(n__s(V1)) -> 438.23/118.03 c_9(isNatKind^#(activate(V1)), activate^#(V1)) :9 438.23/118.03 -->_1 isNatKind^#(n__plus(V1, V2)) -> 438.23/118.03 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) :8 438.23/118.03 438.23/118.03 6: activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.03 -->_1 and^#(tt(), X) -> c_7(activate^#(X)) :7 438.23/118.03 438.23/118.03 7: and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.03 -->_1 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_1 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 438.23/118.03 8: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.03 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 -->_2 isNatKind^#(n__s(V1)) -> 438.23/118.03 c_9(isNatKind^#(activate(V1)), activate^#(V1)) :9 438.23/118.03 -->_2 isNatKind^#(n__plus(V1, V2)) -> 438.23/118.03 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) :8 438.23/118.03 -->_1 and^#(tt(), X) -> c_7(activate^#(X)) :7 438.23/118.03 -->_4 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_3 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_4 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_3 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 438.23/118.03 9: isNatKind^#(n__s(V1)) -> 438.23/118.03 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.03 -->_1 isNatKind^#(n__s(V1)) -> 438.23/118.03 c_9(isNatKind^#(activate(V1)), activate^#(V1)) :9 438.23/118.03 -->_1 isNatKind^#(n__plus(V1, V2)) -> 438.23/118.03 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) :8 438.23/118.03 -->_2 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_2 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 438.23/118.03 10: U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) 438.23/118.03 -->_2 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_2 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_1 isNat^#(n__s(V1)) -> 438.23/118.03 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V1)) :4 438.23/118.03 -->_1 isNat^#(n__plus(V1, V2)) -> 438.23/118.03 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)), 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) :3 438.23/118.03 438.23/118.03 11: U31^#(tt(), N) -> c_11(activate^#(N)) 438.23/118.03 -->_1 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_1 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 438.23/118.03 12: U41^#(tt(), M, N) -> c_12(activate^#(N), activate^#(M)) 438.23/118.03 -->_2 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_1 activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) :6 438.23/118.03 -->_2 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 -->_1 activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) :5 438.23/118.03 438.23/118.03 438.23/118.03 Following roots of the dependency graph are removed, as the 438.23/118.03 considered set of starting terms is closed under reduction with 438.23/118.03 respect to these rules (modulo compound contexts). 438.23/118.03 438.23/118.03 { U31^#(tt(), N) -> c_11(activate^#(N)) 438.23/118.03 , U41^#(tt(), M, N) -> c_12(activate^#(N), activate^#(M)) } 438.23/118.03 438.23/118.03 438.23/118.03 We are left with following problem, upon which TcT provides the 438.23/118.03 certificate YES(O(1),O(n^2)). 438.23/118.03 438.23/118.03 Strict DPs: 438.23/118.03 { U11^#(tt(), V1, V2) -> 438.23/118.03 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> 438.23/118.03 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)), 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , isNat^#(n__s(V1)) -> 438.23/118.03 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V1)) 438.23/118.03 , activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.03 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.03 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.03 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.03 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , isNatKind^#(n__s(V1)) -> 438.23/118.03 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.03 , U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) } 438.23/118.03 Weak Trs: 438.23/118.03 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.03 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.03 , isNat(n__0()) -> tt() 438.23/118.03 , isNat(n__plus(V1, V2)) -> 438.23/118.03 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)) 438.23/118.03 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.03 , activate(X) -> X 438.23/118.03 , activate(n__0()) -> 0() 438.23/118.03 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.03 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.03 , activate(n__s(X)) -> s(X) 438.23/118.03 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.03 , U13(tt()) -> tt() 438.23/118.03 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.03 , U22(tt()) -> tt() 438.23/118.03 , s(X) -> n__s(X) 438.23/118.03 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.03 , and(X1, X2) -> n__and(X1, X2) 438.23/118.03 , and(tt(), X) -> activate(X) 438.23/118.03 , isNatKind(X) -> n__isNatKind(X) 438.23/118.03 , isNatKind(n__0()) -> tt() 438.23/118.03 , isNatKind(n__plus(V1, V2)) -> 438.23/118.03 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.03 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.03 , 0() -> n__0() } 438.23/118.03 Obligation: 438.23/118.03 innermost runtime complexity 438.23/118.03 Answer: 438.23/118.03 YES(O(1),O(n^2)) 438.23/118.03 438.23/118.03 We decompose the input problem according to the dependency graph 438.23/118.03 into the upper component 438.23/118.03 438.23/118.03 { U11^#(tt(), V1, V2) -> 438.23/118.03 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> 438.23/118.03 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)), 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , isNat^#(n__s(V1)) -> 438.23/118.03 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V1)) 438.23/118.03 , U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) } 438.23/118.03 438.23/118.03 and lower component 438.23/118.03 438.23/118.03 { activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.03 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.03 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.03 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.03 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , isNatKind^#(n__s(V1)) -> 438.23/118.03 c_9(isNatKind^#(activate(V1)), activate^#(V1)) } 438.23/118.03 438.23/118.03 Further, following extension rules are added to the lower 438.23/118.03 component. 438.23/118.03 438.23/118.03 { U11^#(tt(), V1, V2) -> U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.03 , U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.03 , U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.03 , U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.03 , U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.03 , U12^#(tt(), V2) -> activate^#(V2) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> 438.23/118.03 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.03 , isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.03 , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.03 , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.03 , U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.03 , U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.03 438.23/118.03 TcT solves the upper component with certificate YES(O(1),O(n^1)). 438.23/118.03 438.23/118.03 Sub-proof: 438.23/118.03 ---------- 438.23/118.03 We are left with following problem, upon which TcT provides the 438.23/118.03 certificate YES(O(1),O(n^1)). 438.23/118.03 438.23/118.03 Strict DPs: 438.23/118.03 { U11^#(tt(), V1, V2) -> 438.23/118.03 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> 438.23/118.03 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)), 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , isNat^#(n__s(V1)) -> 438.23/118.03 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V1)) 438.23/118.03 , U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) } 438.23/118.03 Weak Trs: 438.23/118.03 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.03 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.03 , isNat(n__0()) -> tt() 438.23/118.03 , isNat(n__plus(V1, V2)) -> 438.23/118.03 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)) 438.23/118.03 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.03 , activate(X) -> X 438.23/118.03 , activate(n__0()) -> 0() 438.23/118.03 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.03 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.03 , activate(n__s(X)) -> s(X) 438.23/118.03 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.03 , U13(tt()) -> tt() 438.23/118.03 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.03 , U22(tt()) -> tt() 438.23/118.03 , s(X) -> n__s(X) 438.23/118.03 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.03 , and(X1, X2) -> n__and(X1, X2) 438.23/118.03 , and(tt(), X) -> activate(X) 438.23/118.03 , isNatKind(X) -> n__isNatKind(X) 438.23/118.03 , isNatKind(n__0()) -> tt() 438.23/118.03 , isNatKind(n__plus(V1, V2)) -> 438.23/118.03 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.03 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.03 , 0() -> n__0() } 438.23/118.03 Obligation: 438.23/118.03 innermost runtime complexity 438.23/118.03 Answer: 438.23/118.03 YES(O(1),O(n^1)) 438.23/118.03 438.23/118.03 We use the processor 'matrix interpretation of dimension 1' to 438.23/118.03 orient following rules strictly. 438.23/118.03 438.23/118.03 DPs: 438.23/118.03 { 1: U11^#(tt(), V1, V2) -> 438.23/118.03 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , 5: U21^#(tt(), V1) -> 438.23/118.03 c_10(isNat^#(activate(V1)), activate^#(V1)) } 438.23/118.03 438.23/118.03 Sub-proof: 438.23/118.03 ---------- 438.23/118.03 The following argument positions are usable: 438.23/118.03 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2, 3}, 438.23/118.03 Uargs(c_4) = {1, 2}, Uargs(c_10) = {1} 438.23/118.03 438.23/118.03 TcT has computed the following constructor-based matrix 438.23/118.03 interpretation satisfying not(EDA). 438.23/118.03 438.23/118.03 [U11](x1, x2, x3) = [0] 438.23/118.03 438.23/118.03 [tt] = [4] 438.23/118.03 438.23/118.03 [U12](x1, x2) = [0] 438.23/118.03 438.23/118.03 [isNat](x1) = [0] 438.23/118.03 438.23/118.03 [activate](x1) = [1] x1 + [0] 438.23/118.03 438.23/118.03 [U13](x1) = [0] 438.23/118.03 438.23/118.03 [U21](x1, x2) = [0] 438.23/118.03 438.23/118.03 [U22](x1) = [0] 438.23/118.03 438.23/118.03 [s](x1) = [1] x1 + [1] 438.23/118.03 438.23/118.03 [plus](x1, x2) = [1] x1 + [1] x2 + [4] 438.23/118.03 438.23/118.03 [and](x1, x2) = [1] x2 + [0] 438.23/118.03 438.23/118.03 [n__0] = [0] 438.23/118.03 438.23/118.03 [n__plus](x1, x2) = [1] x1 + [1] x2 + [4] 438.23/118.03 438.23/118.03 [isNatKind](x1) = [4] 438.23/118.03 438.23/118.03 [n__isNatKind](x1) = [4] 438.23/118.03 438.23/118.03 [n__s](x1) = [1] x1 + [1] 438.23/118.03 438.23/118.03 [0] = [0] 438.23/118.03 438.23/118.03 [n__and](x1, x2) = [1] x2 + [0] 438.23/118.03 438.23/118.03 [U11^#](x1, x2, x3) = [2] x1 + [2] x2 + [2] x3 + [0] 438.23/118.03 438.23/118.03 [U12^#](x1, x2) = [2] x2 + [2] 438.23/118.03 438.23/118.03 [isNat^#](x1) = [2] x1 + [2] 438.23/118.03 438.23/118.03 [activate^#](x1) = [0] 438.23/118.03 438.23/118.03 [and^#](x1, x2) = [0] 438.23/118.03 438.23/118.03 [isNatKind^#](x1) = [0] 438.23/118.03 438.23/118.03 [U21^#](x1, x2) = [1] x1 + [2] x2 + [0] 438.23/118.03 438.23/118.03 [c_1](x1, x2, x3, x4) = [1] x1 + [1] x2 + [3] 438.23/118.03 438.23/118.03 [c_2](x1, x2) = [1] x1 + [0] 438.23/118.03 438.23/118.03 [c_3](x1, x2, x3, x4, x5, x6, x7) = [1] x1 + [4] x2 + [2] x3 + [2] 438.23/118.03 438.23/118.03 [c_4](x1, x2, x3, x4) = [1] x1 + [4] x2 + [0] 438.23/118.03 438.23/118.03 [c_10](x1, x2) = [1] x1 + [0] 438.23/118.03 438.23/118.03 The order satisfies the following ordering constraints: 438.23/118.03 438.23/118.03 [U11(tt(), V1, V2)] = [0] 438.23/118.03 >= [0] 438.23/118.03 = [U12(isNat(activate(V1)), activate(V2))] 438.23/118.03 438.23/118.03 [U12(tt(), V2)] = [0] 438.23/118.03 >= [0] 438.23/118.03 = [U13(isNat(activate(V2)))] 438.23/118.03 438.23/118.03 [isNat(n__0())] = [0] 438.23/118.03 ? [4] 438.23/118.03 = [tt()] 438.23/118.03 438.23/118.03 [isNat(n__plus(V1, V2))] = [0] 438.23/118.03 >= [0] 438.23/118.03 = [U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2))] 438.23/118.03 438.23/118.03 [isNat(n__s(V1))] = [0] 438.23/118.03 >= [0] 438.23/118.03 = [U21(isNatKind(activate(V1)), activate(V1))] 438.23/118.03 438.23/118.03 [activate(X)] = [1] X + [0] 438.23/118.03 >= [1] X + [0] 438.23/118.03 = [X] 438.23/118.03 438.23/118.03 [activate(n__0())] = [0] 438.23/118.03 >= [0] 438.23/118.03 = [0()] 438.23/118.03 438.23/118.03 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [4] 438.23/118.03 >= [1] X1 + [1] X2 + [4] 438.23/118.03 = [plus(X1, X2)] 438.23/118.03 438.23/118.03 [activate(n__isNatKind(X))] = [4] 438.23/118.03 >= [4] 438.23/118.03 = [isNatKind(X)] 438.23/118.03 438.23/118.03 [activate(n__s(X))] = [1] X + [1] 438.23/118.03 >= [1] X + [1] 438.23/118.03 = [s(X)] 438.23/118.03 438.23/118.03 [activate(n__and(X1, X2))] = [1] X2 + [0] 438.23/118.03 >= [1] X2 + [0] 438.23/118.03 = [and(X1, X2)] 438.23/118.03 438.23/118.03 [U13(tt())] = [0] 438.23/118.03 ? [4] 438.23/118.03 = [tt()] 438.23/118.03 438.23/118.03 [U21(tt(), V1)] = [0] 438.23/118.03 >= [0] 438.23/118.03 = [U22(isNat(activate(V1)))] 438.23/118.03 438.23/118.03 [U22(tt())] = [0] 438.23/118.03 ? [4] 438.23/118.03 = [tt()] 438.23/118.03 438.23/118.03 [s(X)] = [1] X + [1] 438.23/118.03 >= [1] X + [1] 438.23/118.03 = [n__s(X)] 438.23/118.03 438.23/118.03 [plus(X1, X2)] = [1] X1 + [1] X2 + [4] 438.23/118.03 >= [1] X1 + [1] X2 + [4] 438.23/118.03 = [n__plus(X1, X2)] 438.23/118.03 438.23/118.03 [and(X1, X2)] = [1] X2 + [0] 438.23/118.03 >= [1] X2 + [0] 438.23/118.03 = [n__and(X1, X2)] 438.23/118.03 438.23/118.03 [and(tt(), X)] = [1] X + [0] 438.23/118.03 >= [1] X + [0] 438.23/118.03 = [activate(X)] 438.23/118.03 438.23/118.03 [isNatKind(X)] = [4] 438.23/118.03 >= [4] 438.23/118.03 = [n__isNatKind(X)] 438.23/118.03 438.23/118.03 [isNatKind(n__0())] = [4] 438.23/118.03 >= [4] 438.23/118.03 = [tt()] 438.23/118.03 438.23/118.03 [isNatKind(n__plus(V1, V2))] = [4] 438.23/118.03 >= [4] 438.23/118.03 = [and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))] 438.23/118.03 438.23/118.03 [isNatKind(n__s(V1))] = [4] 438.23/118.03 >= [4] 438.23/118.03 = [isNatKind(activate(V1))] 438.23/118.03 438.23/118.03 [0()] = [0] 438.23/118.03 >= [0] 438.23/118.03 = [n__0()] 438.23/118.03 438.23/118.03 [U11^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [8] 438.23/118.03 > [2] V1 + [2] V2 + [7] 438.23/118.03 = [c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2))] 438.23/118.03 438.23/118.03 [U12^#(tt(), V2)] = [2] V2 + [2] 438.23/118.03 >= [2] V2 + [2] 438.23/118.03 = [c_2(isNat^#(activate(V2)), activate^#(V2))] 438.23/118.03 438.23/118.03 [isNat^#(n__plus(V1, V2))] = [2] V1 + [2] V2 + [10] 438.23/118.03 >= [2] V1 + [2] V2 + [10] 438.23/118.03 = [c_3(U11^#(and(isNatKind(activate(V1)), 438.23/118.03 n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)), 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2))] 438.23/118.03 438.23/118.03 [isNat^#(n__s(V1))] = [2] V1 + [4] 438.23/118.03 >= [2] V1 + [4] 438.23/118.03 = [c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V1))] 438.23/118.03 438.23/118.03 [U21^#(tt(), V1)] = [2] V1 + [4] 438.23/118.03 > [2] V1 + [2] 438.23/118.03 = [c_10(isNat^#(activate(V1)), activate^#(V1))] 438.23/118.03 438.23/118.03 438.23/118.03 We return to the main proof. Consider the set of all dependency 438.23/118.03 pairs 438.23/118.03 438.23/118.03 : 438.23/118.03 { 1: U11^#(tt(), V1, V2) -> 438.23/118.03 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , 2: U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.03 , 3: isNat^#(n__plus(V1, V2)) -> 438.23/118.03 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)), 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , 4: isNat^#(n__s(V1)) -> 438.23/118.03 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.03 isNatKind^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V1)) 438.23/118.03 , 5: U21^#(tt(), V1) -> 438.23/118.03 c_10(isNat^#(activate(V1)), activate^#(V1)) } 438.23/118.03 438.23/118.03 Processor 'matrix interpretation of dimension 1' induces the 438.23/118.03 complexity certificate YES(?,O(n^1)) on application of dependency 438.23/118.03 pairs {1,5}. These cover all (indirect) predecessors of dependency 438.23/118.03 pairs {1,2,3,4,5}, their number of application is equally bounded. 438.23/118.03 The dependency pairs are shifted into the weak component. 438.23/118.03 438.23/118.03 We are left with following problem, upon which TcT provides the 438.23/118.03 certificate YES(O(1),O(1)). 438.23/118.03 438.23/118.03 Weak DPs: 438.23/118.03 { U11^#(tt(), V1, V2) -> 438.23/118.03 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.03 isNat^#(activate(V1)), 438.23/118.03 activate^#(V1), 438.23/118.03 activate^#(V2)) 438.23/118.03 , U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.03 , isNat^#(n__plus(V1, V2)) -> 438.23/118.03 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.03 activate(V1), 438.23/118.03 activate(V2)), 438.23/118.03 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 isNatKind^#(activate(V1)), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V2), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V2)) 438.23/118.04 , isNat^#(n__s(V1)) -> 438.23/118.04 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.04 isNatKind^#(activate(V1)), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V1)) 438.23/118.04 , U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) } 438.23/118.04 Weak Trs: 438.23/118.04 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.04 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.04 , isNat(n__0()) -> tt() 438.23/118.04 , isNat(n__plus(V1, V2)) -> 438.23/118.04 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 activate(V1), 438.23/118.04 activate(V2)) 438.23/118.04 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.04 , activate(X) -> X 438.23/118.04 , activate(n__0()) -> 0() 438.23/118.04 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.04 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.04 , activate(n__s(X)) -> s(X) 438.23/118.04 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.04 , U13(tt()) -> tt() 438.23/118.04 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.04 , U22(tt()) -> tt() 438.23/118.04 , s(X) -> n__s(X) 438.23/118.04 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.04 , and(X1, X2) -> n__and(X1, X2) 438.23/118.04 , and(tt(), X) -> activate(X) 438.23/118.04 , isNatKind(X) -> n__isNatKind(X) 438.23/118.04 , isNatKind(n__0()) -> tt() 438.23/118.04 , isNatKind(n__plus(V1, V2)) -> 438.23/118.04 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.04 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.04 , 0() -> n__0() } 438.23/118.04 Obligation: 438.23/118.04 innermost runtime complexity 438.23/118.04 Answer: 438.23/118.04 YES(O(1),O(1)) 438.23/118.04 438.23/118.04 The following weak DPs constitute a sub-graph of the DG that is 438.23/118.04 closed under successors. The DPs are removed. 438.23/118.04 438.23/118.04 { U11^#(tt(), V1, V2) -> 438.23/118.04 c_1(U12^#(isNat(activate(V1)), activate(V2)), 438.23/118.04 isNat^#(activate(V1)), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V2)) 438.23/118.04 , U12^#(tt(), V2) -> c_2(isNat^#(activate(V2)), activate^#(V2)) 438.23/118.04 , isNat^#(n__plus(V1, V2)) -> 438.23/118.04 c_3(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 activate(V1), 438.23/118.04 activate(V2)), 438.23/118.04 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 isNatKind^#(activate(V1)), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V2), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V2)) 438.23/118.04 , isNat^#(n__s(V1)) -> 438.23/118.04 c_4(U21^#(isNatKind(activate(V1)), activate(V1)), 438.23/118.04 isNatKind^#(activate(V1)), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V1)) 438.23/118.04 , U21^#(tt(), V1) -> c_10(isNat^#(activate(V1)), activate^#(V1)) } 438.23/118.04 438.23/118.04 We are left with following problem, upon which TcT provides the 438.23/118.04 certificate YES(O(1),O(1)). 438.23/118.04 438.23/118.04 Weak Trs: 438.23/118.04 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.04 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.04 , isNat(n__0()) -> tt() 438.23/118.04 , isNat(n__plus(V1, V2)) -> 438.23/118.04 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 activate(V1), 438.23/118.04 activate(V2)) 438.23/118.04 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.04 , activate(X) -> X 438.23/118.04 , activate(n__0()) -> 0() 438.23/118.04 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.04 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.04 , activate(n__s(X)) -> s(X) 438.23/118.04 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.04 , U13(tt()) -> tt() 438.23/118.04 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.04 , U22(tt()) -> tt() 438.23/118.04 , s(X) -> n__s(X) 438.23/118.04 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.04 , and(X1, X2) -> n__and(X1, X2) 438.23/118.04 , and(tt(), X) -> activate(X) 438.23/118.04 , isNatKind(X) -> n__isNatKind(X) 438.23/118.04 , isNatKind(n__0()) -> tt() 438.23/118.04 , isNatKind(n__plus(V1, V2)) -> 438.23/118.04 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.04 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.04 , 0() -> n__0() } 438.23/118.04 Obligation: 438.23/118.04 innermost runtime complexity 438.23/118.04 Answer: 438.23/118.04 YES(O(1),O(1)) 438.23/118.04 438.23/118.04 No rule is usable, rules are removed from the input problem. 438.23/118.04 438.23/118.04 We are left with following problem, upon which TcT provides the 438.23/118.04 certificate YES(O(1),O(1)). 438.23/118.04 438.23/118.04 Rules: Empty 438.23/118.04 Obligation: 438.23/118.04 innermost runtime complexity 438.23/118.04 Answer: 438.23/118.04 YES(O(1),O(1)) 438.23/118.04 438.23/118.04 Empty rules are trivially bounded 438.23/118.04 438.23/118.04 We return to the main proof. 438.23/118.04 438.23/118.04 We are left with following problem, upon which TcT provides the 438.23/118.04 certificate YES(O(1),O(n^1)). 438.23/118.04 438.23/118.04 Strict DPs: 438.23/118.04 { activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.04 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.04 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.04 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.04 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 isNatKind^#(activate(V1)), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V2)) 438.23/118.04 , isNatKind^#(n__s(V1)) -> 438.23/118.04 c_9(isNatKind^#(activate(V1)), activate^#(V1)) } 438.23/118.04 Weak DPs: 438.23/118.04 { U11^#(tt(), V1, V2) -> U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.04 , U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.04 , U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.04 , U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.04 , U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.04 , U12^#(tt(), V2) -> activate^#(V2) 438.23/118.04 , isNat^#(n__plus(V1, V2)) -> 438.23/118.04 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 activate(V1), 438.23/118.04 activate(V2)) 438.23/118.04 , isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.04 , isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.04 , isNat^#(n__plus(V1, V2)) -> 438.23/118.04 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.04 , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.04 , isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.04 , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.04 , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.04 , U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.04 , U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.04 Weak Trs: 438.23/118.04 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.04 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.04 , isNat(n__0()) -> tt() 438.23/118.04 , isNat(n__plus(V1, V2)) -> 438.23/118.04 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 activate(V1), 438.23/118.04 activate(V2)) 438.23/118.04 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.04 , activate(X) -> X 438.23/118.04 , activate(n__0()) -> 0() 438.23/118.04 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.04 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.04 , activate(n__s(X)) -> s(X) 438.23/118.04 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.04 , U13(tt()) -> tt() 438.23/118.04 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.04 , U22(tt()) -> tt() 438.23/118.04 , s(X) -> n__s(X) 438.23/118.04 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.04 , and(X1, X2) -> n__and(X1, X2) 438.23/118.04 , and(tt(), X) -> activate(X) 438.23/118.04 , isNatKind(X) -> n__isNatKind(X) 438.23/118.04 , isNatKind(n__0()) -> tt() 438.23/118.04 , isNatKind(n__plus(V1, V2)) -> 438.23/118.04 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.04 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.04 , 0() -> n__0() } 438.23/118.04 Obligation: 438.23/118.04 innermost runtime complexity 438.23/118.04 Answer: 438.23/118.04 YES(O(1),O(n^1)) 438.23/118.04 438.23/118.04 We use the processor 'matrix interpretation of dimension 2' to 438.23/118.04 orient following rules strictly. 438.23/118.04 438.23/118.04 DPs: 438.23/118.04 { 5: isNatKind^#(n__s(V1)) -> 438.23/118.04 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.04 , 17: isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.04 , 18: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.04 , 19: isNat^#(n__s(V1)) -> 438.23/118.04 U21^#(isNatKind(activate(V1)), activate(V1)) } 438.23/118.04 Trs: 438.23/118.04 { activate(n__s(X)) -> s(X) 438.23/118.04 , s(X) -> n__s(X) 438.23/118.04 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) } 438.23/118.04 438.23/118.04 Sub-proof: 438.23/118.04 ---------- 438.23/118.04 The following argument positions are usable: 438.23/118.04 Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, 438.23/118.04 Uargs(c_8) = {1, 2, 3, 4}, Uargs(c_9) = {1, 2} 438.23/118.04 438.23/118.04 TcT has computed the following constructor-based matrix 438.23/118.04 interpretation satisfying not(EDA) and not(IDA(1)). 438.23/118.04 438.23/118.04 [U11](x1, x2, x3) = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [tt] = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [U12](x1, x2) = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [isNat](x1) = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [activate](x1) = [2 0] x1 + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 438.23/118.04 [U13](x1) = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [U21](x1, x2) = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [U22](x1) = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [s](x1) = [0 0] x1 + [5] 438.23/118.04 [1 1] [2] 438.23/118.04 438.23/118.04 [plus](x1, x2) = [0 0] x1 + [0 0] x2 + [0] 438.23/118.04 [1 1] [1 1] [0] 438.23/118.04 438.23/118.04 [and](x1, x2) = [2 0] x2 + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 438.23/118.04 [n__0] = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [n__plus](x1, x2) = [0 0] x1 + [0 0] x2 + [0] 438.23/118.04 [1 1] [1 1] [0] 438.23/118.04 438.23/118.04 [isNatKind](x1) = [0 2] x1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [n__isNatKind](x1) = [0 1] x1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [n__s](x1) = [0 0] x1 + [4] 438.23/118.04 [1 1] [2] 438.23/118.04 438.23/118.04 [0] = [0] 438.23/118.04 [0] 438.23/118.04 438.23/118.04 [n__and](x1, x2) = [1 0] x2 + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 438.23/118.04 [U11^#](x1, x2, x3) = [2 4] x2 + [2 4] x3 + [0] 438.23/118.04 [0 4] [0 4] [0] 438.23/118.04 438.23/118.04 [U12^#](x1, x2) = [1 4] x2 + [0] 438.23/118.04 [0 4] [0] 438.23/118.04 438.23/118.04 [isNat^#](x1) = [0 4] x1 + [0] 438.23/118.04 [0 4] [0] 438.23/118.04 438.23/118.04 [activate^#](x1) = [1 0] x1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [and^#](x1, x2) = [1 0] x2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [isNatKind^#](x1) = [0 1] x1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [U21^#](x1, x2) = [2 4] x2 + [0] 438.23/118.04 [0 4] [4] 438.23/118.04 438.23/118.04 [c_5](x1) = [1 0] x1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [c_6](x1) = [1 0] x1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [c_7](x1) = [1 0] x1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 438.23/118.04 [c_8](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 438.23/118.04 0] x4 + [0] 438.23/118.04 [0 0] [0 0] [0 0] [0 438.23/118.04 0] [0] 438.23/118.04 438.23/118.04 [c_9](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 438.23/118.04 [0 0] [0 0] [0] 438.23/118.04 438.23/118.04 The order satisfies the following ordering constraints: 438.23/118.04 438.23/118.04 [U11(tt(), V1, V2)] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [U12(isNat(activate(V1)), activate(V2))] 438.23/118.04 438.23/118.04 [U12(tt(), V2)] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [U13(isNat(activate(V2)))] 438.23/118.04 438.23/118.04 [isNat(n__0())] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [tt()] 438.23/118.04 438.23/118.04 [isNat(n__plus(V1, V2))] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 activate(V1), 438.23/118.04 activate(V2))] 438.23/118.04 438.23/118.04 [isNat(n__s(V1))] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [U21(isNatKind(activate(V1)), activate(V1))] 438.23/118.04 438.23/118.04 [activate(X)] = [2 0] X + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 >= [1 0] X + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 = [X] 438.23/118.04 438.23/118.04 [activate(n__0())] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [0()] 438.23/118.04 438.23/118.04 [activate(n__plus(X1, X2))] = [0 0] X1 + [0 0] X2 + [0] 438.23/118.04 [1 1] [1 1] [0] 438.23/118.04 >= [0 0] X1 + [0 0] X2 + [0] 438.23/118.04 [1 1] [1 1] [0] 438.23/118.04 = [plus(X1, X2)] 438.23/118.04 438.23/118.04 [activate(n__isNatKind(X))] = [0 2] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 >= [0 2] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [isNatKind(X)] 438.23/118.04 438.23/118.04 [activate(n__s(X))] = [0 0] X + [8] 438.23/118.04 [1 1] [2] 438.23/118.04 > [0 0] X + [5] 438.23/118.04 [1 1] [2] 438.23/118.04 = [s(X)] 438.23/118.04 438.23/118.04 [activate(n__and(X1, X2))] = [2 0] X2 + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 >= [2 0] X2 + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 = [and(X1, X2)] 438.23/118.04 438.23/118.04 [U13(tt())] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [tt()] 438.23/118.04 438.23/118.04 [U21(tt(), V1)] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [U22(isNat(activate(V1)))] 438.23/118.04 438.23/118.04 [U22(tt())] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [tt()] 438.23/118.04 438.23/118.04 [s(X)] = [0 0] X + [5] 438.23/118.04 [1 1] [2] 438.23/118.04 > [0 0] X + [4] 438.23/118.04 [1 1] [2] 438.23/118.04 = [n__s(X)] 438.23/118.04 438.23/118.04 [plus(X1, X2)] = [0 0] X1 + [0 0] X2 + [0] 438.23/118.04 [1 1] [1 1] [0] 438.23/118.04 >= [0 0] X1 + [0 0] X2 + [0] 438.23/118.04 [1 1] [1 1] [0] 438.23/118.04 = [n__plus(X1, X2)] 438.23/118.04 438.23/118.04 [and(X1, X2)] = [2 0] X2 + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 >= [1 0] X2 + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 = [n__and(X1, X2)] 438.23/118.04 438.23/118.04 [and(tt(), X)] = [2 0] X + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 >= [2 0] X + [0] 438.23/118.04 [0 1] [0] 438.23/118.04 = [activate(X)] 438.23/118.04 438.23/118.04 [isNatKind(X)] = [0 2] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 >= [0 1] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [n__isNatKind(X)] 438.23/118.04 438.23/118.04 [isNatKind(n__0())] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [tt()] 438.23/118.04 438.23/118.04 [isNatKind(n__plus(V1, V2))] = [2 2] V1 + [2 2] V2 + [0] 438.23/118.04 [0 0] [0 0] [0] 438.23/118.04 >= [0 2] V2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))] 438.23/118.04 438.23/118.04 [isNatKind(n__s(V1))] = [2 2] V1 + [4] 438.23/118.04 [0 0] [0] 438.23/118.04 > [0 2] V1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [isNatKind(activate(V1))] 438.23/118.04 438.23/118.04 [0()] = [0] 438.23/118.04 [0] 438.23/118.04 >= [0] 438.23/118.04 [0] 438.23/118.04 = [n__0()] 438.23/118.04 438.23/118.04 [U11^#(tt(), V1, V2)] = [2 4] V1 + [2 4] V2 + [0] 438.23/118.04 [0 4] [0 4] [0] 438.23/118.04 >= [2 4] V2 + [0] 438.23/118.04 [0 4] [0] 438.23/118.04 = [U12^#(isNat(activate(V1)), activate(V2))] 438.23/118.04 438.23/118.04 [U11^#(tt(), V1, V2)] = [2 4] V1 + [2 4] V2 + [0] 438.23/118.04 [0 4] [0 4] [0] 438.23/118.04 >= [0 4] V1 + [0] 438.23/118.04 [0 4] [0] 438.23/118.04 = [isNat^#(activate(V1))] 438.23/118.04 438.23/118.04 [U11^#(tt(), V1, V2)] = [2 4] V1 + [2 4] V2 + [0] 438.23/118.04 [0 4] [0 4] [0] 438.23/118.04 >= [1 0] V1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [activate^#(V1)] 438.23/118.04 438.23/118.04 [U11^#(tt(), V1, V2)] = [2 4] V1 + [2 4] V2 + [0] 438.23/118.04 [0 4] [0 4] [0] 438.23/118.04 >= [1 0] V2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [activate^#(V2)] 438.23/118.04 438.23/118.04 [U12^#(tt(), V2)] = [1 4] V2 + [0] 438.23/118.04 [0 4] [0] 438.23/118.04 >= [0 4] V2 + [0] 438.23/118.04 [0 4] [0] 438.23/118.04 = [isNat^#(activate(V2))] 438.23/118.04 438.23/118.04 [U12^#(tt(), V2)] = [1 4] V2 + [0] 438.23/118.04 [0 4] [0] 438.23/118.04 >= [1 0] V2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [activate^#(V2)] 438.23/118.04 438.23/118.04 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [0] 438.23/118.04 [4 4] [4 4] [0] 438.23/118.04 >= [4 4] V1 + [4 4] V2 + [0] 438.23/118.04 [0 4] [0 4] [0] 438.23/118.04 = [U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 activate(V1), 438.23/118.04 activate(V2))] 438.23/118.04 438.23/118.04 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [0] 438.23/118.04 [4 4] [4 4] [0] 438.23/118.04 >= [1 0] V1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [activate^#(V1)] 438.23/118.04 438.23/118.04 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [0] 438.23/118.04 [4 4] [4 4] [0] 438.23/118.04 >= [1 0] V2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [activate^#(V2)] 438.23/118.04 438.23/118.04 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [0] 438.23/118.04 [4 4] [4 4] [0] 438.23/118.04 >= [0 1] V2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))] 438.23/118.04 438.23/118.04 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [0] 438.23/118.04 [4 4] [4 4] [0] 438.23/118.04 >= [0 1] V1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [isNatKind^#(activate(V1))] 438.23/118.04 438.23/118.04 [isNat^#(n__s(V1))] = [4 4] V1 + [8] 438.23/118.04 [4 4] [8] 438.23/118.04 > [1 0] V1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [activate^#(V1)] 438.23/118.04 438.23/118.04 [isNat^#(n__s(V1))] = [4 4] V1 + [8] 438.23/118.04 [4 4] [8] 438.23/118.04 > [0 1] V1 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [isNatKind^#(activate(V1))] 438.23/118.04 438.23/118.04 [isNat^#(n__s(V1))] = [4 4] V1 + [8] 438.23/118.04 [4 4] [8] 438.23/118.04 > [4 4] V1 + [0] 438.23/118.04 [0 4] [4] 438.23/118.04 = [U21^#(isNatKind(activate(V1)), activate(V1))] 438.23/118.04 438.23/118.04 [activate^#(n__isNatKind(X))] = [0 1] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 >= [0 1] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [c_5(isNatKind^#(X))] 438.23/118.04 438.23/118.04 [activate^#(n__and(X1, X2))] = [1 0] X2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 >= [1 0] X2 + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [c_6(and^#(X1, X2))] 438.23/118.04 438.23/118.04 [and^#(tt(), X)] = [1 0] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 >= [1 0] X + [0] 438.23/118.04 [0 0] [0] 438.23/118.04 = [c_7(activate^#(X))] 438.23/118.04 438.23/118.04 [isNatKind^#(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [0] 438.23/118.04 [0 0] [0 0] [0] 438.23/118.04 >= [1 1] V1 + [1 1] V2 + [0] 438.23/118.04 [0 0] [0 0] [0] 438.23/118.04 = [c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.04 isNatKind^#(activate(V1)), 438.23/118.04 activate^#(V1), 438.23/118.04 activate^#(V2))] 438.23/118.04 438.23/118.04 [isNatKind^#(n__s(V1))] = [1 1] V1 + [2] 438.23/118.04 [0 0] [0] 438.23/118.04 > [1 1] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [c_9(isNatKind^#(activate(V1)), activate^#(V1))] 438.23/118.05 438.23/118.05 [U21^#(tt(), V1)] = [2 4] V1 + [0] 438.23/118.05 [0 4] [4] 438.23/118.05 >= [0 4] V1 + [0] 438.23/118.05 [0 4] [0] 438.23/118.05 = [isNat^#(activate(V1))] 438.23/118.05 438.23/118.05 [U21^#(tt(), V1)] = [2 4] V1 + [0] 438.23/118.05 [0 4] [4] 438.23/118.05 >= [1 0] V1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V1)] 438.23/118.05 438.23/118.05 438.23/118.05 We return to the main proof. Consider the set of all dependency 438.23/118.05 pairs 438.23/118.05 438.23/118.05 : 438.23/118.05 { 1: activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.05 , 2: activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.05 , 3: and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.05 , 4: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.05 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 isNatKind^#(activate(V1)), 438.23/118.05 activate^#(V1), 438.23/118.05 activate^#(V2)) 438.23/118.05 , 5: isNatKind^#(n__s(V1)) -> 438.23/118.05 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.05 , 6: U11^#(tt(), V1, V2) -> 438.23/118.05 U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.05 , 7: U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.05 , 8: U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.05 , 9: U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.05 , 10: U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.05 , 11: U12^#(tt(), V2) -> activate^#(V2) 438.23/118.05 , 12: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , 13: isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.05 , 14: isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.05 , 15: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , 16: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.05 , 17: isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.05 , 18: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.05 , 19: isNat^#(n__s(V1)) -> 438.23/118.05 U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.05 , 20: U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.05 , 21: U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.05 438.23/118.05 Processor 'matrix interpretation of dimension 2' induces the 438.23/118.05 complexity certificate YES(?,O(n^1)) on application of dependency 438.23/118.05 pairs {5,17,18,19}. These cover all (indirect) predecessors of 438.23/118.05 dependency pairs {5,17,18,19,20,21}, their number of application is 438.23/118.05 equally bounded. The dependency pairs are shifted into the weak 438.23/118.05 component. 438.23/118.05 438.23/118.05 We are left with following problem, upon which TcT provides the 438.23/118.05 certificate YES(O(1),O(n^1)). 438.23/118.05 438.23/118.05 Strict DPs: 438.23/118.05 { activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.05 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.05 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.05 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.05 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 isNatKind^#(activate(V1)), 438.23/118.05 activate^#(V1), 438.23/118.05 activate^#(V2)) } 438.23/118.05 Weak DPs: 438.23/118.05 { U11^#(tt(), V1, V2) -> U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.05 , U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.05 , U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.05 , U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.05 , U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.05 , U12^#(tt(), V2) -> activate^#(V2) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> 438.23/118.05 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> 438.23/118.05 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.05 , isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.05 , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.05 , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.05 , isNatKind^#(n__s(V1)) -> 438.23/118.05 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.05 , U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.05 , U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.05 Weak Trs: 438.23/118.05 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.05 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.05 , isNat(n__0()) -> tt() 438.23/118.05 , isNat(n__plus(V1, V2)) -> 438.23/118.05 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.05 , activate(X) -> X 438.23/118.05 , activate(n__0()) -> 0() 438.23/118.05 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.05 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.05 , activate(n__s(X)) -> s(X) 438.23/118.05 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.05 , U13(tt()) -> tt() 438.23/118.05 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.05 , U22(tt()) -> tt() 438.23/118.05 , s(X) -> n__s(X) 438.23/118.05 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.05 , and(X1, X2) -> n__and(X1, X2) 438.23/118.05 , and(tt(), X) -> activate(X) 438.23/118.05 , isNatKind(X) -> n__isNatKind(X) 438.23/118.05 , isNatKind(n__0()) -> tt() 438.23/118.05 , isNatKind(n__plus(V1, V2)) -> 438.23/118.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.05 , 0() -> n__0() } 438.23/118.05 Obligation: 438.23/118.05 innermost runtime complexity 438.23/118.05 Answer: 438.23/118.05 YES(O(1),O(n^1)) 438.23/118.05 438.23/118.05 We use the processor 'matrix interpretation of dimension 2' to 438.23/118.05 orient following rules strictly. 438.23/118.05 438.23/118.05 DPs: 438.23/118.05 { 2: activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.05 , 4: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.05 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 isNatKind^#(activate(V1)), 438.23/118.05 activate^#(V1), 438.23/118.05 activate^#(V2)) 438.23/118.05 , 6: U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.05 , 7: U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.05 , 8: U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.05 , 9: U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.05 , 10: U12^#(tt(), V2) -> activate^#(V2) 438.23/118.05 , 11: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , 12: isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.05 , 13: isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.05 , 14: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , 15: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.05 , 16: isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.05 , 21: U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.05 Trs: 438.23/118.05 { activate(n__0()) -> 0() 438.23/118.05 , activate(n__s(X)) -> s(X) 438.23/118.05 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.05 , s(X) -> n__s(X) 438.23/118.05 , and(tt(), X) -> activate(X) 438.23/118.05 , isNatKind(X) -> n__isNatKind(X) 438.23/118.05 , isNatKind(n__0()) -> tt() 438.23/118.05 , isNatKind(n__plus(V1, V2)) -> 438.23/118.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , 0() -> n__0() } 438.23/118.05 438.23/118.05 Sub-proof: 438.23/118.05 ---------- 438.23/118.05 The following argument positions are usable: 438.23/118.05 Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, 438.23/118.05 Uargs(c_8) = {1, 2, 3, 4}, Uargs(c_9) = {1, 2} 438.23/118.05 438.23/118.05 TcT has computed the following constructor-based matrix 438.23/118.05 interpretation satisfying not(EDA) and not(IDA(1)). 438.23/118.05 438.23/118.05 [U11](x1, x2, x3) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [tt] = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [U12](x1, x2) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [isNat](x1) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [activate](x1) = [2 0] x1 + [0] 438.23/118.05 [0 1] [0] 438.23/118.05 438.23/118.05 [U13](x1) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [U21](x1, x2) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [U22](x1) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [s](x1) = [0 0] x1 + [5] 438.23/118.05 [1 1] [0] 438.23/118.05 438.23/118.05 [plus](x1, x2) = [0 0] x1 + [0 0] x2 + [0] 438.23/118.05 [1 1] [1 1] [3] 438.23/118.05 438.23/118.05 [and](x1, x2) = [2 0] x2 + [1] 438.23/118.05 [0 1] [0] 438.23/118.05 438.23/118.05 [n__0] = [4] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [n__plus](x1, x2) = [0 0] x1 + [0 0] x2 + [0] 438.23/118.05 [1 1] [1 1] [3] 438.23/118.05 438.23/118.05 [isNatKind](x1) = [0 2] x1 + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [n__isNatKind](x1) = [0 1] x1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [n__s](x1) = [0 0] x1 + [4] 438.23/118.05 [1 1] [0] 438.23/118.05 438.23/118.05 [0] = [5] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [n__and](x1, x2) = [1 0] x2 + [1] 438.23/118.05 [0 1] [0] 438.23/118.05 438.23/118.05 [U11^#](x1, x2, x3) = [1 4] x2 + [2 4] x3 + [2] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 438.23/118.05 [U12^#](x1, x2) = [1 4] x2 + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [isNat^#](x1) = [0 4] x1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [activate^#](x1) = [1 0] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [and^#](x1, x2) = [1 0] x2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [isNatKind^#](x1) = [0 1] x1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [U21^#](x1, x2) = [2 4] x2 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_5](x1) = [1 0] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_6](x1) = [1 0] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_7](x1) = [1 0] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_8](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 438.23/118.05 0] x4 + [1] 438.23/118.05 [0 0] [0 0] [0 0] [0 438.23/118.05 0] [0] 438.23/118.05 438.23/118.05 [c_9](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 438.23/118.05 The order satisfies the following ordering constraints: 438.23/118.05 438.23/118.05 [U11(tt(), V1, V2)] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [U12(isNat(activate(V1)), activate(V2))] 438.23/118.05 438.23/118.05 [U12(tt(), V2)] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [U13(isNat(activate(V2)))] 438.23/118.05 438.23/118.05 [isNat(n__0())] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [tt()] 438.23/118.05 438.23/118.05 [isNat(n__plus(V1, V2))] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2))] 438.23/118.05 438.23/118.05 [isNat(n__s(V1))] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [U21(isNatKind(activate(V1)), activate(V1))] 438.23/118.05 438.23/118.05 [activate(X)] = [2 0] X + [0] 438.23/118.05 [0 1] [0] 438.23/118.05 >= [1 0] X + [0] 438.23/118.05 [0 1] [0] 438.23/118.05 = [X] 438.23/118.05 438.23/118.05 [activate(n__0())] = [8] 438.23/118.05 [0] 438.23/118.05 > [5] 438.23/118.05 [0] 438.23/118.05 = [0()] 438.23/118.05 438.23/118.05 [activate(n__plus(X1, X2))] = [0 0] X1 + [0 0] X2 + [0] 438.23/118.05 [1 1] [1 1] [3] 438.23/118.05 >= [0 0] X1 + [0 0] X2 + [0] 438.23/118.05 [1 1] [1 1] [3] 438.23/118.05 = [plus(X1, X2)] 438.23/118.05 438.23/118.05 [activate(n__isNatKind(X))] = [0 2] X + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [0 2] X + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 = [isNatKind(X)] 438.23/118.05 438.23/118.05 [activate(n__s(X))] = [0 0] X + [8] 438.23/118.05 [1 1] [0] 438.23/118.05 > [0 0] X + [5] 438.23/118.05 [1 1] [0] 438.23/118.05 = [s(X)] 438.23/118.05 438.23/118.05 [activate(n__and(X1, X2))] = [2 0] X2 + [2] 438.23/118.05 [0 1] [0] 438.23/118.05 > [2 0] X2 + [1] 438.23/118.05 [0 1] [0] 438.23/118.05 = [and(X1, X2)] 438.23/118.05 438.23/118.05 [U13(tt())] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [tt()] 438.23/118.05 438.23/118.05 [U21(tt(), V1)] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [U22(isNat(activate(V1)))] 438.23/118.05 438.23/118.05 [U22(tt())] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [tt()] 438.23/118.05 438.23/118.05 [s(X)] = [0 0] X + [5] 438.23/118.05 [1 1] [0] 438.23/118.05 > [0 0] X + [4] 438.23/118.05 [1 1] [0] 438.23/118.05 = [n__s(X)] 438.23/118.05 438.23/118.05 [plus(X1, X2)] = [0 0] X1 + [0 0] X2 + [0] 438.23/118.05 [1 1] [1 1] [3] 438.23/118.05 >= [0 0] X1 + [0 0] X2 + [0] 438.23/118.05 [1 1] [1 1] [3] 438.23/118.05 = [n__plus(X1, X2)] 438.23/118.05 438.23/118.05 [and(X1, X2)] = [2 0] X2 + [1] 438.23/118.05 [0 1] [0] 438.23/118.05 >= [1 0] X2 + [1] 438.23/118.05 [0 1] [0] 438.23/118.05 = [n__and(X1, X2)] 438.23/118.05 438.23/118.05 [and(tt(), X)] = [2 0] X + [1] 438.23/118.05 [0 1] [0] 438.23/118.05 > [2 0] X + [0] 438.23/118.05 [0 1] [0] 438.23/118.05 = [activate(X)] 438.23/118.05 438.23/118.05 [isNatKind(X)] = [0 2] X + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 > [0 1] X + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [n__isNatKind(X)] 438.23/118.05 438.23/118.05 [isNatKind(n__0())] = [2] 438.23/118.05 [0] 438.23/118.05 > [0] 438.23/118.05 [0] 438.23/118.05 = [tt()] 438.23/118.05 438.23/118.05 [isNatKind(n__plus(V1, V2))] = [2 2] V1 + [2 2] V2 + [8] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [0 2] V2 + [3] 438.23/118.05 [0 0] [0] 438.23/118.05 = [and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))] 438.23/118.05 438.23/118.05 [isNatKind(n__s(V1))] = [2 2] V1 + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [0 2] V1 + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 = [isNatKind(activate(V1))] 438.23/118.05 438.23/118.05 [0()] = [5] 438.23/118.05 [0] 438.23/118.05 > [4] 438.23/118.05 [0] 438.23/118.05 = [n__0()] 438.23/118.05 438.23/118.05 [U11^#(tt(), V1, V2)] = [1 4] V1 + [2 4] V2 + [2] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 >= [2 4] V2 + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 = [U12^#(isNat(activate(V1)), activate(V2))] 438.23/118.05 438.23/118.05 [U11^#(tt(), V1, V2)] = [1 4] V1 + [2 4] V2 + [2] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [0 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [isNat^#(activate(V1))] 438.23/118.05 438.23/118.05 [U11^#(tt(), V1, V2)] = [1 4] V1 + [2 4] V2 + [2] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [1 0] V1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V1)] 438.23/118.05 438.23/118.05 [U11^#(tt(), V1, V2)] = [1 4] V1 + [2 4] V2 + [2] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [1 0] V2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V2)] 438.23/118.05 438.23/118.05 [U12^#(tt(), V2)] = [1 4] V2 + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 > [0 4] V2 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [isNat^#(activate(V2))] 438.23/118.05 438.23/118.05 [U12^#(tt(), V2)] = [1 4] V2 + [2] 438.23/118.05 [0 0] [0] 438.23/118.05 > [1 0] V2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V2)] 438.23/118.05 438.23/118.05 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [13] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [2 4] V1 + [4 4] V2 + [2] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 = [U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2))] 438.23/118.05 438.23/118.05 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [13] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [1 0] V1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V1)] 438.23/118.05 438.23/118.05 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [13] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [1 0] V2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V2)] 438.23/118.05 438.23/118.05 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [13] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [0 1] V2 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))] 438.23/118.05 438.23/118.05 [isNat^#(n__plus(V1, V2))] = [4 4] V1 + [4 4] V2 + [13] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [0 1] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [isNatKind^#(activate(V1))] 438.23/118.05 438.23/118.05 [isNat^#(n__s(V1))] = [4 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 > [1 0] V1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V1)] 438.23/118.05 438.23/118.05 [isNat^#(n__s(V1))] = [4 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [0 1] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [isNatKind^#(activate(V1))] 438.23/118.05 438.23/118.05 [isNat^#(n__s(V1))] = [4 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [4 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [U21^#(isNatKind(activate(V1)), activate(V1))] 438.23/118.05 438.23/118.05 [activate^#(n__isNatKind(X))] = [0 1] X + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [0 1] X + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [c_5(isNatKind^#(X))] 438.23/118.05 438.23/118.05 [activate^#(n__and(X1, X2))] = [1 0] X2 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 > [1 0] X2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [c_6(and^#(X1, X2))] 438.23/118.05 438.23/118.05 [and^#(tt(), X)] = [1 0] X + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [1 0] X + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [c_7(activate^#(X))] 438.23/118.05 438.23/118.05 [isNatKind^#(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [4] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 > [1 1] V1 + [1 1] V2 + [3] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 = [c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 isNatKind^#(activate(V1)), 438.23/118.05 activate^#(V1), 438.23/118.05 activate^#(V2))] 438.23/118.05 438.23/118.05 [isNatKind^#(n__s(V1))] = [1 1] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [1 1] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [c_9(isNatKind^#(activate(V1)), activate^#(V1))] 438.23/118.05 438.23/118.05 [U21^#(tt(), V1)] = [2 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 >= [0 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 = [isNat^#(activate(V1))] 438.23/118.05 438.23/118.05 [U21^#(tt(), V1)] = [2 4] V1 + [1] 438.23/118.05 [0 0] [0] 438.23/118.05 > [1 0] V1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 = [activate^#(V1)] 438.23/118.05 438.23/118.05 438.23/118.05 We return to the main proof. Consider the set of all dependency 438.23/118.05 pairs 438.23/118.05 438.23/118.05 : 438.23/118.05 { 1: activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.05 , 2: activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.05 , 3: and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.05 , 4: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.05 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 isNatKind^#(activate(V1)), 438.23/118.05 activate^#(V1), 438.23/118.05 activate^#(V2)) 438.23/118.05 , 5: U11^#(tt(), V1, V2) -> 438.23/118.05 U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.05 , 6: U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.05 , 7: U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.05 , 8: U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.05 , 9: U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.05 , 10: U12^#(tt(), V2) -> activate^#(V2) 438.23/118.05 , 11: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , 12: isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.05 , 13: isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.05 , 14: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , 15: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.05 , 16: isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.05 , 17: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.05 , 18: isNat^#(n__s(V1)) -> 438.23/118.05 U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.05 , 19: isNatKind^#(n__s(V1)) -> 438.23/118.05 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.05 , 20: U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.05 , 21: U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.05 438.23/118.05 Processor 'matrix interpretation of dimension 2' induces the 438.23/118.05 complexity certificate YES(?,O(n^1)) on application of dependency 438.23/118.05 pairs {2,4,6,7,8,9,10,11,12,13,14,15,16,21}. These cover all 438.23/118.05 (indirect) predecessors of dependency pairs 438.23/118.05 {2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,21}, their number of 438.23/118.05 application is equally bounded. The dependency pairs are shifted 438.23/118.05 into the weak component. 438.23/118.05 438.23/118.05 We are left with following problem, upon which TcT provides the 438.23/118.05 certificate YES(O(1),O(n^1)). 438.23/118.05 438.23/118.05 Strict DPs: { activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) } 438.23/118.05 Weak DPs: 438.23/118.05 { U11^#(tt(), V1, V2) -> U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.05 , U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.05 , U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.05 , U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.05 , U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.05 , U12^#(tt(), V2) -> activate^#(V2) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> 438.23/118.05 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> 438.23/118.05 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.05 , isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.05 , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.05 , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.05 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.05 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.05 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.05 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 isNatKind^#(activate(V1)), 438.23/118.05 activate^#(V1), 438.23/118.05 activate^#(V2)) 438.23/118.05 , isNatKind^#(n__s(V1)) -> 438.23/118.05 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.05 , U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.05 , U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.05 Weak Trs: 438.23/118.05 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.05 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.05 , isNat(n__0()) -> tt() 438.23/118.05 , isNat(n__plus(V1, V2)) -> 438.23/118.05 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.05 , activate(X) -> X 438.23/118.05 , activate(n__0()) -> 0() 438.23/118.05 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.05 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.05 , activate(n__s(X)) -> s(X) 438.23/118.05 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.05 , U13(tt()) -> tt() 438.23/118.05 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.05 , U22(tt()) -> tt() 438.23/118.05 , s(X) -> n__s(X) 438.23/118.05 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.05 , and(X1, X2) -> n__and(X1, X2) 438.23/118.05 , and(tt(), X) -> activate(X) 438.23/118.05 , isNatKind(X) -> n__isNatKind(X) 438.23/118.05 , isNatKind(n__0()) -> tt() 438.23/118.05 , isNatKind(n__plus(V1, V2)) -> 438.23/118.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.05 , 0() -> n__0() } 438.23/118.05 Obligation: 438.23/118.05 innermost runtime complexity 438.23/118.05 Answer: 438.23/118.05 YES(O(1),O(n^1)) 438.23/118.05 438.23/118.05 We use the processor 'matrix interpretation of dimension 2' to 438.23/118.05 orient following rules strictly. 438.23/118.05 438.23/118.05 DPs: 438.23/118.05 { 1: activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.05 , 2: U11^#(tt(), V1, V2) -> 438.23/118.05 U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.05 , 3: U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.05 , 4: U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.05 , 5: U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.05 , 8: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 activate(V1), 438.23/118.05 activate(V2)) 438.23/118.05 , 9: isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.05 , 10: isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.05 , 11: isNat^#(n__plus(V1, V2)) -> 438.23/118.05 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , 12: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.05 , 13: isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.05 , 14: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.05 , 15: isNat^#(n__s(V1)) -> 438.23/118.05 U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.05 , 16: activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.05 , 18: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.05 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.05 isNatKind^#(activate(V1)), 438.23/118.05 activate^#(V1), 438.23/118.05 activate^#(V2)) } 438.23/118.05 Trs: 438.23/118.05 { and(tt(), X) -> activate(X) 438.23/118.05 , isNatKind(n__0()) -> tt() 438.23/118.05 , isNatKind(n__plus(V1, V2)) -> 438.23/118.05 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.05 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) } 438.23/118.05 438.23/118.05 Sub-proof: 438.23/118.05 ---------- 438.23/118.05 The following argument positions are usable: 438.23/118.05 Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, 438.23/118.05 Uargs(c_8) = {1, 2, 3, 4}, Uargs(c_9) = {1, 2} 438.23/118.05 438.23/118.05 TcT has computed the following constructor-based matrix 438.23/118.05 interpretation satisfying not(EDA) and not(IDA(1)). 438.23/118.05 438.23/118.05 [U11](x1, x2, x3) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [tt] = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [U12](x1, x2) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [isNat](x1) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [activate](x1) = [1 0] x1 + [0] 438.23/118.05 [0 1] [0] 438.23/118.05 438.23/118.05 [U13](x1) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [U21](x1, x2) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [U22](x1) = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [s](x1) = [0 0] x1 + [0] 438.23/118.05 [1 1] [2] 438.23/118.05 438.23/118.05 [plus](x1, x2) = [0 0] x1 + [0 0] x2 + [0] 438.23/118.05 [1 1] [1 1] [7] 438.23/118.05 438.23/118.05 [and](x1, x2) = [0 1] x1 + [1 0] x2 + [4] 438.23/118.05 [0 0] [0 1] [0] 438.23/118.05 438.23/118.05 [n__0] = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [n__plus](x1, x2) = [0 0] x1 + [0 0] x2 + [0] 438.23/118.05 [1 1] [1 1] [7] 438.23/118.05 438.23/118.05 [isNatKind](x1) = [0 1] x1 + [1] 438.23/118.05 [0 0] [2] 438.23/118.05 438.23/118.05 [n__isNatKind](x1) = [0 1] x1 + [1] 438.23/118.05 [0 0] [2] 438.23/118.05 438.23/118.05 [n__s](x1) = [0 0] x1 + [0] 438.23/118.05 [1 1] [2] 438.23/118.05 438.23/118.05 [0] = [0] 438.23/118.05 [0] 438.23/118.05 438.23/118.05 [n__and](x1, x2) = [0 1] x1 + [1 0] x2 + [4] 438.23/118.05 [0 0] [0 1] [0] 438.23/118.05 438.23/118.05 [U11^#](x1, x2, x3) = [1 2] x2 + [1 2] x3 + [4] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 438.23/118.05 [U12^#](x1, x2) = [1 2] x2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [isNat^#](x1) = [0 2] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [activate^#](x1) = [1 0] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [and^#](x1, x2) = [1 0] x2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [isNatKind^#](x1) = [0 1] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [U21^#](x1, x2) = [2 2] x2 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_5](x1) = [1 0] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_6](x1) = [1 0] x1 + [3] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_7](x1) = [1 0] x1 + [0] 438.23/118.05 [0 0] [0] 438.23/118.05 438.23/118.05 [c_8](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 438.23/118.05 0] x4 + [1] 438.23/118.05 [0 0] [0 0] [0 0] [0 438.23/118.05 0] [0] 438.23/118.05 438.23/118.05 [c_9](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 438.23/118.05 [0 0] [0 0] [0] 438.23/118.05 438.23/118.05 The order satisfies the following ordering constraints: 438.23/118.05 438.23/118.05 [U11(tt(), V1, V2)] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [U12(isNat(activate(V1)), activate(V2))] 438.23/118.05 438.23/118.05 [U12(tt(), V2)] = [0] 438.23/118.05 [0] 438.23/118.05 >= [0] 438.23/118.05 [0] 438.23/118.05 = [U13(isNat(activate(V2)))] 438.23/118.05 438.23/118.06 [isNat(n__0())] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [tt()] 438.23/118.06 438.23/118.06 [isNat(n__plus(V1, V2))] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 activate(V1), 438.23/118.06 activate(V2))] 438.23/118.06 438.23/118.06 [isNat(n__s(V1))] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [U21(isNatKind(activate(V1)), activate(V1))] 438.23/118.06 438.23/118.06 [activate(X)] = [1 0] X + [0] 438.23/118.06 [0 1] [0] 438.23/118.06 >= [1 0] X + [0] 438.23/118.06 [0 1] [0] 438.23/118.06 = [X] 438.23/118.06 438.23/118.06 [activate(n__0())] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [0()] 438.23/118.06 438.23/118.06 [activate(n__plus(X1, X2))] = [0 0] X1 + [0 0] X2 + [0] 438.23/118.06 [1 1] [1 1] [7] 438.23/118.06 >= [0 0] X1 + [0 0] X2 + [0] 438.23/118.06 [1 1] [1 1] [7] 438.23/118.06 = [plus(X1, X2)] 438.23/118.06 438.23/118.06 [activate(n__isNatKind(X))] = [0 1] X + [1] 438.23/118.06 [0 0] [2] 438.23/118.06 >= [0 1] X + [1] 438.23/118.06 [0 0] [2] 438.23/118.06 = [isNatKind(X)] 438.23/118.06 438.23/118.06 [activate(n__s(X))] = [0 0] X + [0] 438.23/118.06 [1 1] [2] 438.23/118.06 >= [0 0] X + [0] 438.23/118.06 [1 1] [2] 438.23/118.06 = [s(X)] 438.23/118.06 438.23/118.06 [activate(n__and(X1, X2))] = [0 1] X1 + [1 0] X2 + [4] 438.23/118.06 [0 0] [0 1] [0] 438.23/118.06 >= [0 1] X1 + [1 0] X2 + [4] 438.23/118.06 [0 0] [0 1] [0] 438.23/118.06 = [and(X1, X2)] 438.23/118.06 438.23/118.06 [U13(tt())] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [tt()] 438.23/118.06 438.23/118.06 [U21(tt(), V1)] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [U22(isNat(activate(V1)))] 438.23/118.06 438.23/118.06 [U22(tt())] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [tt()] 438.23/118.06 438.23/118.06 [s(X)] = [0 0] X + [0] 438.23/118.06 [1 1] [2] 438.23/118.06 >= [0 0] X + [0] 438.23/118.06 [1 1] [2] 438.23/118.06 = [n__s(X)] 438.23/118.06 438.23/118.06 [plus(X1, X2)] = [0 0] X1 + [0 0] X2 + [0] 438.23/118.06 [1 1] [1 1] [7] 438.23/118.06 >= [0 0] X1 + [0 0] X2 + [0] 438.23/118.06 [1 1] [1 1] [7] 438.23/118.06 = [n__plus(X1, X2)] 438.23/118.06 438.23/118.06 [and(X1, X2)] = [0 1] X1 + [1 0] X2 + [4] 438.23/118.06 [0 0] [0 1] [0] 438.23/118.06 >= [0 1] X1 + [1 0] X2 + [4] 438.23/118.06 [0 0] [0 1] [0] 438.23/118.06 = [n__and(X1, X2)] 438.23/118.06 438.23/118.06 [and(tt(), X)] = [1 0] X + [4] 438.23/118.06 [0 1] [0] 438.23/118.06 > [1 0] X + [0] 438.23/118.06 [0 1] [0] 438.23/118.06 = [activate(X)] 438.23/118.06 438.23/118.06 [isNatKind(X)] = [0 1] X + [1] 438.23/118.06 [0 0] [2] 438.23/118.06 >= [0 1] X + [1] 438.23/118.06 [0 0] [2] 438.23/118.06 = [n__isNatKind(X)] 438.23/118.06 438.23/118.06 [isNatKind(n__0())] = [1] 438.23/118.06 [2] 438.23/118.06 > [0] 438.23/118.06 [0] 438.23/118.06 = [tt()] 438.23/118.06 438.23/118.06 [isNatKind(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [8] 438.23/118.06 [0 0] [0 0] [2] 438.23/118.06 > [0 1] V2 + [7] 438.23/118.06 [0 0] [2] 438.23/118.06 = [and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))] 438.23/118.06 438.23/118.06 [isNatKind(n__s(V1))] = [1 1] V1 + [3] 438.23/118.06 [0 0] [2] 438.23/118.06 > [0 1] V1 + [1] 438.23/118.06 [0 0] [2] 438.23/118.06 = [isNatKind(activate(V1))] 438.23/118.06 438.23/118.06 [0()] = [0] 438.23/118.06 [0] 438.23/118.06 >= [0] 438.23/118.06 [0] 438.23/118.06 = [n__0()] 438.23/118.06 438.23/118.06 [U11^#(tt(), V1, V2)] = [1 2] V1 + [1 2] V2 + [4] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 2] V2 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [U12^#(isNat(activate(V1)), activate(V2))] 438.23/118.06 438.23/118.06 [U11^#(tt(), V1, V2)] = [1 2] V1 + [1 2] V2 + [4] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [0 2] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [isNat^#(activate(V1))] 438.23/118.06 438.23/118.06 [U11^#(tt(), V1, V2)] = [1 2] V1 + [1 2] V2 + [4] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 0] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [activate^#(V1)] 438.23/118.06 438.23/118.06 [U11^#(tt(), V1, V2)] = [1 2] V1 + [1 2] V2 + [4] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 0] V2 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [activate^#(V2)] 438.23/118.06 438.23/118.06 [U12^#(tt(), V2)] = [1 2] V2 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 >= [0 2] V2 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [isNat^#(activate(V2))] 438.23/118.06 438.23/118.06 [U12^#(tt(), V2)] = [1 2] V2 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 >= [1 0] V2 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [activate^#(V2)] 438.23/118.06 438.23/118.06 [isNat^#(n__plus(V1, V2))] = [2 2] V1 + [2 2] V2 + [14] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 2] V1 + [1 2] V2 + [4] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 = [U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 activate(V1), 438.23/118.06 activate(V2))] 438.23/118.06 438.23/118.06 [isNat^#(n__plus(V1, V2))] = [2 2] V1 + [2 2] V2 + [14] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 0] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [activate^#(V1)] 438.23/118.06 438.23/118.06 [isNat^#(n__plus(V1, V2))] = [2 2] V1 + [2 2] V2 + [14] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 0] V2 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [activate^#(V2)] 438.23/118.06 438.23/118.06 [isNat^#(n__plus(V1, V2))] = [2 2] V1 + [2 2] V2 + [14] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [0 1] V2 + [1] 438.23/118.06 [0 0] [0] 438.23/118.06 = [and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))] 438.23/118.06 438.23/118.06 [isNat^#(n__plus(V1, V2))] = [2 2] V1 + [2 2] V2 + [14] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [0 1] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [isNatKind^#(activate(V1))] 438.23/118.06 438.23/118.06 [isNat^#(n__s(V1))] = [2 2] V1 + [4] 438.23/118.06 [0 0] [0] 438.23/118.06 > [1 0] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [activate^#(V1)] 438.23/118.06 438.23/118.06 [isNat^#(n__s(V1))] = [2 2] V1 + [4] 438.23/118.06 [0 0] [0] 438.23/118.06 > [0 1] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [isNatKind^#(activate(V1))] 438.23/118.06 438.23/118.06 [isNat^#(n__s(V1))] = [2 2] V1 + [4] 438.23/118.06 [0 0] [0] 438.23/118.06 > [2 2] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [U21^#(isNatKind(activate(V1)), activate(V1))] 438.23/118.06 438.23/118.06 [activate^#(n__isNatKind(X))] = [0 1] X + [1] 438.23/118.06 [0 0] [0] 438.23/118.06 > [0 1] X + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [c_5(isNatKind^#(X))] 438.23/118.06 438.23/118.06 [activate^#(n__and(X1, X2))] = [0 1] X1 + [1 0] X2 + [4] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 0] X2 + [3] 438.23/118.06 [0 0] [0] 438.23/118.06 = [c_6(and^#(X1, X2))] 438.23/118.06 438.23/118.06 [and^#(tt(), X)] = [1 0] X + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 >= [1 0] X + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [c_7(activate^#(X))] 438.23/118.06 438.23/118.06 [isNatKind^#(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [7] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 > [1 1] V1 + [1 1] V2 + [2] 438.23/118.06 [0 0] [0 0] [0] 438.23/118.06 = [c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 isNatKind^#(activate(V1)), 438.23/118.06 activate^#(V1), 438.23/118.06 activate^#(V2))] 438.23/118.06 438.23/118.06 [isNatKind^#(n__s(V1))] = [1 1] V1 + [2] 438.23/118.06 [0 0] [0] 438.23/118.06 >= [1 1] V1 + [2] 438.23/118.06 [0 0] [0] 438.23/118.06 = [c_9(isNatKind^#(activate(V1)), activate^#(V1))] 438.23/118.06 438.23/118.06 [U21^#(tt(), V1)] = [2 2] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 >= [0 2] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [isNat^#(activate(V1))] 438.23/118.06 438.23/118.06 [U21^#(tt(), V1)] = [2 2] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 >= [1 0] V1 + [0] 438.23/118.06 [0 0] [0] 438.23/118.06 = [activate^#(V1)] 438.23/118.06 438.23/118.06 438.23/118.06 We return to the main proof. Consider the set of all dependency 438.23/118.06 pairs 438.23/118.06 438.23/118.06 : 438.23/118.06 { 1: activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.06 , 2: U11^#(tt(), V1, V2) -> 438.23/118.06 U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.06 , 3: U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.06 , 4: U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.06 , 5: U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.06 , 6: U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.06 , 7: U12^#(tt(), V2) -> activate^#(V2) 438.23/118.06 , 8: isNat^#(n__plus(V1, V2)) -> 438.23/118.06 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 activate(V1), 438.23/118.06 activate(V2)) 438.23/118.06 , 9: isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.06 , 10: isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.06 , 11: isNat^#(n__plus(V1, V2)) -> 438.23/118.06 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.06 , 12: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.06 , 13: isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.06 , 14: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.06 , 15: isNat^#(n__s(V1)) -> 438.23/118.06 U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.06 , 16: activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.06 , 17: and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.06 , 18: isNatKind^#(n__plus(V1, V2)) -> 438.23/118.06 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 isNatKind^#(activate(V1)), 438.23/118.06 activate^#(V1), 438.23/118.06 activate^#(V2)) 438.23/118.06 , 19: isNatKind^#(n__s(V1)) -> 438.23/118.06 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.06 , 20: U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.06 , 21: U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.06 438.23/118.06 Processor 'matrix interpretation of dimension 2' induces the 438.23/118.06 complexity certificate YES(?,O(n^1)) on application of dependency 438.23/118.06 pairs {1,2,3,4,5,8,9,10,11,12,13,14,15,16,18}. These cover all 438.23/118.06 (indirect) predecessors of dependency pairs 438.23/118.06 {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,20,21}, their number 438.23/118.06 of application is equally bounded. The dependency pairs are shifted 438.23/118.06 into the weak component. 438.23/118.06 438.23/118.06 We are left with following problem, upon which TcT provides the 438.23/118.06 certificate YES(O(1),O(1)). 438.23/118.06 438.23/118.06 Weak DPs: 438.23/118.06 { U11^#(tt(), V1, V2) -> U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.06 , U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.06 , U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.06 , U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.06 , U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.06 , U12^#(tt(), V2) -> activate^#(V2) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> 438.23/118.06 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 activate(V1), 438.23/118.06 activate(V2)) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> 438.23/118.06 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.06 , isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.06 , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.06 , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.06 , activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.06 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.06 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.06 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.06 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 isNatKind^#(activate(V1)), 438.23/118.06 activate^#(V1), 438.23/118.06 activate^#(V2)) 438.23/118.06 , isNatKind^#(n__s(V1)) -> 438.23/118.06 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.06 , U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.06 , U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.06 Weak Trs: 438.23/118.06 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.06 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.06 , isNat(n__0()) -> tt() 438.23/118.06 , isNat(n__plus(V1, V2)) -> 438.23/118.06 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 activate(V1), 438.23/118.06 activate(V2)) 438.23/118.06 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.06 , activate(X) -> X 438.23/118.06 , activate(n__0()) -> 0() 438.23/118.06 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.06 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.06 , activate(n__s(X)) -> s(X) 438.23/118.06 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.06 , U13(tt()) -> tt() 438.23/118.06 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.06 , U22(tt()) -> tt() 438.23/118.06 , s(X) -> n__s(X) 438.23/118.06 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.06 , and(X1, X2) -> n__and(X1, X2) 438.23/118.06 , and(tt(), X) -> activate(X) 438.23/118.06 , isNatKind(X) -> n__isNatKind(X) 438.23/118.06 , isNatKind(n__0()) -> tt() 438.23/118.06 , isNatKind(n__plus(V1, V2)) -> 438.23/118.06 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.06 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.06 , 0() -> n__0() } 438.23/118.06 Obligation: 438.23/118.06 innermost runtime complexity 438.23/118.06 Answer: 438.23/118.06 YES(O(1),O(1)) 438.23/118.06 438.23/118.06 The following weak DPs constitute a sub-graph of the DG that is 438.23/118.06 closed under successors. The DPs are removed. 438.23/118.06 438.23/118.06 { U11^#(tt(), V1, V2) -> U12^#(isNat(activate(V1)), activate(V2)) 438.23/118.06 , U11^#(tt(), V1, V2) -> isNat^#(activate(V1)) 438.23/118.06 , U11^#(tt(), V1, V2) -> activate^#(V1) 438.23/118.06 , U11^#(tt(), V1, V2) -> activate^#(V2) 438.23/118.06 , U12^#(tt(), V2) -> isNat^#(activate(V2)) 438.23/118.06 , U12^#(tt(), V2) -> activate^#(V2) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> 438.23/118.06 U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 activate(V1), 438.23/118.06 activate(V2)) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> activate^#(V1) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> activate^#(V2) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> 438.23/118.06 and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.06 , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) 438.23/118.06 , isNat^#(n__s(V1)) -> activate^#(V1) 438.23/118.06 , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) 438.23/118.06 , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) 438.23/118.06 , activate^#(n__isNatKind(X)) -> c_5(isNatKind^#(X)) 438.23/118.06 , activate^#(n__and(X1, X2)) -> c_6(and^#(X1, X2)) 438.23/118.06 , and^#(tt(), X) -> c_7(activate^#(X)) 438.23/118.06 , isNatKind^#(n__plus(V1, V2)) -> 438.23/118.06 c_8(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 isNatKind^#(activate(V1)), 438.23/118.06 activate^#(V1), 438.23/118.06 activate^#(V2)) 438.23/118.06 , isNatKind^#(n__s(V1)) -> 438.23/118.06 c_9(isNatKind^#(activate(V1)), activate^#(V1)) 438.23/118.06 , U21^#(tt(), V1) -> isNat^#(activate(V1)) 438.23/118.06 , U21^#(tt(), V1) -> activate^#(V1) } 438.23/118.06 438.23/118.06 We are left with following problem, upon which TcT provides the 438.23/118.06 certificate YES(O(1),O(1)). 438.23/118.06 438.23/118.06 Weak Trs: 438.23/118.06 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 438.23/118.06 , U12(tt(), V2) -> U13(isNat(activate(V2))) 438.23/118.06 , isNat(n__0()) -> tt() 438.23/118.06 , isNat(n__plus(V1, V2)) -> 438.23/118.06 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 438.23/118.06 activate(V1), 438.23/118.06 activate(V2)) 438.23/118.06 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 438.23/118.06 , activate(X) -> X 438.23/118.06 , activate(n__0()) -> 0() 438.23/118.06 , activate(n__plus(X1, X2)) -> plus(X1, X2) 438.23/118.06 , activate(n__isNatKind(X)) -> isNatKind(X) 438.23/118.06 , activate(n__s(X)) -> s(X) 438.23/118.06 , activate(n__and(X1, X2)) -> and(X1, X2) 438.23/118.06 , U13(tt()) -> tt() 438.23/118.06 , U21(tt(), V1) -> U22(isNat(activate(V1))) 438.23/118.06 , U22(tt()) -> tt() 438.23/118.06 , s(X) -> n__s(X) 438.23/118.06 , plus(X1, X2) -> n__plus(X1, X2) 438.23/118.06 , and(X1, X2) -> n__and(X1, X2) 438.23/118.06 , and(tt(), X) -> activate(X) 438.23/118.06 , isNatKind(X) -> n__isNatKind(X) 438.23/118.06 , isNatKind(n__0()) -> tt() 438.23/118.06 , isNatKind(n__plus(V1, V2)) -> 438.23/118.06 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 438.23/118.06 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 438.23/118.06 , 0() -> n__0() } 438.23/118.06 Obligation: 438.23/118.06 innermost runtime complexity 438.23/118.06 Answer: 438.23/118.06 YES(O(1),O(1)) 438.23/118.06 438.23/118.06 No rule is usable, rules are removed from the input problem. 438.23/118.06 438.23/118.06 We are left with following problem, upon which TcT provides the 438.23/118.06 certificate YES(O(1),O(1)). 438.23/118.06 438.23/118.06 Rules: Empty 438.23/118.06 Obligation: 438.23/118.06 innermost runtime complexity 438.23/118.06 Answer: 438.23/118.06 YES(O(1),O(1)) 438.23/118.06 438.23/118.06 Empty rules are trivially bounded 438.23/118.06 438.23/118.06 Hurray, we answered YES(O(1),O(n^2)) 438.41/118.11 EOF