YES TRS: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} DP: Strict: { +#(0(x), 0(y)) -> 0#(+(x, y)), +#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))), +#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())), -#(0(x), 0(y)) -> 0#(-(x, y)), -#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y)), -#(1(x), 1(y)) -> -#(x, y), eq#(#(), 0(y)) -> eq#(#(), y), eq#(0(x), #()) -> eq#(x, #()), eq#(0(x), 0(y)) -> eq#(x, y), eq#(1(x), 1(y)) -> eq#(x, y), ge#(#(), 0(x)) -> ge#(#(), x), ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x)), ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y), log'#(0(x)) -> +#(log'(x), 1(#())), log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'#(0(x)) -> ge#(x, 1(#())), log'#(0(x)) -> log'#(x), log'#(1(x)) -> +#(log'(x), 1(#())), log'#(1(x)) -> log'#(x), log#(x) -> -#(log'(x), 1(#())), log#(x) -> log'#(x), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)), *#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> 0#(*(x, y)), *#(0(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)), *#(1(x), y) -> +#(0(*(x, y)), y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z), app#(cons(x, l1), l2) -> app#(l1, l2), sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l2), sum#(nil()) -> 0#(#()), sum#(cons(x, l)) -> +#(x, sum(l)), sum#(cons(x, l)) -> sum#(l), prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> *#(x, prod(l)), prod#(cons(x, l)) -> prod#(l), mem#(x, cons(y, l)) -> if#(eq(x, y), true(), mem(x, l)), mem#(x, cons(y, l)) -> eq#(x, y), mem#(x, cons(y, l)) -> mem#(x, l), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3)), inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, cons(x, l2)) -> mem#(x, l1), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1), inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3)), inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(cons(x, l1), l2) -> mem#(x, l2), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2), ifinter#(false(), x, l1, l2) -> inter#(l1, l2), ifinter#(true(), x, l1, l2) -> inter#(l1, l2)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} EDG: { (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y)) (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y)) (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y)) (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y)) (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y))) (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y)) (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y)) (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y)) (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y)) (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y))) (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y)) (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y))) (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y)) (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y)) (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y)) (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y))) (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y)) (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y))) (-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y)) (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y)) (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y)) (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y))) (eq#(0(x), 0(y)) -> eq#(x, y), eq#(1(x), 1(y)) -> eq#(x, y)) (eq#(0(x), 0(y)) -> eq#(x, y), eq#(0(x), 0(y)) -> eq#(x, y)) (eq#(0(x), 0(y)) -> eq#(x, y), eq#(0(x), #()) -> eq#(x, #())) (eq#(0(x), 0(y)) -> eq#(x, y), eq#(#(), 0(y)) -> eq#(#(), y)) (ge#(0(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y)) (ge#(0(x), 0(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y)) (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x)) (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x))) (ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y)) (ge#(0(x), 0(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x)) (ge#(1(x), 1(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y)) (ge#(1(x), 1(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y)) (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x)) (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x))) (ge#(1(x), 1(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y)) (ge#(1(x), 1(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x)) (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y))) (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y))) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (mem#(x, cons(y, l)) -> eq#(x, y), eq#(1(x), 1(y)) -> eq#(x, y)) (mem#(x, cons(y, l)) -> eq#(x, y), eq#(0(x), 0(y)) -> eq#(x, y)) (mem#(x, cons(y, l)) -> eq#(x, y), eq#(0(x), #()) -> eq#(x, #())) (mem#(x, cons(y, l)) -> eq#(x, y), eq#(#(), 0(y)) -> eq#(#(), y)) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y)) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(y, z)) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y)) (log'#(0(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (log'#(0(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(x, y)) (log'#(0(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (log'#(0(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(y, z)) (log'#(0(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z))) (log'#(0(x)) -> +#(log'(x), 1(#())), +#(0(x), 1(y)) -> +#(x, y)) (log'#(1(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (log'#(1(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> +#(x, y)) (log'#(1(x)) -> +#(log'(x), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (log'#(1(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(y, z)) (log'#(1(x)) -> +#(log'(x), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z))) (log'#(1(x)) -> +#(log'(x), 1(#())), +#(0(x), 1(y)) -> +#(x, y)) (sum#(app(l1, l2)) -> sum#(l2), sum#(cons(x, l)) -> sum#(l)) (sum#(app(l1, l2)) -> sum#(l2), sum#(cons(x, l)) -> +#(x, sum(l))) (sum#(app(l1, l2)) -> sum#(l2), sum#(nil()) -> 0#(#())) (sum#(app(l1, l2)) -> sum#(l2), sum#(app(l1, l2)) -> sum#(l2)) (sum#(app(l1, l2)) -> sum#(l2), sum#(app(l1, l2)) -> sum#(l1)) (sum#(app(l1, l2)) -> sum#(l2), sum#(app(l1, l2)) -> +#(sum(l1), sum(l2))) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(cons(x, l1), l2) -> mem#(x, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3))) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, cons(x, l2)) -> mem#(x, l1)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3))) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(cons(x, l1), l2) -> mem#(x, l2)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3))) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, cons(x, l2)) -> mem#(x, l1)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3))) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 1(y)) -> +#(x, y)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 0(y)) -> +#(x, y)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(y, z)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(0(x), 1(y)) -> +#(x, y)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(0(x), 0(y)) -> +#(x, y)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(0(x), 0(y)) -> 0#(+(x, y))) (inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3)), app#(cons(x, l1), l2) -> app#(l1, l2)) (inter#(l1, cons(x, l2)) -> mem#(x, l1), mem#(x, cons(y, l)) -> mem#(x, l)) (inter#(l1, cons(x, l2)) -> mem#(x, l1), mem#(x, cons(y, l)) -> eq#(x, y)) (inter#(l1, cons(x, l2)) -> mem#(x, l1), mem#(x, cons(y, l)) -> if#(eq(x, y), true(), mem(x, l))) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> 0#(+(x, y))) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1), ifinter#(true(), x, l1, l2) -> inter#(l1, l2)) (inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1), ifinter#(false(), x, l1, l2) -> inter#(l1, l2)) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(1(x), 1(y)) -> +#(x, y)) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(1(x), 0(y)) -> +#(x, y)) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(+(x, y), z) -> +#(y, z)) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(+(x, y), z) -> +#(x, +(y, z))) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(0(x), 1(y)) -> +#(x, y)) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(0(x), 0(y)) -> +#(x, y)) (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(0(x), 0(y)) -> 0#(+(x, y))) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(*(x, y), z) -> *#(y, z)) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(*(x, y), z) -> *#(x, *(y, z))) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(1(x), y) -> *#(x, y)) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(1(x), y) -> +#(0(*(x, y)), y)) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(1(x), y) -> 0#(*(x, y))) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(0(x), y) -> *#(x, y)) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(0(x), y) -> 0#(*(x, y))) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(x, +(y, z)) -> *#(x, z)) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(x, +(y, z)) -> *#(x, y)) (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 1(y)) -> ge#(x, y)) (ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 0(y)) -> ge#(x, y)) (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 1(y)) -> ge#(y, x)) (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 1(y)) -> not#(ge(y, x))) (ge#(0(x), 1(y)) -> ge#(y, x), ge#(0(x), 0(y)) -> ge#(x, y)) (ge#(0(x), 1(y)) -> ge#(y, x), ge#(#(), 0(x)) -> ge#(#(), x)) (prod#(app(l1, l2)) -> prod#(l1), prod#(cons(x, l)) -> prod#(l)) (prod#(app(l1, l2)) -> prod#(l1), prod#(cons(x, l)) -> *#(x, prod(l))) (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l2)) (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l1)) (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> *#(prod(l1), prod(l2))) (log'#(0(x)) -> log'#(x), log'#(1(x)) -> log'#(x)) (log'#(0(x)) -> log'#(x), log'#(1(x)) -> +#(log'(x), 1(#()))) (log'#(0(x)) -> log'#(x), log'#(0(x)) -> log'#(x)) (log'#(0(x)) -> log'#(x), log'#(0(x)) -> ge#(x, 1(#()))) (log'#(0(x)) -> log'#(x), log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #())) (log'#(0(x)) -> log'#(x), log'#(0(x)) -> +#(log'(x), 1(#()))) (log#(x) -> log'#(x), log'#(1(x)) -> log'#(x)) (log#(x) -> log'#(x), log'#(1(x)) -> +#(log'(x), 1(#()))) (log#(x) -> log'#(x), log'#(0(x)) -> log'#(x)) (log#(x) -> log'#(x), log'#(0(x)) -> ge#(x, 1(#()))) (log#(x) -> log'#(x), log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #())) (log#(x) -> log'#(x), log'#(0(x)) -> +#(log'(x), 1(#()))) (sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> sum#(l)) (sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> +#(x, sum(l))) (sum#(cons(x, l)) -> sum#(l), sum#(nil()) -> 0#(#())) (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> sum#(l2)) (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> sum#(l1)) (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> +#(sum(l1), sum(l2))) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(cons(x, l1), l2) -> mem#(x, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3))) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, cons(x, l2)) -> mem#(x, l1)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3))) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(cons(x, l1), l2) -> mem#(x, l2)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3))) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, cons(x, l2)) -> mem#(x, l1)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3))) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3))) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, cons(x, l2)) -> mem#(x, l1)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3))) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(cons(x, l1), l2) -> mem#(x, l2)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (inter#(cons(x, l1), l2) -> mem#(x, l2), mem#(x, cons(y, l)) -> if#(eq(x, y), true(), mem(x, l))) (inter#(cons(x, l1), l2) -> mem#(x, l2), mem#(x, cons(y, l)) -> eq#(x, y)) (inter#(cons(x, l1), l2) -> mem#(x, l2), mem#(x, cons(y, l)) -> mem#(x, l)) (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> *#(prod(l1), prod(l2))) (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> prod#(l1)) (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> prod#(l2)) (prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> *#(x, prod(l))) (prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> prod#(l)) (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2)) (ge#(#(), 0(x)) -> ge#(#(), x), ge#(#(), 0(x)) -> ge#(#(), x)) (log'#(1(x)) -> log'#(x), log'#(0(x)) -> +#(log'(x), 1(#()))) (log'#(1(x)) -> log'#(x), log'#(0(x)) -> if#(ge(x, 1(#())), +(log'(x), 1(#())), #())) (log'#(1(x)) -> log'#(x), log'#(0(x)) -> ge#(x, 1(#()))) (log'#(1(x)) -> log'#(x), log'#(0(x)) -> log'#(x)) (log'#(1(x)) -> log'#(x), log'#(1(x)) -> +#(log'(x), 1(#()))) (log'#(1(x)) -> log'#(x), log'#(1(x)) -> log'#(x)) (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> +#(sum(l1), sum(l2))) (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l1)) (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l2)) (sum#(app(l1, l2)) -> sum#(l1), sum#(nil()) -> 0#(#())) (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> +#(x, sum(l))) (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l)) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(x, +(y, z)) -> *#(x, y)) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(x, +(y, z)) -> *#(x, z)) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(0(x), y) -> 0#(*(x, y))) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(0(x), y) -> *#(x, y)) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> 0#(*(x, y))) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> +#(0(*(x, y)), y)) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> *#(x, y)) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(*(x, y), z) -> *#(x, *(y, z))) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(*(x, y), z) -> *#(y, z)) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 0(y)) -> 0#(+(x, y))) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 0(y)) -> +#(x, y)) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 1(y)) -> +#(x, y)) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(+(x, y), z) -> +#(x, +(y, z))) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(+(x, y), z) -> +#(y, z)) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 0(y)) -> +#(x, y)) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> +#(x, y)) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (eq#(0(x), #()) -> eq#(x, #()), eq#(0(x), #()) -> eq#(x, #())) (inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2), ifinter#(false(), x, l1, l2) -> inter#(l1, l2)) (inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2), ifinter#(true(), x, l1, l2) -> inter#(l1, l2)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> 0#(*(x, y))) (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(1(x), y) -> 0#(*(x, y))) (*#(x, +(y, z)) -> *#(x, z), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(x, +(y, z)) -> *#(x, z), *#(1(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (eq#(#(), 0(y)) -> eq#(#(), y), eq#(#(), 0(y)) -> eq#(#(), y)) (inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3)), app#(cons(x, l1), l2) -> app#(l1, l2)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> 0#(+(x, y))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3))) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, cons(x, l2)) -> mem#(x, l1)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3))) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(cons(x, l1), l2) -> mem#(x, l2)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> *#(prod(l1), prod(l2))) (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> prod#(l1)) (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> prod#(l2)) (prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> *#(x, prod(l))) (prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l)) (log#(x) -> -#(log'(x), 1(#())), -#(0(x), 1(y)) -> -#(x, y)) (log#(x) -> -#(log'(x), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (log#(x) -> -#(log'(x), 1(#())), -#(1(x), 1(y)) -> 0#(-(x, y))) (log#(x) -> -#(log'(x), 1(#())), -#(1(x), 1(y)) -> -#(x, y)) (log'#(0(x)) -> ge#(x, 1(#())), ge#(0(x), 1(y)) -> not#(ge(y, x))) (log'#(0(x)) -> ge#(x, 1(#())), ge#(0(x), 1(y)) -> ge#(y, x)) (log'#(0(x)) -> ge#(x, 1(#())), ge#(1(x), 1(y)) -> ge#(x, y)) (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(x, y)) (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 1(y)) -> 0#(-(x, y))) (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 1(y)) -> -#(x, y)) (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y))) (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y))) (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y))) (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y))) (*#(x, +(y, z)) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(x, +(y, z)) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (ge#(1(x), 0(y)) -> ge#(x, y), ge#(#(), 0(x)) -> ge#(#(), x)) (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y)) (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> not#(ge(y, x))) (ge#(1(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x)) (ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 0(y)) -> ge#(x, y)) (ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y)) (eq#(1(x), 1(y)) -> eq#(x, y), eq#(#(), 0(y)) -> eq#(#(), y)) (eq#(1(x), 1(y)) -> eq#(x, y), eq#(0(x), #()) -> eq#(x, #())) (eq#(1(x), 1(y)) -> eq#(x, y), eq#(0(x), 0(y)) -> eq#(x, y)) (eq#(1(x), 1(y)) -> eq#(x, y), eq#(1(x), 1(y)) -> eq#(x, y)) (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y))) (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y)) (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y)) (-#(1(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y)) (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y))) (-#(1(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y)) (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> 0#(-(x, y))) (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y)) (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y)) (-#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y)) (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> 0#(-(x, y))) (-#(0(x), 1(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y)) (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y))) (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y)) (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y)) (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y)) (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y)) (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y))) (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y)) (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y)) (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y)) (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y)) (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (mem#(x, cons(y, l)) -> mem#(x, l), mem#(x, cons(y, l)) -> if#(eq(x, y), true(), mem(x, l))) (mem#(x, cons(y, l)) -> mem#(x, l), mem#(x, cons(y, l)) -> eq#(x, y)) (mem#(x, cons(y, l)) -> mem#(x, l), mem#(x, cons(y, l)) -> mem#(x, l)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> 0#(+(x, y))) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> +#(x, y)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 1(y)) -> +#(x, y)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(y, z)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 0(y)) -> +#(x, y)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(x, y)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) } SCCS: Scc: { inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1), inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2), ifinter#(false(), x, l1, l2) -> inter#(l1, l2), ifinter#(true(), x, l1, l2) -> inter#(l1, l2)} Scc: {mem#(x, cons(y, l)) -> mem#(x, l)} Scc: {prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l)} Scc: {sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l2), sum#(cons(x, l)) -> sum#(l)} Scc: {app#(cons(x, l1), l2) -> app#(l1, l2)} Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Scc: {log'#(0(x)) -> log'#(x), log'#(1(x)) -> log'#(x)} Scc: {ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y)} Scc: {ge#(#(), 0(x)) -> ge#(#(), x)} Scc: {eq#(0(x), 0(y)) -> eq#(x, y), eq#(1(x), 1(y)) -> eq#(x, y)} Scc: {eq#(0(x), #()) -> eq#(x, #())} Scc: {eq#(#(), 0(y)) -> eq#(#(), y)} Scc: {-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y)} Scc: {+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))} SCC: Strict: { inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1), inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2), ifinter#(false(), x, l1, l2) -> inter#(l1, l2), ifinter#(true(), x, l1, l2) -> inter#(l1, l2)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} POLY: Argument Filtering: pi(ifinter#) = [2,3], pi(ifinter) = [], pi(inter#) = [0,1], pi(inter) = [], pi(mem) = [], pi(prod) = [], pi(sum) = [], pi(cons) = [1], pi(nil) = [], pi(app) = [0,1], pi(*) = [], pi(log) = [], pi(log') = [], pi(ge) = [], pi(eq) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-) = [], pi(1) = [], pi(+) = [], pi(0) = [], pi(#) = [] Usable Rules: {} Interpretation: [ifinter#](x0, x1) = x0 + x1, [inter#](x0, x1) = x0 + x1, [cons](x0) = x0 + 1, [app](x0, x1) = x0 + x1 Strict: { inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3), ifinter#(false(), x, l1, l2) -> inter#(l1, l2), ifinter#(true(), x, l1, l2) -> inter#(l1, l2)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} EDG: {(inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3))} SCCS: Scc: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)} SCC: Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(inter#) = 0 Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)} EDG: {(inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3))} SCCS: Scc: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)} SCC: Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(inter#) = 1 Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)} EDG: {(inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, l2)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3))} SCCS: Scc: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)} SCC: Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l1, l3)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(inter#) = 0 Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l2)} EDG: {(inter#(l1, app(l2, l3)) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, l2))} SCCS: Scc: {inter#(l1, app(l2, l3)) -> inter#(l1, l2)} SCC: Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l2)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(inter#) = 1 Strict: {} Qed SCC: Strict: {mem#(x, cons(y, l)) -> mem#(x, l)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(mem#) = 1 Strict: {} Qed SCC: Strict: {prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(prod#) = 0 Strict: {prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l)} EDG: {(prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> prod#(l)) (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> prod#(l2)) (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> prod#(l2)) (prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l))} SCCS: Scc: {prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l)} SCC: Strict: {prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(prod#) = 0 Strict: {prod#(cons(x, l)) -> prod#(l)} EDG: {(prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> prod#(l))} SCCS: Scc: {prod#(cons(x, l)) -> prod#(l)} SCC: Strict: {prod#(cons(x, l)) -> prod#(l)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(prod#) = 0 Strict: {} Qed SCC: Strict: {sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l2), sum#(cons(x, l)) -> sum#(l)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(sum#) = 0 Strict: {sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l)} EDG: {(sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> sum#(l)) (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> sum#(l1)) (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l1)) (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l))} SCCS: Scc: {sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l)} SCC: Strict: {sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(sum#) = 0 Strict: {sum#(cons(x, l)) -> sum#(l)} EDG: {(sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> sum#(l))} SCCS: Scc: {sum#(cons(x, l)) -> sum#(l)} SCC: Strict: {sum#(cons(x, l)) -> sum#(l)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(sum#) = 0 Strict: {} Qed SCC: Strict: {app#(cons(x, l1), l2) -> app#(l1, l2)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(app#) = 0 Strict: {} Qed SCC: Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(1(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z))} SCCS: Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC: Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z))} SCCS: Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC: Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y)} EDG: {(*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y))} SCCS: Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y)} SCC: Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} EDG: {(*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))} SCCS: Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} SCC: Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(*#) = 1 Strict: {*#(x, +(y, z)) -> *#(x, z)} EDG: {(*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))} SCCS: Scc: {*#(x, +(y, z)) -> *#(x, z)} SCC: Strict: {*#(x, +(y, z)) -> *#(x, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(*#) = 1 Strict: {} Qed SCC: Strict: {log'#(0(x)) -> log'#(x), log'#(1(x)) -> log'#(x)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(log'#) = 0 Strict: {log'#(0(x)) -> log'#(x)} EDG: {(log'#(0(x)) -> log'#(x), log'#(0(x)) -> log'#(x))} SCCS: Scc: {log'#(0(x)) -> log'#(x)} SCC: Strict: {log'#(0(x)) -> log'#(x)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(log'#) = 0 Strict: {} Qed SCC: Strict: {ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 1(y)) -> ge#(y, x), ge#(1(x), 0(y)) -> ge#(x, y), ge#(1(x), 1(y)) -> ge#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} POLY: Argument Filtering: pi(ifinter) = [], pi(inter) = [], pi(mem) = [], pi(prod) = [], pi(sum) = [], pi(cons) = [], pi(nil) = [], pi(app) = [], pi(*) = [], pi(log) = [], pi(log') = [], pi(ge#) = [0,1], pi(ge) = [], pi(eq) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-) = [], pi(1) = [0], pi(+) = [], pi(0) = 0, pi(#) = [] Usable Rules: {} Interpretation: [ge#](x0, x1) = x0 + x1 + 1, [1](x0) = x0 + 1 Strict: {ge#(0(x), 0(y)) -> ge#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} EDG: {(ge#(0(x), 0(y)) -> ge#(x, y), ge#(0(x), 0(y)) -> ge#(x, y))} SCCS: Scc: {ge#(0(x), 0(y)) -> ge#(x, y)} SCC: Strict: {ge#(0(x), 0(y)) -> ge#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(ge#) = 0 Strict: {} Qed SCC: Strict: {ge#(#(), 0(x)) -> ge#(#(), x)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(ge#) = 1 Strict: {} Qed SCC: Strict: {eq#(0(x), 0(y)) -> eq#(x, y), eq#(1(x), 1(y)) -> eq#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(eq#) = 0 Strict: {eq#(0(x), 0(y)) -> eq#(x, y)} EDG: {(eq#(0(x), 0(y)) -> eq#(x, y), eq#(0(x), 0(y)) -> eq#(x, y))} SCCS: Scc: {eq#(0(x), 0(y)) -> eq#(x, y)} SCC: Strict: {eq#(0(x), 0(y)) -> eq#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(eq#) = 0 Strict: {} Qed SCC: Strict: {eq#(0(x), #()) -> eq#(x, #())} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(eq#) = 0 Strict: {} Qed SCC: Strict: {eq#(#(), 0(y)) -> eq#(#(), y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(eq#) = 1 Strict: {} Qed SCC: Strict: {-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 0(y)) -> -#(x, y), -#(1(x), 1(y)) -> -#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} POLY: Argument Filtering: pi(ifinter) = [], pi(inter) = [], pi(mem) = [], pi(prod) = [], pi(sum) = [], pi(cons) = [], pi(nil) = [], pi(app) = [], pi(*) = [], pi(log) = [], pi(log') = [], pi(ge) = [], pi(eq) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-#) = [1], pi(-) = [], pi(1) = [0], pi(+) = [], pi(0) = 0, pi(#) = [] Usable Rules: {} Interpretation: [-#](x0) = x0 + 1, [1](x0) = x0 + 1, [#] = 0 Strict: {-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(1(x), 0(y)) -> -#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} EDG: {(-#(1(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y)) (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(1(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y)) (-#(0(x), 1(y)) -> -#(-(x, y), 1(#())), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y)) (-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 1(y)) -> -#(-(x, y), 1(#()))) (-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y))} SCCS: Scc: {-#(0(x), 1(y)) -> -#(-(x, y), 1(#()))} Scc: {-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y)} SCC: Strict: {-#(0(x), 1(y)) -> -#(-(x, y), 1(#()))} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} POLY: Argument Filtering: pi(ifinter) = [], pi(inter) = [], pi(mem) = [], pi(prod) = [], pi(sum) = [], pi(cons) = [], pi(nil) = [], pi(app) = [], pi(*) = [], pi(log) = [], pi(log') = [], pi(ge) = [], pi(eq) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-#) = [0], pi(-) = 0, pi(1) = [0], pi(+) = [], pi(0) = [0], pi(#) = [] Usable Rules: {} Interpretation: [-#](x0) = x0 + 1, [0](x0) = x0 + 1 Strict: {} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} Qed SCC: Strict: {-#(0(x), 0(y)) -> -#(x, y), -#(1(x), 0(y)) -> -#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(-#) = 0 Strict: {-#(0(x), 0(y)) -> -#(x, y)} EDG: {(-#(0(x), 0(y)) -> -#(x, y), -#(0(x), 0(y)) -> -#(x, y))} SCCS: Scc: {-#(0(x), 0(y)) -> -#(x, y)} SCC: Strict: {-#(0(x), 0(y)) -> -#(x, y)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(-#) = 0 Strict: {} Qed SCC: Strict: {+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} POLY: Argument Filtering: pi(ifinter) = [], pi(inter) = [], pi(mem) = [], pi(prod) = [], pi(sum) = [], pi(cons) = [], pi(nil) = [], pi(app) = [], pi(*) = [], pi(log) = [], pi(log') = [], pi(ge) = [], pi(eq) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-) = [], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = 0, pi(#) = [] Usable Rules: {} Interpretation: [+#](x0, x1) = x0 + x1, [+](x0, x1) = x0 + x1, [1](x0) = x0 + 1, [#] = 1 Strict: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y)) (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(y, z)) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))} SCCS: Scc: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))} SCC: Strict: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} POLY: Argument Filtering: pi(ifinter) = [], pi(inter) = [], pi(mem) = [], pi(prod) = [], pi(sum) = [], pi(cons) = [], pi(nil) = [], pi(app) = [], pi(*) = [], pi(log) = [], pi(log') = [], pi(ge) = [], pi(eq) = [], pi(if) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(-) = [], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = 0, pi(#) = [] Usable Rules: {} Interpretation: [+#](x0, x1) = x0 + x1, [+](x0, x1) = x0 + x1, [1](x0) = x0 + 1, [#] = 0 Strict: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y)) (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y)) (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} SCCS: Scc: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC: Strict: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))} EDG: {(+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))} SCCS: Scc: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))} SCC: Strict: {+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(+(x, y), z) -> +#(x, +(y, z))} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))} SCCS: Scc: {+#(+(x, y), z) -> +#(x, +(y, z))} SCC: Strict: {+#(+(x, y), z) -> +#(x, +(y, z))} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(1(x), 0(y)) -> 1(+(x, y)), +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))), -(x, #()) -> x, -(#(), x) -> #(), -(0(x), 0(y)) -> 0(-(x, y)), -(0(x), 1(y)) -> 1(-(-(x, y), 1(#()))), -(1(x), 0(y)) -> 1(-(x, y)), -(1(x), 1(y)) -> 0(-(x, y)), not(false()) -> true(), not(true()) -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, eq(#(), #()) -> true(), eq(#(), 0(y)) -> eq(#(), y), eq(#(), 1(y)) -> false(), eq(0(x), #()) -> eq(x, #()), eq(0(x), 0(y)) -> eq(x, y), eq(0(x), 1(y)) -> false(), eq(1(x), #()) -> false(), eq(1(x), 0(y)) -> false(), eq(1(x), 1(y)) -> eq(x, y), ge(x, #()) -> true(), ge(#(), 0(x)) -> ge(#(), x), ge(#(), 1(x)) -> false(), ge(0(x), 0(y)) -> ge(x, y), ge(0(x), 1(y)) -> not(ge(y, x)), ge(1(x), 0(y)) -> ge(x, y), ge(1(x), 1(y)) -> ge(x, y), log'(#()) -> #(), log'(0(x)) -> if(ge(x, 1(#())), +(log'(x), 1(#())), #()), log'(1(x)) -> +(log'(x), 1(#())), log(x) -> -(log'(x), 1(#())), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(#(), x) -> #(), *(0(x), y) -> 0(*(x, y)), *(1(x), y) -> +(0(*(x, y)), y), *(*(x, y), z) -> *(x, *(y, z)), app(nil(), l) -> l, app(cons(x, l1), l2) -> cons(x, app(l1, l2)), sum(app(l1, l2)) -> +(sum(l1), sum(l2)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(app(l1, l2)) -> *(prod(l1), prod(l2)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l)), mem(x, nil()) -> false(), mem(x, cons(y, l)) -> if(eq(x, y), true(), mem(x, l)), inter(x, nil()) -> nil(), inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)), inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1), inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)), inter(nil(), x) -> nil(), inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2), ifinter(false(), x, l1, l2) -> inter(l1, l2), ifinter(true(), x, l1, l2) -> cons(x, inter(l1, l2))} SPSC: Simple Projection: pi(+#) = 0 Strict: {} Qed