YES Time: 0.355600 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: DP: { +#(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)} 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))} EDG: { (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, z), *#(1 x, y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(x, +(y, z)) -> *#(x, z), *#(1 x, y) -> 0# *(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(0 x, y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(0 x, y) -> 0# *(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (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)) (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)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 1 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 1 y) -> 0# -(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 1 y) -> -#(x, y)) (log'# 0 x -> ge#(x, 1 #()), ge#(1 x, 1 y) -> ge#(x, y)) (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> ge#(y, x)) (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> not# ge(y, x)) (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> -#(x, y)) (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> 0# -(x, y)) (log# x -> -#(log' x, 1 #()), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (log# x -> -#(log' x, 1 #()), -#(0 x, 1 y) -> -#(x, y)) (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)) (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))) (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> +#(+(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) -> 0# +(+(x, y), 1 #())) (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 0 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(+(x, y), z) -> +#(y, z)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 1 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> +#(x, y)) (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> 0# +(x, y)) (*#(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)) (mem#(x, cons(y, l)) -> mem#(x, l), mem#(x, cons(y, l)) -> 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)) -> if#(eq(x, y), true(), mem(x, l))) (log'# 1 x -> log'# x, log'# 1 x -> log'# x) (log'# 1 x -> log'# x, log'# 1 x -> +#(log' x, 1 #())) (log'# 1 x -> log'# x, log'# 0 x -> log'# x) (log'# 1 x -> log'# x, log'# 0 x -> ge#(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 -> +#(log' x, 1 #())) (ge#(#(), 0 x) -> ge#(#(), x), ge#(#(), 0 x) -> ge#(#(), x)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(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) -> 0# +(+(x, y), 1 #())) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(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) -> 0# +(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (eq#(1 x, 1 y) -> eq#(x, y), eq#(1 x, 1 y) -> eq#(x, y)) (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#(0 x, #()) -> eq#(x, #())) (eq#(1 x, 1 y) -> eq#(x, y), eq#(#(), 0 y) -> eq#(#(), y)) (ge#(1 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)) (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#(0 x, 1 y) -> ge#(y, x)) (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, 0 y) -> ge#(x, y)) (ge#(1 x, 0 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), x)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(x, +(y, z)) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(0 x, y) -> 0# *(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y)) (*#(1 x, y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(1 x, y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2), ifinter#(true(), 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)) (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))) (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#(app(l1, l2), l3) -> inter#(l1, l3), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (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#(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#(app(l1, l2), l3) -> app#(inter(l1, l3), inter(l2, l3))) (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#(l1, cons(x, l2)) -> mem#(x, l1)) (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#(app(l1, l2), l3) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), inter(l1, l3))) (inter#(l1, cons(x, l2)) -> mem#(x, l1), mem#(x, cons(y, l)) -> if#(eq(x, y), true(), 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)) -> mem#(x, l)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), 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)) -> inter#(l1, l3)) (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, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1)) (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#(app(l1, l2), l3) -> inter#(l1, l3)) (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#(cons(x, l1), l2) -> mem#(x, l2)) (inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> app#(inter(l1, l2), 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#(l1, cons(x, l2)) -> mem#(x, l1)) (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#(app(l1, l2), l3) -> app#(inter(l1, 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) -> inter#(l2, l3)) (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#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2)) (eq#(0 x, #()) -> eq#(x, #()), eq#(0 x, #()) -> eq#(x, #())) (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) (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 #())) (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)) -> ifinter#(mem(x, l1), x, l2, l1), ifinter#(true(), x, l1, l2) -> inter#(l1, l2)) (mem#(x, cons(y, l)) -> eq#(x, y), eq#(#(), 0 y) -> eq#(#(), y)) (mem#(x, cons(y, l)) -> eq#(x, y), eq#(0 x, #()) -> eq#(x, #())) (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#(1 x, 1 y) -> eq#(x, y)) (*#(0 x, y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(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) -> 0# *(x, y)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), 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, 1 y) -> not# ge(y, x)) (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#(1 x, 0 y) -> ge#(x, y)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), 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, 1 y) -> not# ge(y, x)) (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#(1 x, 0 y) -> ge#(x, y)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)) (eq#(0 x, 0 y) -> eq#(x, y), eq#(#(), 0 y) -> eq#(#(), y)) (eq#(0 x, 0 y) -> eq#(x, y), eq#(0 x, #()) -> eq#(x, #())) (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#(1 x, 1 y) -> eq#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 1 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)) (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 0 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, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 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)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 0 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, 1 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (log# x -> log'# x, log'# 0 x -> +#(log' x, 1 #())) (log# x -> log'# x, log'# 0 x -> if#(ge(x, 1 #()), +(log' x, 1 #()), #())) (log# x -> log'# x, log'# 0 x -> ge#(x, 1 #())) (log# x -> log'# x, log'# 0 x -> log'# x) (log# x -> log'# x, log'# 1 x -> +#(log' x, 1 #())) (log# x -> log'# x, log'# 1 x -> log'# x) (log'# 0 x -> log'# x, log'# 0 x -> +#(log' 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 -> ge#(x, 1 #())) (log'# 0 x -> log'# x, log'# 0 x -> log'# x) (log'# 0 x -> log'# x, log'# 1 x -> +#(log' x, 1 #())) (log'# 0 x -> log'# x, log'# 1 x -> log'# x) (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 #())) (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)) (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2)) (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) (log'# 1 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z)) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(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) -> +#(+(x, y), 1 #())) (log'# 0 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z)) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(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) -> +#(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y)) (+#(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) -> 0# +(+(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) -> +#(+(x, y), 1 #())) (eq#(#(), 0 y) -> eq#(#(), y), eq#(#(), 0 y) -> eq#(#(), y)) (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) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> 0# *(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> 0# *(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> +#(0 *(x, y), y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, 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), +#(0 x, 0 y) -> 0# +(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0 x, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0 x, 1 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, 0 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) } SCCS (14): 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 (8): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifinter](x0, x1, x2, x3) = x0 + x1, [if](x0, x1, x2) = 0, [+](x0, x1) = 0, [-](x0, x1) = x0 + x1 + 1, [eq](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + x1 + 1, [*](x0, x1) = 0, [app](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + 1, [mem](x0, x1) = x0, [inter](x0, x1) = x0, [0](x0) = 0, [1](x0) = 0, [not](x0) = 0, [log'](x0) = x0 + 1, [log](x0) = 0, [sum](x0) = 0, [prod](x0) = 0, [#] = 1, [false] = 0, [true] = 0, [nil] = 0, [ifinter#](x0, x1, x2, x3) = x0 + x1, [inter#](x0, x1) = x0 + x1 Strict: ifinter#(true(), x, l1, l2) -> inter#(l1, l2) 0 + 0x + 1l1 + 1l2 >= 0 + 1l1 + 1l2 ifinter#(false(), x, l1, l2) -> inter#(l1, l2) 0 + 0x + 1l1 + 1l2 >= 0 + 1l1 + 1l2 inter#(cons(x, l1), l2) -> ifinter#(mem(x, l2), x, l1, l2) 1 + 0x + 1l1 + 1l2 >= 0 + 0x + 1l1 + 1l2 inter#(app(l1, l2), l3) -> inter#(l2, l3) 0 + 1l1 + 1l2 + 1l3 >= 0 + 1l2 + 1l3 inter#(app(l1, l2), l3) -> inter#(l1, l3) 0 + 1l1 + 1l2 + 1l3 >= 0 + 1l1 + 1l3 inter#(l1, cons(x, l2)) -> ifinter#(mem(x, l1), x, l2, l1) 1 + 0x + 1l1 + 1l2 >= 0 + 0x + 1l1 + 1l2 inter#(l1, app(l2, l3)) -> inter#(l1, l3) 0 + 1l1 + 1l2 + 1l3 >= 0 + 1l1 + 1l3 inter#(l1, app(l2, l3)) -> inter#(l1, l2) 0 + 1l1 + 1l2 + 1l3 >= 0 + 1l1 + 1l2 Weak: EDG: {(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#(l1, app(l2, l3)) -> inter#(l1, l3)) (ifinter#(false(), x, l1, l2) -> inter#(l1, l2), inter#(l1, app(l2, l3)) -> inter#(l1, 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#(l1, app(l2, l3)) -> inter#(l1, l3)) (inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(l1, app(l2, l3)) -> inter#(l1, 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#(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#(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#(app(l1, l2), l3) -> inter#(l1, l3)) (inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, 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#(app(l1, l2), l3) -> inter#(l1, l3)) (ifinter#(true(), x, l1, l2) -> inter#(l1, l2), inter#(app(l1, l2), l3) -> inter#(l2, 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, 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) -> inter#(l2, l3))} SCCS (1): 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 (4): 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#) = 1 Strict: {inter#(l1, app(l2, l3)) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)} 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#(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, 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 (1): Scc: {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 (3): Strict: {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#) = 1 Strict: {inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)} EDG: {(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#(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))} SCCS (1): Scc: {inter#(app(l1, l2), l3) -> inter#(l1, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3)} SCC (2): Strict: {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#(app(l1, l2), l3) -> inter#(l2, l3)} EDG: {(inter#(app(l1, l2), l3) -> inter#(l2, l3), inter#(app(l1, l2), l3) -> inter#(l2, l3))} SCCS (1): Scc: {inter#(app(l1, l2), l3) -> inter#(l2, l3)} SCC (1): Strict: {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: {} Qed SCC (1): 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 (3): 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# l1, 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# l1) (prod# app(l1, l2) -> prod# l1, prod# app(l1, l2) -> prod# l1) (prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> prod# l)} SCCS (1): Scc: {prod# app(l1, l2) -> prod# l1, prod# cons(x, l) -> prod# l} SCC (2): Strict: {prod# app(l1, l2) -> prod# l1, 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 (1): Scc: {prod# cons(x, l) -> prod# l} SCC (1): 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 (3): 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 (1): Scc: {sum# app(l1, l2) -> sum# l1, sum# cons(x, l) -> sum# l} SCC (2): 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 (1): Scc: {sum# cons(x, l) -> sum# l} SCC (1): 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 (1): 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 (6): 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 (1): 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 (5): 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(*#) = 1 Strict: {*#(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)) (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(1 x, y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(0 x, y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(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 (1): Scc: {*#(x, +(y, z)) -> *#(x, z), *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC (4): Strict: {*#(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(*#) = 1 Strict: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(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)) (*#(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) -> *#(y, z), *#(0 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))} SCCS (1): Scc: { *#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC (3): Strict: { *#(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: { *#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))} SCCS (1): Scc: { *#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC (2): Strict: { *#(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) -> *#(y, z)} EDG: {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(*(x, y), z) -> *#(y, z)} SCC (1): Strict: {*#(*(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: {} Qed SCC (2): 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'# 1 x -> log'# x} EDG: {(log'# 1 x -> log'# x, log'# 1 x -> log'# x)} SCCS (1): Scc: {log'# 1 x -> log'# x} SCC (1): Strict: {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: {} Qed SCC (4): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifinter](x0, x1, x2, x3) = x0 + x1 + 1, [if](x0, x1, x2) = x0 + x1 + 1, [+](x0, x1) = x0 + 1, [-](x0, x1) = x0 + x1 + 1, [eq](x0, x1) = 0, [ge](x0, x1) = x0 + 1, [*](x0, x1) = 0, [app](x0, x1) = x0 + 1, [cons](x0, x1) = 0, [mem](x0, x1) = x0 + 1, [inter](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [log'](x0) = x0 + 1, [log](x0) = 0, [sum](x0) = 0, [prod](x0) = x0 + 1, [#] = 1, [false] = 1, [true] = 1, [nil] = 1, [ge#](x0, x1) = x0 + x1 + 1 Strict: ge#(1 x, 1 y) -> ge#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge#(1 x, 0 y) -> ge#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge#(0 x, 1 y) -> ge#(y, x) 3 + 1x + 1y >= 1 + 1x + 1y ge#(0 x, 0 y) -> ge#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y Weak: Qed SCC (1): 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 (2): 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#) = 1 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 (1): Scc: {eq#(0 x, 0 y) -> eq#(x, y)} SCC (1): 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#) = 1 Strict: {} Qed SCC (1): 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 (1): 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 (5): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifinter](x0, x1, x2, x3) = 0, [if](x0, x1, x2) = x0 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0, [eq](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + 1, [*](x0, x1) = x0 + x1, [app](x0, x1) = x0 + 1, [cons](x0, x1) = 0, [mem](x0, x1) = x0 + 1, [inter](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [log'](x0) = x0 + 1, [log](x0) = 0, [sum](x0) = 0, [prod](x0) = 0, [#] = 1, [false] = 1, [true] = 1, [nil] = 1, [-#](x0, x1) = x0 + 1 Strict: -#(1 x, 1 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(1 x, 0 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(0 x, 1 y) -> -#(-(x, y), 1 #()) 2 + 1x + 0y >= 1 + 1x + 0y -#(0 x, 1 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(0 x, 0 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: Qed SCC (7): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifinter](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [if](x0, x1, x2) = x0 + x1 + 1, [+](x0, x1) = x0 + x1, [-](x0, x1) = 0, [eq](x0, x1) = 0, [ge](x0, x1) = 0, [*](x0, x1) = x0 + 1, [app](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = 0, [mem](x0, x1) = x0 + x1 + 1, [inter](x0, x1) = x0, [0](x0) = x0, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [log'](x0) = 0, [log](x0) = 0, [sum](x0) = 0, [prod](x0) = 1, [#] = 0, [false] = 1, [true] = 1, [nil] = 1, [+#](x0, x1) = x0 + x1 + 1 Strict: +#(1 x, 1 y) -> +#(+(x, y), 1 #()) 3 + 1x + 1y >= 2 + 1x + 1y +#(1 x, 1 y) -> +#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y +#(1 x, 0 y) -> +#(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +#(+(x, y), z) -> +#(y, z) 1 + 1x + 1y + 1z >= 1 + 1y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z +#(0 x, 1 y) -> +#(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +#(0 x, 0 y) -> +#(x, y) 1 + 1x + 1y >= 1 + 1x + 1y Weak: EDG: {(+#(+(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), +#(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) -> +#(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))} SCCS (1): Scc: { +#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC (3): 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) -> +#(y, z)} EDG: {(+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(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) -> +#(y, z))} SCCS (1): Scc: { +#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)} SCC (2): Strict: { +#(0 x, 0 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(+#) = 1 Strict: {+#(+(x, y), z) -> +#(y, z)} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))} SCCS (1): Scc: {+#(+(x, y), z) -> +#(y, z)} SCC (1): Strict: {+#(+(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: {} Qed