YES Time: 0.279804 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, 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 #())} 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), 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} 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, 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 #())} UR: { 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, 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 #()), a(w, v) -> w, a(w, v) -> v} EDG: { (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 0 y) -> 0# +(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 0 y) -> +#(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z)) (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (log'# 0 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(0 x, 0 y) -> +#(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(0 x, 0 y) -> 0# +(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 0 y) -> +#(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z)) (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (log'# 1 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(0 x, 0 y) -> +#(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(0 x, 0 y) -> 0# +(x, y)) (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#(1 x, 1 y) -> ge#(x, y)) (ge#(#(), 0 x) -> ge#(#(), x), ge#(1 x, 0 y) -> ge#(x, y)) (ge#(#(), 0 x) -> ge#(#(), x), ge#(0 x, 1 y) -> ge#(y, x)) (ge#(#(), 0 x) -> ge#(#(), x), ge#(0 x, 1 y) -> not# ge(y, x)) (ge#(#(), 0 x) -> ge#(#(), x), ge#(0 x, 0 y) -> ge#(x, y)) (ge#(#(), 0 x) -> ge#(#(), x), ge#(#(), 0 x) -> ge#(#(), x)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(0 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(1 x, 0 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(1 x, 0 y) -> ge#(x, y)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(0 x, 1 y) -> ge#(y, x)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(0 x, 1 y) -> not# ge(y, x)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(0 x, 0 y) -> ge#(x, y)) (ge#(0 x, 0 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), x)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(1 x, 0 y) -> ge#(x, y)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(0 x, 1 y) -> ge#(y, x)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(0 x, 1 y) -> not# ge(y, x)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(0 x, 0 y) -> ge#(x, y)) (ge#(1 x, 1 y) -> ge#(x, y), ge#(#(), 0 x) -> ge#(#(), x)) (ge#(0 x, 1 y) -> ge#(y, x), ge#(#(), 0 x) -> ge#(#(), 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, 1 y) -> not# ge(y, x)) (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#(1 x, 0 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#(#(), 0 x) -> ge#(#(), x)) (ge#(1 x, 0 y) -> ge#(x, y), ge#(0 x, 0 y) -> ge#(x, y)) (ge#(1 x, 0 y) -> ge#(x, y), ge#(0 x, 1 y) -> not# ge(y, x)) (ge#(1 x, 0 y) -> ge#(x, y), ge#(0 x, 1 y) -> ge#(y, x)) (ge#(1 x, 0 y) -> ge#(x, y), ge#(1 x, 0 y) -> ge#(x, y)) (ge#(1 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(1 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> 0# -(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 0 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 0 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> 0# -(x, y)) (-#(0 x, 1 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(+(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 #())) (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) (log# x -> -#(log' x, 1 #()), -#(0 x, 0 y) -> 0# -(x, y)) (log# x -> -#(log' x, 1 #()), -#(0 x, 0 y) -> -#(x, y)) (log# x -> -#(log' x, 1 #()), -#(0 x, 1 y) -> -#(x, y)) (log# x -> -#(log' x, 1 #()), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (log# x -> -#(log' x, 1 #()), -#(1 x, 0 y) -> -#(x, y)) (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> 0# -(x, y)) (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> -#(x, y)) (log'# 0 x -> ge#(x, 1 #()), ge#(#(), 0 x) -> ge#(#(), x)) (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 0 y) -> ge#(x, y)) (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> not# ge(y, x)) (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> ge#(y, x)) (log'# 0 x -> ge#(x, 1 #()), ge#(1 x, 0 y) -> ge#(x, y)) (log'# 0 x -> ge#(x, 1 #()), ge#(1 x, 1 y) -> ge#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 0 y) -> 0# -(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 0 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 1 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 0 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 1 y) -> 0# -(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 1 y) -> -#(x, y)) (+#(+(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 #())) } STATUS: arrows: 0.803333 SCCS (4): Scc: {log'# 0 x -> log'# x, log'# 1 x -> log'# x} Scc: {ge#(#(), 0 x) -> ge#(#(), x), 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: {-#(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 (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, 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 #())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = x0, [not](x0) = x0 + 1, [log'](x0) = x0 + 1, [log](x0) = 0, [#] = 1, [false] = 1, [true] = 1, [log'#](x0) = x0 Strict: log'# 1 x -> log'# x 0 + 1x >= 0 + 1x log'# 0 x -> log'# x 1 + 1x >= 0 + 1x Weak: log x -> -(log' x, 1 #()) 0 + 0x >= 3 + 1x log' 1 x -> +(log' x, 1 #()) 1 + 1x >= 3 + 1x log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()) 2 + 1x >= 3 + 0x log' #() -> #() 2 >= 1 ge(1 x, 1 y) -> ge(x, y) 1 + 0x + 1y >= 1 + 0x + 1y ge(1 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0 x, 1 y) -> not ge(y, x) 1 + 0x + 1y >= 2 + 1x + 0y ge(0 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(#(), 1 x) -> false() 1 + 1x >= 1 ge(#(), 0 x) -> ge(#(), x) 2 + 1x >= 1 + 1x ge(x, #()) -> true() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 1 + 1x + 1y >= 2 + 1x + 1y -(1 x, 0 y) -> 1 -(x, y) 2 + 1x + 1y >= 1 + 1x + 1y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 2 + 1x + 1y >= 3 + 1x + 1y -(0 x, 0 y) -> 0 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(#(), x) -> #() 2 + 1x >= 1 -(x, #()) -> x 2 + 1x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 1 + 1x + 1y >= 4 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(#(), x) -> x 2 + 1x >= 1x +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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, 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 #())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [log'](x0) = x0 + 1, [log](x0) = 0, [#] = 1, [false] = 1, [true] = 1, [log'#](x0) = x0 Strict: log'# 1 x -> log'# x 1 + 1x >= 0 + 1x Weak: log x -> -(log' x, 1 #()) 0 + 0x >= 4 + 1x log' 1 x -> +(log' x, 1 #()) 2 + 1x >= 4 + 1x log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()) 2 + 1x >= 4 + 0x log' #() -> #() 2 >= 1 ge(1 x, 1 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(1 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0 x, 1 y) -> not ge(y, x) 2 + 0x + 1y >= 2 + 1x + 0y ge(0 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(#(), 1 x) -> false() 2 + 1x >= 1 ge(#(), 0 x) -> ge(#(), x) 2 + 1x >= 1 + 1x ge(x, #()) -> true() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(1 x, 0 y) -> 1 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 3 + 1x + 1y >= 5 + 1x + 1y -(0 x, 0 y) -> 0 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(#(), x) -> #() 2 + 1x >= 1 -(x, #()) -> x 2 + 1x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 3 + 1x + 1y >= 5 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(0 x, 1 y) -> 1 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(#(), x) -> x 2 + 1x >= 1x +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 Qed SCC (5): Strict: {ge#(#(), 0 x) -> ge#(#(), x), 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, 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 #())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [+](x0, x1) = 0, [-](x0, x1) = 0, [ge](x0, x1) = 0, [0](x0) = x0 + 1, [1](x0) = x0, [not](x0) = x0 + 1, [log'](x0) = 0, [log](x0) = 0, [#] = 0, [false] = 1, [true] = 1, [ge#](x0, x1) = x0 + x1 Strict: ge#(1 x, 1 y) -> ge#(x, y) 0 + 1x + 1y >= 0 + 1x + 1y ge#(1 x, 0 y) -> ge#(x, y) 1 + 1x + 1y >= 0 + 1x + 1y ge#(0 x, 1 y) -> ge#(y, x) 1 + 1x + 1y >= 0 + 1x + 1y ge#(0 x, 0 y) -> ge#(x, y) 2 + 1x + 1y >= 0 + 1x + 1y ge#(#(), 0 x) -> ge#(#(), x) 1 + 1x >= 0 + 1x Weak: log x -> -(log' x, 1 #()) 0 + 0x >= 0 + 0x log' 1 x -> +(log' x, 1 #()) 0 + 0x >= 0 + 0x log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()) 0 + 0x >= 0 + 0x log' #() -> #() 0 >= 0 ge(1 x, 1 y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(1 x, 0 y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(0 x, 1 y) -> not ge(y, x) 0 + 0x + 0y >= 1 + 0x + 0y ge(0 x, 0 y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(#(), 1 x) -> false() 0 + 0x >= 1 ge(#(), 0 x) -> ge(#(), x) 0 + 0x >= 0 + 0x ge(x, #()) -> true() 0 + 0x >= 1 if(true(), x, y) -> x 0 + 0x + 0y >= 1x if(false(), x, y) -> y 0 + 0x + 0y >= 1y not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(1 x, 0 y) -> 1 -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 0 + 0x + 0y >= 0 + 0x + 0y -(0 x, 0 y) -> 0 -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(#(), x) -> #() 0 + 0x >= 0 -(x, #()) -> x 0 + 0x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 0 + 0x + 0y >= 1 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z +(0 x, 1 y) -> 1 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(#(), x) -> x 0 + 0x >= 1x +(x, #()) -> x 0 + 0x >= 1x 0 #() -> #() 1 >= 0 SCCS (1): Scc: {ge#(1 x, 1 y) -> ge#(x, y)} SCC (1): Strict: {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, 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 #())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [log'](x0) = x0 + 1, [log](x0) = 0, [#] = 1, [false] = 1, [true] = 1, [ge#](x0, x1) = x0 + 1 Strict: ge#(1 x, 1 y) -> ge#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: log x -> -(log' x, 1 #()) 0 + 0x >= 4 + 1x log' 1 x -> +(log' x, 1 #()) 2 + 1x >= 4 + 1x log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()) 2 + 1x >= 8 + 1x log' #() -> #() 2 >= 1 ge(1 x, 1 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(1 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0 x, 1 y) -> not ge(y, x) 2 + 0x + 1y >= 2 + 1x + 0y ge(0 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(#(), 1 x) -> false() 2 + 1x >= 1 ge(#(), 0 x) -> ge(#(), x) 2 + 1x >= 1 + 1x ge(x, #()) -> true() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 1x + 0y >= 1x if(false(), x, y) -> y 2 + 1x + 0y >= 1y not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(1 x, 0 y) -> 1 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 3 + 1x + 1y >= 5 + 1x + 1y -(0 x, 0 y) -> 0 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(#(), x) -> #() 2 + 1x >= 1 -(x, #()) -> x 2 + 1x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 3 + 1x + 1y >= 5 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(0 x, 1 y) -> 1 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(#(), x) -> x 2 + 1x >= 1x +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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, 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 #())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [+](x0, x1) = x0 + 1, [-](x0, x1) = x0, [ge](x0, x1) = x0, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [not](x0) = 0, [log'](x0) = 0, [log](x0) = 0, [#] = 1, [false] = 0, [true] = 0, [-#](x0, x1) = x0 Strict: -#(1 x, 1 y) -> -#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y -#(1 x, 0 y) -> -#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y -#(0 x, 1 y) -> -#(-(x, y), 1 #()) 1 + 1x + 0y >= 0 + 1x + 0y -#(0 x, 1 y) -> -#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y -#(0 x, 0 y) -> -#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: log x -> -(log' x, 1 #()) 0 + 0x >= 0 + 0x log' 1 x -> +(log' x, 1 #()) 0 + 0x >= 1 + 0x log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()) 0 + 0x >= 0 + 0x log' #() -> #() 0 >= 1 ge(1 x, 1 y) -> ge(x, y) 1 + 1x + 0y >= 0 + 1x + 0y ge(1 x, 0 y) -> ge(x, y) 1 + 1x + 0y >= 0 + 1x + 0y ge(0 x, 1 y) -> not ge(y, x) 1 + 1x + 0y >= 0 + 0x + 0y ge(0 x, 0 y) -> ge(x, y) 1 + 1x + 0y >= 0 + 1x + 0y ge(#(), 1 x) -> false() 1 + 0x >= 0 ge(#(), 0 x) -> ge(#(), x) 1 + 0x >= 1 + 0x ge(x, #()) -> true() 0 + 1x >= 0 if(true(), x, y) -> x 0 + 0x + 0y >= 1x if(false(), x, y) -> y 0 + 0x + 0y >= 1y not true() -> false() 0 >= 0 not false() -> true() 0 >= 0 -(1 x, 1 y) -> 0 -(x, y) 1 + 1x + 0y >= 1 + 1x + 0y -(1 x, 0 y) -> 1 -(x, y) 1 + 1x + 0y >= 1 + 1x + 0y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 1 + 1x + 0y >= 1 + 1x + 0y -(0 x, 0 y) -> 0 -(x, y) 1 + 1x + 0y >= 1 + 1x + 0y -(#(), x) -> #() 1 + 0x >= 1 -(x, #()) -> x 0 + 1x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 2 + 1x + 0y >= 3 + 1x + 0y +(1 x, 0 y) -> 1 +(x, y) 2 + 1x + 0y >= 2 + 1x + 0y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 0y >= 2 + 1x + 0y +(0 x, 0 y) -> 0 +(x, y) 2 + 1x + 0y >= 2 + 1x + 0y +(#(), x) -> x 2 + 0x >= 1x +(x, #()) -> x 1 + 1x >= 1x 0 #() -> #() 2 >= 1 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, 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 #())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0, [+](x0, x1) = x0 + x1, [-](x0, x1) = x0 + x1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [log'](x0) = 1, [log](x0) = 0, [#] = 0, [false] = 1, [true] = 1, [+#](x0, x1) = x0 + x1 Strict: +#(1 x, 1 y) -> +#(+(x, y), 1 #()) 2 + 1x + 1y >= 1 + 1x + 1y +#(1 x, 1 y) -> +#(x, y) 2 + 1x + 1y >= 0 + 1x + 1y +#(1 x, 0 y) -> +#(x, y) 2 + 1x + 1y >= 0 + 1x + 1y +#(+(x, y), z) -> +#(y, z) 0 + 1x + 1y + 1z >= 0 + 1y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +#(0 x, 1 y) -> +#(x, y) 2 + 1x + 1y >= 0 + 1x + 1y +#(0 x, 0 y) -> +#(x, y) 2 + 1x + 1y >= 0 + 1x + 1y Weak: log x -> -(log' x, 1 #()) 0 + 0x >= 2 + 0x log' 1 x -> +(log' x, 1 #()) 1 + 0x >= 2 + 0x log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()) 1 + 0x >= 2 + 0x log' #() -> #() 1 >= 0 ge(1 x, 1 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(1 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0 x, 1 y) -> not ge(y, x) 2 + 0x + 1y >= 2 + 1x + 0y ge(0 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(#(), 1 x) -> false() 2 + 1x >= 1 ge(#(), 0 x) -> ge(#(), x) 2 + 1x >= 1 + 1x ge(x, #()) -> true() 1 + 0x >= 1 if(true(), x, y) -> x 0 + 1x + 0y >= 1x if(false(), x, y) -> y 0 + 1x + 0y >= 1y not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 2 + 1x + 1y >= 1 + 1x + 1y -(1 x, 0 y) -> 1 -(x, y) 2 + 1x + 1y >= 1 + 1x + 1y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 2 + 1x + 1y >= 2 + 1x + 1y -(0 x, 0 y) -> 0 -(x, y) 2 + 1x + 1y >= 1 + 1x + 1y -(#(), x) -> #() 0 + 1x >= 0 -(x, #()) -> x 0 + 1x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 2 + 1x + 1y >= 2 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(+(x, y), z) -> +(x, +(y, z)) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(#(), x) -> x 0 + 1x >= 1x +(x, #()) -> x 0 + 1x >= 1x 0 #() -> #() 1 >= 0 SCCS (1): Scc: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC (2): Strict: {+#(+(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, 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 #())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = 0, [not](x0) = x0 + 1, [log'](x0) = x0 + 1, [log](x0) = 0, [#] = 1, [false] = 1, [true] = 1, [+#](x0, x1) = x0 + 1 Strict: +#(+(x, y), z) -> +#(y, z) 2 + 1x + 1y + 0z >= 1 + 1y + 0z +#(+(x, y), z) -> +#(x, +(y, z)) 2 + 1x + 1y + 0z >= 1 + 1x + 0y + 0z Weak: log x -> -(log' x, 1 #()) 0 + 0x >= 2 + 1x log' 1 x -> +(log' x, 1 #()) 1 + 0x >= 2 + 1x log' 0 x -> if(ge(x, 1 #()), +(log' x, 1 #()), #()) 2 + 1x >= 4 + 1x log' #() -> #() 2 >= 1 ge(1 x, 1 y) -> ge(x, y) 1 + 0x + 0y >= 1 + 0x + 1y ge(1 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0 x, 1 y) -> not ge(y, x) 1 + 0x + 0y >= 2 + 1x + 0y ge(0 x, 0 y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(#(), 1 x) -> false() 1 + 0x >= 1 ge(#(), 0 x) -> ge(#(), x) 2 + 1x >= 1 + 1x ge(x, #()) -> true() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 1x + 0y >= 1x if(false(), x, y) -> y 2 + 1x + 0y >= 1y not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 1 + 0x + 0y >= 2 + 1x + 1y -(1 x, 0 y) -> 1 -(x, y) 2 + 0x + 1y >= 0 + 0x + 0y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 2 + 1x + 0y >= 0 + 0x + 0y -(0 x, 0 y) -> 0 -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(#(), x) -> #() 2 + 1x >= 1 -(x, #()) -> x 2 + 1x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 1 + 0x + 0y >= 3 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(0 x, 1 y) -> 1 +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(#(), x) -> x 2 + 1x >= 1x +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 Qed