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