YES Time: 0.094620 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 #())} 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 #()), +#(+(x, y), z) -> +#(y, z)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(x, y)) (log'# 0 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z)) (log'# 0 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (log'# 0 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> +#(x, y)) (log'# 1 x -> +#(log' x, 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(y, z)) (log'# 1 x -> +#(log' x, 1 #()), +#(+(x, y), z) -> +#(x, +(y, z))) (log'# 1 x -> +#(log' x, 1 #()), +#(0 x, 1 y) -> +#(x, y)) (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, 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, 1 y) -> -#(x, y)) (log# x -> -#(log' x, 1 #()), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> 0# -(x, y)) (log# x -> -#(log' x, 1 #()), -#(1 x, 1 y) -> -#(x, y)) (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> not# ge(y, x)) (log'# 0 x -> ge#(x, 1 #()), ge#(0 x, 1 y) -> ge#(y, x)) (log'# 0 x -> ge#(x, 1 #()), ge#(1 x, 1 y) -> ge#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 1 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 1 y) -> 0# -(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 1 y) -> -#(x, y)) (+#(+(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 #()))} SCCS (5): Scc: {log'# 0 x -> log'# x, log'# 1 x -> log'# x} Scc: {ge#(0 x, 0 y) -> ge#(x, y), ge#(0 x, 1 y) -> ge#(y, x), ge#(1 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)} Scc: {ge#(#(), 0 x) -> ge#(#(), x)} Scc: {-#(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 #())} SPSC: Simple Projection: pi(log'#) = 0 Strict: {log'# 1 x -> log'# x} EDG: {(log'# 1 x -> log'# x, log'# 1 x -> log'# x)} SCCS (1): Scc: {log'# 1 x -> log'# x} SCC (1): Strict: {log'# 1 x -> log'# x} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), -(x, #()) -> x, -(#(), x) -> #(), -(0 x, 0 y) -> 0 -(x, y), -(0 x, 1 y) -> 1 -(-(x, y), 1 #()), -(1 x, 0 y) -> 1 -(x, y), -(1 x, 1 y) -> 0 -(x, y), not false() -> true(), not true() -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, 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 #())} SPSC: Simple Projection: pi(log'#) = 0 Strict: {} Qed SCC (4): Strict: {ge#(0 x, 0 y) -> ge#(x, y), ge#(0 x, 1 y) -> ge#(y, x), ge#(1 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), -(x, #()) -> x, -(#(), x) -> #(), -(0 x, 0 y) -> 0 -(x, y), -(0 x, 1 y) -> 1 -(-(x, y), 1 #()), -(1 x, 0 y) -> 1 -(x, y), -(1 x, 1 y) -> 0 -(x, y), not false() -> true(), not true() -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, 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) = 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 Weak: EDG: {(ge#(1 x, 1 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y))} 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 #())} SPSC: Simple Projection: pi(ge#) = 1 Strict: {} Qed SCC (1): Strict: {ge#(#(), 0 x) -> ge#(#(), x)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), -(x, #()) -> x, -(#(), x) -> #(), -(0 x, 0 y) -> 0 -(x, y), -(0 x, 1 y) -> 1 -(-(x, y), 1 #()), -(1 x, 0 y) -> 1 -(x, y), -(1 x, 1 y) -> 0 -(x, y), not false() -> true(), not true() -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, 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 #())} SPSC: Simple Projection: pi(ge#) = 1 Strict: {} Qed SCC (5): Strict: {-#(0 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), -(x, #()) -> x, -(#(), x) -> #(), -(0 x, 0 y) -> 0 -(x, y), -(0 x, 1 y) -> 1 -(-(x, y), 1 #()), -(1 x, 0 y) -> 1 -(x, y), -(1 x, 1 y) -> 0 -(x, y), not false() -> true(), not true() -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, 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: 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: EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} 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 #())} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(+(x, y), z) -> +#(y, z)} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))} SCCS (1): Scc: {+#(+(x, y), z) -> +#(y, z)} SCC (1): Strict: {+#(+(x, y), z) -> +#(y, z)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(+(x, y), z) -> +(x, +(y, z)), +(1 x, 0 y) -> 1 +(x, y), +(1 x, 1 y) -> 0 +(+(x, y), 1 #()), -(x, #()) -> x, -(#(), x) -> #(), -(0 x, 0 y) -> 0 -(x, y), -(0 x, 1 y) -> 1 -(-(x, y), 1 #()), -(1 x, 0 y) -> 1 -(x, y), -(1 x, 1 y) -> 0 -(x, y), not false() -> true(), not true() -> false(), if(false(), x, y) -> y, if(true(), x, y) -> x, 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 #())} SPSC: Simple Projection: pi(+#) = 0 Strict: {} Qed