YES(O(1),O(n^2)) 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: innermost 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] = [0] [eq](x1, x2) = [0] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [1] [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 following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} 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 + [0] >= [1] l1 + [1] l2 + [1] l3 + [0] = [app(l1, app(l2, l3))] [app(nil(), l)] = [1] l + [1] > [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] >= [0] = [false()] [mem(x, cons(y, l))] = [0] >= [0] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [0] >= [0] = [true()] [ifmem(false(), x, l)] = [0] >= [0] = [mem(x, l)] [inter(l1, app(l2, l3))] = [0] >= [0] = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = [0] ? [1] = [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] ? [1] = [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)] = [0] >= [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) , 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) } Weak Trs: { app(nil(), l) -> l } Obligation: innermost 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] = [0] [false] = [0] [eq](x1, x2) = [0] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [7] [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 following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} 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())] = [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 + [0] >= [1] l1 + [1] l2 + [1] l3 + [0] = [app(l1, app(l2, l3))] [app(nil(), l)] = [1] l + [7] > [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] >= [0] = [false()] [mem(x, cons(y, l))] = [0] >= [0] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [0] >= [0] = [true()] [ifmem(false(), x, l)] = [0] >= [0] = [mem(x, l)] [inter(l1, app(l2, l3))] = [0] >= [0] = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = [0] ? [7] = [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] ? [7] = [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)] = [0] >= [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(), 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) , 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) } Weak Trs: { if(true(), x, y) -> x , if(false(), x, y) -> y , app(nil(), l) -> l } Obligation: innermost 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 + [7] [true] = [0] [false] = [0] [eq](x1, x2) = [4] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [7] [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 following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} The order satisfies the following ordering constraints: [if(true(), x, y)] = [1] x + [1] y + [7] > [1] x + [0] = [x] [if(false(), x, y)] = [1] x + [1] y + [7] > [1] y + [0] = [y] [eq(0(), 0())] = [4] > [0] = [true()] [eq(0(), s(x))] = [4] > [0] = [false()] [eq(s(x), 0())] = [4] > [0] = [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 + [7] > [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] >= [0] = [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)] = [0] >= [0] = [mem(x, l)] [inter(l1, app(l2, l3))] = [0] >= [0] = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = [0] ? [7] = [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] ? [7] = [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)] = [0] >= [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) , 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) } 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 } Obligation: innermost 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 + [7] [true] = [0] [false] = [0] [eq](x1, x2) = [4] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [7] [cons](x1, x2) = [1] x2 + [0] [mem](x1, x2) = [4] [ifmem](x1, x2, x3) = [1] x1 + [0] [inter](x1, x2) = [0] [ifinter](x1, x2, x3, x4) = [1] x1 + [0] The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} The order satisfies the following ordering constraints: [if(true(), x, y)] = [1] x + [1] y + [7] > [1] x + [0] = [x] [if(false(), x, y)] = [1] x + [1] y + [7] > [1] y + [0] = [y] [eq(0(), 0())] = [4] > [0] = [true()] [eq(0(), s(x))] = [4] > [0] = [false()] [eq(s(x), 0())] = [4] > [0] = [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 + [7] > [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())] = [4] > [0] = [false()] [mem(x, cons(y, l))] = [4] >= [4] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [0] >= [0] = [true()] [ifmem(false(), x, l)] = [0] ? [4] = [mem(x, l)] [inter(l1, app(l2, l3))] = [0] >= [0] = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = [0] ? [7] = [nil()] [inter(l1, cons(x, l2))] = [0] ? [4] = [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] ? [7] = [nil()] [inter(cons(x, l1), l2)] = [0] ? [4] = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = [0] >= [0] = [cons(x, inter(l1, l2))] [ifinter(false(), x, l1, l2)] = [0] >= [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, 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) } 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 , mem(x, nil()) -> false() } Obligation: innermost 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 + [7] [true] = [0] [false] = [0] [eq](x1, x2) = [4] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [7] [cons](x1, x2) = [1] x2 + [0] [mem](x1, x2) = [6] [ifmem](x1, x2, x3) = [1] x1 + [0] [inter](x1, x2) = [0] [ifinter](x1, x2, x3, x4) = [1] x1 + [0] The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} The order satisfies the following ordering constraints: [if(true(), x, y)] = [1] x + [1] y + [7] > [1] x + [0] = [x] [if(false(), x, y)] = [1] x + [1] y + [7] > [1] y + [0] = [y] [eq(0(), 0())] = [4] > [0] = [true()] [eq(0(), s(x))] = [4] > [0] = [false()] [eq(s(x), 0())] = [4] > [0] = [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 + [7] > [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())] = [6] > [0] = [false()] [mem(x, cons(y, l))] = [6] > [4] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [0] >= [0] = [true()] [ifmem(false(), x, l)] = [0] ? [6] = [mem(x, l)] [inter(l1, app(l2, l3))] = [0] >= [0] = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = [0] ? [7] = [nil()] [inter(l1, cons(x, l2))] = [0] ? [6] = [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] ? [7] = [nil()] [inter(cons(x, l1), l2)] = [0] ? [6] = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = [0] >= [0] = [cons(x, inter(l1, l2))] [ifinter(false(), x, l1, l2)] = [0] >= [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)) , 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) } 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 , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) } Obligation: innermost 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 + [5] [true] = [1] [false] = [0] [eq](x1, x2) = [1] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [7] [cons](x1, x2) = [1] x2 + [0] [mem](x1, x2) = [4] [ifmem](x1, x2, x3) = [1] x1 + [0] [inter](x1, x2) = [0] [ifinter](x1, x2, x3, x4) = [1] x1 + [0] The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} The order satisfies the following ordering constraints: [if(true(), x, y)] = [1] x + [1] y + [6] > [1] x + [0] = [x] [if(false(), x, y)] = [1] x + [1] y + [5] > [1] y + [0] = [y] [eq(0(), 0())] = [1] >= [1] = [true()] [eq(0(), s(x))] = [1] > [0] = [false()] [eq(s(x), 0())] = [1] > [0] = [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 + [7] > [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())] = [4] > [0] = [false()] [mem(x, cons(y, l))] = [4] > [1] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [1] >= [1] = [true()] [ifmem(false(), x, l)] = [0] ? [4] = [mem(x, l)] [inter(l1, app(l2, l3))] = [0] >= [0] = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = [0] ? [7] = [nil()] [inter(l1, cons(x, l2))] = [0] ? [4] = [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] ? [7] = [nil()] [inter(cons(x, l1), l2)] = [0] ? [4] = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = [1] > [0] = [cons(x, inter(l1, l2))] [ifinter(false(), x, l1, l2)] = [0] >= [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)) , 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(false(), x, l1, l2) -> inter(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 , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) } Obligation: innermost 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 + [7] [true] = [1] [false] = [0] [eq](x1, x2) = [1] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [cons](x1, x2) = [1] x2 + [0] [mem](x1, x2) = [4] [ifmem](x1, x2, x3) = [1] x1 + [0] [inter](x1, x2) = [1] [ifinter](x1, x2, x3, x4) = [1] x1 + [0] The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} The order satisfies the following ordering constraints: [if(true(), x, y)] = [1] x + [1] y + [8] > [1] x + [0] = [x] [if(false(), x, y)] = [1] x + [1] y + [7] > [1] y + [0] = [y] [eq(0(), 0())] = [1] >= [1] = [true()] [eq(0(), s(x))] = [1] > [0] = [false()] [eq(s(x), 0())] = [1] > [0] = [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())] = [4] > [0] = [false()] [mem(x, cons(y, l))] = [4] > [1] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [1] >= [1] = [true()] [ifmem(false(), x, l)] = [0] ? [4] = [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] ? [4] = [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] ? [4] = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = [1] >= [1] = [cons(x, inter(l1, l2))] [ifinter(false(), x, l1, l2)] = [0] ? [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)) , 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(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) , ifinter(false(), x, l1, l2) -> inter(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 , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) , inter(x, nil()) -> nil() , inter(nil(), x) -> nil() , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) } Obligation: innermost 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 + [7] [true] = [4] [false] = [1] [eq](x1, x2) = [4] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [cons](x1, x2) = [1] x2 + [0] [mem](x1, x2) = [4] [ifmem](x1, x2, x3) = [1] x1 + [0] [inter](x1, x2) = [0] [ifinter](x1, x2, x3, x4) = [1] x1 + [0] The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} The order satisfies the following ordering constraints: [if(true(), x, y)] = [1] x + [1] y + [11] > [1] x + [0] = [x] [if(false(), x, y)] = [1] x + [1] y + [8] > [1] y + [0] = [y] [eq(0(), 0())] = [4] >= [4] = [true()] [eq(0(), s(x))] = [4] > [1] = [false()] [eq(s(x), 0())] = [4] > [1] = [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())] = [4] > [1] = [false()] [mem(x, cons(y, l))] = [4] >= [4] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [4] >= [4] = [true()] [ifmem(false(), x, l)] = [1] ? [4] = [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] ? [4] = [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] ? [4] = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = [4] > [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: { 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)) , 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(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 , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> ifmem(eq(x, y), 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: innermost 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 + [7] [true] = [0] [false] = [0] [eq](x1, x2) = [0] [0] = [7] [s](x1) = [1] x1 + [7] [app](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [cons](x1, x2) = [1] x2 + [0] [mem](x1, x2) = [4] [ifmem](x1, x2, x3) = [1] x1 + [1] [inter](x1, x2) = [0] [ifinter](x1, x2, x3, x4) = [1] x1 + [4] The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} The order satisfies the following ordering constraints: [if(true(), x, y)] = [1] x + [1] y + [7] > [1] x + [0] = [x] [if(false(), x, y)] = [1] x + [1] y + [7] > [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 + [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())] = [4] > [0] = [false()] [mem(x, cons(y, l))] = [4] > [1] = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = [1] > [0] = [true()] [ifmem(false(), x, l)] = [1] ? [4] = [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] ? [8] = [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] ? [8] = [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)) , ifmem(false(), x, l) -> mem(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 , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) , ifmem(true(), x, l) -> true() , 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: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { 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) } 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) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*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 + 2*x1*x2 + 2*x2 [ifinter](x1, x2, x3, x4) = 2 + x1 + 2*x3 + 2*x3*x4 + 2*x4 The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} This order satisfies the following ordering constraints. [if(true(), x, y)] = 3 + 3*x + 3*y > x = [x] [if(false(), x, y)] = 3 + 3*x + 3*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))] = 6*l1 + 2*l1*l2 + 2*l1*l3 + 4 + 2*l2 + 2*l3 > 2 + 4*l1 + 2*l1*l2 + 2*l2 + 2*l1*l3 + 2*l3 = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = 2*x >= = [nil()] [inter(l1, cons(x, l2))] = 6*l1 + 2*l1*l2 + 4 + 2*l2 > 2 + 2*l2 + 2*l2*l1 + 2*l1 = [ifinter(mem(x, l1), x, l2, l1)] [inter(app(l1, l2), l3)] = 4 + 2*l1 + 2*l2 + 6*l3 + 2*l1*l3 + 2*l2*l3 > 2 + 2*l1 + 2*l1*l3 + 4*l3 + 2*l2 + 2*l2*l3 = [app(inter(l1, l3), inter(l2, l3))] [inter(nil(), x)] = 2*x >= = [nil()] [inter(cons(x, l1), l2)] = 4 + 2*l1 + 6*l2 + 2*l1*l2 > 2 + 2*l1 + 2*l1*l2 + 2*l2 = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = 2 + 2*l1 + 2*l1*l2 + 2*l2 >= 2 + 2*l1 + 2*l1*l2 + 2*l2 = [cons(x, inter(l1, l2))] [ifinter(false(), x, l1, l2)] = 2 + 2*l1 + 2*l1*l2 + 2*l2 > 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: { 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)) , ifmem(false(), x, l) -> mem(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 , mem(x, nil()) -> false() , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) , ifmem(true(), x, l) -> true() , 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: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { ifmem(false(), x, l) -> mem(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) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 [true]() = 1 [false]() = 0 [eq](x1, x2) = 1 [0]() = 0 [s](x1) = 0 [app](x1, x2) = x1 + x2 [nil]() = 0 [cons](x1, x2) = 2 + x2 [mem](x1, x2) = 2*x2 [ifmem](x1, x2, x3) = 2 + 2*x1 + 2*x3 [inter](x1, x2) = 2*x1*x2 [ifinter](x1, x2, x3, x4) = 2*x1 + 2*x3*x4 The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} This order satisfies the following ordering constraints. [if(true(), x, y)] = 3 + 6*x + 6*y > x = [x] [if(false(), x, y)] = 3 + 3*x + 3*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)] = l1 + l2 + l3 >= l1 + l2 + l3 = [app(l1, app(l2, l3))] [app(nil(), l)] = l >= l = [l] [app(cons(x, l1), l2)] = 2 + l1 + l2 >= 2 + l1 + l2 = [cons(x, app(l1, l2))] [mem(x, nil())] = >= = [false()] [mem(x, cons(y, l))] = 4 + 2*l >= 4 + 2*l = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = 4 + 2*l > 1 = [true()] [ifmem(false(), x, l)] = 2 + 2*l > 2*l = [mem(x, l)] [inter(l1, app(l2, l3))] = 2*l1*l2 + 2*l1*l3 >= 2*l1*l2 + 2*l1*l3 = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = >= = [nil()] [inter(l1, cons(x, l2))] = 4*l1 + 2*l1*l2 >= 4*l1 + 2*l2*l1 = [ifinter(mem(x, l1), x, l2, l1)] [inter(app(l1, l2), l3)] = 2*l1*l3 + 2*l2*l3 >= 2*l1*l3 + 2*l2*l3 = [app(inter(l1, l3), inter(l2, l3))] [inter(nil(), x)] = >= = [nil()] [inter(cons(x, l1), l2)] = 4*l2 + 2*l1*l2 >= 4*l2 + 2*l1*l2 = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = 2 + 2*l1*l2 >= 2 + 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)) , app(cons(x, l1), l2) -> cons(x, app(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 , 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: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { app(cons(x, l1), l2) -> cons(x, app(l1, l2)) } 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) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*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) = 2 + x2 [mem](x1, x2) = 2*x2 [ifmem](x1, x2, x3) = 1 + x1 + 2*x3 [inter](x1, x2) = 2*x1*x2 [ifinter](x1, x2, x3, x4) = 2*x1 + 2*x3*x4 The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} This order satisfies the following ordering constraints. [if(true(), x, y)] = 3 + 6*x + 6*y > x = [x] [if(false(), x, y)] = 3 + 3*x + 3*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)] = 4 + 2*l1 + l2 > 2 + 2*l1 + l2 = [cons(x, app(l1, l2))] [mem(x, nil())] = >= = [false()] [mem(x, cons(y, l))] = 4 + 2*l > 2 + 2*l = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = 2 + 2*l > 1 = [true()] [ifmem(false(), x, l)] = 1 + 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))] = 4*l1 + 2*l1*l2 >= 4*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)] = 4*l2 + 2*l1*l2 >= 4*l2 + 2*l1*l2 = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = 2 + 2*l1*l2 >= 2 + 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)) } 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, 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: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor '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) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 [true]() = 0 [false]() = 0 [eq](x1, x2) = 0 [0]() = 0 [s](x1) = 0 [app](x1, x2) = 2 + 2*x1 + x2 [nil]() = 0 [cons](x1, x2) = x2 [mem](x1, x2) = 0 [ifmem](x1, x2, x3) = 2*x1 [inter](x1, x2) = 1 + 2*x1 + 2*x1*x2 + 2*x2 [ifinter](x1, x2, x3, x4) = 1 + 2*x1 + 2*x3 + 2*x3*x4 + 2*x4 The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} This order satisfies the following ordering constraints. [if(true(), x, y)] = 3 + 3*x + 3*y > x = [x] [if(false(), x, y)] = 3 + 3*x + 3*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(n^2)). Strict Trs: { eq(s(x), s(y)) -> eq(x, y) } 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(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: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { eq(s(x), s(y)) -> eq(x, y) } 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) = 3 + x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 [true]() = 2 [false]() = 0 [eq](x1, x2) = 2 + x2 [0]() = 0 [s](x1) = 1 + x1 [app](x1, x2) = 2 + 2*x1 + x2 [nil]() = 0 [cons](x1, x2) = 2 + x1 + x2 [mem](x1, x2) = 2*x1*x2 + x2 [ifmem](x1, x2, x3) = x1 + 2*x2*x3 + x3 [inter](x1, x2) = x1 + 2*x1*x2 + 2*x2 [ifinter](x1, x2, x3, x4) = x1 + x2 + x3 + 2*x3*x4 + 2*x4 The following symbols are considered usable {if, eq, app, mem, ifmem, inter, ifinter} This order satisfies the following ordering constraints. [if(true(), x, y)] = 3 + 5*x + 9*y > x = [x] [if(false(), x, y)] = 3 + 3*x + 3*y > y = [y] [eq(0(), 0())] = 2 >= 2 = [true()] [eq(0(), s(x))] = 3 + x > = [false()] [eq(s(x), 0())] = 2 > = [false()] [eq(s(x), s(y))] = 3 + y > 2 + 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)] = 6 + 2*x + 2*l1 + l2 > 4 + x + 2*l1 + l2 = [cons(x, app(l1, l2))] [mem(x, nil())] = >= = [false()] [mem(x, cons(y, l))] = 4*x + 2*x*y + 2*x*l + 2 + y + l >= 2 + y + 2*x*l + l = [ifmem(eq(x, y), x, l)] [ifmem(true(), x, l)] = 2 + 2*x*l + l >= 2 = [true()] [ifmem(false(), x, l)] = 2*x*l + l >= 2*x*l + l = [mem(x, l)] [inter(l1, app(l2, l3))] = 5*l1 + 4*l1*l2 + 2*l1*l3 + 4 + 4*l2 + 2*l3 > 2 + 3*l1 + 4*l1*l2 + 4*l2 + 2*l1*l3 + 2*l3 = [app(inter(l1, l2), inter(l1, l3))] [inter(x, nil())] = x >= = [nil()] [inter(l1, cons(x, l2))] = 5*l1 + 2*l1*x + 2*l1*l2 + 4 + 2*x + 2*l2 > 2*x*l1 + 3*l1 + x + l2 + 2*l2*l1 = [ifinter(mem(x, l1), x, l2, l1)] [inter(app(l1, l2), l3)] = 2 + 2*l1 + l2 + 6*l3 + 4*l1*l3 + 2*l2*l3 >= 2 + 2*l1 + 4*l1*l3 + 6*l3 + l2 + 2*l2*l3 = [app(inter(l1, l3), inter(l2, l3))] [inter(nil(), x)] = 2*x >= = [nil()] [inter(cons(x, l1), l2)] = 2 + x + l1 + 6*l2 + 2*x*l2 + 2*l1*l2 > 2*x*l2 + 3*l2 + x + l1 + 2*l1*l2 = [ifinter(mem(x, l2), x, l1, l2)] [ifinter(true(), x, l1, l2)] = 2 + x + l1 + 2*l1*l2 + 2*l2 >= 2 + x + l1 + 2*l1*l2 + 2*l2 = [cons(x, inter(l1, l2))] [ifinter(false(), x, l1, l2)] = x + l1 + 2*l1*l2 + 2*l2 >= 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: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))