YES(O(1),O(n^2)) 655.53/297.53 YES(O(1),O(n^2)) 655.53/297.53 655.53/297.53 We are left with following problem, upon which TcT provides the 655.53/297.53 certificate YES(O(1),O(n^2)). 655.53/297.53 655.53/297.53 Strict Trs: 655.53/297.53 { if(true(), x, y) -> x 655.53/297.53 , if(false(), x, y) -> y 655.53/297.53 , eq(0(), 0()) -> true() 655.53/297.53 , eq(0(), s(x)) -> false() 655.53/297.53 , eq(s(x), 0()) -> false() 655.53/297.53 , eq(s(x), s(y)) -> eq(x, y) 655.53/297.53 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.53 , app(nil(), l) -> l 655.53/297.53 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.53 , mem(x, nil()) -> false() 655.53/297.53 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.53 , ifmem(true(), x, l) -> true() 655.53/297.53 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.53 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.53 , inter(x, nil()) -> nil() 655.53/297.53 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.53 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.53 , inter(nil(), x) -> nil() 655.53/297.53 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.53 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.53 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.53 Obligation: 655.53/297.53 innermost runtime complexity 655.53/297.53 Answer: 655.53/297.53 YES(O(1),O(n^2)) 655.53/297.53 655.53/297.53 The weightgap principle applies (using the following nonconstant 655.53/297.53 growth matrix-interpretation) 655.53/297.53 655.53/297.53 The following argument positions are usable: 655.53/297.53 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.53 Uargs(ifinter) = {1} 655.53/297.53 655.53/297.53 TcT has computed the following matrix interpretation satisfying 655.53/297.53 not(EDA) and not(IDA(1)). 655.53/297.53 655.53/297.53 [if](x1, x2, x3) = [1] x2 + [1] x3 + [0] 655.53/297.53 655.53/297.53 [true] = [0] 655.53/297.53 655.53/297.53 [false] = [0] 655.53/297.53 655.53/297.53 [eq](x1, x2) = [0] 655.53/297.53 655.53/297.53 [0] = [7] 655.53/297.53 655.53/297.53 [s](x1) = [1] x1 + [7] 655.53/297.53 655.53/297.53 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.53 655.53/297.53 [nil] = [1] 655.53/297.53 655.53/297.53 [cons](x1, x2) = [1] x2 + [0] 655.53/297.53 655.53/297.53 [mem](x1, x2) = [0] 655.53/297.53 655.53/297.53 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.53 655.53/297.53 [inter](x1, x2) = [0] 655.53/297.53 655.53/297.53 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.53 655.53/297.53 The order satisfies the following ordering constraints: 655.53/297.53 655.53/297.53 [if(true(), x, y)] = [1] x + [1] y + [0] 655.53/297.53 >= [1] x + [0] 655.53/297.53 = [x] 655.53/297.53 655.53/297.53 [if(false(), x, y)] = [1] x + [1] y + [0] 655.53/297.53 >= [1] y + [0] 655.53/297.53 = [y] 655.53/297.53 655.53/297.53 [eq(0(), 0())] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [true()] 655.53/297.53 655.53/297.53 [eq(0(), s(x))] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [false()] 655.53/297.53 655.53/297.53 [eq(s(x), 0())] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [false()] 655.53/297.53 655.53/297.53 [eq(s(x), s(y))] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [eq(x, y)] 655.53/297.53 655.53/297.53 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.53 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.53 = [app(l1, app(l2, l3))] 655.53/297.53 655.53/297.53 [app(nil(), l)] = [1] l + [1] 655.53/297.53 > [1] l + [0] 655.53/297.53 = [l] 655.53/297.53 655.53/297.53 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.53 >= [1] l1 + [1] l2 + [0] 655.53/297.53 = [cons(x, app(l1, l2))] 655.53/297.53 655.53/297.53 [mem(x, nil())] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [false()] 655.53/297.53 655.53/297.53 [mem(x, cons(y, l))] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [ifmem(eq(x, y), x, l)] 655.53/297.53 655.53/297.53 [ifmem(true(), x, l)] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [true()] 655.53/297.53 655.53/297.53 [ifmem(false(), x, l)] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [mem(x, l)] 655.53/297.53 655.53/297.53 [inter(l1, app(l2, l3))] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.53 655.53/297.53 [inter(x, nil())] = [0] 655.53/297.53 ? [1] 655.53/297.53 = [nil()] 655.53/297.53 655.53/297.53 [inter(l1, cons(x, l2))] = [0] 655.53/297.53 >= [0] 655.53/297.53 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.54 655.53/297.54 [inter(app(l1, l2), l3)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.54 655.53/297.54 [inter(nil(), x)] = [0] 655.53/297.54 ? [1] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(cons(x, l1), l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.54 655.53/297.54 [ifinter(true(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [cons(x, inter(l1, l2))] 655.53/297.54 655.53/297.54 [ifinter(false(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [inter(l1, l2)] 655.53/297.54 655.53/297.54 655.53/297.54 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.54 655.53/297.54 We are left with following problem, upon which TcT provides the 655.53/297.54 certificate YES(O(1),O(n^2)). 655.53/297.54 655.53/297.54 Strict Trs: 655.53/297.54 { if(true(), x, y) -> x 655.53/297.54 , if(false(), x, y) -> y 655.53/297.54 , eq(0(), 0()) -> true() 655.53/297.54 , eq(0(), s(x)) -> false() 655.53/297.54 , eq(s(x), 0()) -> false() 655.53/297.54 , eq(s(x), s(y)) -> eq(x, y) 655.53/297.54 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.54 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.54 , mem(x, nil()) -> false() 655.53/297.54 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.54 , ifmem(true(), x, l) -> true() 655.53/297.54 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.54 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.54 , inter(x, nil()) -> nil() 655.53/297.54 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.54 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.54 , inter(nil(), x) -> nil() 655.53/297.54 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.54 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.54 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.54 Weak Trs: { app(nil(), l) -> l } 655.53/297.54 Obligation: 655.53/297.54 innermost runtime complexity 655.53/297.54 Answer: 655.53/297.54 YES(O(1),O(n^2)) 655.53/297.54 655.53/297.54 The weightgap principle applies (using the following nonconstant 655.53/297.54 growth matrix-interpretation) 655.53/297.54 655.53/297.54 The following argument positions are usable: 655.53/297.54 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.54 Uargs(ifinter) = {1} 655.53/297.54 655.53/297.54 TcT has computed the following matrix interpretation satisfying 655.53/297.54 not(EDA) and not(IDA(1)). 655.53/297.54 655.53/297.54 [if](x1, x2, x3) = [1] x2 + [1] x3 + [1] 655.53/297.54 655.53/297.54 [true] = [0] 655.53/297.54 655.53/297.54 [false] = [0] 655.53/297.54 655.53/297.54 [eq](x1, x2) = [0] 655.53/297.54 655.53/297.54 [0] = [7] 655.53/297.54 655.53/297.54 [s](x1) = [1] x1 + [7] 655.53/297.54 655.53/297.54 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.54 655.53/297.54 [nil] = [7] 655.53/297.54 655.53/297.54 [cons](x1, x2) = [1] x2 + [0] 655.53/297.54 655.53/297.54 [mem](x1, x2) = [0] 655.53/297.54 655.53/297.54 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.54 655.53/297.54 [inter](x1, x2) = [0] 655.53/297.54 655.53/297.54 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.54 655.53/297.54 The order satisfies the following ordering constraints: 655.53/297.54 655.53/297.54 [if(true(), x, y)] = [1] x + [1] y + [1] 655.53/297.54 > [1] x + [0] 655.53/297.54 = [x] 655.53/297.54 655.53/297.54 [if(false(), x, y)] = [1] x + [1] y + [1] 655.53/297.54 > [1] y + [0] 655.53/297.54 = [y] 655.53/297.54 655.53/297.54 [eq(0(), 0())] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [eq(0(), s(x))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), 0())] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), s(y))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [eq(x, y)] 655.53/297.54 655.53/297.54 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 = [app(l1, app(l2, l3))] 655.53/297.54 655.53/297.54 [app(nil(), l)] = [1] l + [7] 655.53/297.54 > [1] l + [0] 655.53/297.54 = [l] 655.53/297.54 655.53/297.54 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [0] 655.53/297.54 = [cons(x, app(l1, l2))] 655.53/297.54 655.53/297.54 [mem(x, nil())] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [mem(x, cons(y, l))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [ifmem(eq(x, y), x, l)] 655.53/297.54 655.53/297.54 [ifmem(true(), x, l)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [ifmem(false(), x, l)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [mem(x, l)] 655.53/297.54 655.53/297.54 [inter(l1, app(l2, l3))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.54 655.53/297.54 [inter(x, nil())] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(l1, cons(x, l2))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.54 655.53/297.54 [inter(app(l1, l2), l3)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.54 655.53/297.54 [inter(nil(), x)] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(cons(x, l1), l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.54 655.53/297.54 [ifinter(true(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [cons(x, inter(l1, l2))] 655.53/297.54 655.53/297.54 [ifinter(false(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [inter(l1, l2)] 655.53/297.54 655.53/297.54 655.53/297.54 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.54 655.53/297.54 We are left with following problem, upon which TcT provides the 655.53/297.54 certificate YES(O(1),O(n^2)). 655.53/297.54 655.53/297.54 Strict Trs: 655.53/297.54 { eq(0(), 0()) -> true() 655.53/297.54 , eq(0(), s(x)) -> false() 655.53/297.54 , eq(s(x), 0()) -> false() 655.53/297.54 , eq(s(x), s(y)) -> eq(x, y) 655.53/297.54 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.54 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.54 , mem(x, nil()) -> false() 655.53/297.54 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.54 , ifmem(true(), x, l) -> true() 655.53/297.54 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.54 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.54 , inter(x, nil()) -> nil() 655.53/297.54 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.54 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.54 , inter(nil(), x) -> nil() 655.53/297.54 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.54 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.54 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.54 Weak Trs: 655.53/297.54 { if(true(), x, y) -> x 655.53/297.54 , if(false(), x, y) -> y 655.53/297.54 , app(nil(), l) -> l } 655.53/297.54 Obligation: 655.53/297.54 innermost runtime complexity 655.53/297.54 Answer: 655.53/297.54 YES(O(1),O(n^2)) 655.53/297.54 655.53/297.54 The weightgap principle applies (using the following nonconstant 655.53/297.54 growth matrix-interpretation) 655.53/297.54 655.53/297.54 The following argument positions are usable: 655.53/297.54 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.54 Uargs(ifinter) = {1} 655.53/297.54 655.53/297.54 TcT has computed the following matrix interpretation satisfying 655.53/297.54 not(EDA) and not(IDA(1)). 655.53/297.54 655.53/297.54 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 655.53/297.54 655.53/297.54 [true] = [0] 655.53/297.54 655.53/297.54 [false] = [0] 655.53/297.54 655.53/297.54 [eq](x1, x2) = [4] 655.53/297.54 655.53/297.54 [0] = [7] 655.53/297.54 655.53/297.54 [s](x1) = [1] x1 + [7] 655.53/297.54 655.53/297.54 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.54 655.53/297.54 [nil] = [7] 655.53/297.54 655.53/297.54 [cons](x1, x2) = [1] x2 + [0] 655.53/297.54 655.53/297.54 [mem](x1, x2) = [0] 655.53/297.54 655.53/297.54 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.54 655.53/297.54 [inter](x1, x2) = [0] 655.53/297.54 655.53/297.54 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.54 655.53/297.54 The order satisfies the following ordering constraints: 655.53/297.54 655.53/297.54 [if(true(), x, y)] = [1] x + [1] y + [7] 655.53/297.54 > [1] x + [0] 655.53/297.54 = [x] 655.53/297.54 655.53/297.54 [if(false(), x, y)] = [1] x + [1] y + [7] 655.53/297.54 > [1] y + [0] 655.53/297.54 = [y] 655.53/297.54 655.53/297.54 [eq(0(), 0())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [eq(0(), s(x))] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), 0())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), s(y))] = [4] 655.53/297.54 >= [4] 655.53/297.54 = [eq(x, y)] 655.53/297.54 655.53/297.54 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 = [app(l1, app(l2, l3))] 655.53/297.54 655.53/297.54 [app(nil(), l)] = [1] l + [7] 655.53/297.54 > [1] l + [0] 655.53/297.54 = [l] 655.53/297.54 655.53/297.54 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [0] 655.53/297.54 = [cons(x, app(l1, l2))] 655.53/297.54 655.53/297.54 [mem(x, nil())] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [mem(x, cons(y, l))] = [0] 655.53/297.54 ? [4] 655.53/297.54 = [ifmem(eq(x, y), x, l)] 655.53/297.54 655.53/297.54 [ifmem(true(), x, l)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [ifmem(false(), x, l)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [mem(x, l)] 655.53/297.54 655.53/297.54 [inter(l1, app(l2, l3))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.54 655.53/297.54 [inter(x, nil())] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(l1, cons(x, l2))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.54 655.53/297.54 [inter(app(l1, l2), l3)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.54 655.53/297.54 [inter(nil(), x)] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(cons(x, l1), l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.54 655.53/297.54 [ifinter(true(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [cons(x, inter(l1, l2))] 655.53/297.54 655.53/297.54 [ifinter(false(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [inter(l1, l2)] 655.53/297.54 655.53/297.54 655.53/297.54 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.54 655.53/297.54 We are left with following problem, upon which TcT provides the 655.53/297.54 certificate YES(O(1),O(n^2)). 655.53/297.54 655.53/297.54 Strict Trs: 655.53/297.54 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.54 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.54 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.54 , mem(x, nil()) -> false() 655.53/297.54 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.54 , ifmem(true(), x, l) -> true() 655.53/297.54 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.54 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.54 , inter(x, nil()) -> nil() 655.53/297.54 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.54 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.54 , inter(nil(), x) -> nil() 655.53/297.54 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.54 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.54 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.54 Weak Trs: 655.53/297.54 { if(true(), x, y) -> x 655.53/297.54 , if(false(), x, y) -> y 655.53/297.54 , eq(0(), 0()) -> true() 655.53/297.54 , eq(0(), s(x)) -> false() 655.53/297.54 , eq(s(x), 0()) -> false() 655.53/297.54 , app(nil(), l) -> l } 655.53/297.54 Obligation: 655.53/297.54 innermost runtime complexity 655.53/297.54 Answer: 655.53/297.54 YES(O(1),O(n^2)) 655.53/297.54 655.53/297.54 The weightgap principle applies (using the following nonconstant 655.53/297.54 growth matrix-interpretation) 655.53/297.54 655.53/297.54 The following argument positions are usable: 655.53/297.54 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.54 Uargs(ifinter) = {1} 655.53/297.54 655.53/297.54 TcT has computed the following matrix interpretation satisfying 655.53/297.54 not(EDA) and not(IDA(1)). 655.53/297.54 655.53/297.54 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 655.53/297.54 655.53/297.54 [true] = [0] 655.53/297.54 655.53/297.54 [false] = [0] 655.53/297.54 655.53/297.54 [eq](x1, x2) = [4] 655.53/297.54 655.53/297.54 [0] = [7] 655.53/297.54 655.53/297.54 [s](x1) = [1] x1 + [7] 655.53/297.54 655.53/297.54 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.54 655.53/297.54 [nil] = [7] 655.53/297.54 655.53/297.54 [cons](x1, x2) = [1] x2 + [0] 655.53/297.54 655.53/297.54 [mem](x1, x2) = [4] 655.53/297.54 655.53/297.54 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.54 655.53/297.54 [inter](x1, x2) = [0] 655.53/297.54 655.53/297.54 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.54 655.53/297.54 The order satisfies the following ordering constraints: 655.53/297.54 655.53/297.54 [if(true(), x, y)] = [1] x + [1] y + [7] 655.53/297.54 > [1] x + [0] 655.53/297.54 = [x] 655.53/297.54 655.53/297.54 [if(false(), x, y)] = [1] x + [1] y + [7] 655.53/297.54 > [1] y + [0] 655.53/297.54 = [y] 655.53/297.54 655.53/297.54 [eq(0(), 0())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [eq(0(), s(x))] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), 0())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), s(y))] = [4] 655.53/297.54 >= [4] 655.53/297.54 = [eq(x, y)] 655.53/297.54 655.53/297.54 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 = [app(l1, app(l2, l3))] 655.53/297.54 655.53/297.54 [app(nil(), l)] = [1] l + [7] 655.53/297.54 > [1] l + [0] 655.53/297.54 = [l] 655.53/297.54 655.53/297.54 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [0] 655.53/297.54 = [cons(x, app(l1, l2))] 655.53/297.54 655.53/297.54 [mem(x, nil())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [mem(x, cons(y, l))] = [4] 655.53/297.54 >= [4] 655.53/297.54 = [ifmem(eq(x, y), x, l)] 655.53/297.54 655.53/297.54 [ifmem(true(), x, l)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [ifmem(false(), x, l)] = [0] 655.53/297.54 ? [4] 655.53/297.54 = [mem(x, l)] 655.53/297.54 655.53/297.54 [inter(l1, app(l2, l3))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.54 655.53/297.54 [inter(x, nil())] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(l1, cons(x, l2))] = [0] 655.53/297.54 ? [4] 655.53/297.54 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.54 655.53/297.54 [inter(app(l1, l2), l3)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.54 655.53/297.54 [inter(nil(), x)] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(cons(x, l1), l2)] = [0] 655.53/297.54 ? [4] 655.53/297.54 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.54 655.53/297.54 [ifinter(true(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [cons(x, inter(l1, l2))] 655.53/297.54 655.53/297.54 [ifinter(false(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [inter(l1, l2)] 655.53/297.54 655.53/297.54 655.53/297.54 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.54 655.53/297.54 We are left with following problem, upon which TcT provides the 655.53/297.54 certificate YES(O(1),O(n^2)). 655.53/297.54 655.53/297.54 Strict Trs: 655.53/297.54 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.54 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.54 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.54 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.54 , ifmem(true(), x, l) -> true() 655.53/297.54 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.54 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.54 , inter(x, nil()) -> nil() 655.53/297.54 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.54 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.54 , inter(nil(), x) -> nil() 655.53/297.54 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.54 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.54 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.54 Weak Trs: 655.53/297.54 { if(true(), x, y) -> x 655.53/297.54 , if(false(), x, y) -> y 655.53/297.54 , eq(0(), 0()) -> true() 655.53/297.54 , eq(0(), s(x)) -> false() 655.53/297.54 , eq(s(x), 0()) -> false() 655.53/297.54 , app(nil(), l) -> l 655.53/297.54 , mem(x, nil()) -> false() } 655.53/297.54 Obligation: 655.53/297.54 innermost runtime complexity 655.53/297.54 Answer: 655.53/297.54 YES(O(1),O(n^2)) 655.53/297.54 655.53/297.54 The weightgap principle applies (using the following nonconstant 655.53/297.54 growth matrix-interpretation) 655.53/297.54 655.53/297.54 The following argument positions are usable: 655.53/297.54 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.54 Uargs(ifinter) = {1} 655.53/297.54 655.53/297.54 TcT has computed the following matrix interpretation satisfying 655.53/297.54 not(EDA) and not(IDA(1)). 655.53/297.54 655.53/297.54 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 655.53/297.54 655.53/297.54 [true] = [0] 655.53/297.54 655.53/297.54 [false] = [0] 655.53/297.54 655.53/297.54 [eq](x1, x2) = [4] 655.53/297.54 655.53/297.54 [0] = [7] 655.53/297.54 655.53/297.54 [s](x1) = [1] x1 + [7] 655.53/297.54 655.53/297.54 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.54 655.53/297.54 [nil] = [7] 655.53/297.54 655.53/297.54 [cons](x1, x2) = [1] x2 + [0] 655.53/297.54 655.53/297.54 [mem](x1, x2) = [6] 655.53/297.54 655.53/297.54 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.54 655.53/297.54 [inter](x1, x2) = [0] 655.53/297.54 655.53/297.54 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.54 655.53/297.54 The order satisfies the following ordering constraints: 655.53/297.54 655.53/297.54 [if(true(), x, y)] = [1] x + [1] y + [7] 655.53/297.54 > [1] x + [0] 655.53/297.54 = [x] 655.53/297.54 655.53/297.54 [if(false(), x, y)] = [1] x + [1] y + [7] 655.53/297.54 > [1] y + [0] 655.53/297.54 = [y] 655.53/297.54 655.53/297.54 [eq(0(), 0())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [eq(0(), s(x))] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), 0())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), s(y))] = [4] 655.53/297.54 >= [4] 655.53/297.54 = [eq(x, y)] 655.53/297.54 655.53/297.54 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 = [app(l1, app(l2, l3))] 655.53/297.54 655.53/297.54 [app(nil(), l)] = [1] l + [7] 655.53/297.54 > [1] l + [0] 655.53/297.54 = [l] 655.53/297.54 655.53/297.54 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [0] 655.53/297.54 = [cons(x, app(l1, l2))] 655.53/297.54 655.53/297.54 [mem(x, nil())] = [6] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [mem(x, cons(y, l))] = [6] 655.53/297.54 > [4] 655.53/297.54 = [ifmem(eq(x, y), x, l)] 655.53/297.54 655.53/297.54 [ifmem(true(), x, l)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [ifmem(false(), x, l)] = [0] 655.53/297.54 ? [6] 655.53/297.54 = [mem(x, l)] 655.53/297.54 655.53/297.54 [inter(l1, app(l2, l3))] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.54 655.53/297.54 [inter(x, nil())] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(l1, cons(x, l2))] = [0] 655.53/297.54 ? [6] 655.53/297.54 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.54 655.53/297.54 [inter(app(l1, l2), l3)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.54 655.53/297.54 [inter(nil(), x)] = [0] 655.53/297.54 ? [7] 655.53/297.54 = [nil()] 655.53/297.54 655.53/297.54 [inter(cons(x, l1), l2)] = [0] 655.53/297.54 ? [6] 655.53/297.54 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.54 655.53/297.54 [ifinter(true(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [cons(x, inter(l1, l2))] 655.53/297.54 655.53/297.54 [ifinter(false(), x, l1, l2)] = [0] 655.53/297.54 >= [0] 655.53/297.54 = [inter(l1, l2)] 655.53/297.54 655.53/297.54 655.53/297.54 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.54 655.53/297.54 We are left with following problem, upon which TcT provides the 655.53/297.54 certificate YES(O(1),O(n^2)). 655.53/297.54 655.53/297.54 Strict Trs: 655.53/297.54 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.54 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.54 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.54 , ifmem(true(), x, l) -> true() 655.53/297.54 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.54 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.54 , inter(x, nil()) -> nil() 655.53/297.54 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.54 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.54 , inter(nil(), x) -> nil() 655.53/297.54 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.54 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.54 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.54 Weak Trs: 655.53/297.54 { if(true(), x, y) -> x 655.53/297.54 , if(false(), x, y) -> y 655.53/297.54 , eq(0(), 0()) -> true() 655.53/297.54 , eq(0(), s(x)) -> false() 655.53/297.54 , eq(s(x), 0()) -> false() 655.53/297.54 , app(nil(), l) -> l 655.53/297.54 , mem(x, nil()) -> false() 655.53/297.54 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) } 655.53/297.54 Obligation: 655.53/297.54 innermost runtime complexity 655.53/297.54 Answer: 655.53/297.54 YES(O(1),O(n^2)) 655.53/297.54 655.53/297.54 The weightgap principle applies (using the following nonconstant 655.53/297.54 growth matrix-interpretation) 655.53/297.54 655.53/297.54 The following argument positions are usable: 655.53/297.54 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.54 Uargs(ifinter) = {1} 655.53/297.54 655.53/297.54 TcT has computed the following matrix interpretation satisfying 655.53/297.54 not(EDA) and not(IDA(1)). 655.53/297.54 655.53/297.54 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [5] 655.53/297.54 655.53/297.54 [true] = [1] 655.53/297.54 655.53/297.54 [false] = [0] 655.53/297.54 655.53/297.54 [eq](x1, x2) = [1] 655.53/297.54 655.53/297.54 [0] = [7] 655.53/297.54 655.53/297.54 [s](x1) = [1] x1 + [7] 655.53/297.54 655.53/297.54 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.54 655.53/297.54 [nil] = [7] 655.53/297.54 655.53/297.54 [cons](x1, x2) = [1] x2 + [0] 655.53/297.54 655.53/297.54 [mem](x1, x2) = [4] 655.53/297.54 655.53/297.54 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.54 655.53/297.54 [inter](x1, x2) = [0] 655.53/297.54 655.53/297.54 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.54 655.53/297.54 The order satisfies the following ordering constraints: 655.53/297.54 655.53/297.54 [if(true(), x, y)] = [1] x + [1] y + [6] 655.53/297.54 > [1] x + [0] 655.53/297.54 = [x] 655.53/297.54 655.53/297.54 [if(false(), x, y)] = [1] x + [1] y + [5] 655.53/297.54 > [1] y + [0] 655.53/297.54 = [y] 655.53/297.54 655.53/297.54 [eq(0(), 0())] = [1] 655.53/297.54 >= [1] 655.53/297.54 = [true()] 655.53/297.54 655.53/297.54 [eq(0(), s(x))] = [1] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), 0())] = [1] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [eq(s(x), s(y))] = [1] 655.53/297.54 >= [1] 655.53/297.54 = [eq(x, y)] 655.53/297.54 655.53/297.54 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.54 = [app(l1, app(l2, l3))] 655.53/297.54 655.53/297.54 [app(nil(), l)] = [1] l + [7] 655.53/297.54 > [1] l + [0] 655.53/297.54 = [l] 655.53/297.54 655.53/297.54 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.54 >= [1] l1 + [1] l2 + [0] 655.53/297.54 = [cons(x, app(l1, l2))] 655.53/297.54 655.53/297.54 [mem(x, nil())] = [4] 655.53/297.54 > [0] 655.53/297.54 = [false()] 655.53/297.54 655.53/297.54 [mem(x, cons(y, l))] = [4] 655.53/297.54 > [1] 655.53/297.54 = [ifmem(eq(x, y), x, l)] 655.53/297.54 655.53/297.55 [ifmem(true(), x, l)] = [1] 655.53/297.55 >= [1] 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [ifmem(false(), x, l)] = [0] 655.53/297.55 ? [4] 655.53/297.55 = [mem(x, l)] 655.53/297.55 655.53/297.55 [inter(l1, app(l2, l3))] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.55 655.53/297.55 [inter(x, nil())] = [0] 655.53/297.55 ? [7] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(l1, cons(x, l2))] = [0] 655.53/297.55 ? [4] 655.53/297.55 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.55 655.53/297.55 [inter(app(l1, l2), l3)] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.55 655.53/297.55 [inter(nil(), x)] = [0] 655.53/297.55 ? [7] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(cons(x, l1), l2)] = [0] 655.53/297.55 ? [4] 655.53/297.55 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.55 655.53/297.55 [ifinter(true(), x, l1, l2)] = [1] 655.53/297.55 > [0] 655.53/297.55 = [cons(x, inter(l1, l2))] 655.53/297.55 655.53/297.55 [ifinter(false(), x, l1, l2)] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [inter(l1, l2)] 655.53/297.55 655.53/297.55 655.53/297.55 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.55 655.53/297.55 We are left with following problem, upon which TcT provides the 655.53/297.55 certificate YES(O(1),O(n^2)). 655.53/297.55 655.53/297.55 Strict Trs: 655.53/297.55 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.55 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.55 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.55 , ifmem(true(), x, l) -> true() 655.53/297.55 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.55 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.55 , inter(x, nil()) -> nil() 655.53/297.55 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.55 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.55 , inter(nil(), x) -> nil() 655.53/297.55 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.55 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.55 Weak Trs: 655.53/297.55 { if(true(), x, y) -> x 655.53/297.55 , if(false(), x, y) -> y 655.53/297.55 , eq(0(), 0()) -> true() 655.53/297.55 , eq(0(), s(x)) -> false() 655.53/297.55 , eq(s(x), 0()) -> false() 655.53/297.55 , app(nil(), l) -> l 655.53/297.55 , mem(x, nil()) -> false() 655.53/297.55 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.55 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) } 655.53/297.55 Obligation: 655.53/297.55 innermost runtime complexity 655.53/297.55 Answer: 655.53/297.55 YES(O(1),O(n^2)) 655.53/297.55 655.53/297.55 The weightgap principle applies (using the following nonconstant 655.53/297.55 growth matrix-interpretation) 655.53/297.55 655.53/297.55 The following argument positions are usable: 655.53/297.55 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.55 Uargs(ifinter) = {1} 655.53/297.55 655.53/297.55 TcT has computed the following matrix interpretation satisfying 655.53/297.55 not(EDA) and not(IDA(1)). 655.53/297.55 655.53/297.55 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 655.53/297.55 655.53/297.55 [true] = [1] 655.53/297.55 655.53/297.55 [false] = [0] 655.53/297.55 655.53/297.55 [eq](x1, x2) = [1] 655.53/297.55 655.53/297.55 [0] = [7] 655.53/297.55 655.53/297.55 [s](x1) = [1] x1 + [7] 655.53/297.55 655.53/297.55 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.55 655.53/297.55 [nil] = [0] 655.53/297.55 655.53/297.55 [cons](x1, x2) = [1] x2 + [0] 655.53/297.55 655.53/297.55 [mem](x1, x2) = [4] 655.53/297.55 655.53/297.55 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.55 655.53/297.55 [inter](x1, x2) = [1] 655.53/297.55 655.53/297.55 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.55 655.53/297.55 The order satisfies the following ordering constraints: 655.53/297.55 655.53/297.55 [if(true(), x, y)] = [1] x + [1] y + [8] 655.53/297.55 > [1] x + [0] 655.53/297.55 = [x] 655.53/297.55 655.53/297.55 [if(false(), x, y)] = [1] x + [1] y + [7] 655.53/297.55 > [1] y + [0] 655.53/297.55 = [y] 655.53/297.55 655.53/297.55 [eq(0(), 0())] = [1] 655.53/297.55 >= [1] 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [eq(0(), s(x))] = [1] 655.53/297.55 > [0] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), 0())] = [1] 655.53/297.55 > [0] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), s(y))] = [1] 655.53/297.55 >= [1] 655.53/297.55 = [eq(x, y)] 655.53/297.55 655.53/297.55 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.55 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.55 = [app(l1, app(l2, l3))] 655.53/297.55 655.53/297.55 [app(nil(), l)] = [1] l + [0] 655.53/297.55 >= [1] l + [0] 655.53/297.55 = [l] 655.53/297.55 655.53/297.55 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.55 >= [1] l1 + [1] l2 + [0] 655.53/297.55 = [cons(x, app(l1, l2))] 655.53/297.55 655.53/297.55 [mem(x, nil())] = [4] 655.53/297.55 > [0] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [mem(x, cons(y, l))] = [4] 655.53/297.55 > [1] 655.53/297.55 = [ifmem(eq(x, y), x, l)] 655.53/297.55 655.53/297.55 [ifmem(true(), x, l)] = [1] 655.53/297.55 >= [1] 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [ifmem(false(), x, l)] = [0] 655.53/297.55 ? [4] 655.53/297.55 = [mem(x, l)] 655.53/297.55 655.53/297.55 [inter(l1, app(l2, l3))] = [1] 655.53/297.55 ? [2] 655.53/297.55 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.55 655.53/297.55 [inter(x, nil())] = [1] 655.53/297.55 > [0] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(l1, cons(x, l2))] = [1] 655.53/297.55 ? [4] 655.53/297.55 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.55 655.53/297.55 [inter(app(l1, l2), l3)] = [1] 655.53/297.55 ? [2] 655.53/297.55 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.55 655.53/297.55 [inter(nil(), x)] = [1] 655.53/297.55 > [0] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(cons(x, l1), l2)] = [1] 655.53/297.55 ? [4] 655.53/297.55 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.55 655.53/297.55 [ifinter(true(), x, l1, l2)] = [1] 655.53/297.55 >= [1] 655.53/297.55 = [cons(x, inter(l1, l2))] 655.53/297.55 655.53/297.55 [ifinter(false(), x, l1, l2)] = [0] 655.53/297.55 ? [1] 655.53/297.55 = [inter(l1, l2)] 655.53/297.55 655.53/297.55 655.53/297.55 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.55 655.53/297.55 We are left with following problem, upon which TcT provides the 655.53/297.55 certificate YES(O(1),O(n^2)). 655.53/297.55 655.53/297.55 Strict Trs: 655.53/297.55 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.55 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.55 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.55 , ifmem(true(), x, l) -> true() 655.53/297.55 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.55 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.55 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.55 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.55 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.55 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.55 Weak Trs: 655.53/297.55 { if(true(), x, y) -> x 655.53/297.55 , if(false(), x, y) -> y 655.53/297.55 , eq(0(), 0()) -> true() 655.53/297.55 , eq(0(), s(x)) -> false() 655.53/297.55 , eq(s(x), 0()) -> false() 655.53/297.55 , app(nil(), l) -> l 655.53/297.55 , mem(x, nil()) -> false() 655.53/297.55 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.55 , inter(x, nil()) -> nil() 655.53/297.55 , inter(nil(), x) -> nil() 655.53/297.55 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) } 655.53/297.55 Obligation: 655.53/297.55 innermost runtime complexity 655.53/297.55 Answer: 655.53/297.55 YES(O(1),O(n^2)) 655.53/297.55 655.53/297.55 The weightgap principle applies (using the following nonconstant 655.53/297.55 growth matrix-interpretation) 655.53/297.55 655.53/297.55 The following argument positions are usable: 655.53/297.55 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.55 Uargs(ifinter) = {1} 655.53/297.55 655.53/297.55 TcT has computed the following matrix interpretation satisfying 655.53/297.55 not(EDA) and not(IDA(1)). 655.53/297.55 655.53/297.55 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 655.53/297.55 655.53/297.55 [true] = [4] 655.53/297.55 655.53/297.55 [false] = [1] 655.53/297.55 655.53/297.55 [eq](x1, x2) = [4] 655.53/297.55 655.53/297.55 [0] = [7] 655.53/297.55 655.53/297.55 [s](x1) = [1] x1 + [7] 655.53/297.55 655.53/297.55 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.55 655.53/297.55 [nil] = [0] 655.53/297.55 655.53/297.55 [cons](x1, x2) = [1] x2 + [0] 655.53/297.55 655.53/297.55 [mem](x1, x2) = [4] 655.53/297.55 655.53/297.55 [ifmem](x1, x2, x3) = [1] x1 + [0] 655.53/297.55 655.53/297.55 [inter](x1, x2) = [0] 655.53/297.55 655.53/297.55 [ifinter](x1, x2, x3, x4) = [1] x1 + [0] 655.53/297.55 655.53/297.55 The order satisfies the following ordering constraints: 655.53/297.55 655.53/297.55 [if(true(), x, y)] = [1] x + [1] y + [11] 655.53/297.55 > [1] x + [0] 655.53/297.55 = [x] 655.53/297.55 655.53/297.55 [if(false(), x, y)] = [1] x + [1] y + [8] 655.53/297.55 > [1] y + [0] 655.53/297.55 = [y] 655.53/297.55 655.53/297.55 [eq(0(), 0())] = [4] 655.53/297.55 >= [4] 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [eq(0(), s(x))] = [4] 655.53/297.55 > [1] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), 0())] = [4] 655.53/297.55 > [1] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), s(y))] = [4] 655.53/297.55 >= [4] 655.53/297.55 = [eq(x, y)] 655.53/297.55 655.53/297.55 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.55 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.55 = [app(l1, app(l2, l3))] 655.53/297.55 655.53/297.55 [app(nil(), l)] = [1] l + [0] 655.53/297.55 >= [1] l + [0] 655.53/297.55 = [l] 655.53/297.55 655.53/297.55 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.55 >= [1] l1 + [1] l2 + [0] 655.53/297.55 = [cons(x, app(l1, l2))] 655.53/297.55 655.53/297.55 [mem(x, nil())] = [4] 655.53/297.55 > [1] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [mem(x, cons(y, l))] = [4] 655.53/297.55 >= [4] 655.53/297.55 = [ifmem(eq(x, y), x, l)] 655.53/297.55 655.53/297.55 [ifmem(true(), x, l)] = [4] 655.53/297.55 >= [4] 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [ifmem(false(), x, l)] = [1] 655.53/297.55 ? [4] 655.53/297.55 = [mem(x, l)] 655.53/297.55 655.53/297.55 [inter(l1, app(l2, l3))] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.55 655.53/297.55 [inter(x, nil())] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(l1, cons(x, l2))] = [0] 655.53/297.55 ? [4] 655.53/297.55 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.55 655.53/297.55 [inter(app(l1, l2), l3)] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.55 655.53/297.55 [inter(nil(), x)] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(cons(x, l1), l2)] = [0] 655.53/297.55 ? [4] 655.53/297.55 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.55 655.53/297.55 [ifinter(true(), x, l1, l2)] = [4] 655.53/297.55 > [0] 655.53/297.55 = [cons(x, inter(l1, l2))] 655.53/297.55 655.53/297.55 [ifinter(false(), x, l1, l2)] = [1] 655.53/297.55 > [0] 655.53/297.55 = [inter(l1, l2)] 655.53/297.55 655.53/297.55 655.53/297.55 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.55 655.53/297.55 We are left with following problem, upon which TcT provides the 655.53/297.55 certificate YES(O(1),O(n^2)). 655.53/297.55 655.53/297.55 Strict Trs: 655.53/297.55 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.55 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.55 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.55 , ifmem(true(), x, l) -> true() 655.53/297.55 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.55 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.55 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.55 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.55 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) } 655.53/297.55 Weak Trs: 655.53/297.55 { if(true(), x, y) -> x 655.53/297.55 , if(false(), x, y) -> y 655.53/297.55 , eq(0(), 0()) -> true() 655.53/297.55 , eq(0(), s(x)) -> false() 655.53/297.55 , eq(s(x), 0()) -> false() 655.53/297.55 , app(nil(), l) -> l 655.53/297.55 , mem(x, nil()) -> false() 655.53/297.55 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.55 , inter(x, nil()) -> nil() 655.53/297.55 , inter(nil(), x) -> nil() 655.53/297.55 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.55 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.55 Obligation: 655.53/297.55 innermost runtime complexity 655.53/297.55 Answer: 655.53/297.55 YES(O(1),O(n^2)) 655.53/297.55 655.53/297.55 The weightgap principle applies (using the following nonconstant 655.53/297.55 growth matrix-interpretation) 655.53/297.55 655.53/297.55 The following argument positions are usable: 655.53/297.55 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.55 Uargs(ifinter) = {1} 655.53/297.55 655.53/297.55 TcT has computed the following matrix interpretation satisfying 655.53/297.55 not(EDA) and not(IDA(1)). 655.53/297.55 655.53/297.55 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 655.53/297.55 655.53/297.55 [true] = [0] 655.53/297.55 655.53/297.55 [false] = [0] 655.53/297.55 655.53/297.55 [eq](x1, x2) = [0] 655.53/297.55 655.53/297.55 [0] = [7] 655.53/297.55 655.53/297.55 [s](x1) = [1] x1 + [7] 655.53/297.55 655.53/297.55 [app](x1, x2) = [1] x1 + [1] x2 + [0] 655.53/297.55 655.53/297.55 [nil] = [0] 655.53/297.55 655.53/297.55 [cons](x1, x2) = [1] x2 + [0] 655.53/297.55 655.53/297.55 [mem](x1, x2) = [4] 655.53/297.55 655.53/297.55 [ifmem](x1, x2, x3) = [1] x1 + [1] 655.53/297.55 655.53/297.55 [inter](x1, x2) = [0] 655.53/297.55 655.53/297.55 [ifinter](x1, x2, x3, x4) = [1] x1 + [4] 655.53/297.55 655.53/297.55 The order satisfies the following ordering constraints: 655.53/297.55 655.53/297.55 [if(true(), x, y)] = [1] x + [1] y + [7] 655.53/297.55 > [1] x + [0] 655.53/297.55 = [x] 655.53/297.55 655.53/297.55 [if(false(), x, y)] = [1] x + [1] y + [7] 655.53/297.55 > [1] y + [0] 655.53/297.55 = [y] 655.53/297.55 655.53/297.55 [eq(0(), 0())] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [eq(0(), s(x))] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), 0())] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), s(y))] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [eq(x, y)] 655.53/297.55 655.53/297.55 [app(app(l1, l2), l3)] = [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.55 >= [1] l1 + [1] l2 + [1] l3 + [0] 655.53/297.55 = [app(l1, app(l2, l3))] 655.53/297.55 655.53/297.55 [app(nil(), l)] = [1] l + [0] 655.53/297.55 >= [1] l + [0] 655.53/297.55 = [l] 655.53/297.55 655.53/297.55 [app(cons(x, l1), l2)] = [1] l1 + [1] l2 + [0] 655.53/297.55 >= [1] l1 + [1] l2 + [0] 655.53/297.55 = [cons(x, app(l1, l2))] 655.53/297.55 655.53/297.55 [mem(x, nil())] = [4] 655.53/297.55 > [0] 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [mem(x, cons(y, l))] = [4] 655.53/297.55 > [1] 655.53/297.55 = [ifmem(eq(x, y), x, l)] 655.53/297.55 655.53/297.55 [ifmem(true(), x, l)] = [1] 655.53/297.55 > [0] 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [ifmem(false(), x, l)] = [1] 655.53/297.55 ? [4] 655.53/297.55 = [mem(x, l)] 655.53/297.55 655.53/297.55 [inter(l1, app(l2, l3))] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.55 655.53/297.55 [inter(x, nil())] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(l1, cons(x, l2))] = [0] 655.53/297.55 ? [8] 655.53/297.55 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.55 655.53/297.55 [inter(app(l1, l2), l3)] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.55 655.53/297.55 [inter(nil(), x)] = [0] 655.53/297.55 >= [0] 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(cons(x, l1), l2)] = [0] 655.53/297.55 ? [8] 655.53/297.55 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.55 655.53/297.55 [ifinter(true(), x, l1, l2)] = [4] 655.53/297.55 > [0] 655.53/297.55 = [cons(x, inter(l1, l2))] 655.53/297.55 655.53/297.55 [ifinter(false(), x, l1, l2)] = [4] 655.53/297.55 > [0] 655.53/297.55 = [inter(l1, l2)] 655.53/297.55 655.53/297.55 655.53/297.55 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 655.53/297.55 655.53/297.55 We are left with following problem, upon which TcT provides the 655.53/297.55 certificate YES(O(1),O(n^2)). 655.53/297.55 655.53/297.55 Strict Trs: 655.53/297.55 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.55 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.55 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.55 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.55 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.55 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.55 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.55 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) } 655.53/297.55 Weak Trs: 655.53/297.55 { if(true(), x, y) -> x 655.53/297.55 , if(false(), x, y) -> y 655.53/297.55 , eq(0(), 0()) -> true() 655.53/297.55 , eq(0(), s(x)) -> false() 655.53/297.55 , eq(s(x), 0()) -> false() 655.53/297.55 , app(nil(), l) -> l 655.53/297.55 , mem(x, nil()) -> false() 655.53/297.55 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.55 , ifmem(true(), x, l) -> true() 655.53/297.55 , inter(x, nil()) -> nil() 655.53/297.55 , inter(nil(), x) -> nil() 655.53/297.55 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.55 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.55 Obligation: 655.53/297.55 innermost runtime complexity 655.53/297.55 Answer: 655.53/297.55 YES(O(1),O(n^2)) 655.53/297.55 655.53/297.55 We use the processor 'polynomial interpretation' to orient 655.53/297.55 following rules strictly. 655.53/297.55 655.53/297.55 Trs: { ifmem(false(), x, l) -> mem(x, l) } 655.53/297.55 655.53/297.55 The induced complexity on above rules (modulo remaining rules) is 655.53/297.55 YES(?,O(n^2)) . These rules are moved into the corresponding weak 655.53/297.55 component(s). 655.53/297.55 655.53/297.55 Sub-proof: 655.53/297.55 ---------- 655.53/297.55 We consider the following typing: 655.53/297.55 655.53/297.55 if :: (b,a,a) -> a 655.53/297.55 true :: b 655.53/297.55 false :: b 655.53/297.55 eq :: (c,c) -> b 655.53/297.55 0 :: c 655.53/297.55 s :: c -> c 655.53/297.55 app :: (d,d) -> d 655.53/297.55 nil :: d 655.53/297.55 cons :: (c,d) -> d 655.53/297.55 mem :: (c,d) -> b 655.53/297.55 ifmem :: (b,c,d) -> b 655.53/297.55 inter :: (d,d) -> d 655.53/297.55 ifinter :: (b,c,d,d) -> d 655.53/297.55 655.53/297.55 The following argument positions are considered usable: 655.53/297.55 655.53/297.55 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.55 Uargs(ifinter) = {1} 655.53/297.55 655.53/297.55 TcT has computed the following constructor-restricted 655.53/297.55 typedpolynomial interpretation. 655.53/297.55 655.53/297.55 [if](x1, x2, x3) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 655.53/297.55 655.53/297.55 [true]() = 1 655.53/297.55 655.53/297.55 [false]() = 0 655.53/297.55 655.53/297.55 [eq](x1, x2) = 1 655.53/297.55 655.53/297.55 [0]() = 0 655.53/297.55 655.53/297.55 [s](x1) = 0 655.53/297.55 655.53/297.55 [app](x1, x2) = x1 + x2 655.53/297.55 655.53/297.55 [nil]() = 0 655.53/297.55 655.53/297.55 [cons](x1, x2) = 2 + x2 655.53/297.55 655.53/297.55 [mem](x1, x2) = 2*x2 655.53/297.55 655.53/297.55 [ifmem](x1, x2, x3) = 3 + x1 + 2*x3 655.53/297.55 655.53/297.55 [inter](x1, x2) = 2*x1*x2 655.53/297.55 655.53/297.55 [ifinter](x1, x2, x3, x4) = 2*x1 + 2*x3*x4 655.53/297.55 655.53/297.55 655.53/297.55 This order satisfies the following ordering constraints. 655.53/297.55 655.53/297.55 [if(true(), x, y)] = 3 + 6*x + 6*y 655.53/297.55 > x 655.53/297.55 = [x] 655.53/297.55 655.53/297.55 [if(false(), x, y)] = 3 + 3*x + 3*y 655.53/297.55 > y 655.53/297.55 = [y] 655.53/297.55 655.53/297.55 [eq(0(), 0())] = 1 655.53/297.55 >= 1 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [eq(0(), s(x))] = 1 655.53/297.55 > 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), 0())] = 1 655.53/297.55 > 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), s(y))] = 1 655.53/297.55 >= 1 655.53/297.55 = [eq(x, y)] 655.53/297.55 655.53/297.55 [app(app(l1, l2), l3)] = l1 + l2 + l3 655.53/297.55 >= l1 + l2 + l3 655.53/297.55 = [app(l1, app(l2, l3))] 655.53/297.55 655.53/297.55 [app(nil(), l)] = l 655.53/297.55 >= l 655.53/297.55 = [l] 655.53/297.55 655.53/297.55 [app(cons(x, l1), l2)] = 2 + l1 + l2 655.53/297.55 >= 2 + l1 + l2 655.53/297.55 = [cons(x, app(l1, l2))] 655.53/297.55 655.53/297.55 [mem(x, nil())] = 655.53/297.55 >= 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [mem(x, cons(y, l))] = 4 + 2*l 655.53/297.55 >= 4 + 2*l 655.53/297.55 = [ifmem(eq(x, y), x, l)] 655.53/297.55 655.53/297.55 [ifmem(true(), x, l)] = 4 + 2*l 655.53/297.55 > 1 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [ifmem(false(), x, l)] = 3 + 2*l 655.53/297.55 > 2*l 655.53/297.55 = [mem(x, l)] 655.53/297.55 655.53/297.55 [inter(l1, app(l2, l3))] = 2*l1*l2 + 2*l1*l3 655.53/297.55 >= 2*l1*l2 + 2*l1*l3 655.53/297.55 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.55 655.53/297.55 [inter(x, nil())] = 655.53/297.55 >= 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(l1, cons(x, l2))] = 4*l1 + 2*l1*l2 655.53/297.55 >= 4*l1 + 2*l2*l1 655.53/297.55 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.55 655.53/297.55 [inter(app(l1, l2), l3)] = 2*l1*l3 + 2*l2*l3 655.53/297.55 >= 2*l1*l3 + 2*l2*l3 655.53/297.55 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.55 655.53/297.55 [inter(nil(), x)] = 655.53/297.55 >= 655.53/297.55 = [nil()] 655.53/297.55 655.53/297.55 [inter(cons(x, l1), l2)] = 4*l2 + 2*l1*l2 655.53/297.55 >= 4*l2 + 2*l1*l2 655.53/297.55 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.55 655.53/297.55 [ifinter(true(), x, l1, l2)] = 2 + 2*l1*l2 655.53/297.55 >= 2 + 2*l1*l2 655.53/297.55 = [cons(x, inter(l1, l2))] 655.53/297.55 655.53/297.55 [ifinter(false(), x, l1, l2)] = 2*l1*l2 655.53/297.55 >= 2*l1*l2 655.53/297.55 = [inter(l1, l2)] 655.53/297.55 655.53/297.55 655.53/297.55 We return to the main proof. 655.53/297.55 655.53/297.55 We are left with following problem, upon which TcT provides the 655.53/297.55 certificate YES(O(1),O(n^2)). 655.53/297.55 655.53/297.55 Strict Trs: 655.53/297.55 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.55 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.55 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.55 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.55 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.55 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.55 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) } 655.53/297.55 Weak Trs: 655.53/297.55 { if(true(), x, y) -> x 655.53/297.55 , if(false(), x, y) -> y 655.53/297.55 , eq(0(), 0()) -> true() 655.53/297.55 , eq(0(), s(x)) -> false() 655.53/297.55 , eq(s(x), 0()) -> false() 655.53/297.55 , app(nil(), l) -> l 655.53/297.55 , mem(x, nil()) -> false() 655.53/297.55 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.55 , ifmem(true(), x, l) -> true() 655.53/297.55 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.55 , inter(x, nil()) -> nil() 655.53/297.55 , inter(nil(), x) -> nil() 655.53/297.55 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.55 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.55 Obligation: 655.53/297.55 innermost runtime complexity 655.53/297.55 Answer: 655.53/297.55 YES(O(1),O(n^2)) 655.53/297.55 655.53/297.55 We use the processor 'polynomial interpretation' to orient 655.53/297.55 following rules strictly. 655.53/297.55 655.53/297.55 Trs: 655.53/297.55 { inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.55 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.55 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.55 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) } 655.53/297.55 655.53/297.55 The induced complexity on above rules (modulo remaining rules) is 655.53/297.55 YES(?,O(n^2)) . These rules are moved into the corresponding weak 655.53/297.55 component(s). 655.53/297.55 655.53/297.55 Sub-proof: 655.53/297.55 ---------- 655.53/297.55 We consider the following typing: 655.53/297.55 655.53/297.55 if :: (b,a,a) -> a 655.53/297.55 true :: b 655.53/297.55 false :: b 655.53/297.55 eq :: (c,c) -> b 655.53/297.55 0 :: c 655.53/297.55 s :: c -> c 655.53/297.55 app :: (d,d) -> d 655.53/297.55 nil :: d 655.53/297.55 cons :: (c,d) -> d 655.53/297.55 mem :: (c,d) -> b 655.53/297.55 ifmem :: (b,c,d) -> b 655.53/297.55 inter :: (d,d) -> d 655.53/297.55 ifinter :: (b,c,d,d) -> d 655.53/297.55 655.53/297.55 The following argument positions are considered usable: 655.53/297.55 655.53/297.55 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.55 Uargs(ifinter) = {1} 655.53/297.55 655.53/297.55 TcT has computed the following constructor-restricted 655.53/297.55 typedpolynomial interpretation. 655.53/297.55 655.53/297.55 [if](x1, x2, x3) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 655.53/297.55 655.53/297.55 [true]() = 0 655.53/297.55 655.53/297.55 [false]() = 0 655.53/297.55 655.53/297.55 [eq](x1, x2) = 0 655.53/297.55 655.53/297.55 [0]() = 0 655.53/297.55 655.53/297.55 [s](x1) = 0 655.53/297.55 655.53/297.55 [app](x1, x2) = 2 + x1 + x2 655.53/297.55 655.53/297.55 [nil]() = 0 655.53/297.55 655.53/297.55 [cons](x1, x2) = 2 + x2 655.53/297.55 655.53/297.55 [mem](x1, x2) = 0 655.53/297.55 655.53/297.55 [ifmem](x1, x2, x3) = 2*x1 655.53/297.55 655.53/297.55 [inter](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 655.53/297.55 655.53/297.55 [ifinter](x1, x2, x3, x4) = 2 + x1 + 2*x3 + 2*x3*x4 + 2*x4 655.53/297.55 655.53/297.55 655.53/297.55 This order satisfies the following ordering constraints. 655.53/297.55 655.53/297.55 [if(true(), x, y)] = 3 + 3*x + 3*y 655.53/297.55 > x 655.53/297.55 = [x] 655.53/297.55 655.53/297.55 [if(false(), x, y)] = 3 + 3*x + 3*y 655.53/297.55 > y 655.53/297.55 = [y] 655.53/297.55 655.53/297.55 [eq(0(), 0())] = 655.53/297.55 >= 655.53/297.55 = [true()] 655.53/297.55 655.53/297.55 [eq(0(), s(x))] = 655.53/297.55 >= 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), 0())] = 655.53/297.55 >= 655.53/297.55 = [false()] 655.53/297.55 655.53/297.55 [eq(s(x), s(y))] = 655.53/297.55 >= 655.53/297.55 = [eq(x, y)] 655.53/297.55 655.53/297.55 [app(app(l1, l2), l3)] = 4 + l1 + l2 + l3 655.53/297.55 >= 4 + l1 + l2 + l3 655.53/297.55 = [app(l1, app(l2, l3))] 655.53/297.55 655.53/297.55 [app(nil(), l)] = 2 + l 655.53/297.55 > l 655.53/297.55 = [l] 655.53/297.55 655.53/297.55 [app(cons(x, l1), l2)] = 4 + l1 + l2 655.53/297.55 >= 4 + l1 + l2 655.53/297.55 = [cons(x, app(l1, l2))] 655.53/297.55 655.53/297.56 [mem(x, nil())] = 655.53/297.56 >= 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [mem(x, cons(y, l))] = 655.53/297.56 >= 655.53/297.56 = [ifmem(eq(x, y), x, l)] 655.53/297.56 655.53/297.56 [ifmem(true(), x, l)] = 655.53/297.56 >= 655.53/297.56 = [true()] 655.53/297.56 655.53/297.56 [ifmem(false(), x, l)] = 655.53/297.56 >= 655.53/297.56 = [mem(x, l)] 655.53/297.56 655.53/297.56 [inter(l1, app(l2, l3))] = 6*l1 + 2*l1*l2 + 2*l1*l3 + 4 + 2*l2 + 2*l3 655.53/297.56 > 2 + 4*l1 + 2*l1*l2 + 2*l2 + 2*l1*l3 + 2*l3 655.53/297.56 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.56 655.53/297.56 [inter(x, nil())] = 2*x 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(l1, cons(x, l2))] = 6*l1 + 2*l1*l2 + 4 + 2*l2 655.53/297.56 > 2 + 2*l2 + 2*l2*l1 + 2*l1 655.53/297.56 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.56 655.53/297.56 [inter(app(l1, l2), l3)] = 4 + 2*l1 + 2*l2 + 6*l3 + 2*l1*l3 + 2*l2*l3 655.53/297.56 > 2 + 2*l1 + 2*l1*l3 + 4*l3 + 2*l2 + 2*l2*l3 655.53/297.56 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.56 655.53/297.56 [inter(nil(), x)] = 2*x 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(cons(x, l1), l2)] = 4 + 2*l1 + 6*l2 + 2*l1*l2 655.53/297.56 > 2 + 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.56 655.53/297.56 [ifinter(true(), x, l1, l2)] = 2 + 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 >= 2 + 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 = [cons(x, inter(l1, l2))] 655.53/297.56 655.53/297.56 [ifinter(false(), x, l1, l2)] = 2 + 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 > 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 = [inter(l1, l2)] 655.53/297.56 655.53/297.56 655.53/297.56 We return to the main proof. 655.53/297.56 655.53/297.56 We are left with following problem, upon which TcT provides the 655.53/297.56 certificate YES(O(1),O(n^2)). 655.53/297.56 655.53/297.56 Strict Trs: 655.53/297.56 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.56 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.56 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) } 655.53/297.56 Weak Trs: 655.53/297.56 { if(true(), x, y) -> x 655.53/297.56 , if(false(), x, y) -> y 655.53/297.56 , eq(0(), 0()) -> true() 655.53/297.56 , eq(0(), s(x)) -> false() 655.53/297.56 , eq(s(x), 0()) -> false() 655.53/297.56 , app(nil(), l) -> l 655.53/297.56 , mem(x, nil()) -> false() 655.53/297.56 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.56 , ifmem(true(), x, l) -> true() 655.53/297.56 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.56 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.56 , inter(x, nil()) -> nil() 655.53/297.56 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.56 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.56 , inter(nil(), x) -> nil() 655.53/297.56 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.56 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.56 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.56 Obligation: 655.53/297.56 innermost runtime complexity 655.53/297.56 Answer: 655.53/297.56 YES(O(1),O(n^2)) 655.53/297.56 655.53/297.56 We use the processor 'polynomial interpretation' to orient 655.53/297.56 following rules strictly. 655.53/297.56 655.53/297.56 Trs: { app(cons(x, l1), l2) -> cons(x, app(l1, l2)) } 655.53/297.56 655.53/297.56 The induced complexity on above rules (modulo remaining rules) is 655.53/297.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 655.53/297.56 component(s). 655.53/297.56 655.53/297.56 Sub-proof: 655.53/297.56 ---------- 655.53/297.56 We consider the following typing: 655.53/297.56 655.53/297.56 if :: (b,a,a) -> a 655.53/297.56 true :: b 655.53/297.56 false :: b 655.53/297.56 eq :: (c,c) -> b 655.53/297.56 0 :: c 655.53/297.56 s :: c -> c 655.53/297.56 app :: (d,d) -> d 655.53/297.56 nil :: d 655.53/297.56 cons :: (c,d) -> d 655.53/297.56 mem :: (c,d) -> b 655.53/297.56 ifmem :: (b,c,d) -> b 655.53/297.56 inter :: (d,d) -> d 655.53/297.56 ifinter :: (b,c,d,d) -> d 655.53/297.56 655.53/297.56 The following argument positions are considered usable: 655.53/297.56 655.53/297.56 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.56 Uargs(ifinter) = {1} 655.53/297.56 655.53/297.56 TcT has computed the following constructor-restricted 655.53/297.56 typedpolynomial interpretation. 655.53/297.56 655.53/297.56 [if](x1, x2, x3) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 655.53/297.56 655.53/297.56 [true]() = 1 655.53/297.56 655.53/297.56 [false]() = 0 655.53/297.56 655.53/297.56 [eq](x1, x2) = 1 655.53/297.56 655.53/297.56 [0]() = 0 655.53/297.56 655.53/297.56 [s](x1) = 0 655.53/297.56 655.53/297.56 [app](x1, x2) = 2*x1 + x2 655.53/297.56 655.53/297.56 [nil]() = 0 655.53/297.56 655.53/297.56 [cons](x1, x2) = 2 + x2 655.53/297.56 655.53/297.56 [mem](x1, x2) = 2*x2 655.53/297.56 655.53/297.56 [ifmem](x1, x2, x3) = 2*x1 + 2*x1^2 + 2*x3 655.53/297.56 655.53/297.56 [inter](x1, x2) = 2*x1*x2 655.53/297.56 655.53/297.56 [ifinter](x1, x2, x3, x4) = 2*x1 + 2*x3*x4 655.53/297.56 655.53/297.56 655.53/297.56 This order satisfies the following ordering constraints. 655.53/297.56 655.53/297.56 [if(true(), x, y)] = 3 + 6*x + 6*y 655.53/297.56 > x 655.53/297.56 = [x] 655.53/297.56 655.53/297.56 [if(false(), x, y)] = 3 + 3*x + 3*y 655.53/297.56 > y 655.53/297.56 = [y] 655.53/297.56 655.53/297.56 [eq(0(), 0())] = 1 655.53/297.56 >= 1 655.53/297.56 = [true()] 655.53/297.56 655.53/297.56 [eq(0(), s(x))] = 1 655.53/297.56 > 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [eq(s(x), 0())] = 1 655.53/297.56 > 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [eq(s(x), s(y))] = 1 655.53/297.56 >= 1 655.53/297.56 = [eq(x, y)] 655.53/297.56 655.53/297.56 [app(app(l1, l2), l3)] = 4*l1 + 2*l2 + l3 655.53/297.56 >= 2*l1 + 2*l2 + l3 655.53/297.56 = [app(l1, app(l2, l3))] 655.53/297.56 655.53/297.56 [app(nil(), l)] = l 655.53/297.56 >= l 655.53/297.56 = [l] 655.53/297.56 655.53/297.56 [app(cons(x, l1), l2)] = 4 + 2*l1 + l2 655.53/297.56 > 2 + 2*l1 + l2 655.53/297.56 = [cons(x, app(l1, l2))] 655.53/297.56 655.53/297.56 [mem(x, nil())] = 655.53/297.56 >= 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [mem(x, cons(y, l))] = 4 + 2*l 655.53/297.56 >= 4 + 2*l 655.53/297.56 = [ifmem(eq(x, y), x, l)] 655.53/297.56 655.53/297.56 [ifmem(true(), x, l)] = 4 + 2*l 655.53/297.56 > 1 655.53/297.56 = [true()] 655.53/297.56 655.53/297.56 [ifmem(false(), x, l)] = 2*l 655.53/297.56 >= 2*l 655.53/297.56 = [mem(x, l)] 655.53/297.56 655.53/297.56 [inter(l1, app(l2, l3))] = 4*l1*l2 + 2*l1*l3 655.53/297.56 >= 4*l1*l2 + 2*l1*l3 655.53/297.56 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.56 655.53/297.56 [inter(x, nil())] = 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(l1, cons(x, l2))] = 4*l1 + 2*l1*l2 655.53/297.56 >= 4*l1 + 2*l2*l1 655.53/297.56 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.56 655.53/297.56 [inter(app(l1, l2), l3)] = 4*l1*l3 + 2*l2*l3 655.53/297.56 >= 4*l1*l3 + 2*l2*l3 655.53/297.56 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.56 655.53/297.56 [inter(nil(), x)] = 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(cons(x, l1), l2)] = 4*l2 + 2*l1*l2 655.53/297.56 >= 4*l2 + 2*l1*l2 655.53/297.56 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.56 655.53/297.56 [ifinter(true(), x, l1, l2)] = 2 + 2*l1*l2 655.53/297.56 >= 2 + 2*l1*l2 655.53/297.56 = [cons(x, inter(l1, l2))] 655.53/297.56 655.53/297.56 [ifinter(false(), x, l1, l2)] = 2*l1*l2 655.53/297.56 >= 2*l1*l2 655.53/297.56 = [inter(l1, l2)] 655.53/297.56 655.53/297.56 655.53/297.56 We return to the main proof. 655.53/297.56 655.53/297.56 We are left with following problem, upon which TcT provides the 655.53/297.56 certificate YES(O(1),O(n^2)). 655.53/297.56 655.53/297.56 Strict Trs: 655.53/297.56 { eq(s(x), s(y)) -> eq(x, y) 655.53/297.56 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) } 655.53/297.56 Weak Trs: 655.53/297.56 { if(true(), x, y) -> x 655.53/297.56 , if(false(), x, y) -> y 655.53/297.56 , eq(0(), 0()) -> true() 655.53/297.56 , eq(0(), s(x)) -> false() 655.53/297.56 , eq(s(x), 0()) -> false() 655.53/297.56 , app(nil(), l) -> l 655.53/297.56 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.56 , mem(x, nil()) -> false() 655.53/297.56 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.56 , ifmem(true(), x, l) -> true() 655.53/297.56 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.56 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.56 , inter(x, nil()) -> nil() 655.53/297.56 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.56 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.56 , inter(nil(), x) -> nil() 655.53/297.56 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.56 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.56 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.56 Obligation: 655.53/297.56 innermost runtime complexity 655.53/297.56 Answer: 655.53/297.56 YES(O(1),O(n^2)) 655.53/297.56 655.53/297.56 We use the processor 'polynomial interpretation' to orient 655.53/297.56 following rules strictly. 655.53/297.56 655.53/297.56 Trs: { app(app(l1, l2), l3) -> app(l1, app(l2, l3)) } 655.53/297.56 655.53/297.56 The induced complexity on above rules (modulo remaining rules) is 655.53/297.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 655.53/297.56 component(s). 655.53/297.56 655.53/297.56 Sub-proof: 655.53/297.56 ---------- 655.53/297.56 We consider the following typing: 655.53/297.56 655.53/297.56 if :: (b,a,a) -> a 655.53/297.56 true :: b 655.53/297.56 false :: b 655.53/297.56 eq :: (c,c) -> b 655.53/297.56 0 :: c 655.53/297.56 s :: c -> c 655.53/297.56 app :: (d,d) -> d 655.53/297.56 nil :: d 655.53/297.56 cons :: (c,d) -> d 655.53/297.56 mem :: (c,d) -> b 655.53/297.56 ifmem :: (b,c,d) -> b 655.53/297.56 inter :: (d,d) -> d 655.53/297.56 ifinter :: (b,c,d,d) -> d 655.53/297.56 655.53/297.56 The following argument positions are considered usable: 655.53/297.56 655.53/297.56 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.56 Uargs(ifinter) = {1} 655.53/297.56 655.53/297.56 TcT has computed the following constructor-restricted 655.53/297.56 typedpolynomial interpretation. 655.53/297.56 655.53/297.56 [if](x1, x2, x3) = 3 + 3*x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 655.53/297.56 655.53/297.56 [true]() = 0 655.53/297.56 655.53/297.56 [false]() = 0 655.53/297.56 655.53/297.56 [eq](x1, x2) = 0 655.53/297.56 655.53/297.56 [0]() = 0 655.53/297.56 655.53/297.56 [s](x1) = 0 655.53/297.56 655.53/297.56 [app](x1, x2) = 2 + 2*x1 + x2 655.53/297.56 655.53/297.56 [nil]() = 0 655.53/297.56 655.53/297.56 [cons](x1, x2) = x2 655.53/297.56 655.53/297.56 [mem](x1, x2) = 0 655.53/297.56 655.53/297.56 [ifmem](x1, x2, x3) = 2*x1 655.53/297.56 655.53/297.56 [inter](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 655.53/297.56 655.53/297.56 [ifinter](x1, x2, x3, x4) = 2*x1 + 2*x3 + 2*x3*x4 + 2*x4 655.53/297.56 655.53/297.56 655.53/297.56 This order satisfies the following ordering constraints. 655.53/297.56 655.53/297.56 [if(true(), x, y)] = 3 + 3*x + 3*y 655.53/297.56 > x 655.53/297.56 = [x] 655.53/297.56 655.53/297.56 [if(false(), x, y)] = 3 + 3*x + 3*y 655.53/297.56 > y 655.53/297.56 = [y] 655.53/297.56 655.53/297.56 [eq(0(), 0())] = 655.53/297.56 >= 655.53/297.56 = [true()] 655.53/297.56 655.53/297.56 [eq(0(), s(x))] = 655.53/297.56 >= 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [eq(s(x), 0())] = 655.53/297.56 >= 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [eq(s(x), s(y))] = 655.53/297.56 >= 655.53/297.56 = [eq(x, y)] 655.53/297.56 655.53/297.56 [app(app(l1, l2), l3)] = 6 + 4*l1 + 2*l2 + l3 655.53/297.56 > 4 + 2*l1 + 2*l2 + l3 655.53/297.56 = [app(l1, app(l2, l3))] 655.53/297.56 655.53/297.56 [app(nil(), l)] = 2 + l 655.53/297.56 > l 655.53/297.56 = [l] 655.53/297.56 655.53/297.56 [app(cons(x, l1), l2)] = 2 + 2*l1 + l2 655.53/297.56 >= 2 + 2*l1 + l2 655.53/297.56 = [cons(x, app(l1, l2))] 655.53/297.56 655.53/297.56 [mem(x, nil())] = 655.53/297.56 >= 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [mem(x, cons(y, l))] = 655.53/297.56 >= 655.53/297.56 = [ifmem(eq(x, y), x, l)] 655.53/297.56 655.53/297.56 [ifmem(true(), x, l)] = 655.53/297.56 >= 655.53/297.56 = [true()] 655.53/297.56 655.53/297.56 [ifmem(false(), x, l)] = 655.53/297.56 >= 655.53/297.56 = [mem(x, l)] 655.53/297.56 655.53/297.56 [inter(l1, app(l2, l3))] = 6*l1 + 4*l1*l2 + 2*l1*l3 + 4 + 4*l2 + 2*l3 655.53/297.56 > 2 + 6*l1 + 4*l1*l2 + 4*l2 + 2*l1*l3 + 2*l3 655.53/297.56 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.56 655.53/297.56 [inter(x, nil())] = 2*x 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(l1, cons(x, l2))] = 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 >= 2*l2 + 2*l2*l1 + 2*l1 655.53/297.56 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.56 655.53/297.56 [inter(app(l1, l2), l3)] = 4 + 4*l1 + 2*l2 + 6*l3 + 4*l1*l3 + 2*l2*l3 655.53/297.56 > 2 + 4*l1 + 4*l1*l3 + 6*l3 + 2*l2 + 2*l2*l3 655.53/297.56 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.56 655.53/297.56 [inter(nil(), x)] = 2*x 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(cons(x, l1), l2)] = 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 >= 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.56 655.53/297.56 [ifinter(true(), x, l1, l2)] = 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 >= 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 = [cons(x, inter(l1, l2))] 655.53/297.56 655.53/297.56 [ifinter(false(), x, l1, l2)] = 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 >= 2*l1 + 2*l1*l2 + 2*l2 655.53/297.56 = [inter(l1, l2)] 655.53/297.56 655.53/297.56 655.53/297.56 We return to the main proof. 655.53/297.56 655.53/297.56 We are left with following problem, upon which TcT provides the 655.53/297.56 certificate YES(O(1),O(n^2)). 655.53/297.56 655.53/297.56 Strict Trs: { eq(s(x), s(y)) -> eq(x, y) } 655.53/297.56 Weak Trs: 655.53/297.56 { if(true(), x, y) -> x 655.53/297.56 , if(false(), x, y) -> y 655.53/297.56 , eq(0(), 0()) -> true() 655.53/297.56 , eq(0(), s(x)) -> false() 655.53/297.56 , eq(s(x), 0()) -> false() 655.53/297.56 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.56 , app(nil(), l) -> l 655.53/297.56 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.56 , mem(x, nil()) -> false() 655.53/297.56 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.56 , ifmem(true(), x, l) -> true() 655.53/297.56 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.56 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.56 , inter(x, nil()) -> nil() 655.53/297.56 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.56 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.56 , inter(nil(), x) -> nil() 655.53/297.56 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.56 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.56 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.56 Obligation: 655.53/297.56 innermost runtime complexity 655.53/297.56 Answer: 655.53/297.56 YES(O(1),O(n^2)) 655.53/297.56 655.53/297.56 We use the processor 'polynomial interpretation' to orient 655.53/297.56 following rules strictly. 655.53/297.56 655.53/297.56 Trs: { eq(s(x), s(y)) -> eq(x, y) } 655.53/297.56 655.53/297.56 The induced complexity on above rules (modulo remaining rules) is 655.53/297.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 655.53/297.56 component(s). 655.53/297.56 655.53/297.56 Sub-proof: 655.53/297.56 ---------- 655.53/297.56 We consider the following typing: 655.53/297.56 655.53/297.56 if :: (b,a,a) -> a 655.53/297.56 true :: b 655.53/297.56 false :: b 655.53/297.56 eq :: (c,c) -> b 655.53/297.56 0 :: c 655.53/297.56 s :: c -> c 655.53/297.56 app :: (d,d) -> d 655.53/297.56 nil :: d 655.53/297.56 cons :: (c,d) -> d 655.53/297.56 mem :: (c,d) -> b 655.53/297.56 ifmem :: (b,c,d) -> b 655.53/297.56 inter :: (d,d) -> d 655.53/297.56 ifinter :: (b,c,d,d) -> d 655.53/297.56 655.53/297.56 The following argument positions are considered usable: 655.53/297.56 655.53/297.56 Uargs(app) = {1, 2}, Uargs(cons) = {2}, Uargs(ifmem) = {1}, 655.53/297.56 Uargs(ifinter) = {1} 655.53/297.56 655.53/297.56 TcT has computed the following constructor-restricted 655.53/297.56 typedpolynomial interpretation. 655.53/297.56 655.53/297.56 [if](x1, x2, x3) = 3 + x1*x2 + 3*x1*x3 + 3*x2 + 3*x3 655.53/297.56 655.53/297.56 [true]() = 2 655.53/297.56 655.53/297.56 [false]() = 0 655.53/297.56 655.53/297.56 [eq](x1, x2) = x2 655.53/297.56 655.53/297.56 [0]() = 2 655.53/297.56 655.53/297.56 [s](x1) = 1 + x1 655.53/297.56 655.53/297.56 [app](x1, x2) = 2*x1 + x2 655.53/297.56 655.53/297.56 [nil]() = 0 655.53/297.56 655.53/297.56 [cons](x1, x2) = 1 + 2*x1 + x2 655.53/297.56 655.53/297.56 [mem](x1, x2) = x2 655.53/297.56 655.53/297.56 [ifmem](x1, x2, x3) = 2*x1 + x3 655.53/297.56 655.53/297.56 [inter](x1, x2) = 2*x1*x2 655.53/297.56 655.53/297.56 [ifinter](x1, x2, x3, x4) = 2*x1 + x1*x2 + 2*x3*x4 655.53/297.56 655.53/297.56 655.53/297.56 This order satisfies the following ordering constraints. 655.53/297.56 655.53/297.56 [if(true(), x, y)] = 3 + 5*x + 9*y 655.53/297.56 > x 655.53/297.56 = [x] 655.53/297.56 655.53/297.56 [if(false(), x, y)] = 3 + 3*x + 3*y 655.53/297.56 > y 655.53/297.56 = [y] 655.53/297.56 655.53/297.56 [eq(0(), 0())] = 2 655.53/297.56 >= 2 655.53/297.56 = [true()] 655.53/297.56 655.53/297.56 [eq(0(), s(x))] = 1 + x 655.53/297.56 > 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [eq(s(x), 0())] = 2 655.53/297.56 > 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [eq(s(x), s(y))] = 1 + y 655.53/297.56 > y 655.53/297.56 = [eq(x, y)] 655.53/297.56 655.53/297.56 [app(app(l1, l2), l3)] = 4*l1 + 2*l2 + l3 655.53/297.56 >= 2*l1 + 2*l2 + l3 655.53/297.56 = [app(l1, app(l2, l3))] 655.53/297.56 655.53/297.56 [app(nil(), l)] = l 655.53/297.56 >= l 655.53/297.56 = [l] 655.53/297.56 655.53/297.56 [app(cons(x, l1), l2)] = 2 + 4*x + 2*l1 + l2 655.53/297.56 > 1 + 2*x + 2*l1 + l2 655.53/297.56 = [cons(x, app(l1, l2))] 655.53/297.56 655.53/297.56 [mem(x, nil())] = 655.53/297.56 >= 655.53/297.56 = [false()] 655.53/297.56 655.53/297.56 [mem(x, cons(y, l))] = 1 + 2*y + l 655.53/297.56 > 2*y + l 655.53/297.56 = [ifmem(eq(x, y), x, l)] 655.53/297.56 655.53/297.56 [ifmem(true(), x, l)] = 4 + l 655.53/297.56 > 2 655.53/297.56 = [true()] 655.53/297.56 655.53/297.56 [ifmem(false(), x, l)] = l 655.53/297.56 >= l 655.53/297.56 = [mem(x, l)] 655.53/297.56 655.53/297.56 [inter(l1, app(l2, l3))] = 4*l1*l2 + 2*l1*l3 655.53/297.56 >= 4*l1*l2 + 2*l1*l3 655.53/297.56 = [app(inter(l1, l2), inter(l1, l3))] 655.53/297.56 655.53/297.56 [inter(x, nil())] = 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(l1, cons(x, l2))] = 2*l1 + 4*l1*x + 2*l1*l2 655.53/297.56 >= 2*l1 + l1*x + 2*l2*l1 655.53/297.56 = [ifinter(mem(x, l1), x, l2, l1)] 655.53/297.56 655.53/297.56 [inter(app(l1, l2), l3)] = 4*l1*l3 + 2*l2*l3 655.53/297.56 >= 4*l1*l3 + 2*l2*l3 655.53/297.56 = [app(inter(l1, l3), inter(l2, l3))] 655.53/297.56 655.53/297.56 [inter(nil(), x)] = 655.53/297.56 >= 655.53/297.56 = [nil()] 655.53/297.56 655.53/297.56 [inter(cons(x, l1), l2)] = 2*l2 + 4*x*l2 + 2*l1*l2 655.53/297.56 >= 2*l2 + l2*x + 2*l1*l2 655.53/297.56 = [ifinter(mem(x, l2), x, l1, l2)] 655.53/297.56 655.53/297.56 [ifinter(true(), x, l1, l2)] = 4 + 2*x + 2*l1*l2 655.53/297.56 > 1 + 2*x + 2*l1*l2 655.53/297.56 = [cons(x, inter(l1, l2))] 655.53/297.56 655.53/297.56 [ifinter(false(), x, l1, l2)] = 2*l1*l2 655.53/297.56 >= 2*l1*l2 655.53/297.56 = [inter(l1, l2)] 655.53/297.56 655.53/297.56 655.53/297.56 We return to the main proof. 655.53/297.56 655.53/297.56 We are left with following problem, upon which TcT provides the 655.53/297.56 certificate YES(O(1),O(1)). 655.53/297.56 655.53/297.56 Weak Trs: 655.53/297.56 { if(true(), x, y) -> x 655.53/297.56 , if(false(), x, y) -> y 655.53/297.56 , eq(0(), 0()) -> true() 655.53/297.56 , eq(0(), s(x)) -> false() 655.53/297.56 , eq(s(x), 0()) -> false() 655.53/297.56 , eq(s(x), s(y)) -> eq(x, y) 655.53/297.56 , app(app(l1, l2), l3) -> app(l1, app(l2, l3)) 655.53/297.56 , app(nil(), l) -> l 655.53/297.56 , app(cons(x, l1), l2) -> cons(x, app(l1, l2)) 655.53/297.56 , mem(x, nil()) -> false() 655.53/297.56 , mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l) 655.53/297.56 , ifmem(true(), x, l) -> true() 655.53/297.56 , ifmem(false(), x, l) -> mem(x, l) 655.53/297.56 , inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) 655.53/297.56 , inter(x, nil()) -> nil() 655.53/297.56 , inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) 655.53/297.56 , inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) 655.53/297.56 , inter(nil(), x) -> nil() 655.53/297.56 , inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) 655.53/297.56 , ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2)) 655.53/297.56 , ifinter(false(), x, l1, l2) -> inter(l1, l2) } 655.53/297.56 Obligation: 655.53/297.56 innermost runtime complexity 655.53/297.56 Answer: 655.53/297.56 YES(O(1),O(1)) 655.53/297.56 655.53/297.56 Empty rules are trivially bounded 655.53/297.56 655.53/297.56 Hurray, we answered YES(O(1),O(n^2)) 655.90/297.85 EOF