We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Arguments of following rules are not normal-forms:
{ e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z) }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We add the following weak dependency pairs:
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e5^#(i(), x, y, z) -> c_14()
, e2^#(x, x, y, z, z) -> c_12()
, e2^#(i(), x, y, z, i()) -> c_13()
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16()
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e5^#(i(), x, y, z) -> c_14()
, e2^#(x, x, y, z, z) -> c_12()
, e2^#(i(), x, y, z, i()) -> c_13()
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16()
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
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)).
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e5^#(i(), x, y, z) -> c_14()
, e2^#(x, x, y, z, z) -> c_12()
, e2^#(i(), x, y, z, i()) -> c_13()
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16()
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_11) = {1},
Uargs(c_15) = {1}, Uargs(c_18) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[i] = [0]
[1]
[f1^#] = [1]
[0]
[c_1](x1) = [1
0] x1 + [0]
[0
1] [0]
[g1^#] = [1]
[1]
[c_2](x1) = [1
0] x1 + [0]
[0
1] [0]
[g2^#] = [1]
[1]
[c_3](x1) = [1
0] x1 + [0]
[0
1] [1]
[h1^#] = [1]
[1]
[c_4](x1) = [1
0] x1 + [0]
[0
1] [0]
[h2^#] = [1]
[1]
[c_5](x1) = [1
0] x1 + [1]
[0
1] [0]
[c_6](x1) = [1
0] x1 + [0]
[0
1] [1]
[f2^#] = [0]
[0]
[c_7](x1) = [1
0] x1 + [0]
[0
1] [0]
[c_8](x1) = [1
0] x1 + [1]
[0
1] [1]
[c_9] = [0]
[0]
[c_10] = [0]
[0]
[e1^#](x1, x2, x3, x4, x5) = [2
2] x1 + [0 0] x2 + [2 2] x3 + [1 1] x4 + [2
0] x5 + [0]
[1
0] [1 0] [1 1] [2 2] [2
1] [2]
[c_11](x1) = [1
0] x1 + [0]
[0
1] [0]
[e5^#](x1, x2, x3, x4) = [0]
[1]
[e2^#](x1, x2, x3, x4, x5) = [0]
[0]
[c_12] = [0]
[0]
[c_13] = [0]
[0]
[c_14] = [0]
[0]
[e3^#](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [2
2] x1 + [2 2] x2 + [2 2] x3 + [2 2] x4 + [2
2] x5 + [2
2] x6 + [2
2] x7 + [2
2] x8 + [2
1] x9 + [2
1] x10 + [2
2] x11 + [1]
[1
0] [1 0] [1 0] [1 0] [0
1] [0
1] [1
1] [1
1] [1
2] [1
2] [2
1] [1]
[c_15](x1) = [1
0] x1 + [0]
[0
1] [0]
[e4^#](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [2
2] x4 + [1 0] x9 + [0 1] x10 + [2
2] x11 + [0]
[0
0] [0 0] [0 0] [0
0] [0]
[c_16] = [0]
[0]
[c_17] = [0]
[0]
[c_18](x1) = [1
0] x1 + [0]
[0
1] [0]
The order satisfies the following ordering constraints:
[f1^#()] = [1]
[0]
? [1]
[1]
= [c_1(g1^#())]
[f1^#()] = [1]
[0]
? [1]
[1]
= [c_2(g2^#())]
[g1^#()] = [1]
[1]
? [1]
[2]
= [c_3(h1^#())]
[g1^#()] = [1]
[1]
>= [1]
[1]
= [c_4(h2^#())]
[g2^#()] = [1]
[1]
? [2]
[1]
= [c_5(h1^#())]
[g2^#()] = [1]
[1]
? [1]
[2]
= [c_6(h2^#())]
[h1^#()] = [1]
[1]
> [0]
[0]
= [c_9()]
[h2^#()] = [1]
[1]
> [0]
[0]
= [c_10()]
[f2^#()] = [0]
[0]
? [1]
[1]
= [c_7(g1^#())]
[f2^#()] = [0]
[0]
? [2]
[2]
= [c_8(g2^#())]
[e1^#(x1, x1, x, y, z)] = [2 2] x + [1 1] y + [2 0] z + [2 2] x1 + [0]
[1 1] [2 2] [2 1] [2 0] [2]
>= [0]
[1]
= [c_11(e5^#(x1, x, y, z))]
[e5^#(i(), x, y, z)] = [0]
[1]
>= [0]
[0]
= [c_14()]
[e2^#(x, x, y, z, z)] = [0]
[0]
>= [0]
[0]
= [c_12()]
[e2^#(i(), x, y, z, i())] = [0]
[0]
>= [0]
[0]
= [c_13()]
[e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)] = [2 1] x + [2 1] y + [2 2] z + [4 4] x1 + [4 4] x2 + [4 4] x3 + [4
4] x4 + [1]
[1 2] [1 2] [2 1] [2 0] [2 0] [0 2] [2
2] [1]
> [1 0] x + [0 1] y + [2 2] z + [2 2] x2 + [0]
[0 0] [0 0] [0 0] [0 0] [0]
= [c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))]
[e3^#(x, y, x, y, y, z, y, z, x, y, z)] = [6 5] x + [10 9] y + [6 6] z + [1]
[3 2] [ 4 4] [3 3] [1]
> [0]
[0]
= [c_16()]
[e4^#(x, x, x, x, x, x, x, x, x, x, x)] = [5 5] x + [0]
[0 0] [0]
>= [0]
[0]
= [c_17()]
[e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z)] = [1 0] x + [0 1] y + [2 2] z + [2 2] x1 + [0]
[0 0] [0 0] [0 0] [0 0] [0]
? [0]
[1]
= [c_18(e5^#(x1, x, y, z))]
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(1)).
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e5^#(i(), x, y, z) -> c_14()
, e2^#(x, x, y, z, z) -> c_12()
, e2^#(i(), x, y, z, i()) -> c_13()
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
Weak DPs:
{ h1^#() -> c_9()
, h2^#() -> c_10()
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {3,4,5,6,10,11,12} by
applications of Pre({3,4,5,6,10,11,12}) = {1,2,7,8,9,14}. Here
rules are labeled as follows:
DPs:
{ 1: f1^#() -> c_1(g1^#())
, 2: f1^#() -> c_2(g2^#())
, 3: g1^#() -> c_3(h1^#())
, 4: g1^#() -> c_4(h2^#())
, 5: g2^#() -> c_5(h1^#())
, 6: g2^#() -> c_6(h2^#())
, 7: f2^#() -> c_7(g1^#())
, 8: f2^#() -> c_8(g2^#())
, 9: e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, 10: e5^#(i(), x, y, z) -> c_14()
, 11: e2^#(x, x, y, z, z) -> c_12()
, 12: e2^#(i(), x, y, z, i()) -> c_13()
, 13: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, 14: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z))
, 15: h1^#() -> c_9()
, 16: h2^#() -> c_10()
, 17: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, 18: e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
Weak DPs:
{ g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, e5^#(i(), x, y, z) -> c_14()
, e2^#(x, x, y, z, z) -> c_12()
, e2^#(i(), x, y, z, i()) -> c_13()
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {1,2,3,4,5} by
applications of Pre({1,2,3,4,5}) = {}. Here rules are labeled as
follows:
DPs:
{ 1: f1^#() -> c_1(g1^#())
, 2: f1^#() -> c_2(g2^#())
, 3: f2^#() -> c_7(g1^#())
, 4: f2^#() -> c_8(g2^#())
, 5: e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, 6: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, 7: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z))
, 8: g1^#() -> c_3(h1^#())
, 9: g1^#() -> c_4(h2^#())
, 10: g2^#() -> c_5(h1^#())
, 11: g2^#() -> c_6(h2^#())
, 12: h1^#() -> c_9()
, 13: h2^#() -> c_10()
, 14: e5^#(i(), x, y, z) -> c_14()
, 15: e2^#(x, x, y, z, z) -> c_12()
, 16: e2^#(i(), x, y, z, i()) -> c_13()
, 17: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, 18: e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
Weak DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e5^#(i(), x, y, z) -> c_14()
, e2^#(x, x, y, z, z) -> c_12()
, e2^#(i(), x, y, z, i()) -> c_13()
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() }
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.
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e5^#(i(), x, y, z) -> c_14()
, e2^#(x, x, y, z, z) -> c_12()
, e2^#(i(), x, y, z, i()) -> c_13()
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_16() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_17()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
Weak DPs:
{ e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_15(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) }
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:
{ e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_18(e5^#(x1, x, y, z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_1()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_2() }
Weak DPs:
{ e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_3(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Consider the dependency graph
1: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_1()
2: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_2()
3: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_3(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
-->_1 e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_2() :2
-->_1 e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_1() :1
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).
{ e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_3(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_1()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_2() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Consider the dependency graph
1: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_1()
2: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_2()
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).
{ e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_1()
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) -> c_2() }
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(1))