We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, plus(N, s(M)) -> U51(isNat(M), M, N)
, plus(N, 0()) -> U41(isNat(N), N)
, U61(tt()) -> 0()
, 0() -> n__0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, x(X1, X2) -> n__x(X1, X2)
, x(N, s(M)) -> U71(isNat(M), M, N)
, x(N, 0()) -> U61(isNat(N)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
Arguments of following rules are not normal-forms:
{ plus(N, s(M)) -> U51(isNat(M), M, N)
, plus(N, 0()) -> U41(isNat(N), N)
, x(N, s(M)) -> U71(isNat(M), M, N)
, x(N, 0()) -> U61(isNat(N)) }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, U61(tt()) -> 0()
, 0() -> n__0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
We add the following dependency tuples:
Strict DPs:
{ U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, U12^#(tt()) -> c_2()
, isNat^#(n__0()) -> c_3()
, isNat^#(n__plus(V1, V2)) ->
c_4(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_6(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(X) -> c_7()
, activate^#(n__0()) -> c_8(0^#())
, activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, U21^#(tt()) -> c_12()
, U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, 0^#() -> c_21()
, plus^#(X1, X2) -> c_19()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_24()
, U32^#(tt()) -> c_14()
, U41^#(tt(), N) -> c_15(activate^#(N))
, U51^#(tt(), M, N) ->
c_16(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, U61^#(tt()) -> c_20(0^#())
, U71^#(tt(), M, N) ->
c_22(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, U12^#(tt()) -> c_2()
, isNat^#(n__0()) -> c_3()
, isNat^#(n__plus(V1, V2)) ->
c_4(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_6(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(X) -> c_7()
, activate^#(n__0()) -> c_8(0^#())
, activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, U21^#(tt()) -> c_12()
, U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, 0^#() -> c_21()
, plus^#(X1, X2) -> c_19()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_24()
, U32^#(tt()) -> c_14()
, U41^#(tt(), N) -> c_15(activate^#(N))
, U51^#(tt(), M, N) ->
c_16(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, U61^#(tt()) -> c_20(0^#())
, U71^#(tt(), M, N) ->
c_22(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, U61(tt()) -> 0()
, 0() -> n__0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
We estimate the number of application of {2,3,7,12,14,15,16,17,18}
by applications of Pre({2,3,7,12,14,15,16,17,18}) =
{1,4,5,6,8,9,10,11,13,19,20,21,22,23,24}. Here rules are labeled as
follows:
DPs:
{ 1: U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, 2: U12^#(tt()) -> c_2()
, 3: isNat^#(n__0()) -> c_3()
, 4: isNat^#(n__plus(V1, V2)) ->
c_4(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 5: isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, 6: isNat^#(n__x(V1, V2)) ->
c_6(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 7: activate^#(X) -> c_7()
, 8: activate^#(n__0()) -> c_8(0^#())
, 9: activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 10: activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, 11: activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 12: U21^#(tt()) -> c_12()
, 13: U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, 14: 0^#() -> c_21()
, 15: plus^#(X1, X2) -> c_19()
, 16: s^#(X) -> c_18()
, 17: x^#(X1, X2) -> c_24()
, 18: U32^#(tt()) -> c_14()
, 19: U41^#(tt(), N) -> c_15(activate^#(N))
, 20: U51^#(tt(), M, N) ->
c_16(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 21: U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, 22: U61^#(tt()) -> c_20(0^#())
, 23: U71^#(tt(), M, N) ->
c_22(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 24: U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_4(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_6(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__0()) -> c_8(0^#())
, activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, U41^#(tt(), N) -> c_15(activate^#(N))
, U51^#(tt(), M, N) ->
c_16(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, U61^#(tt()) -> c_20(0^#())
, U71^#(tt(), M, N) ->
c_22(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ U12^#(tt()) -> c_2()
, isNat^#(n__0()) -> c_3()
, activate^#(X) -> c_7()
, U21^#(tt()) -> c_12()
, 0^#() -> c_21()
, plus^#(X1, X2) -> c_19()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_24()
, U32^#(tt()) -> c_14() }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, U61(tt()) -> 0()
, 0() -> n__0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
We estimate the number of application of {5,13} by applications of
Pre({5,13}) = {1,2,3,4,6,7,8,9,10,11,12,14,15}. Here rules are
labeled as follows:
DPs:
{ 1: U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, 2: isNat^#(n__plus(V1, V2)) ->
c_4(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 3: isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, 4: isNat^#(n__x(V1, V2)) ->
c_6(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 5: activate^#(n__0()) -> c_8(0^#())
, 6: activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 7: activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, 8: activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, 9: U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, 10: U41^#(tt(), N) -> c_15(activate^#(N))
, 11: U51^#(tt(), M, N) ->
c_16(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 12: U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, 13: U61^#(tt()) -> c_20(0^#())
, 14: U71^#(tt(), M, N) ->
c_22(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 15: U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N))
, 16: U12^#(tt()) -> c_2()
, 17: isNat^#(n__0()) -> c_3()
, 18: activate^#(X) -> c_7()
, 19: U21^#(tt()) -> c_12()
, 20: 0^#() -> c_21()
, 21: plus^#(X1, X2) -> c_19()
, 22: s^#(X) -> c_18()
, 23: x^#(X1, X2) -> c_24()
, 24: U32^#(tt()) -> c_14() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_4(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_6(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, U41^#(tt(), N) -> c_15(activate^#(N))
, U51^#(tt(), M, N) ->
c_16(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, U71^#(tt(), M, N) ->
c_22(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ U12^#(tt()) -> c_2()
, isNat^#(n__0()) -> c_3()
, activate^#(X) -> c_7()
, activate^#(n__0()) -> c_8(0^#())
, U21^#(tt()) -> c_12()
, 0^#() -> c_21()
, plus^#(X1, X2) -> c_19()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_24()
, U32^#(tt()) -> c_14()
, U61^#(tt()) -> c_20(0^#()) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, U61(tt()) -> 0()
, 0() -> n__0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ U12^#(tt()) -> c_2()
, isNat^#(n__0()) -> c_3()
, activate^#(X) -> c_7()
, activate^#(n__0()) -> c_8(0^#())
, U21^#(tt()) -> c_12()
, 0^#() -> c_21()
, plus^#(X1, X2) -> c_19()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_24()
, U32^#(tt()) -> c_14()
, U61^#(tt()) -> c_20(0^#()) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_4(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_6(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, U41^#(tt(), N) -> c_15(activate^#(N))
, U51^#(tt(), M, N) ->
c_16(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, U71^#(tt(), M, N) ->
c_22(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, U61(tt()) -> 0()
, 0() -> n__0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U11^#(tt(), V2) ->
c_1(U12^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, isNat^#(n__s(V1)) ->
c_5(U21^#(isNat(activate(V1))),
isNat^#(activate(V1)),
activate^#(V1))
, activate^#(n__plus(X1, X2)) ->
c_9(plus^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, activate^#(n__s(X)) -> c_10(s^#(activate(X)), activate^#(X))
, activate^#(n__x(X1, X2)) ->
c_11(x^#(activate(X1), activate(X2)),
activate^#(X1),
activate^#(X2))
, U31^#(tt(), V2) ->
c_13(U32^#(isNat(activate(V2))),
isNat^#(activate(V2)),
activate^#(V2))
, U52^#(tt(), M, N) ->
c_17(s^#(plus(activate(N), activate(M))),
plus^#(activate(N), activate(M)),
activate^#(N),
activate^#(M))
, U72^#(tt(), M, N) ->
c_23(plus^#(x(activate(N), activate(M)), activate(N)),
x^#(activate(N), activate(M)),
activate^#(N),
activate^#(M),
activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U41^#(tt(), N) -> c_9(activate^#(N))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, U61(tt()) -> 0()
, 0() -> n__0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U41^#(tt(), N) -> c_9(activate^#(N))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
Consider the dependency graph
1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
-->_2 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_2 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_2 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :4
-->_1 isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1)) :3
-->_1 isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :2
2: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
-->_4 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_3 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_4 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_3 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_4 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_3 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_2 isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :4
-->_2 isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1)) :3
-->_2 isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :2
-->_1 U11^#(tt(), V2) ->
c_1(isNat^#(activate(V2)), activate^#(V2)) :1
3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
-->_2 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_2 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_2 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :4
-->_1 isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1)) :3
-->_1 isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :2
4: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
-->_1 U31^#(tt(), V2) ->
c_8(isNat^#(activate(V2)), activate^#(V2)) :8
-->_4 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_3 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_4 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_3 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_4 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_3 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_2 isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :4
-->_2 isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1)) :3
-->_2 isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :2
5: activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
-->_2 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_1 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_2 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_1 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_2 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_1 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
6: activate^#(n__s(X)) -> c_6(activate^#(X))
-->_1 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_1 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_1 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
7: activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
-->_2 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_1 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_2 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_1 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_2 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_1 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
8: U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
-->_2 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_2 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_2 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :4
-->_1 isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1)) :3
-->_1 isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :2
9: U41^#(tt(), N) -> c_9(activate^#(N))
-->_1 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_1 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_1 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
10: U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
-->_1 U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) :11
-->_5 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_4 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_3 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_5 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_4 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_3 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_5 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_4 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_3 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_2 isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :4
-->_2 isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1)) :3
-->_2 isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :2
11: U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
-->_2 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_1 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_2 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_1 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_2 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_1 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
12: U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
-->_1 U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) :13
-->_5 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_4 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_3 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_5 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_4 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_3 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_5 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_4 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_3 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_2 isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :4
-->_2 isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1)) :3
-->_2 isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2)) :2
13: U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N))
-->_3 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_2 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_1 activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2)) :7
-->_3 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_2 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_1 activate^#(n__s(X)) -> c_6(activate^#(X)) :6
-->_3 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_2 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
-->_1 activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) :5
Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).
{ U41^#(tt(), N) -> c_9(activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:
Problem (R):
------------
Strict DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
Problem (S):
------------
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
Overall, the transformation results in the following sub-problem(s):
Generated new problems:
-----------------------
R) Strict DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(n^5)).
S) Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(n^1)).
Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:
Problem (R):
------------
Strict DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
Problem (S):
------------
Strict DPs:
{ U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
Overall, the transformation results in the following sub-problem(s):
Generated new problems:
-----------------------
R) Strict DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(n^5)).
S) Strict DPs:
{ U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(1)).
Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^5)).
Strict DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^5))
We decompose the input problem according to the dependency graph
into the upper component
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
and lower component
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2)) }
Further, following extension rules are added to the lower
component.
{ U11^#(tt(), V2) -> isNat^#(activate(V2))
, U11^#(tt(), V2) -> activate^#(V2)
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__plus(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__plus(V1, V2)) -> activate^#(V1)
, isNat^#(n__plus(V1, V2)) -> activate^#(V2)
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__s(V1)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> activate^#(V2)
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, U31^#(tt(), V2) -> isNat^#(activate(V2))
, U31^#(tt(), V2) -> activate^#(V2)
, U51^#(tt(), M, N) -> isNat^#(activate(N))
, U51^#(tt(), M, N) -> activate^#(M)
, U51^#(tt(), M, N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> activate^#(M)
, U52^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) -> isNat^#(activate(N))
, U71^#(tt(), M, N) -> activate^#(M)
, U71^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) -> activate^#(M)
, U72^#(tt(), M, N) -> activate^#(N) }
TcT solves the upper component with certificate YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {7,9} by applications of
Pre({7,9}) = {6,8}. Here rules are labeled as follows:
DPs:
{ 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, 2: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 3: isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1))
, 4: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 5: U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, 6: U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 7: U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, 8: U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 9: U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Trs:
{ U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[U11](x1, x2) = [1] x1 + [0]
[tt] = [7]
[U12](x1) = [7]
[isNat](x1) = [1] x1 + [1]
[activate](x1) = [1] x1 + [0]
[U21](x1) = [1] x1 + [1]
[U31](x1, x2) = [1] x1 + [1] x2 + [0]
[U32](x1) = [1] x1 + [4]
[s](x1) = [1] x1 + [1]
[plus](x1, x2) = [1] x1 + [1] x2 + [0]
[0] = [6]
[x](x1, x2) = [1] x1 + [1] x2 + [0]
[n__0] = [6]
[n__plus](x1, x2) = [1] x1 + [1] x2 + [0]
[n__s](x1) = [1] x1 + [1]
[n__x](x1, x2) = [1] x1 + [1] x2 + [0]
[U11^#](x1, x2) = [4] x2 + [0]
[isNat^#](x1) = [4] x1 + [0]
[activate^#](x1) = [0]
[U31^#](x1, x2) = [4] x2 + [0]
[U51^#](x1, x2, x3) = [2] x2 + [7] x3 + [5]
[U52^#](x1, x2, x3) = [0]
[U71^#](x1, x2, x3) = [2] x2 + [7] x3 + [5]
[U72^#](x1, x2, x3) = [0]
[c_1](x1, x2) = [0]
[c_2](x1, x2, x3, x4) = [0]
[c_3](x1, x2) = [0]
[c_4](x1, x2, x3, x4) = [0]
[c_8](x1, x2) = [0]
[c_10](x1, x2, x3, x4, x5) = [0]
[c_11](x1, x2) = [0]
[c_12](x1, x2, x3, x4, x5) = [0]
[c_13](x1, x2, x3) = [0]
[c] = [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1, x2) = [1] x1 + [1] x2 + [0]
[c_3](x1) = [1] x1 + [1]
[c_4](x1, x2) = [1] x1 + [1] x2 + [0]
[c_5](x1) = [1] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [7]
>= [7]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [7]
>= [7]
= [tt()]
[isNat(n__0())] = [7]
>= [7]
= [tt()]
[isNat(n__plus(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V1 + [1]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [1] V1 + [2]
>= [1] V1 + [2]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__0())] = [6]
>= [6]
= [0()]
[activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1] X + [1]
>= [1] X + [1]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [8]
> [7]
= [tt()]
[U31(tt(), V2)] = [1] V2 + [7]
> [1] V2 + [5]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [11]
> [7]
= [tt()]
[s(X)] = [1] X + [1]
>= [1] X + [1]
= [n__s(X)]
[plus(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n__plus(X1, X2)]
[0()] = [6]
>= [6]
= [n__0()]
[x(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [4] V2 + [0]
>= [4] V2 + [0]
= [c_1(isNat^#(activate(V2)))]
[isNat^#(n__plus(V1, V2))] = [4] V2 + [4] V1 + [0]
>= [4] V2 + [4] V1 + [0]
= [c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[isNat^#(n__s(V1))] = [4] V1 + [4]
> [4] V1 + [1]
= [c_3(isNat^#(activate(V1)))]
[isNat^#(n__x(V1, V2))] = [4] V2 + [4] V1 + [0]
>= [4] V2 + [4] V1 + [0]
= [c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[U31^#(tt(), V2)] = [4] V2 + [0]
>= [4] V2 + [0]
= [c_5(isNat^#(activate(V2)))]
[U51^#(tt(), M, N)] = [7] N + [2] M + [5]
> [4] N + [0]
= [c_6(isNat^#(activate(N)))]
[U71^#(tt(), M, N)] = [7] N + [2] M + [5]
> [4] N + [0]
= [c_7(isNat^#(activate(N)))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) }
Weak DPs:
{ isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 4: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[U11](x1, x2) = [0]
[tt] = [0]
[U12](x1) = [0]
[isNat](x1) = [0]
[activate](x1) = [1] x1 + [0]
[U21](x1) = [0]
[U31](x1, x2) = [0]
[U32](x1) = [0]
[s](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [1] x2 + [0]
[0] = [7]
[x](x1, x2) = [1] x1 + [1] x2 + [4]
[n__0] = [7]
[n__plus](x1, x2) = [1] x1 + [1] x2 + [0]
[n__s](x1) = [1] x1 + [0]
[n__x](x1, x2) = [1] x1 + [1] x2 + [4]
[U11^#](x1, x2) = [1] x2 + [0]
[isNat^#](x1) = [1] x1 + [0]
[activate^#](x1) = [0]
[U31^#](x1, x2) = [1] x2 + [4]
[U51^#](x1, x2, x3) = [2] x2 + [7] x3 + [4]
[U52^#](x1, x2, x3) = [0]
[U71^#](x1, x2, x3) = [2] x2 + [7] x3 + [5]
[U72^#](x1, x2, x3) = [0]
[c_1](x1, x2) = [0]
[c_2](x1, x2, x3, x4) = [0]
[c_3](x1, x2) = [0]
[c_4](x1, x2, x3, x4) = [0]
[c_8](x1, x2) = [0]
[c_10](x1, x2, x3, x4, x5) = [0]
[c_11](x1, x2) = [0]
[c_12](x1, x2, x3, x4, x5) = [0]
[c_13](x1, x2, x3) = [0]
[c] = [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1, x2) = [1] x1 + [1] x2 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1, x2) = [1] x1 + [1] x2 + [0]
[c_5](x1) = [1] x1 + [1]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [4] x1 + [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [0]
>= [0]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [0]
>= [0]
= [tt()]
[isNat(n__0())] = [0]
>= [0]
= [tt()]
[isNat(n__plus(V1, V2))] = [0]
>= [0]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [0]
>= [0]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [0]
>= [0]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__0())] = [7]
>= [7]
= [0()]
[activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1] X + [0]
>= [1] X + [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [0]
>= [0]
= [tt()]
[U31(tt(), V2)] = [0]
>= [0]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [0]
>= [0]
= [tt()]
[s(X)] = [1] X + [0]
>= [1] X + [0]
= [n__s(X)]
[plus(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n__plus(X1, X2)]
[0()] = [7]
>= [7]
= [n__0()]
[x(X1, X2)] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [c_1(isNat^#(activate(V2)))]
[isNat^#(n__plus(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[isNat^#(n__s(V1))] = [1] V1 + [0]
>= [1] V1 + [0]
= [c_3(isNat^#(activate(V1)))]
[isNat^#(n__x(V1, V2))] = [1] V2 + [1] V1 + [4]
>= [1] V2 + [1] V1 + [4]
= [c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[U31^#(tt(), V2)] = [1] V2 + [4]
> [1] V2 + [1]
= [c_5(isNat^#(activate(V2)))]
[U51^#(tt(), M, N)] = [7] N + [2] M + [4]
> [1] N + [0]
= [c_6(isNat^#(activate(N)))]
[U71^#(tt(), M, N)] = [7] N + [2] M + [5]
> [4] N + [0]
= [c_7(isNat^#(activate(N)))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1))) }
Weak DPs:
{ isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, 3: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 5: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Trs:
{ U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, U21(tt()) -> tt()
, U32(tt()) -> tt() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[U11](x1, x2) = [4]
[tt] = [2]
[U12](x1) = [4]
[isNat](x1) = [5]
[activate](x1) = [1] x1 + [0]
[U21](x1) = [4]
[U31](x1, x2) = [4]
[U32](x1) = [4]
[s](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [1] x2 + [2]
[0] = [4]
[x](x1, x2) = [1] x1 + [1] x2 + [2]
[n__0] = [4]
[n__plus](x1, x2) = [1] x1 + [1] x2 + [2]
[n__s](x1) = [1] x1 + [0]
[n__x](x1, x2) = [1] x1 + [1] x2 + [2]
[U11^#](x1, x2) = [2] x1 + [6] x2 + [2]
[isNat^#](x1) = [6] x1 + [3]
[activate^#](x1) = [0]
[U31^#](x1, x2) = [1] x1 + [6] x2 + [2]
[U51^#](x1, x2, x3) = [1] x2 + [7] x3 + [7]
[U52^#](x1, x2, x3) = [0]
[U71^#](x1, x2, x3) = [4] x2 + [7] x3 + [4]
[U72^#](x1, x2, x3) = [0]
[c_1](x1, x2) = [0]
[c_2](x1, x2, x3, x4) = [0]
[c_3](x1, x2) = [0]
[c_4](x1, x2, x3, x4) = [0]
[c_8](x1, x2) = [0]
[c_10](x1, x2, x3, x4, x5) = [0]
[c_11](x1, x2) = [0]
[c_12](x1, x2, x3, x4, x5) = [0]
[c_13](x1, x2, x3) = [0]
[c] = [0]
[c_1](x1) = [1] x1 + [1]
[c_2](x1, x2) = [1] x1 + [1] x2 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1, x2) = [1] x1 + [1] x2 + [0]
[c_5](x1) = [1] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [4]
>= [4]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [4]
> [2]
= [tt()]
[isNat(n__0())] = [5]
> [2]
= [tt()]
[isNat(n__plus(V1, V2))] = [5]
> [4]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [5]
> [4]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [5]
> [4]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__0())] = [4]
>= [4]
= [0()]
[activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [2]
>= [1] X1 + [1] X2 + [2]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1] X + [0]
>= [1] X + [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [2]
>= [1] X1 + [1] X2 + [2]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [4]
> [2]
= [tt()]
[U31(tt(), V2)] = [4]
>= [4]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [4]
> [2]
= [tt()]
[s(X)] = [1] X + [0]
>= [1] X + [0]
= [n__s(X)]
[plus(X1, X2)] = [1] X1 + [1] X2 + [2]
>= [1] X1 + [1] X2 + [2]
= [n__plus(X1, X2)]
[0()] = [4]
>= [4]
= [n__0()]
[x(X1, X2)] = [1] X1 + [1] X2 + [2]
>= [1] X1 + [1] X2 + [2]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [6] V2 + [6]
> [6] V2 + [4]
= [c_1(isNat^#(activate(V2)))]
[isNat^#(n__plus(V1, V2))] = [6] V2 + [6] V1 + [15]
>= [6] V2 + [6] V1 + [15]
= [c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[isNat^#(n__s(V1))] = [6] V1 + [3]
>= [6] V1 + [3]
= [c_3(isNat^#(activate(V1)))]
[isNat^#(n__x(V1, V2))] = [6] V2 + [6] V1 + [15]
> [6] V2 + [6] V1 + [10]
= [c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[U31^#(tt(), V2)] = [6] V2 + [4]
> [6] V2 + [3]
= [c_5(isNat^#(activate(V2)))]
[U51^#(tt(), M, N)] = [7] N + [1] M + [7]
> [6] N + [3]
= [c_6(isNat^#(activate(N)))]
[U71^#(tt(), M, N)] = [7] N + [4] M + [4]
> [6] N + [3]
= [c_7(isNat^#(activate(N)))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1))) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 5: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[U11](x1, x2) = [1]
[tt] = [1]
[U12](x1) = [1] x1 + [0]
[isNat](x1) = [1]
[activate](x1) = [1] x1 + [0]
[U21](x1) = [1] x1 + [0]
[U31](x1, x2) = [1] x1 + [0]
[U32](x1) = [1]
[s](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [1] x2 + [4]
[0] = [0]
[x](x1, x2) = [1] x1 + [1] x2 + [4]
[n__0] = [0]
[n__plus](x1, x2) = [1] x1 + [1] x2 + [4]
[n__s](x1) = [1] x1 + [0]
[n__x](x1, x2) = [1] x1 + [1] x2 + [4]
[U11^#](x1, x2) = [1] x1 + [1] x2 + [1]
[isNat^#](x1) = [1] x1 + [2]
[activate^#](x1) = [0]
[U31^#](x1, x2) = [1] x2 + [4]
[U51^#](x1, x2, x3) = [4] x2 + [7] x3 + [3]
[U52^#](x1, x2, x3) = [0]
[U71^#](x1, x2, x3) = [4] x2 + [7] x3 + [5]
[U72^#](x1, x2, x3) = [0]
[c_1](x1, x2) = [0]
[c_2](x1, x2, x3, x4) = [0]
[c_3](x1, x2) = [0]
[c_4](x1, x2, x3, x4) = [0]
[c_8](x1, x2) = [0]
[c_10](x1, x2, x3, x4, x5) = [0]
[c_11](x1, x2) = [0]
[c_12](x1, x2, x3, x4, x5) = [0]
[c_13](x1, x2, x3) = [0]
[c] = [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1, x2) = [1] x1 + [1] x2 + [1]
[c_3](x1) = [1] x1 + [0]
[c_4](x1, x2) = [1] x1 + [1] x2 + [0]
[c_5](x1) = [1] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [1]
>= [1]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [1]
>= [1]
= [tt()]
[isNat(n__0())] = [1]
>= [1]
= [tt()]
[isNat(n__plus(V1, V2))] = [1]
>= [1]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [1]
>= [1]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [1]
>= [1]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__0())] = [0]
>= [0]
= [0()]
[activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1] X + [0]
>= [1] X + [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [1]
>= [1]
= [tt()]
[U31(tt(), V2)] = [1]
>= [1]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [1]
>= [1]
= [tt()]
[s(X)] = [1] X + [0]
>= [1] X + [0]
= [n__s(X)]
[plus(X1, X2)] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [n__plus(X1, X2)]
[0()] = [0]
>= [0]
= [n__0()]
[x(X1, X2)] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [1] V2 + [2]
>= [1] V2 + [2]
= [c_1(isNat^#(activate(V2)))]
[isNat^#(n__plus(V1, V2))] = [1] V2 + [1] V1 + [6]
> [1] V2 + [1] V1 + [5]
= [c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[isNat^#(n__s(V1))] = [1] V1 + [2]
>= [1] V1 + [2]
= [c_3(isNat^#(activate(V1)))]
[isNat^#(n__x(V1, V2))] = [1] V2 + [1] V1 + [6]
>= [1] V2 + [1] V1 + [6]
= [c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[U31^#(tt(), V2)] = [1] V2 + [4]
> [1] V2 + [2]
= [c_5(isNat^#(activate(V2)))]
[U51^#(tt(), M, N)] = [7] N + [4] M + [3]
> [1] N + [2]
= [c_6(isNat^#(activate(N)))]
[U71^#(tt(), M, N)] = [7] N + [4] M + [5]
> [1] N + [2]
= [c_7(isNat^#(activate(N)))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 2: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, 4: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 5: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,5,6,7}. These cover all (indirect) predecessors of
dependency pairs {1,2,5,6,7}, their number of application is
equally bounded. The dependency pairs are shifted into the weak
component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2)) }
Weak DPs:
{ U11^#(tt(), V2) -> isNat^#(activate(V2))
, U11^#(tt(), V2) -> activate^#(V2)
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__plus(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__plus(V1, V2)) -> activate^#(V1)
, isNat^#(n__plus(V1, V2)) -> activate^#(V2)
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__s(V1)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> activate^#(V2)
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, U31^#(tt(), V2) -> isNat^#(activate(V2))
, U31^#(tt(), V2) -> activate^#(V2)
, U51^#(tt(), M, N) -> isNat^#(activate(N))
, U51^#(tt(), M, N) -> activate^#(M)
, U51^#(tt(), M, N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> activate^#(M)
, U52^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) -> isNat^#(activate(N))
, U71^#(tt(), M, N) -> activate^#(M)
, U71^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) -> activate^#(M)
, U72^#(tt(), M, N) -> activate^#(N) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^4)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1, 2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[1]
[U11](x1, x2) = [0]
[1]
[1]
[1]
[tt] = [0]
[1]
[1]
[0 0 0 0] [1]
[U12](x1) = [0 0 0 0] x1 + [0]
[0 0 0 0] [1]
[1 0 0 0] [0]
[0 0 0 0] [1]
[isNat](x1) = [0 0 0 0] x1 + [1]
[0 0 0 0] [1]
[0 1 0 0] [1]
[1 0 0 0] [0]
[activate](x1) = [0 1 0 0] x1 + [0]
[0 1 1 0] [0]
[0 0 0 1] [0]
[0 0 0 0] [1]
[U21](x1) = [0 0 0 0] x1 + [0]
[1 0 0 0] [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
[U31](x1, x2) = [0 0 0 0] x1 + [0]
[0 0 0 0] [1]
[1 1 0 0] [0]
[1]
[U32](x1) = [0]
[1]
[1]
[0 0 0 0] [0]
[s](x1) = [1 1 0 0] x1 + [0]
[1 0 0 0] [0]
[1 0 0 1] [0]
[0 1 0 0] [1 0 0 0] [0]
[plus](x1, x2) = [1 0 0 0] x1 + [0 1 0 0] x2 + [0]
[1 0 0 0] [0 1 1 0] [0]
[1 0 0 1] [0 1 0 1] [1]
[0]
[0] = [0]
[0]
[0]
[0 0 0 0] [1 1 0 0] [1]
[x](x1, x2) = [1 1 0 0] x1 + [0 0 0 0] x2 + [1]
[1 1 1 0] [0 0 0 0] [1]
[1 0 0 1] [0 1 0 1] [0]
[0]
[n__0] = [0]
[0]
[0]
[0 1 0 0] [1 0 0 0] [0]
[n__plus](x1, x2) = [1 0 0 0] x1 + [0 1 0 0] x2 + [0]
[0 0 0 0] [0 1 1 0] [0]
[1 0 0 1] [0 1 0 1] [1]
[0 0 0 0] [0]
[n__s](x1) = [1 1 0 0] x1 + [0]
[1 0 0 0] [0]
[1 0 0 1] [0]
[0 0 0 0] [1 1 0 0] [1]
[n__x](x1, x2) = [1 1 0 0] x1 + [0 0 0 0] x2 + [1]
[0 1 1 0] [0 0 0 0] [1]
[1 0 0 1] [0 1 0 1] [0]
[0 0 0 0] [1 1 0 1] [0]
[U11^#](x1, x2) = [1 0 0 0] x1 + [1 1 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
[1 0 0 1] [0]
[isNat^#](x1) = [1 1 0 0] x1 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
[0 0 0 1] [0]
[activate^#](x1) = [0 0 0 0] x1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
[0 0 0 0] [1 1 0 1] [0]
[U31^#](x1, x2) = [0 0 1 1] x1 + [1 1 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[U51^#](x1, x2, x3) = [0 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [0]
[0 0 0 0] [0 0 1 1] [0 0 1
1] [0]
[U52^#](x1, x2, x3) = [0 0 0 1] x1 + [0 0 0 0] x2 + [1 0 0
1] x3 + [0]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[U71^#](x1, x2, x3) = [1 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [0]
[0 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[0 0 0 0] [0 0 1 1] [0 0 1
1] [0]
[U72^#](x1, x2, x3) = [0 0 1 1] x1 + [0 0 0 0] x2 + [1 0 0
1] x3 + [0]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0]
[1 0 0 0] [1 0 0 0] [0]
[c_5](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [0]
[c_6](x1) = [0 0 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[1 0 0 0] [1 0 0 0] [0]
[c_7](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [tt()]
[isNat(n__0())] = [1]
[1]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [tt()]
[isNat(n__plus(V1, V2))] = [0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] V2 + [0 0 0 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 1 0 0] [1 0 0 0] [1]
>= [1]
[0]
[1]
[1]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [0 0 0 0] [1]
[0 0 0 0] V1 + [1]
[0 0 0 0] [1]
[1 1 0 0] [1]
>= [1]
[0]
[1]
[1]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [0 0 0 0] [1]
[0 0 0 0] V1 + [1]
[0 0 0 0] [1]
[1 1 0 0] [2]
>= [1]
[0]
[1]
[2]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1 0 0 0] [0]
[0 1 0 0] X + [0]
[0 1 1 0] [0]
[0 0 0 1] [0]
>= [1 0 0 0] [0]
[0 1 0 0] X + [0]
[0 0 1 0] [0]
[0 0 0 1] [0]
= [X]
[activate(n__0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [0()]
[activate(n__plus(X1, X2))] = [0 1 0 0] [1 0 0 0] [0]
[1 0 0 0] X1 + [0 1 0 0] X2 + [0]
[1 0 0 0] [0 2 1 0] [0]
[1 0 0 1] [0 1 0 1] [1]
>= [0 1 0 0] [1 0 0 0] [0]
[1 0 0 0] X1 + [0 1 0 0] X2 + [0]
[1 0 0 0] [0 2 1 0] [0]
[1 0 0 1] [0 1 0 1] [1]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [0 0 0 0] [0]
[1 1 0 0] X + [0]
[2 1 0 0] [0]
[1 0 0 1] [0]
>= [0 0 0 0] [0]
[1 1 0 0] X + [0]
[1 0 0 0] [0]
[1 0 0 1] [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [0 0 0 0] [1 1 0 0] [1]
[1 1 0 0] X1 + [0 0 0 0] X2 + [1]
[1 2 1 0] [0 0 0 0] [2]
[1 0 0 1] [0 1 0 1] [0]
>= [0 0 0 0] [1 1 0 0] [1]
[1 1 0 0] X1 + [0 0 0 0] X2 + [1]
[1 2 1 0] [0 0 0 0] [1]
[1 0 0 1] [0 1 0 1] [0]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [tt()]
[U31(tt(), V2)] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [1]
[0]
[1]
[1]
>= [1]
[0]
[1]
[1]
= [tt()]
[s(X)] = [0 0 0 0] [0]
[1 1 0 0] X + [0]
[1 0 0 0] [0]
[1 0 0 1] [0]
>= [0 0 0 0] [0]
[1 1 0 0] X + [0]
[1 0 0 0] [0]
[1 0 0 1] [0]
= [n__s(X)]
[plus(X1, X2)] = [0 1 0 0] [1 0 0 0] [0]
[1 0 0 0] X1 + [0 1 0 0] X2 + [0]
[1 0 0 0] [0 1 1 0] [0]
[1 0 0 1] [0 1 0 1] [1]
>= [0 1 0 0] [1 0 0 0] [0]
[1 0 0 0] X1 + [0 1 0 0] X2 + [0]
[0 0 0 0] [0 1 1 0] [0]
[1 0 0 1] [0 1 0 1] [1]
= [n__plus(X1, X2)]
[0()] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [n__0()]
[x(X1, X2)] = [0 0 0 0] [1 1 0 0] [1]
[1 1 0 0] X1 + [0 0 0 0] X2 + [1]
[1 1 1 0] [0 0 0 0] [1]
[1 0 0 1] [0 1 0 1] [0]
>= [0 0 0 0] [1 1 0 0] [1]
[1 1 0 0] X1 + [0 0 0 0] X2 + [1]
[0 1 1 0] [0 0 0 0] [1]
[1 0 0 1] [0 1 0 1] [0]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [1 1 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [1 0 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [isNat^#(activate(V2))]
[U11^#(tt(), V2)] = [1 1 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[isNat^#(n__plus(V1, V2))] = [1 1 0 1] [1 1 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [1 1 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [U11^#(isNat(activate(V1)), activate(V2))]
[isNat^#(n__plus(V1, V2))] = [1 1 0 1] [1 1 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [1 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [isNat^#(activate(V1))]
[isNat^#(n__plus(V1, V2))] = [1 1 0 1] [1 1 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [0 0 0 1] [0]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V1)]
[isNat^#(n__plus(V1, V2))] = [1 1 0 1] [1 1 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[isNat^#(n__s(V1))] = [1 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [1 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [isNat^#(activate(V1))]
[isNat^#(n__s(V1))] = [1 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V1)]
[isNat^#(n__x(V1, V2))] = [1 2 0 1] [1 0 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [3]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [1 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [isNat^#(activate(V1))]
[isNat^#(n__x(V1, V2))] = [1 2 0 1] [1 0 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [3]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [0 0 0 1] [0]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V1)]
[isNat^#(n__x(V1, V2))] = [1 2 0 1] [1 0 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [3]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[isNat^#(n__x(V1, V2))] = [1 2 0 1] [1 0 0 1] [1]
[1 1 0 0] V2 + [1 1 0 0] V1 + [3]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
> [1 1 0 1] [0 0 0 0] [0]
[1 1 0 0] V2 + [0 1 0 0] V1 + [2]
[0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1]
= [U31^#(isNat(activate(V1)), activate(V2))]
[activate^#(n__plus(X1, X2))] = [1 0 0 1] [0 1 0 1] [1]
[0 0 0 0] X1 + [0 0 0 0] X2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] X1 + [0 0 0 0] X2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [c_5(activate^#(X1), activate^#(X2))]
[activate^#(n__s(X))] = [1 0 0 1] [0]
[0 0 0 0] X + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
>= [0 0 0 1] [0]
[0 0 0 0] X + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [c_6(activate^#(X))]
[activate^#(n__x(X1, X2))] = [1 0 0 1] [0 1 0 1] [0]
[0 0 0 0] X1 + [0 0 0 0] X2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] X1 + [0 0 0 0] X2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [c_7(activate^#(X1), activate^#(X2))]
[U31^#(tt(), V2)] = [1 1 0 1] [0]
[1 1 0 0] V2 + [2]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [1 0 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [isNat^#(activate(V2))]
[U31^#(tt(), V2)] = [1 1 0 1] [0]
[1 1 0 0] V2 + [2]
[0 0 0 0] [1]
[0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [1 0 0 1] [0]
[1 1 0 0] N + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [isNat^#(activate(N))]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [0 1 1 1] [0 1 1 1] [0]
[1 1 0 1] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [U52^#(isNat(activate(N)), activate(M), activate(N))]
[U52^#(tt(), M, N)] = [0 0 1 1] [0 0 1 1] [0]
[1 0 0 1] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U52^#(tt(), M, N)] = [0 0 1 1] [0 0 1 1] [0]
[1 0 0 1] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [2]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [1]
> [1 0 0 1] [0]
[1 1 0 0] N + [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [isNat^#(activate(N))]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [2]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [1]
> [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [2]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [1]
> [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [2]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [1]
> [0 1 1 1] [0 1 1 1] [0]
[1 1 0 1] N + [0 0 0 0] M + [2]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [U72^#(isNat(activate(N)), activate(M), activate(N))]
[U72^#(tt(), M, N)] = [0 0 1 1] [0 0 1 1] [0]
[1 0 0 1] N + [0 0 0 0] M + [2]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U72^#(tt(), M, N)] = [0 0 1 1] [0 0 1 1] [0]
[1 0 0 1] N + [0 0 0 0] M + [2]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2)) }
Weak DPs:
{ U11^#(tt(), V2) -> isNat^#(activate(V2))
, U11^#(tt(), V2) -> activate^#(V2)
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__plus(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__plus(V1, V2)) -> activate^#(V1)
, isNat^#(n__plus(V1, V2)) -> activate^#(V2)
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__s(V1)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> activate^#(V2)
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> isNat^#(activate(V2))
, U31^#(tt(), V2) -> activate^#(V2)
, U51^#(tt(), M, N) -> isNat^#(activate(N))
, U51^#(tt(), M, N) -> activate^#(M)
, U51^#(tt(), M, N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> activate^#(M)
, U52^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) -> isNat^#(activate(N))
, U71^#(tt(), M, N) -> activate^#(M)
, U71^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) -> activate^#(M)
, U72^#(tt(), M, N) -> activate^#(N) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
DPs: { activate^#(n__s(X)) -> c_6(activate^#(X)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^4)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1, 2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[1]
[U11](x1, x2) = [0]
[0]
[0]
[1]
[tt] = [0]
[0]
[0]
[1]
[U12](x1) = [0]
[0]
[0]
[0 0 0 0] [1]
[isNat](x1) = [0 0 0 0] x1 + [0]
[0 0 0 0] [0]
[1 0 0 1] [1]
[1 0 0 0] [0]
[activate](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [0]
[1 0 0 1] [0]
[1]
[U21](x1) = [0]
[0]
[0]
[1]
[U31](x1, x2) = [0]
[0]
[0]
[1]
[U32](x1) = [0]
[0]
[0]
[1 0 0 0] [1]
[s](x1) = [0 1 1 0] x1 + [1]
[0 0 0 0] [0]
[1 1 0 1] [0]
[1 0 0 0] [1 0 0 0] [1]
[plus](x1, x2) = [1 0 0 0] x1 + [1 0 1 0] x2 + [1]
[0 0 1 0] [0 1 0 0] [0]
[0 1 0 1] [1 1 1 1] [0]
[0]
[0] = [0]
[0]
[0]
[1 0 0 0] [1 0 0 0] [1]
[x](x1, x2) = [1 0 1 0] x1 + [1 0 1 0] x2 + [1]
[0 1 0 0] [0 0 0 0] [0]
[0 1 1 1] [1 1 1 1] [1]
[0]
[n__0] = [0]
[0]
[0]
[1 0 0 0] [1 0 0 0] [1]
[n__plus](x1, x2) = [1 0 0 0] x1 + [1 0 1 0] x2 + [1]
[0 0 1 0] [0 1 0 0] [0]
[0 1 0 1] [1 1 1 1] [0]
[1 0 0 0] [1]
[n__s](x1) = [0 1 1 0] x1 + [1]
[0 0 0 0] [0]
[1 1 0 1] [0]
[1 0 0 0] [1 0 0 0] [1]
[n__x](x1, x2) = [1 0 1 0] x1 + [1 0 1 0] x2 + [1]
[0 1 0 0] [0 0 0 0] [0]
[0 1 1 1] [1 1 1 1] [1]
[1 0 0 0] [1]
[U11^#](x1, x2) = [1 1 0 1] x2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
[1 0 0 0] [1]
[isNat^#](x1) = [0 1 0 1] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[1 0 0 0] [1]
[activate^#](x1) = [0 0 0 0] x1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
[1 0 0 0] [1 0 0 0] [1]
[U31^#](x1, x2) = [0 0 0 0] x1 + [1 1 1 1] x2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [1 1 1 0] [1 1 1
0] [1]
[U51^#](x1, x2, x3) = [1 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [0]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [0]
[0 0 0 0] [1 0 0 0] [1 0 0
0] [1]
[U52^#](x1, x2, x3) = [1 0 0 0] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [0]
[0 0 0 0] [1 1 0 0] [0 1 0
0] [0]
[0 0 0 0] [1 1 0 0] [1 0 0
0] [0]
[1 0 0 0] [1 1 1 0] [1 1 1
0] [1]
[U71^#](x1, x2, x3) = [1 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [0]
[0 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[0 1 0 0] [1 0 0 0] [1 0 0
0] [1]
[U72^#](x1, x2, x3) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [1]
[0 0 0 0] [1 1 0 0] [0 1 0
0] [0]
[0 0 0 0] [1 1 0 0] [1 0 0
0] [0]
[1 0 0 0] [1 0 0 0] [0]
[c_5](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [0]
[c_6](x1) = [0 0 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[1 0 0 0] [1 0 0 0] [0]
[c_7](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [tt()]
[isNat(n__0())] = [1]
[0]
[0]
[1]
>= [1]
[0]
[0]
[0]
= [tt()]
[isNat(n__plus(V1, V2))] = [0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] V2 + [0 0 0 0] V1 + [0]
[0 0 0 0] [0 0 0 0] [0]
[2 1 1 1] [1 1 0 1] [2]
>= [1]
[0]
[0]
[0]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [0 0 0 0] [1]
[0 0 0 0] V1 + [0]
[0 0 0 0] [0]
[2 1 0 1] [2]
>= [1]
[0]
[0]
[0]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [0 0 0 0] [0 0 0 0] [1]
[0 0 0 0] V2 + [0 0 0 0] V1 + [0]
[0 0 0 0] [0 0 0 0] [0]
[2 1 1 1] [1 1 1 1] [3]
>= [1]
[0]
[0]
[0]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1 0 0 0] [0]
[0 1 0 0] X + [0]
[0 0 1 0] [0]
[1 0 0 1] [0]
>= [1 0 0 0] [0]
[0 1 0 0] X + [0]
[0 0 1 0] [0]
[0 0 0 1] [0]
= [X]
[activate(n__0())] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [0()]
[activate(n__plus(X1, X2))] = [1 0 0 0] [1 0 0 0] [1]
[1 0 0 0] X1 + [1 0 1 0] X2 + [1]
[0 0 1 0] [0 1 0 0] [0]
[1 1 0 1] [2 1 1 1] [1]
>= [1 0 0 0] [1 0 0 0] [1]
[1 0 0 0] X1 + [1 0 1 0] X2 + [1]
[0 0 1 0] [0 1 0 0] [0]
[1 1 0 1] [2 1 1 1] [0]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1 0 0 0] [1]
[0 1 1 0] X + [1]
[0 0 0 0] [0]
[2 1 0 1] [1]
>= [1 0 0 0] [1]
[0 1 1 0] X + [1]
[0 0 0 0] [0]
[2 1 0 1] [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1 0 0 0] [1 0 0 0] [1]
[1 0 1 0] X1 + [1 0 1 0] X2 + [1]
[0 1 0 0] [0 0 0 0] [0]
[1 1 1 1] [2 1 1 1] [2]
>= [1 0 0 0] [1 0 0 0] [1]
[1 0 1 0] X1 + [1 0 1 0] X2 + [1]
[0 1 0 0] [0 0 0 0] [0]
[1 1 1 1] [2 1 1 1] [1]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [tt()]
[U31(tt(), V2)] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [1]
[0]
[0]
[0]
>= [1]
[0]
[0]
[0]
= [tt()]
[s(X)] = [1 0 0 0] [1]
[0 1 1 0] X + [1]
[0 0 0 0] [0]
[1 1 0 1] [0]
>= [1 0 0 0] [1]
[0 1 1 0] X + [1]
[0 0 0 0] [0]
[1 1 0 1] [0]
= [n__s(X)]
[plus(X1, X2)] = [1 0 0 0] [1 0 0 0] [1]
[1 0 0 0] X1 + [1 0 1 0] X2 + [1]
[0 0 1 0] [0 1 0 0] [0]
[0 1 0 1] [1 1 1 1] [0]
>= [1 0 0 0] [1 0 0 0] [1]
[1 0 0 0] X1 + [1 0 1 0] X2 + [1]
[0 0 1 0] [0 1 0 0] [0]
[0 1 0 1] [1 1 1 1] [0]
= [n__plus(X1, X2)]
[0()] = [0]
[0]
[0]
[0]
>= [0]
[0]
[0]
[0]
= [n__0()]
[x(X1, X2)] = [1 0 0 0] [1 0 0 0] [1]
[1 0 1 0] X1 + [1 0 1 0] X2 + [1]
[0 1 0 0] [0 0 0 0] [0]
[0 1 1 1] [1 1 1 1] [1]
>= [1 0 0 0] [1 0 0 0] [1]
[1 0 1 0] X1 + [1 0 1 0] X2 + [1]
[0 1 0 0] [0 0 0 0] [0]
[0 1 1 1] [1 1 1 1] [1]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [1 0 0 0] [1]
[1 1 0 1] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
>= [1 0 0 0] [1]
[1 1 0 1] V2 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [isNat^#(activate(V2))]
[U11^#(tt(), V2)] = [1 0 0 0] [1]
[1 1 0 1] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
>= [1 0 0 0] [1]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[isNat^#(n__plus(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 0 1] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [1 0 0 0] [1]
[2 1 0 1] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [U11^#(isNat(activate(V1)), activate(V2))]
[isNat^#(n__plus(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 0 1] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [1 0 0 0] [1]
[1 1 0 1] V1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [isNat^#(activate(V1))]
[isNat^#(n__plus(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 0 1] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [1 0 0 0] [1]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V1)]
[isNat^#(n__plus(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 0 1] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [1 0 0 0] [1]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[isNat^#(n__s(V1))] = [1 0 0 0] [2]
[1 2 1 1] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
> [1 0 0 0] [1]
[1 1 0 1] V1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [isNat^#(activate(V1))]
[isNat^#(n__s(V1))] = [1 0 0 0] [2]
[1 2 1 1] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
> [1 0 0 0] [1]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V1)]
[isNat^#(n__x(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 2 1] V1 + [2]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [1 0 0 0] [1]
[1 1 0 1] V1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [isNat^#(activate(V1))]
[isNat^#(n__x(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 2 1] V1 + [2]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [1 0 0 0] [1]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V1)]
[isNat^#(n__x(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 2 1] V1 + [2]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
> [1 0 0 0] [1]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[isNat^#(n__x(V1, V2))] = [1 0 0 0] [1 0 0 0] [2]
[2 1 2 1] V2 + [1 1 2 1] V1 + [2]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [1 0 0 0] [2]
[2 1 1 1] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [U31^#(isNat(activate(V1)), activate(V2))]
[activate^#(n__plus(X1, X2))] = [1 0 0 0] [1 0 0 0] [2]
[0 0 0 0] X1 + [0 0 0 0] X2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [1 0 0 0] [1 0 0 0] [2]
[0 0 0 0] X1 + [0 0 0 0] X2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [c_5(activate^#(X1), activate^#(X2))]
[activate^#(n__s(X))] = [1 0 0 0] [2]
[0 0 0 0] X + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
> [1 0 0 0] [1]
[0 0 0 0] X + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [c_6(activate^#(X))]
[activate^#(n__x(X1, X2))] = [1 0 0 0] [1 0 0 0] [2]
[0 0 0 0] X1 + [0 0 0 0] X2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
>= [1 0 0 0] [1 0 0 0] [2]
[0 0 0 0] X1 + [0 0 0 0] X2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [c_7(activate^#(X1), activate^#(X2))]
[U31^#(tt(), V2)] = [1 0 0 0] [2]
[1 1 1 1] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
> [1 0 0 0] [1]
[1 1 0 1] V2 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [isNat^#(activate(V2))]
[U31^#(tt(), V2)] = [1 0 0 0] [2]
[1 1 1 1] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
> [1 0 0 0] [1]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(V2)]
[U51^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [1 0 0 0] [1]
[1 1 0 1] N + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [isNat^#(activate(N))]
[U51^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [1 0 0 0] [1]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U51^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [1 0 0 0] [1]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
[U51^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [1]
> [1 0 0 0] [1 0 0 0] [1]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 1 0 0] [1 1 0 0] [0]
[1 0 0 0] [1 1 0 0] [0]
= [U52^#(isNat(activate(N)), activate(M), activate(N))]
[U52^#(tt(), M, N)] = [1 0 0 0] [1 0 0 0] [1]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 1 0 0] [1 1 0 0] [0]
[1 0 0 0] [1 1 0 0] [0]
>= [1 0 0 0] [1]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U52^#(tt(), M, N)] = [1 0 0 0] [1 0 0 0] [1]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 1 0 0] [1 1 0 0] [0]
[1 0 0 0] [1 1 0 0] [0]
>= [1 0 0 0] [1]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
[U71^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [1 0 0 0] [1]
[1 1 0 1] N + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [isNat^#(activate(N))]
[U71^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [1 0 0 0] [1]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U71^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [1 0 0 0] [1]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
[U71^#(tt(), M, N)] = [1 1 1 0] [1 1 1 0] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [1 0 0 0] [1 0 0 0] [1]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 1 0 0] [1 1 0 0] [0]
[1 0 0 0] [1 1 0 0] [0]
= [U72^#(isNat(activate(N)), activate(M), activate(N))]
[U72^#(tt(), M, N)] = [1 0 0 0] [1 0 0 0] [1]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 1 0 0] [1 1 0 0] [0]
[1 0 0 0] [1 1 0 0] [0]
>= [1 0 0 0] [1]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(M)]
[U72^#(tt(), M, N)] = [1 0 0 0] [1 0 0 0] [1]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 1 0 0] [1 1 0 0] [0]
[1 0 0 0] [1 1 0 0] [0]
>= [1 0 0 0] [1]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [activate^#(N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^4)).
Strict DPs:
{ activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2)) }
Weak DPs:
{ U11^#(tt(), V2) -> isNat^#(activate(V2))
, U11^#(tt(), V2) -> activate^#(V2)
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__plus(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__plus(V1, V2)) -> activate^#(V1)
, isNat^#(n__plus(V1, V2)) -> activate^#(V2)
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__s(V1)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> activate^#(V2)
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, U31^#(tt(), V2) -> isNat^#(activate(V2))
, U31^#(tt(), V2) -> activate^#(V2)
, U51^#(tt(), M, N) -> isNat^#(activate(N))
, U51^#(tt(), M, N) -> activate^#(M)
, U51^#(tt(), M, N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> activate^#(M)
, U52^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) -> isNat^#(activate(N))
, U71^#(tt(), M, N) -> activate^#(M)
, U71^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) -> activate^#(M)
, U72^#(tt(), M, N) -> activate^#(N) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^4))
We use the processor 'matrix interpretation of dimension 4' to
orient following rules strictly.
DPs:
{ activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^4)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1, 2}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[1 0 0 0] [0]
[U11](x1, x2) = [0 1 0 0] x1 + [0]
[0 1 0 0] [0]
[0 0 0 0] [1]
[1]
[tt] = [1]
[1]
[1]
[0 0 0 0] [1]
[U12](x1) = [1 0 0 0] x1 + [0]
[1 0 0 0] [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
[isNat](x1) = [1 0 0 0] x1 + [0]
[0 1 0 0] [1]
[0 0 0 1] [1]
[1 0 0 0] [0]
[activate](x1) = [0 1 0 0] x1 + [0]
[0 0 1 0] [0]
[0 0 0 1] [0]
[0 0 0 0] [1]
[U21](x1) = [0 1 0 0] x1 + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
[0 0 0 0] [1]
[U31](x1, x2) = [0 0 0 0] x1 + [1]
[0 0 0 0] [1]
[1 0 0 0] [0]
[0 0 0 0] [1]
[U32](x1) = [1 0 0 0] x1 + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
[1 0 0 0] [0]
[s](x1) = [0 1 1 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 1] [0]
[1 0 0 0] [0 0 1 0] [0]
[plus](x1, x2) = [1 1 1 0] x1 + [1 1 1 1] x2 + [0]
[0 0 1 0] [1 0 0 0] [0]
[1 0 0 1] [1 0 0 1] [0]
[1]
[0] = [1]
[0]
[1]
[1 0 0 0] [1 0 1 0] [1]
[x](x1, x2) = [0 1 1 1] x1 + [1 1 1 1] x2 + [1]
[0 0 1 0] [0 0 0 0] [0]
[1 0 0 1] [0 0 1 1] [1]
[1]
[n__0] = [1]
[0]
[1]
[1 0 0 0] [0 0 1 0] [0]
[n__plus](x1, x2) = [1 1 1 0] x1 + [1 1 1 1] x2 + [0]
[0 0 1 0] [1 0 0 0] [0]
[1 0 0 1] [1 0 0 1] [0]
[1 0 0 0] [0]
[n__s](x1) = [0 1 1 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 1] [0]
[1 0 0 0] [1 0 1 0] [1]
[n__x](x1, x2) = [0 1 1 1] x1 + [1 1 1 1] x2 + [1]
[0 0 1 0] [0 0 0 0] [0]
[1 0 0 1] [0 0 1 1] [1]
[0 0 0 0] [1 0 0 1] [0]
[U11^#](x1, x2) = [0 0 0 0] x1 + [1 1 0 0] x2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [1 1 0 1] [0]
[0 0 0 1] [0]
[isNat^#](x1) = [1 1 0 0] x1 + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
[0 0 0 1] [0]
[activate^#](x1) = [0 0 0 0] x1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
[0 0 0 0] [0 0 0 1] [0]
[U31^#](x1, x2) = [1 0 1 0] x1 + [1 1 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 1 1] [1 1 0 1] [0]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[U51^#](x1, x2, x3) = [1 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [0]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[0 0 0 1] [0 0 0 1] [0]
[U52^#](x1, x2, x3) = [0 0 0 0] x2 + [0 0 0 0] x3 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[U71^#](x1, x2, x3) = [1 0 0 0] x1 + [1 1 1 1] x2 + [1 1 1
1] x3 + [0]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [0]
[1 0 0 0] [1 1 1 1] [1 1 1
1] [1]
[0 0 0 0] [0 0 0 1] [0 0 0
1] [0]
[U72^#](x1, x2, x3) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0 0 0
0] x3 + [1]
[0 0 0 0] [0 0 0 0] [0 0 0
0] [0]
[0 1 0 0] [0 0 0 0] [0 0 0
0] [0]
[1 0 0 0] [1 0 0 0] [0]
[c_5](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [0]
[c_6](x1) = [0 0 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[1 0 1 0] [1 0 0 0] [0]
[c_7](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [1]
[1]
[1]
[1]
>= [1]
[1]
[1]
[1]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [1]
[1]
[1]
[1]
>= [1]
[1]
[1]
[1]
= [tt()]
[isNat(n__0())] = [1]
[1]
[2]
[2]
>= [1]
[1]
[1]
[1]
= [tt()]
[isNat(n__plus(V1, V2))] = [0 0 0 0] [0 0 0 0] [1]
[0 0 1 0] V2 + [1 0 0 0] V1 + [0]
[1 1 1 1] [1 1 1 0] [1]
[1 0 0 1] [1 0 0 1] [1]
>= [0 0 0 0] [1]
[1 0 0 0] V1 + [0]
[1 0 0 0] [0]
[0 0 0 0] [1]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [0 0 0 0] [1]
[1 0 0 0] V1 + [0]
[0 1 1 0] [1]
[0 0 0 1] [1]
>= [0 0 0 0] [1]
[1 0 0 0] V1 + [0]
[0 0 0 0] [1]
[0 0 0 0] [1]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [0 0 0 0] [0 0 0 0] [1]
[1 0 1 0] V2 + [1 0 0 0] V1 + [1]
[1 1 1 1] [0 1 1 1] [2]
[0 0 1 1] [1 0 0 1] [2]
>= [1]
[1]
[1]
[1]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1 0 0 0] [0]
[0 1 0 0] X + [0]
[0 0 1 0] [0]
[0 0 0 1] [0]
>= [1 0 0 0] [0]
[0 1 0 0] X + [0]
[0 0 1 0] [0]
[0 0 0 1] [0]
= [X]
[activate(n__0())] = [1]
[1]
[0]
[1]
>= [1]
[1]
[0]
[1]
= [0()]
[activate(n__plus(X1, X2))] = [1 0 0 0] [0 0 1 0] [0]
[1 1 1 0] X1 + [1 1 1 1] X2 + [0]
[0 0 1 0] [1 0 0 0] [0]
[1 0 0 1] [1 0 0 1] [0]
>= [1 0 0 0] [0 0 1 0] [0]
[1 1 1 0] X1 + [1 1 1 1] X2 + [0]
[0 0 1 0] [1 0 0 0] [0]
[1 0 0 1] [1 0 0 1] [0]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1 0 0 0] [0]
[0 1 1 0] X + [0]
[0 0 0 0] [0]
[0 0 0 1] [0]
>= [1 0 0 0] [0]
[0 1 1 0] X + [0]
[0 0 0 0] [0]
[0 0 0 1] [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1 0 0 0] [1 0 1 0] [1]
[0 1 1 1] X1 + [1 1 1 1] X2 + [1]
[0 0 1 0] [0 0 0 0] [0]
[1 0 0 1] [0 0 1 1] [1]
>= [1 0 0 0] [1 0 1 0] [1]
[0 1 1 1] X1 + [1 1 1 1] X2 + [1]
[0 0 1 0] [0 0 0 0] [0]
[1 0 0 1] [0 0 1 1] [1]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [1]
[1]
[1]
[1]
>= [1]
[1]
[1]
[1]
= [tt()]
[U31(tt(), V2)] = [1]
[1]
[1]
[1]
>= [1]
[1]
[1]
[1]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [1]
[1]
[1]
[1]
>= [1]
[1]
[1]
[1]
= [tt()]
[s(X)] = [1 0 0 0] [0]
[0 1 1 0] X + [0]
[0 0 0 0] [0]
[0 0 0 1] [0]
>= [1 0 0 0] [0]
[0 1 1 0] X + [0]
[0 0 0 0] [0]
[0 0 0 1] [0]
= [n__s(X)]
[plus(X1, X2)] = [1 0 0 0] [0 0 1 0] [0]
[1 1 1 0] X1 + [1 1 1 1] X2 + [0]
[0 0 1 0] [1 0 0 0] [0]
[1 0 0 1] [1 0 0 1] [0]
>= [1 0 0 0] [0 0 1 0] [0]
[1 1 1 0] X1 + [1 1 1 1] X2 + [0]
[0 0 1 0] [1 0 0 0] [0]
[1 0 0 1] [1 0 0 1] [0]
= [n__plus(X1, X2)]
[0()] = [1]
[1]
[0]
[1]
>= [1]
[1]
[0]
[1]
= [n__0()]
[x(X1, X2)] = [1 0 0 0] [1 0 1 0] [1]
[0 1 1 1] X1 + [1 1 1 1] X2 + [1]
[0 0 1 0] [0 0 0 0] [0]
[1 0 0 1] [0 0 1 1] [1]
>= [1 0 0 0] [1 0 1 0] [1]
[0 1 1 1] X1 + [1 1 1 1] X2 + [1]
[0 0 1 0] [0 0 0 0] [0]
[1 0 0 1] [0 0 1 1] [1]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [1 0 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [0]
[1 1 0 1] [1]
>= [0 0 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
= [isNat^#(activate(V2))]
[U11^#(tt(), V2)] = [1 0 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [0]
[1 1 0 1] [1]
>= [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(V2)]
[isNat^#(n__plus(V1, V2))] = [1 0 0 1] [1 0 0 1] [0]
[1 1 2 1] V2 + [2 1 1 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [1 1 1 0] [1]
>= [1 0 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [0]
[1 1 0 1] [1]
= [U11^#(isNat(activate(V1)), activate(V2))]
[isNat^#(n__plus(V1, V2))] = [1 0 0 1] [1 0 0 1] [0]
[1 1 2 1] V2 + [2 1 1 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [1 1 1 0] [1]
>= [0 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
= [isNat^#(activate(V1))]
[isNat^#(n__plus(V1, V2))] = [1 0 0 1] [1 0 0 1] [0]
[1 1 2 1] V2 + [2 1 1 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [1 1 1 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(V1)]
[isNat^#(n__plus(V1, V2))] = [1 0 0 1] [1 0 0 1] [0]
[1 1 2 1] V2 + [2 1 1 0] V1 + [1]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [1 1 1 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(V2)]
[isNat^#(n__s(V1))] = [0 0 0 1] [0]
[1 1 1 0] V1 + [1]
[0 0 0 0] [0]
[0 1 1 0] [1]
>= [0 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
= [isNat^#(activate(V1))]
[isNat^#(n__s(V1))] = [0 0 0 1] [0]
[1 1 1 0] V1 + [1]
[0 0 0 0] [0]
[0 1 1 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(V1)]
[isNat^#(n__x(V1, V2))] = [0 0 1 1] [1 0 0 1] [1]
[2 1 2 1] V2 + [1 1 1 1] V1 + [3]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [0 1 1 1] [2]
> [0 0 0 1] [0]
[1 1 0 0] V1 + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
= [isNat^#(activate(V1))]
[isNat^#(n__x(V1, V2))] = [0 0 1 1] [1 0 0 1] [1]
[2 1 2 1] V2 + [1 1 1 1] V1 + [3]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [0 1 1 1] [2]
> [0 0 0 1] [0]
[0 0 0 0] V1 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(V1)]
[isNat^#(n__x(V1, V2))] = [0 0 1 1] [1 0 0 1] [1]
[2 1 2 1] V2 + [1 1 1 1] V1 + [3]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [0 1 1 1] [2]
> [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(V2)]
[isNat^#(n__x(V1, V2))] = [0 0 1 1] [1 0 0 1] [1]
[2 1 2 1] V2 + [1 1 1 1] V1 + [3]
[0 0 0 0] [0 0 0 0] [0]
[1 1 1 1] [0 1 1 1] [2]
> [0 0 0 1] [0 0 0 0] [0]
[1 1 0 0] V2 + [0 1 0 0] V1 + [2]
[0 0 0 0] [0 0 0 0] [0]
[1 1 0 1] [0 1 0 1] [2]
= [U31^#(isNat(activate(V1)), activate(V2))]
[activate^#(n__plus(X1, X2))] = [1 0 0 1] [1 0 0 1] [0]
[0 0 0 0] X1 + [0 0 0 0] X2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
>= [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] X1 + [0 0 0 0] X2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [c_5(activate^#(X1), activate^#(X2))]
[activate^#(n__s(X))] = [0 0 0 1] [0]
[0 0 0 0] X + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] X + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
= [c_6(activate^#(X))]
[activate^#(n__x(X1, X2))] = [1 0 0 1] [0 0 1 1] [1]
[0 0 0 0] X1 + [0 0 0 0] X2 + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
> [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] X1 + [0 0 0 0] X2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
= [c_7(activate^#(X1), activate^#(X2))]
[U31^#(tt(), V2)] = [0 0 0 1] [0]
[1 1 0 0] V2 + [2]
[0 0 0 0] [0]
[1 1 0 1] [2]
>= [0 0 0 1] [0]
[1 1 0 0] V2 + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
= [isNat^#(activate(V2))]
[U31^#(tt(), V2)] = [0 0 0 1] [0]
[1 1 0 0] V2 + [2]
[0 0 0 0] [0]
[1 1 0 1] [2]
>= [0 0 0 1] [0]
[0 0 0 0] V2 + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(V2)]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0]
[1 1 0 0] N + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
= [isNat^#(activate(N))]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(M)]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(N)]
[U51^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
= [U52^#(isNat(activate(N)), activate(M), activate(N))]
[U52^#(tt(), M, N)] = [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(M)]
[U52^#(tt(), M, N)] = [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(N)]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0]
[1 1 0 0] N + [1]
[0 0 0 0] [0]
[0 1 0 0] [1]
= [isNat^#(activate(N))]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(M)]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(N)]
[U71^#(tt(), M, N)] = [1 1 1 1] [1 1 1 1] [2]
[1 1 1 1] N + [1 1 1 1] M + [1]
[1 1 1 1] [1 1 1 1] [1]
[1 1 1 1] [1 1 1 1] [2]
> [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [0 0 0 0] [0]
= [U72^#(isNat(activate(N)), activate(M), activate(N))]
[U72^#(tt(), M, N)] = [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] M + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(M)]
[U72^#(tt(), M, N)] = [0 0 0 1] [0 0 0 1] [0]
[0 0 0 0] N + [0 0 0 0] M + [1]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
>= [0 0 0 1] [0]
[0 0 0 0] N + [1]
[0 0 0 0] [0]
[0 0 0 0] [1]
= [activate^#(N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ U11^#(tt(), V2) -> isNat^#(activate(V2))
, U11^#(tt(), V2) -> activate^#(V2)
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__plus(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__plus(V1, V2)) -> activate^#(V1)
, isNat^#(n__plus(V1, V2)) -> activate^#(V2)
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__s(V1)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) -> activate^#(V1)
, isNat^#(n__x(V1, V2)) -> activate^#(V2)
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> isNat^#(activate(V2))
, U31^#(tt(), V2) -> activate^#(V2)
, U51^#(tt(), M, N) -> isNat^#(activate(N))
, U51^#(tt(), M, N) -> activate^#(M)
, U51^#(tt(), M, N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> activate^#(M)
, U52^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) -> isNat^#(activate(N))
, U71^#(tt(), M, N) -> activate^#(M)
, U71^#(tt(), M, N) -> activate^#(N)
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) -> activate^#(M)
, U72^#(tt(), M, N) -> activate^#(N) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
S) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak DPs:
{ U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { U52^#(tt(), M, N) -> c_1() }
Weak DPs:
{ U51^#(tt(), M, N) ->
c_2(U52^#(isNat(activate(N)), activate(M), activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The dependency graph contains no loops, we remove all dependency
pairs.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
S) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {7} by applications of
Pre({7}) = {6}. Here rules are labeled as follows:
DPs:
{ 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, 2: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 3: isNat^#(n__s(V1)) ->
c_3(isNat^#(activate(V1)), activate^#(V1))
, 4: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, 5: U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, 6: U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 7: U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N))
, 8: activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, 9: activate^#(n__s(X)) -> c_6(activate^#(X))
, 10: activate^#(n__x(X1, X2)) ->
c_7(activate^#(X1), activate^#(X2))
, 11: U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, 12: U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ activate^#(n__plus(X1, X2)) ->
c_5(activate^#(X1), activate^#(X2))
, activate^#(n__s(X)) -> c_6(activate^#(X))
, activate^#(n__x(X1, X2)) -> c_7(activate^#(X1), activate^#(X2))
, U52^#(tt(), M, N) -> c_11(activate^#(N), activate^#(M))
, U72^#(tt(), M, N) ->
c_13(activate^#(N), activate^#(M), activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak DPs:
{ U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)),
activate^#(V1),
activate^#(V2))
, U31^#(tt(), V2) -> c_8(isNat^#(activate(V2)), activate^#(V2))
, U51^#(tt(), M, N) ->
c_10(U52^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N))
, U71^#(tt(), M, N) ->
c_12(U72^#(isNat(activate(N)), activate(M), activate(N)),
isNat^#(activate(N)),
activate^#(N),
activate^#(M),
activate^#(N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
Weak DPs: { U51^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, 6: U71^#(tt(), M, N) -> c_6(isNat^#(activate(N)))
, 7: U51^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[U11](x1, x2) = [0]
[tt] = [0]
[U12](x1) = [0]
[isNat](x1) = [0]
[activate](x1) = [1] x1 + [0]
[U21](x1) = [0]
[U31](x1, x2) = [0]
[U32](x1) = [0]
[s](x1) = [1] x1 + [4]
[plus](x1, x2) = [1] x1 + [1] x2 + [0]
[0] = [0]
[x](x1, x2) = [1] x1 + [1] x2 + [0]
[n__0] = [0]
[n__plus](x1, x2) = [1] x1 + [1] x2 + [0]
[n__s](x1) = [1] x1 + [4]
[n__x](x1, x2) = [1] x1 + [1] x2 + [0]
[U11^#](x1, x2) = [1] x1 + [1] x2 + [0]
[isNat^#](x1) = [1] x1 + [0]
[U31^#](x1, x2) = [1] x2 + [0]
[U51^#](x1, x2, x3) = [1] x2 + [7] x3 + [5]
[U71^#](x1, x2, x3) = [1] x1 + [4] x2 + [7] x3 + [4]
[c_1](x1) = [1] x1 + [0]
[c_2](x1, x2) = [1] x1 + [1] x2 + [0]
[c_3](x1) = [1] x1 + [1]
[c_4](x1, x2) = [1] x1 + [1] x2 + [0]
[c_5](x1) = [1] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [0]
>= [0]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [0]
>= [0]
= [tt()]
[isNat(n__0())] = [0]
>= [0]
= [tt()]
[isNat(n__plus(V1, V2))] = [0]
>= [0]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [0]
>= [0]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [0]
>= [0]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__0())] = [0]
>= [0]
= [0()]
[activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1] X + [4]
>= [1] X + [4]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [0]
>= [0]
= [tt()]
[U31(tt(), V2)] = [0]
>= [0]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [0]
>= [0]
= [tt()]
[s(X)] = [1] X + [4]
>= [1] X + [4]
= [n__s(X)]
[plus(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n__plus(X1, X2)]
[0()] = [0]
>= [0]
= [n__0()]
[x(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [c_1(isNat^#(activate(V2)))]
[isNat^#(n__plus(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[isNat^#(n__s(V1))] = [1] V1 + [4]
> [1] V1 + [1]
= [c_3(isNat^#(activate(V1)))]
[isNat^#(n__x(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[U31^#(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [c_5(isNat^#(activate(V2)))]
[U51^#(tt(), M, N)] = [7] N + [1] M + [5]
> [1] N + [0]
= [c_7(isNat^#(activate(N)))]
[U71^#(tt(), M, N)] = [7] N + [4] M + [4]
> [1] N + [0]
= [c_6(isNat^#(activate(N)))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) }
Weak DPs:
{ isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, U51^#(tt(), M, N) -> c_7(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, 2: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 4: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, 6: U51^#(tt(), M, N) -> c_7(isNat^#(activate(N))) }
Trs:
{ isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[U11](x1, x2) = [0]
[tt] = [0]
[U12](x1) = [0]
[isNat](x1) = [1] x1 + [4]
[activate](x1) = [1] x1 + [0]
[U21](x1) = [0]
[U31](x1, x2) = [0]
[U32](x1) = [0]
[s](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [1] x2 + [3]
[0] = [6]
[x](x1, x2) = [1] x1 + [1] x2 + [3]
[n__0] = [6]
[n__plus](x1, x2) = [1] x1 + [1] x2 + [3]
[n__s](x1) = [1] x1 + [0]
[n__x](x1, x2) = [1] x1 + [1] x2 + [3]
[U11^#](x1, x2) = [3] x2 + [7]
[isNat^#](x1) = [3] x1 + [4]
[U31^#](x1, x2) = [3] x2 + [5]
[U51^#](x1, x2, x3) = [4] x2 + [7] x3 + [5]
[U71^#](x1, x2, x3) = [4] x2 + [7] x3 + [4]
[c_1](x1) = [1] x1 + [1]
[c_2](x1, x2) = [1] x1 + [1] x2 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1, x2) = [1] x1 + [1] x2 + [4]
[c_5](x1) = [1] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [0]
>= [0]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [0]
>= [0]
= [tt()]
[isNat(n__0())] = [10]
> [0]
= [tt()]
[isNat(n__plus(V1, V2))] = [1] V2 + [1] V1 + [7]
> [0]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [1] V1 + [4]
> [0]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [1] V2 + [1] V1 + [7]
> [0]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__0())] = [6]
>= [6]
= [0()]
[activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [3]
>= [1] X1 + [1] X2 + [3]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1] X + [0]
>= [1] X + [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [3]
>= [1] X1 + [1] X2 + [3]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [0]
>= [0]
= [tt()]
[U31(tt(), V2)] = [0]
>= [0]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [0]
>= [0]
= [tt()]
[s(X)] = [1] X + [0]
>= [1] X + [0]
= [n__s(X)]
[plus(X1, X2)] = [1] X1 + [1] X2 + [3]
>= [1] X1 + [1] X2 + [3]
= [n__plus(X1, X2)]
[0()] = [6]
>= [6]
= [n__0()]
[x(X1, X2)] = [1] X1 + [1] X2 + [3]
>= [1] X1 + [1] X2 + [3]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [3] V2 + [7]
> [3] V2 + [5]
= [c_1(isNat^#(activate(V2)))]
[isNat^#(n__plus(V1, V2))] = [3] V2 + [3] V1 + [13]
> [3] V2 + [3] V1 + [11]
= [c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[isNat^#(n__s(V1))] = [3] V1 + [4]
>= [3] V1 + [4]
= [c_3(isNat^#(activate(V1)))]
[isNat^#(n__x(V1, V2))] = [3] V2 + [3] V1 + [13]
>= [3] V2 + [3] V1 + [13]
= [c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[U31^#(tt(), V2)] = [3] V2 + [5]
> [3] V2 + [4]
= [c_5(isNat^#(activate(V2)))]
[U51^#(tt(), M, N)] = [7] N + [4] M + [5]
> [3] N + [4]
= [c_7(isNat^#(activate(N)))]
[U71^#(tt(), M, N)] = [7] N + [4] M + [4]
>= [3] N + [4]
= [c_6(isNat^#(activate(N)))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, 2: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 3: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 4: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, 5: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, 6: U51^#(tt(), M, N) -> c_7(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,2,4,6}. These cover all (indirect) predecessors of
dependency pairs {1,2,4,6,7}, their number of application is
equally bounded. The dependency pairs are shifted into the weak
component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1))) }
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_7(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 6: U51^#(tt(), M, N) -> c_7(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[U11](x1, x2) = [0]
[tt] = [0]
[U12](x1) = [0]
[isNat](x1) = [0]
[activate](x1) = [1] x1 + [0]
[U21](x1) = [0]
[U31](x1, x2) = [0]
[U32](x1) = [0]
[s](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [1] x2 + [0]
[0] = [0]
[x](x1, x2) = [1] x1 + [1] x2 + [1]
[n__0] = [0]
[n__plus](x1, x2) = [1] x1 + [1] x2 + [0]
[n__s](x1) = [1] x1 + [0]
[n__x](x1, x2) = [1] x1 + [1] x2 + [1]
[U11^#](x1, x2) = [1] x2 + [0]
[isNat^#](x1) = [1] x1 + [0]
[U31^#](x1, x2) = [1] x1 + [1] x2 + [0]
[U51^#](x1, x2, x3) = [4] x2 + [7] x3 + [4]
[U71^#](x1, x2, x3) = [2] x2 + [7] x3 + [4]
[c_1](x1) = [1] x1 + [0]
[c_2](x1, x2) = [1] x1 + [1] x2 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1, x2) = [1] x1 + [1] x2 + [0]
[c_5](x1) = [1] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[U11(tt(), V2)] = [0]
>= [0]
= [U12(isNat(activate(V2)))]
[U12(tt())] = [0]
>= [0]
= [tt()]
[isNat(n__0())] = [0]
>= [0]
= [tt()]
[isNat(n__plus(V1, V2))] = [0]
>= [0]
= [U11(isNat(activate(V1)), activate(V2))]
[isNat(n__s(V1))] = [0]
>= [0]
= [U21(isNat(activate(V1)))]
[isNat(n__x(V1, V2))] = [0]
>= [0]
= [U31(isNat(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__0())] = [0]
>= [0]
= [0()]
[activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [plus(activate(X1), activate(X2))]
[activate(n__s(X))] = [1] X + [0]
>= [1] X + [0]
= [s(activate(X))]
[activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [x(activate(X1), activate(X2))]
[U21(tt())] = [0]
>= [0]
= [tt()]
[U31(tt(), V2)] = [0]
>= [0]
= [U32(isNat(activate(V2)))]
[U32(tt())] = [0]
>= [0]
= [tt()]
[s(X)] = [1] X + [0]
>= [1] X + [0]
= [n__s(X)]
[plus(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n__plus(X1, X2)]
[0()] = [0]
>= [0]
= [n__0()]
[x(X1, X2)] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [n__x(X1, X2)]
[U11^#(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [c_1(isNat^#(activate(V2)))]
[isNat^#(n__plus(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[isNat^#(n__s(V1))] = [1] V1 + [0]
>= [1] V1 + [0]
= [c_3(isNat^#(activate(V1)))]
[isNat^#(n__x(V1, V2))] = [1] V2 + [1] V1 + [1]
> [1] V2 + [1] V1 + [0]
= [c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))]
[U31^#(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [c_5(isNat^#(activate(V2)))]
[U51^#(tt(), M, N)] = [7] N + [4] M + [4]
> [1] N + [0]
= [c_7(isNat^#(activate(N)))]
[U71^#(tt(), M, N)] = [7] N + [2] M + [4]
> [1] N + [0]
= [c_6(isNat^#(activate(N)))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 2: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, 3: isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, 4: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, 5: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, 6: U51^#(tt(), M, N) -> c_7(isNat^#(activate(N)))
, 7: U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {1,6,7}. These cover all (indirect) predecessors of
dependency pairs {1,5,6,7}, their number of application is equally
bounded. The dependency pairs are shifted into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_7(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)))
, isNat^#(n__plus(V1, V2)) ->
c_2(U11^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)))
, isNat^#(n__x(V1, V2)) ->
c_4(U31^#(isNat(activate(V1)), activate(V2)),
isNat^#(activate(V1)))
, U31^#(tt(), V2) -> c_5(isNat^#(activate(V2)))
, U51^#(tt(), M, N) -> c_7(isNat^#(activate(N)))
, U71^#(tt(), M, N) -> c_6(isNat^#(activate(N))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))
, activate(n__x(X1, X2)) -> x(activate(X1), activate(X2))
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, s(X) -> n__s(X)
, plus(X1, X2) -> n__plus(X1, X2)
, 0() -> n__0()
, x(X1, X2) -> n__x(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^5))