MAYBE Time: 0.077956 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), +#(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 #())) } STATUS: arrows: 0.923230 SCCS (14): Scc: {log'# 0 x -> log'# x, log'# 1 x -> log'# x} 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: {eq#(0 x, 0 y) -> eq#(x, y), eq#(1 x, 1 y) -> eq#(x, y)} Scc: {eq#(0 x, #()) -> eq#(x, #())} Scc: {app#(cons(x, l1), l2) -> app#(l1, l2)} 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: {eq#(#(), 0 y) -> eq#(#(), y)} 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: {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: {*#(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: { +#(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 (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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open