We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(nil(), l) -> l
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
[true] = [0]
[false] = [0]
[eq](x1, x2) = [0]
[0] = [0]
[s](x1) = [1] x1 + [0]
[app](x1, x2) = [1] x1 + [1] x2 + [1]
[nil] = [0]
[cons](x1, x2) = [1] x2 + [0]
[mem](x1, x2) = [0]
[ifmem](x1, x2, x3) = [1] x1 + [5]
[inter](x1, x2) = [0]
[ifinter](x1, x2, x3, x4) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[if(true(), x, y)] = [1] x + [1] y + [0]
>= [1] x + [0]
= [x]
[if(false(), x, y)] = [1] x + [1] y + [0]
>= [1] y + [0]
= [y]
[eq(0(), 0())] = [0]
>= [0]
= [true()]
[eq(0(), s(x))] = [0]
>= [0]
= [false()]
[eq(s(x), 0())] = [0]
>= [0]
= [false()]
[eq(s(x), s(y))] = [0]
>= [0]
= [eq(x, y)]
[app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [2]
>= [1] l1 + [1] l2 + [1] l3 + [2]
= [app(l1, app(l2, l3))]
[app(nil(), l)] = [1] l + [1]
> [1] l + [0]
= [l]
[app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [1]
>= [1] l1 + [1] l2 + [1]
= [cons(x, app(l1, l2))]
[mem(x, nil())] = [0]
>= [0]
= [false()]
[mem(x, cons(y, l))] = [0]
? [5]
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = [5]
> [0]
= [true()]
[ifmem(false(), x, l)] = [5]
> [0]
= [mem(x, l)]
[inter(l1, app(l2, l3))] = [0]
? [1]
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = [0]
>= [0]
= [nil()]
[inter(l1, cons(x, l2))] = [0]
? [1]
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = [0]
? [1]
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = [0]
>= [0]
= [nil()]
[inter(cons(x, l1), l2)] = [0]
? [1]
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = [1]
> [0]
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = [1]
> [0]
= [inter(l1, l2)]
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^2)).
Strict Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) }
Weak Trs:
{ app(nil(), l) -> l
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[if](x1, x2, x3) = [1] x2 + [1] x3 + [0]
[true] = [0]
[false] = [4]
[eq](x1, x2) = [4]
[0] = [0]
[s](x1) = [1] x1 + [0]
[app](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[cons](x1, x2) = [1] x2 + [0]
[mem](x1, x2) = [0]
[ifmem](x1, x2, x3) = [1] x1 + [0]
[inter](x1, x2) = [0]
[ifinter](x1, x2, x3, x4) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[if(true(), x, y)] = [1] x + [1] y + [0]
>= [1] x + [0]
= [x]
[if(false(), x, y)] = [1] x + [1] y + [0]
>= [1] y + [0]
= [y]
[eq(0(), 0())] = [4]
> [0]
= [true()]
[eq(0(), s(x))] = [4]
>= [4]
= [false()]
[eq(s(x), 0())] = [4]
>= [4]
= [false()]
[eq(s(x), s(y))] = [4]
>= [4]
= [eq(x, y)]
[app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0]
>= [1] l1 + [1] l2 + [1] l3 + [0]
= [app(l1, app(l2, l3))]
[app(nil(), l)] = [1] l + [0]
>= [1] l + [0]
= [l]
[app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0]
>= [1] l1 + [1] l2 + [0]
= [cons(x, app(l1, l2))]
[mem(x, nil())] = [0]
? [4]
= [false()]
[mem(x, cons(y, l))] = [0]
? [4]
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = [0]
>= [0]
= [true()]
[ifmem(false(), x, l)] = [4]
> [0]
= [mem(x, l)]
[inter(l1, app(l2, l3))] = [0]
>= [0]
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = [0]
>= [0]
= [nil()]
[inter(l1, cons(x, l2))] = [0]
>= [0]
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = [0]
>= [0]
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = [0]
>= [0]
= [nil()]
[inter(cons(x, l1), l2)] = [0]
>= [0]
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = [0]
>= [0]
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = [4]
> [0]
= [inter(l1, l2)]
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^2)).
Strict Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) }
Weak Trs:
{ eq(0(), 0()) -> true()
, app(nil(), l) -> l
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[if](x1, x2, x3) = [1] x2 + [1] x3 + [1]
[true] = [4]
[false] = [4]
[eq](x1, x2) = [4]
[0] = [0]
[s](x1) = [1] x1 + [0]
[app](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[cons](x1, x2) = [1] x2 + [0]
[mem](x1, x2) = [0]
[ifmem](x1, x2, x3) = [1] x1 + [0]
[inter](x1, x2) = [0]
[ifinter](x1, x2, x3, x4) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[if(true(), x, y)] = [1] x + [1] y + [1]
> [1] x + [0]
= [x]
[if(false(), x, y)] = [1] x + [1] y + [1]
> [1] y + [0]
= [y]
[eq(0(), 0())] = [4]
>= [4]
= [true()]
[eq(0(), s(x))] = [4]
>= [4]
= [false()]
[eq(s(x), 0())] = [4]
>= [4]
= [false()]
[eq(s(x), s(y))] = [4]
>= [4]
= [eq(x, y)]
[app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0]
>= [1] l1 + [1] l2 + [1] l3 + [0]
= [app(l1, app(l2, l3))]
[app(nil(), l)] = [1] l + [0]
>= [1] l + [0]
= [l]
[app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0]
>= [1] l1 + [1] l2 + [0]
= [cons(x, app(l1, l2))]
[mem(x, nil())] = [0]
? [4]
= [false()]
[mem(x, cons(y, l))] = [0]
? [4]
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = [4]
>= [4]
= [true()]
[ifmem(false(), x, l)] = [4]
> [0]
= [mem(x, l)]
[inter(l1, app(l2, l3))] = [0]
>= [0]
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = [0]
>= [0]
= [nil()]
[inter(l1, cons(x, l2))] = [0]
>= [0]
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = [0]
>= [0]
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = [0]
>= [0]
= [nil()]
[inter(cons(x, l1), l2)] = [0]
>= [0]
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = [4]
> [0]
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = [4]
> [0]
= [inter(l1, l2)]
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^2)).
Strict Trs:
{ eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) }
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, app(nil(), l) -> l
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[if](x1, x2, x3) = [1] x2 + [1] x3 + [0]
[true] = [4]
[false] = [4]
[eq](x1, x2) = [5]
[0] = [0]
[s](x1) = [1] x1 + [0]
[app](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[cons](x1, x2) = [1] x2 + [0]
[mem](x1, x2) = [0]
[ifmem](x1, x2, x3) = [1] x1 + [0]
[inter](x1, x2) = [0]
[ifinter](x1, x2, x3, x4) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[if(true(), x, y)] = [1] x + [1] y + [0]
>= [1] x + [0]
= [x]
[if(false(), x, y)] = [1] x + [1] y + [0]
>= [1] y + [0]
= [y]
[eq(0(), 0())] = [5]
> [4]
= [true()]
[eq(0(), s(x))] = [5]
> [4]
= [false()]
[eq(s(x), 0())] = [5]
> [4]
= [false()]
[eq(s(x), s(y))] = [5]
>= [5]
= [eq(x, y)]
[app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0]
>= [1] l1 + [1] l2 + [1] l3 + [0]
= [app(l1, app(l2, l3))]
[app(nil(), l)] = [1] l + [0]
>= [1] l + [0]
= [l]
[app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0]
>= [1] l1 + [1] l2 + [0]
= [cons(x, app(l1, l2))]
[mem(x, nil())] = [0]
? [4]
= [false()]
[mem(x, cons(y, l))] = [0]
? [5]
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = [4]
>= [4]
= [true()]
[ifmem(false(), x, l)] = [4]
> [0]
= [mem(x, l)]
[inter(l1, app(l2, l3))] = [0]
>= [0]
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = [0]
>= [0]
= [nil()]
[inter(l1, cons(x, l2))] = [0]
>= [0]
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = [0]
>= [0]
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = [0]
>= [0]
= [nil()]
[inter(cons(x, l1), l2)] = [0]
>= [0]
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = [4]
> [0]
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = [4]
> [0]
= [inter(l1, l2)]
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^2)).
Strict Trs:
{ eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) }
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, app(nil(), l) -> l
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
[true] = [1]
[false] = [1]
[eq](x1, x2) = [1]
[0] = [0]
[s](x1) = [1] x1 + [0]
[app](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[cons](x1, x2) = [1] x2 + [0]
[mem](x1, x2) = [1]
[ifmem](x1, x2, x3) = [1] x1 + [0]
[inter](x1, x2) = [1]
[ifinter](x1, x2, x3, x4) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[if(true(), x, y)] = [1] x + [1] y + [1]
> [1] x + [0]
= [x]
[if(false(), x, y)] = [1] x + [1] y + [1]
> [1] y + [0]
= [y]
[eq(0(), 0())] = [1]
>= [1]
= [true()]
[eq(0(), s(x))] = [1]
>= [1]
= [false()]
[eq(s(x), 0())] = [1]
>= [1]
= [false()]
[eq(s(x), s(y))] = [1]
>= [1]
= [eq(x, y)]
[app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0]
>= [1] l1 + [1] l2 + [1] l3 + [0]
= [app(l1, app(l2, l3))]
[app(nil(), l)] = [1] l + [0]
>= [1] l + [0]
= [l]
[app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0]
>= [1] l1 + [1] l2 + [0]
= [cons(x, app(l1, l2))]
[mem(x, nil())] = [1]
>= [1]
= [false()]
[mem(x, cons(y, l))] = [1]
>= [1]
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = [1]
>= [1]
= [true()]
[ifmem(false(), x, l)] = [1]
>= [1]
= [mem(x, l)]
[inter(l1, app(l2, l3))] = [1]
? [2]
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = [1]
> [0]
= [nil()]
[inter(l1, cons(x, l2))] = [1]
>= [1]
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = [1]
? [2]
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = [1]
> [0]
= [nil()]
[inter(cons(x, l1), l2)] = [1]
>= [1]
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = [1]
>= [1]
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = [1]
>= [1]
= [inter(l1, l2)]
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^2)).
Strict Trs:
{ eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) }
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, app(nil(), l) -> l
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, inter(x, nil()) -> nil()
, inter(nil(), x) -> nil()
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
[true] = [1]
[false] = [5]
[eq](x1, x2) = [5]
[0] = [0]
[s](x1) = [1] x1 + [0]
[app](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[cons](x1, x2) = [1] x2 + [0]
[mem](x1, x2) = [0]
[ifmem](x1, x2, x3) = [1] x1 + [0]
[inter](x1, x2) = [1]
[ifinter](x1, x2, x3, x4) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[if(true(), x, y)] = [1] x + [1] y + [1]
> [1] x + [0]
= [x]
[if(false(), x, y)] = [1] x + [1] y + [5]
> [1] y + [0]
= [y]
[eq(0(), 0())] = [5]
> [1]
= [true()]
[eq(0(), s(x))] = [5]
>= [5]
= [false()]
[eq(s(x), 0())] = [5]
>= [5]
= [false()]
[eq(s(x), s(y))] = [5]
>= [5]
= [eq(x, y)]
[app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0]
>= [1] l1 + [1] l2 + [1] l3 + [0]
= [app(l1, app(l2, l3))]
[app(nil(), l)] = [1] l + [0]
>= [1] l + [0]
= [l]
[app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0]
>= [1] l1 + [1] l2 + [0]
= [cons(x, app(l1, l2))]
[mem(x, nil())] = [0]
? [5]
= [false()]
[mem(x, cons(y, l))] = [0]
? [5]
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = [1]
>= [1]
= [true()]
[ifmem(false(), x, l)] = [5]
> [0]
= [mem(x, l)]
[inter(l1, app(l2, l3))] = [1]
? [2]
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = [1]
> [0]
= [nil()]
[inter(l1, cons(x, l2))] = [1]
> [0]
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = [1]
? [2]
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = [1]
> [0]
= [nil()]
[inter(cons(x, l1), l2)] = [1]
> [0]
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = [1]
>= [1]
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = [5]
> [1]
= [inter(l1, l2)]
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^2)).
Strict Trs:
{ eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) }
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, app(nil(), l) -> l
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs:
{ inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[if](x1, x2, x3) = 2*x2 + 2*x3
[true]() = 0
[false]() = 0
[eq](x1, x2) = 0
[0]() = 0
[s](x1) = 0
[app](x1, x2) = 2 + x1 + x2
[nil]() = 0
[cons](x1, x2) = 2 + x2
[mem](x1, x2) = 0
[ifmem](x1, x2, x3) = 2*x1
[inter](x1, x2) = 2*x1 + x1*x2 + 2*x2
[ifinter](x1, x2, x3, x4) = 3 + x1 + x1*x3 + 2*x3 + x3*x4 + 2*x4
This order satisfies the following ordering constraints.
[if(true(), x, y)] = 2*x + 2*y
>= x
= [x]
[if(false(), x, y)] = 2*x + 2*y
>= y
= [y]
[eq(0(), 0())] =
>=
= [true()]
[eq(0(), s(x))] =
>=
= [false()]
[eq(s(x), 0())] =
>=
= [false()]
[eq(s(x), s(y))] =
>=
= [eq(x, y)]
[app(app(l1, l2), l3)] = 4 + l1 + l2 + l3
>= 4 + l1 + l2 + l3
= [app(l1, app(l2, l3))]
[app(nil(), l)] = 2 + l
> l
= [l]
[app(cons(x, l1), l2)] = 4 + l1 + l2
>= 4 + l1 + l2
= [cons(x, app(l1, l2))]
[mem(x, nil())] =
>=
= [false()]
[mem(x, cons(y, l))] =
>=
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] =
>=
= [true()]
[ifmem(false(), x, l)] =
>=
= [mem(x, l)]
[inter(l1, app(l2, l3))] = 4*l1 + l1*l2 + l1*l3 + 4 + 2*l2 + 2*l3
> 2 + 4*l1 + l1*l2 + 2*l2 + l1*l3 + 2*l3
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = 2*x
>=
= [nil()]
[inter(l1, cons(x, l2))] = 4*l1 + l1*l2 + 4 + 2*l2
> 3 + 2*l2 + l2*l1 + 2*l1
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = 4 + 2*l1 + 2*l2 + 4*l3 + l1*l3 + l2*l3
> 2 + 2*l1 + l1*l3 + 4*l3 + 2*l2 + l2*l3
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = 2*x
>=
= [nil()]
[inter(cons(x, l1), l2)] = 4 + 2*l1 + 4*l2 + l1*l2
> 3 + 2*l1 + l1*l2 + 2*l2
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = 3 + 2*l1 + l1*l2 + 2*l2
> 2 + 2*l1 + l1*l2 + 2*l2
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = 3 + 2*l1 + l1*l2 + 2*l2
> 2*l1 + l1*l2 + 2*l2
= [inter(l1, l2)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) }
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, app(nil(), l) -> l
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs:
{ app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[if](x1, x2, x3) = 2*x2 + 2*x3
[true]() = 1
[false]() = 0
[eq](x1, x2) = 1
[0]() = 0
[s](x1) = 0
[app](x1, x2) = 2*x1 + x2
[nil]() = 0
[cons](x1, x2) = 1 + x2
[mem](x1, x2) = 2*x2
[ifmem](x1, x2, x3) = x1 + 2*x3
[inter](x1, x2) = 2*x1*x2
[ifinter](x1, x2, x3, x4) = x1 + 2*x3*x4
This order satisfies the following ordering constraints.
[if(true(), x, y)] = 2*x + 2*y
>= x
= [x]
[if(false(), x, y)] = 2*x + 2*y
>= y
= [y]
[eq(0(), 0())] = 1
>= 1
= [true()]
[eq(0(), s(x))] = 1
>
= [false()]
[eq(s(x), 0())] = 1
>
= [false()]
[eq(s(x), s(y))] = 1
>= 1
= [eq(x, y)]
[app(app(l1, l2), l3)] = 4*l1 + 2*l2 + l3
>= 2*l1 + 2*l2 + l3
= [app(l1, app(l2, l3))]
[app(nil(), l)] = l
>= l
= [l]
[app(cons(x, l1), l2)] = 2 + 2*l1 + l2
> 1 + 2*l1 + l2
= [cons(x, app(l1, l2))]
[mem(x, nil())] =
>=
= [false()]
[mem(x, cons(y, l))] = 2 + 2*l
> 1 + 2*l
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = 1 + 2*l
>= 1
= [true()]
[ifmem(false(), x, l)] = 2*l
>= 2*l
= [mem(x, l)]
[inter(l1, app(l2, l3))] = 4*l1*l2 + 2*l1*l3
>= 4*l1*l2 + 2*l1*l3
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] =
>=
= [nil()]
[inter(l1, cons(x, l2))] = 2*l1 + 2*l1*l2
>= 2*l1 + 2*l2*l1
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = 4*l1*l3 + 2*l2*l3
>= 4*l1*l3 + 2*l2*l3
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] =
>=
= [nil()]
[inter(cons(x, l1), l2)] = 2*l2 + 2*l1*l2
>= 2*l2 + 2*l1*l2
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = 1 + 2*l1*l2
>= 1 + 2*l1*l2
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = 2*l1*l2
>= 2*l1*l2
= [inter(l1, l2)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, mem(x, nil()) -> false() }
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, app(nil(), l) -> l
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs:
{ eq(s(x), s(y)) -> eq(x, y)
, mem(x, nil()) -> false() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[if](x1, x2, x3) = 2*x2 + 2*x3
[true]() = 1
[false]() = 0
[eq](x1, x2) = 1 + 2*x1
[0]() = 1
[s](x1) = 1 + x1
[app](x1, x2) = 2 + x1 + x2
[nil]() = 2
[cons](x1, x2) = 2 + x1 + x2
[mem](x1, x2) = 2 + 2*x1*x2 + x2
[ifmem](x1, x2, x3) = 2 + 2*x1 + 2*x2*x3 + x3
[inter](x1, x2) = 2 + 2*x1 + 2*x1*x2 + 2*x2
[ifinter](x1, x2, x3, x4) = 3 + x1 + x2 + 2*x3 + 2*x3*x4 + 2*x4
This order satisfies the following ordering constraints.
[if(true(), x, y)] = 2*x + 2*y
>= x
= [x]
[if(false(), x, y)] = 2*x + 2*y
>= y
= [y]
[eq(0(), 0())] = 3
> 1
= [true()]
[eq(0(), s(x))] = 3
>
= [false()]
[eq(s(x), 0())] = 3 + 2*x
>
= [false()]
[eq(s(x), s(y))] = 3 + 2*x
> 1 + 2*x
= [eq(x, y)]
[app(app(l1, l2), l3)] = 4 + l1 + l2 + l3
>= 4 + l1 + l2 + l3
= [app(l1, app(l2, l3))]
[app(nil(), l)] = 4 + l
> l
= [l]
[app(cons(x, l1), l2)] = 4 + x + l1 + l2
>= 4 + x + l1 + l2
= [cons(x, app(l1, l2))]
[mem(x, nil())] = 4 + 4*x
>
= [false()]
[mem(x, cons(y, l))] = 4 + 4*x + 2*x*y + 2*x*l + y + l
>= 4 + 4*x + 2*x*l + l
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] = 4 + 2*x*l + l
> 1
= [true()]
[ifmem(false(), x, l)] = 2 + 2*x*l + l
>= 2 + 2*x*l + l
= [mem(x, l)]
[inter(l1, app(l2, l3))] = 6 + 6*l1 + 2*l1*l2 + 2*l1*l3 + 2*l2 + 2*l3
>= 6 + 4*l1 + 2*l1*l2 + 2*l2 + 2*l1*l3 + 2*l3
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = 6 + 6*x
> 2
= [nil()]
[inter(l1, cons(x, l2))] = 6 + 6*l1 + 2*l1*x + 2*l1*l2 + 2*x + 2*l2
> 5 + 2*x*l1 + 3*l1 + x + 2*l2 + 2*l2*l1
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = 6 + 2*l1 + 2*l2 + 6*l3 + 2*l1*l3 + 2*l2*l3
>= 6 + 2*l1 + 2*l1*l3 + 4*l3 + 2*l2 + 2*l2*l3
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = 6 + 6*x
> 2
= [nil()]
[inter(cons(x, l1), l2)] = 6 + 2*x + 2*l1 + 6*l2 + 2*x*l2 + 2*l1*l2
> 5 + 2*x*l2 + 3*l2 + x + 2*l1 + 2*l1*l2
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = 4 + x + 2*l1 + 2*l1*l2 + 2*l2
>= 4 + x + 2*l1 + 2*l1*l2 + 2*l2
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = 3 + x + 2*l1 + 2*l1*l2 + 2*l2
> 2 + 2*l1 + 2*l1*l2 + 2*l2
= [inter(l1, l2)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs: { app(app(l1, l2), l3) -> app(l1, app(l2, l3)) }
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, app(nil(), l) -> l
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs: { app(app(l1, l2), l3) -> app(l1, app(l2, l3)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1},
Uargs(ifinter) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[if](x1, x2, x3) = 2*x2 + 2*x3
[true]() = 0
[false]() = 0
[eq](x1, x2) = 0
[0]() = 2
[s](x1) = 2 + x1
[app](x1, x2) = 2 + 2*x1 + x2
[nil]() = 0
[cons](x1, x2) = x2
[mem](x1, x2) = 0
[ifmem](x1, x2, x3) = x1 + x1^2
[inter](x1, x2) = 1 + 2*x1 + 2*x1*x2 + 2*x2
[ifinter](x1, x2, x3, x4) = 1 + x1 + x1*x3 + 2*x3 + 2*x3*x4 + 2*x4
This order satisfies the following ordering constraints.
[if(true(), x, y)] = 2*x + 2*y
>= x
= [x]
[if(false(), x, y)] = 2*x + 2*y
>= y
= [y]
[eq(0(), 0())] =
>=
= [true()]
[eq(0(), s(x))] =
>=
= [false()]
[eq(s(x), 0())] =
>=
= [false()]
[eq(s(x), s(y))] =
>=
= [eq(x, y)]
[app(app(l1, l2), l3)] = 6 + 4*l1 + 2*l2 + l3
> 4 + 2*l1 + 2*l2 + l3
= [app(l1, app(l2, l3))]
[app(nil(), l)] = 2 + l
> l
= [l]
[app(cons(x, l1), l2)] = 2 + 2*l1 + l2
>= 2 + 2*l1 + l2
= [cons(x, app(l1, l2))]
[mem(x, nil())] =
>=
= [false()]
[mem(x, cons(y, l))] =
>=
= [ifmem(eq(x, y), x, l)]
[ifmem(true(), x, l)] =
>=
= [true()]
[ifmem(false(), x, l)] =
>=
= [mem(x, l)]
[inter(l1, app(l2, l3))] = 5 + 6*l1 + 4*l1*l2 + 2*l1*l3 + 4*l2 + 2*l3
>= 5 + 6*l1 + 4*l1*l2 + 4*l2 + 2*l1*l3 + 2*l3
= [app(inter(l1, l2), inter(l1, l3))]
[inter(x, nil())] = 1 + 2*x
>
= [nil()]
[inter(l1, cons(x, l2))] = 1 + 2*l1 + 2*l1*l2 + 2*l2
>= 1 + 2*l2 + 2*l2*l1 + 2*l1
= [ifinter(mem(x, l1), x, l2, l1)]
[inter(app(l1, l2), l3)] = 5 + 4*l1 + 2*l2 + 6*l3 + 4*l1*l3 + 2*l2*l3
>= 5 + 4*l1 + 4*l1*l3 + 6*l3 + 2*l2 + 2*l2*l3
= [app(inter(l1, l3), inter(l2, l3))]
[inter(nil(), x)] = 1 + 2*x
>
= [nil()]
[inter(cons(x, l1), l2)] = 1 + 2*l1 + 2*l1*l2 + 2*l2
>= 1 + 2*l1 + 2*l1*l2 + 2*l2
= [ifinter(mem(x, l2), x, l1, l2)]
[ifinter(true(), x, l1, l2)] = 1 + 2*l1 + 2*l1*l2 + 2*l2
>= 1 + 2*l1 + 2*l1*l2 + 2*l2
= [cons(x, inter(l1, l2))]
[ifinter(false(), x, l1, l2)] = 1 + 2*l1 + 2*l1*l2 + 2*l2
>= 1 + 2*l1 + 2*l1*l2 + 2*l2
= [inter(l1, l2)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ if(true(), x, y) -> x
, if(false(), x, y) -> y
, eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, app(app(l1, l2), l3) -> app(l1, app(l2, l3))
, app(nil(), l) -> l
, app(cons(x, l1), l2) -> cons(x, app(l1, l2))
, mem(x, nil()) -> false()
, mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
, ifmem(true(), x, l) -> true()
, ifmem(false(), x, l) -> mem(x, l)
, inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3))
, inter(x, nil()) -> nil()
, inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1)
, inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3))
, inter(nil(), x) -> nil()
, inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2)
, ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))
, ifinter(false(), x, l1, l2) -> inter(l1, l2) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))