We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f4(S(x''), S(x'), x3, x4, S(x)) -> f2(S(x''), x', x3, x4, x)
, f4(S(x'), S(x), x3, x4, 0()) -> 0()
, f4(S(x'), 0(), x3, x4, S(x)) -> f3(x', 0(), x3, x4, x)
, f4(S(x), 0(), x3, x4, 0()) -> 0()
, f4(0(), x2, x3, x4, x5) -> 0()
, f2(x1, x2, S(x''), S(x'), S(x)) -> f5(x1, x2, S(x''), x', x)
, f2(x1, x2, S(x'), S(x), 0()) -> 0()
, f2(x1, x2, S(x'), 0(), S(x)) -> f3(x1, x2, x', 0(), x)
, f2(x1, x2, S(x), 0(), 0()) -> 0()
, f2(x1, x2, 0(), x4, x5) -> 0()
, f3(x1, x2, x3, x4, S(x)) -> f4(x1, x2, x4, x3, x)
, f3(x1, x2, x3, x4, 0()) -> 0()
, f5(x1, x2, x3, x4, S(x)) -> f6(x2, x1, x3, x4, x)
, f5(x1, x2, x3, x4, 0()) -> 0()
, f0(x1, S(x'), x3, S(x), x5) -> f1(x', S(x'), x, S(x), S(x))
, f0(x1, S(x), x3, 0(), x5) -> 0()
, f0(x1, 0(), x3, x4, x5) -> 0()
, f1(x1, x2, x3, x4, S(x)) -> f2(x2, x1, x3, x4, x)
, f1(x1, x2, x3, x4, 0()) -> 0()
, f6(x1, x2, x3, x4, S(x)) -> f0(x1, x2, x4, x3, x)
, f6(x1, x2, x3, x4, 0()) -> 0() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
Strict Trs:
{ f4(S(x''), S(x'), x3, x4, S(x)) -> f2(S(x''), x', x3, x4, x)
, f4(S(x'), S(x), x3, x4, 0()) -> 0()
, f4(S(x'), 0(), x3, x4, S(x)) -> f3(x', 0(), x3, x4, x)
, f4(S(x), 0(), x3, x4, 0()) -> 0()
, f4(0(), x2, x3, x4, x5) -> 0()
, f2(x1, x2, S(x''), S(x'), S(x)) -> f5(x1, x2, S(x''), x', x)
, f2(x1, x2, S(x'), S(x), 0()) -> 0()
, f2(x1, x2, S(x'), 0(), S(x)) -> f3(x1, x2, x', 0(), x)
, f2(x1, x2, S(x), 0(), 0()) -> 0()
, f2(x1, x2, 0(), x4, x5) -> 0()
, f3(x1, x2, x3, x4, S(x)) -> f4(x1, x2, x4, x3, x)
, f3(x1, x2, x3, x4, 0()) -> 0()
, f5(x1, x2, x3, x4, S(x)) -> f6(x2, x1, x3, x4, x)
, f5(x1, x2, x3, x4, 0()) -> 0()
, f0(x1, S(x'), x3, S(x), x5) -> f1(x', S(x'), x, S(x), S(x))
, f0(x1, S(x), x3, 0(), x5) -> 0()
, f0(x1, 0(), x3, x4, x5) -> 0()
, f1(x1, x2, x3, x4, S(x)) -> f2(x2, x1, x3, x4, x)
, f1(x1, x2, x3, x4, 0()) -> 0()
, f6(x1, x2, x3, x4, S(x)) -> f0(x1, x2, x4, x3, x)
, f6(x1, x2, x3, x4, 0()) -> 0() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^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(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_6) = {1},
Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1},
Uargs(c_15) = {1}, Uargs(c_18) = {1}, Uargs(c_20) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[S](x1) = [0]
[0]
[0] = [0]
[0]
[f4^#](x1, x2, x3, x4, x5) = [0 0] x3 + [0 0] x4 + [0]
[2 1] [0 2] [0]
[c_1](x1) = [1 0] x1 + [0]
[0 1] [0]
[f2^#](x1, x2, x3, x4, x5) = [0]
[0]
[c_2] = [0]
[0]
[c_3](x1) = [1 0] x1 + [0]
[0 1] [2]
[f3^#](x1, x2, x3, x4, x5) = [0]
[0]
[c_4] = [0]
[0]
[c_5] = [0]
[0]
[c_6](x1) = [1 0] x1 + [0]
[0 1] [0]
[f5^#](x1, x2, x3, x4, x5) = [0 0] x1 + [0]
[0 2] [0]
[c_7] = [0]
[0]
[c_8](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_9] = [0]
[0]
[c_10] = [0]
[0]
[c_11](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_12] = [0]
[0]
[c_13](x1) = [1 0] x1 + [0]
[0 1] [0]
[f6^#](x1, x2, x3, x4, x5) = [0]
[0]
[c_14] = [0]
[0]
[f0^#](x1, x2, x3, x4, x5) = [0]
[0]
[c_15](x1) = [1 0] x1 + [0]
[0 1] [0]
[f1^#](x1, x2, x3, x4, x5) = [1]
[0]
[c_16] = [0]
[0]
[c_17] = [0]
[0]
[c_18](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_19] = [0]
[0]
[c_20](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_21] = [0]
[0]
The order satisfies the following ordering constraints:
[f4^#(S(x''), S(x'), x3, x4, S(x))] = [0 0] x3 + [0 0] x4 + [0]
[2 1] [0 2] [0]
>= [0]
[0]
= [c_1(f2^#(S(x''), x', x3, x4, x))]
[f4^#(S(x'), S(x), x3, x4, 0())] = [0 0] x3 + [0 0] x4 + [0]
[2 1] [0 2] [0]
>= [0]
[0]
= [c_2()]
[f4^#(S(x'), 0(), x3, x4, S(x))] = [0 0] x3 + [0 0] x4 + [0]
[2 1] [0 2] [0]
? [0]
[2]
= [c_3(f3^#(x', 0(), x3, x4, x))]
[f4^#(S(x), 0(), x3, x4, 0())] = [0 0] x3 + [0 0] x4 + [0]
[2 1] [0 2] [0]
>= [0]
[0]
= [c_4()]
[f4^#(0(), x2, x3, x4, x5)] = [0 0] x3 + [0 0] x4 + [0]
[2 1] [0 2] [0]
>= [0]
[0]
= [c_5()]
[f2^#(x1, x2, S(x''), S(x'), S(x))] = [0]
[0]
? [0 0] x1 + [0]
[0 2] [0]
= [c_6(f5^#(x1, x2, S(x''), x', x))]
[f2^#(x1, x2, S(x'), S(x), 0())] = [0]
[0]
>= [0]
[0]
= [c_7()]
[f2^#(x1, x2, S(x'), 0(), S(x))] = [0]
[0]
>= [0]
[0]
= [c_8(f3^#(x1, x2, x', 0(), x))]
[f2^#(x1, x2, S(x), 0(), 0())] = [0]
[0]
>= [0]
[0]
= [c_9()]
[f2^#(x1, x2, 0(), x4, x5)] = [0]
[0]
>= [0]
[0]
= [c_10()]
[f3^#(x1, x2, x3, x4, S(x))] = [0]
[0]
? [0 0] x3 + [0 0] x4 + [0]
[0 2] [2 1] [0]
= [c_11(f4^#(x1, x2, x4, x3, x))]
[f3^#(x1, x2, x3, x4, 0())] = [0]
[0]
>= [0]
[0]
= [c_12()]
[f5^#(x1, x2, x3, x4, S(x))] = [0 0] x1 + [0]
[0 2] [0]
>= [0]
[0]
= [c_13(f6^#(x2, x1, x3, x4, x))]
[f5^#(x1, x2, x3, x4, 0())] = [0 0] x1 + [0]
[0 2] [0]
>= [0]
[0]
= [c_14()]
[f6^#(x1, x2, x3, x4, S(x))] = [0]
[0]
>= [0]
[0]
= [c_20(f0^#(x1, x2, x4, x3, x))]
[f6^#(x1, x2, x3, x4, 0())] = [0]
[0]
>= [0]
[0]
= [c_21()]
[f0^#(x1, S(x'), x3, S(x), x5)] = [0]
[0]
? [1]
[0]
= [c_15(f1^#(x', S(x'), x, S(x), S(x)))]
[f0^#(x1, S(x), x3, 0(), x5)] = [0]
[0]
>= [0]
[0]
= [c_16()]
[f0^#(x1, 0(), x3, x4, x5)] = [0]
[0]
>= [0]
[0]
= [c_17()]
[f1^#(x1, x2, x3, x4, S(x))] = [1]
[0]
> [0]
[0]
= [c_18(f2^#(x2, x1, x3, x4, x))]
[f1^#(x1, x2, x3, x4, 0())] = [1]
[0]
> [0]
[0]
= [c_19()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17() }
Weak DPs:
{ f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {2,4,5,12,14,16,18,19} by
applications of Pre({2,4,5,12,14,16,18,19}) = {3,6,8,11,13,15}.
Here rules are labeled as follows:
DPs:
{ 1: f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, 2: f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, 3: f4^#(S(x'), 0(), x3, x4, S(x)) ->
c_3(f3^#(x', 0(), x3, x4, x))
, 4: f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, 5: f4^#(0(), x2, x3, x4, x5) -> c_5()
, 6: f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, 7: f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, 8: f2^#(x1, x2, S(x'), 0(), S(x)) ->
c_8(f3^#(x1, x2, x', 0(), x))
, 9: f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, 10: f2^#(x1, x2, 0(), x4, x5) -> c_10()
, 11: f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, 12: f3^#(x1, x2, x3, x4, 0()) -> c_12()
, 13: f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, 14: f5^#(x1, x2, x3, x4, 0()) -> c_14()
, 15: f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, 16: f6^#(x1, x2, x3, x4, 0()) -> c_21()
, 17: f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, 18: f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, 19: f0^#(x1, 0(), x3, x4, x5) -> c_17()
, 20: f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, 21: f1^#(x1, x2, x3, x4, 0()) -> c_19() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x))) }
Weak DPs:
{ f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {11} by applications of
Pre({11}) = {10}. Here rules are labeled as follows:
DPs:
{ 1: f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, 2: f4^#(S(x'), 0(), x3, x4, S(x)) ->
c_3(f3^#(x', 0(), x3, x4, x))
, 3: f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, 4: f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, 5: f2^#(x1, x2, S(x'), 0(), S(x)) ->
c_8(f3^#(x1, x2, x', 0(), x))
, 6: f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, 7: f2^#(x1, x2, 0(), x4, x5) -> c_10()
, 8: f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, 9: f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, 10: f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, 11: f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, 12: f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, 13: f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, 14: f4^#(0(), x2, x3, x4, x5) -> c_5()
, 15: f3^#(x1, x2, x3, x4, 0()) -> c_12()
, 16: f5^#(x1, x2, x3, x4, 0()) -> c_14()
, 17: f6^#(x1, x2, x3, x4, 0()) -> c_21()
, 18: f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, 19: f0^#(x1, 0(), x3, x4, x5) -> c_17()
, 20: f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, 21: f1^#(x1, x2, x3, x4, 0()) -> c_19() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x)) }
Weak DPs:
{ f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {10} by applications of
Pre({10}) = {9}. Here rules are labeled as follows:
DPs:
{ 1: f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, 2: f4^#(S(x'), 0(), x3, x4, S(x)) ->
c_3(f3^#(x', 0(), x3, x4, x))
, 3: f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, 4: f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, 5: f2^#(x1, x2, S(x'), 0(), S(x)) ->
c_8(f3^#(x1, x2, x', 0(), x))
, 6: f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, 7: f2^#(x1, x2, 0(), x4, x5) -> c_10()
, 8: f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, 9: f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, 10: f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, 11: f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, 12: f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, 13: f4^#(0(), x2, x3, x4, x5) -> c_5()
, 14: f3^#(x1, x2, x3, x4, 0()) -> c_12()
, 15: f5^#(x1, x2, x3, x4, 0()) -> c_14()
, 16: f6^#(x1, x2, x3, x4, 0()) -> c_21()
, 17: f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, 18: f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, 19: f0^#(x1, 0(), x3, x4, x5) -> c_17()
, 20: f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, 21: f1^#(x1, x2, x3, x4, 0()) -> c_19() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x)) }
Weak DPs:
{ f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {9} by applications of
Pre({9}) = {3}. Here rules are labeled as follows:
DPs:
{ 1: f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, 2: f4^#(S(x'), 0(), x3, x4, S(x)) ->
c_3(f3^#(x', 0(), x3, x4, x))
, 3: f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, 4: f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, 5: f2^#(x1, x2, S(x'), 0(), S(x)) ->
c_8(f3^#(x1, x2, x', 0(), x))
, 6: f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, 7: f2^#(x1, x2, 0(), x4, x5) -> c_10()
, 8: f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, 9: f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, 10: f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, 11: f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, 12: f4^#(0(), x2, x3, x4, x5) -> c_5()
, 13: f3^#(x1, x2, x3, x4, 0()) -> c_12()
, 14: f5^#(x1, x2, x3, x4, 0()) -> c_14()
, 15: f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, 16: f6^#(x1, x2, x3, x4, 0()) -> c_21()
, 17: f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, 18: f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, 19: f0^#(x1, 0(), x3, x4, x5) -> c_17()
, 20: f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, 21: f1^#(x1, x2, x3, x4, 0()) -> c_19() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x)) }
Weak DPs:
{ f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x))
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
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.
{ f4^#(S(x'), S(x), x3, x4, 0()) -> c_2()
, f4^#(S(x), 0(), x3, x4, 0()) -> c_4()
, f4^#(0(), x2, x3, x4, x5) -> c_5()
, f3^#(x1, x2, x3, x4, 0()) -> c_12()
, f5^#(x1, x2, x3, x4, 0()) -> c_14()
, f6^#(x1, x2, x3, x4, 0()) -> c_21()
, f0^#(x1, S(x), x3, 0(), x5) -> c_16()
, f0^#(x1, 0(), x3, x4, x5) -> c_17()
, f1^#(x1, x2, x3, x4, 0()) -> c_19() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x)) }
Weak DPs:
{ f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x)) }
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: f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, 6: f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, 7: f2^#(x1, x2, 0(), x4, x5) -> c_10() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_6) = {1},
Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1},
Uargs(c_15) = {1}, Uargs(c_18) = {1}, Uargs(c_20) = {1}
TcT has computed the following constructor-restricted matrix
interpretation. Note that the diagonal of the component-wise maxima
of interpretation-entries (of constructors) contains no more than 0
non-zero entries.
[S](x1) = [3]
[0] = [0]
[f4^#](x1, x2, x3, x4, x5) = [1]
[c_1](x1) = [1] x1 + [0]
[f2^#](x1, x2, x3, x4, x5) = [1]
[c_3](x1) = [1] x1 + [0]
[f3^#](x1, x2, x3, x4, x5) = [1]
[c_6](x1) = [1] x1 + [0]
[f5^#](x1, x2, x3, x4, x5) = [1]
[c_7] = [0]
[c_8](x1) = [1] x1 + [0]
[c_9] = [0]
[c_10] = [0]
[c_11](x1) = [1] x1 + [0]
[c_13](x1) = [1] x1 + [0]
[f6^#](x1, x2, x3, x4, x5) = [1]
[f0^#](x1, x2, x3, x4, x5) = [1]
[c_15](x1) = [1] x1 + [0]
[f1^#](x1, x2, x3, x4, x5) = [1]
[c_18](x1) = [1] x1 + [0]
[c_20](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[f4^#(S(x''), S(x'), x3, x4, S(x))] = [1]
>= [1]
= [c_1(f2^#(S(x''), x', x3, x4, x))]
[f4^#(S(x'), 0(), x3, x4, S(x))] = [1]
>= [1]
= [c_3(f3^#(x', 0(), x3, x4, x))]
[f2^#(x1, x2, S(x''), S(x'), S(x))] = [1]
>= [1]
= [c_6(f5^#(x1, x2, S(x''), x', x))]
[f2^#(x1, x2, S(x'), S(x), 0())] = [1]
> [0]
= [c_7()]
[f2^#(x1, x2, S(x'), 0(), S(x))] = [1]
>= [1]
= [c_8(f3^#(x1, x2, x', 0(), x))]
[f2^#(x1, x2, S(x), 0(), 0())] = [1]
> [0]
= [c_9()]
[f2^#(x1, x2, 0(), x4, x5)] = [1]
> [0]
= [c_10()]
[f3^#(x1, x2, x3, x4, S(x))] = [1]
>= [1]
= [c_11(f4^#(x1, x2, x4, x3, x))]
[f5^#(x1, x2, x3, x4, S(x))] = [1]
>= [1]
= [c_13(f6^#(x2, x1, x3, x4, x))]
[f6^#(x1, x2, x3, x4, S(x))] = [1]
>= [1]
= [c_20(f0^#(x1, x2, x4, x3, x))]
[f0^#(x1, S(x'), x3, S(x), x5)] = [1]
>= [1]
= [c_15(f1^#(x', S(x'), x, S(x), S(x)))]
[f1^#(x1, x2, x3, x4, S(x))] = [1]
>= [1]
= [c_18(f2^#(x2, x1, x3, x4, x))]
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:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x)) }
Weak DPs:
{ f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10()
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x)) }
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.
{ f2^#(x1, x2, S(x'), S(x), 0()) -> c_7()
, f2^#(x1, x2, S(x), 0(), 0()) -> c_9()
, f2^#(x1, x2, 0(), x4, x5) -> c_10() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x)) }
Weak DPs:
{ f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x)) }
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:
{ 2: f4^#(S(x'), 0(), x3, x4, S(x)) ->
c_3(f3^#(x', 0(), x3, x4, x))
, 4: f2^#(x1, x2, S(x'), 0(), S(x)) ->
c_8(f3^#(x1, x2, x', 0(), x))
, 5: f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, 7: f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, 8: f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, 9: f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_6) = {1},
Uargs(c_8) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1},
Uargs(c_15) = {1}, Uargs(c_18) = {1}, Uargs(c_20) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[S](x1) = [1] x1 + [3]
[0] = [0]
[f4^#](x1, x2, x3, x4, x5) = [3] x1 + [2] x3 + [2] x4 + [2]
[c_1](x1) = [1] x1 + [0]
[f2^#](x1, x2, x3, x4, x5) = [3] x1 + [2] x3 + [2]
[c_3](x1) = [1] x1 + [0]
[f3^#](x1, x2, x3, x4, x5) = [3] x1 + [2] x3 + [2] x4 + [3]
[c_6](x1) = [1] x1 + [1]
[f5^#](x1, x2, x3, x4, x5) = [3] x1 + [2] x3 + [1]
[c_7] = [0]
[c_8](x1) = [1] x1 + [4]
[c_9] = [0]
[c_10] = [0]
[c_11](x1) = [1] x1 + [0]
[c_13](x1) = [1] x1 + [0]
[f6^#](x1, x2, x3, x4, x5) = [3] x2 + [2] x3 + [1]
[f0^#](x1, x2, x3, x4, x5) = [3] x2 + [2] x4 + [0]
[c_15](x1) = [1] x1 + [1]
[f1^#](x1, x2, x3, x4, x5) = [3] x2 + [2] x3 + [3]
[c_18](x1) = [1] x1 + [0]
[c_20](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[f4^#(S(x''), S(x'), x3, x4, S(x))] = [3] x'' + [2] x3 + [2] x4 + [11]
>= [3] x'' + [2] x3 + [11]
= [c_1(f2^#(S(x''), x', x3, x4, x))]
[f4^#(S(x'), 0(), x3, x4, S(x))] = [3] x' + [2] x3 + [2] x4 + [11]
> [3] x' + [2] x3 + [2] x4 + [3]
= [c_3(f3^#(x', 0(), x3, x4, x))]
[f2^#(x1, x2, S(x''), S(x'), S(x))] = [2] x'' + [3] x1 + [8]
>= [2] x'' + [3] x1 + [8]
= [c_6(f5^#(x1, x2, S(x''), x', x))]
[f2^#(x1, x2, S(x'), 0(), S(x))] = [2] x' + [3] x1 + [8]
> [2] x' + [3] x1 + [7]
= [c_8(f3^#(x1, x2, x', 0(), x))]
[f3^#(x1, x2, x3, x4, S(x))] = [2] x3 + [2] x4 + [3] x1 + [3]
> [2] x3 + [2] x4 + [3] x1 + [2]
= [c_11(f4^#(x1, x2, x4, x3, x))]
[f5^#(x1, x2, x3, x4, S(x))] = [2] x3 + [3] x1 + [1]
>= [2] x3 + [3] x1 + [1]
= [c_13(f6^#(x2, x1, x3, x4, x))]
[f6^#(x1, x2, x3, x4, S(x))] = [2] x3 + [3] x2 + [1]
> [2] x3 + [3] x2 + [0]
= [c_20(f0^#(x1, x2, x4, x3, x))]
[f0^#(x1, S(x'), x3, S(x), x5)] = [3] x' + [2] x + [15]
> [3] x' + [2] x + [13]
= [c_15(f1^#(x', S(x'), x, S(x), S(x)))]
[f1^#(x1, x2, x3, x4, S(x))] = [2] x3 + [3] x2 + [3]
> [2] x3 + [3] x2 + [2]
= [c_18(f2^#(x2, x1, x3, x4, x))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, 2: f4^#(S(x'), 0(), x3, x4, S(x)) ->
c_3(f3^#(x', 0(), x3, x4, x))
, 3: f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, 4: f2^#(x1, x2, S(x'), 0(), S(x)) ->
c_8(f3^#(x1, x2, x', 0(), x))
, 5: f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, 6: f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, 7: f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, 8: f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, 9: f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x)) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2,4,5,7,8,9}. These cover all (indirect) predecessors of
dependency pairs {1,2,3,4,5,6,7,8,9}, 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:
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x)) }
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.
{ f4^#(S(x''), S(x'), x3, x4, S(x)) ->
c_1(f2^#(S(x''), x', x3, x4, x))
, f4^#(S(x'), 0(), x3, x4, S(x)) -> c_3(f3^#(x', 0(), x3, x4, x))
, f2^#(x1, x2, S(x''), S(x'), S(x)) ->
c_6(f5^#(x1, x2, S(x''), x', x))
, f2^#(x1, x2, S(x'), 0(), S(x)) -> c_8(f3^#(x1, x2, x', 0(), x))
, f3^#(x1, x2, x3, x4, S(x)) -> c_11(f4^#(x1, x2, x4, x3, x))
, f5^#(x1, x2, x3, x4, S(x)) -> c_13(f6^#(x2, x1, x3, x4, x))
, f6^#(x1, x2, x3, x4, S(x)) -> c_20(f0^#(x1, x2, x4, x3, x))
, f0^#(x1, S(x'), x3, S(x), x5) ->
c_15(f1^#(x', S(x'), x, S(x), S(x)))
, f1^#(x1, x2, x3, x4, S(x)) -> c_18(f2^#(x2, x1, x3, x4, x)) }
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^1))