YES Time: 0.347650 TRS: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} DP: DP: { +#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(0 x, 0 y) -> 0# +(x, y), +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y), +#(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), min# n(x, y, z) -> min# y, max# n(x, y, z) -> max# z, bs# n(x, y, z) -> and#(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), bs# n(x, y, z) -> and#(ge(x, max y), ge(min z, x)), bs# n(x, y, z) -> and#(bs y, bs z), bs# n(x, y, z) -> ge#(x, max y), bs# n(x, y, z) -> ge#(min z, x), bs# n(x, y, z) -> min# z, bs# n(x, y, z) -> max# y, bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> bs# z, size# n(x, y, z) -> +#(+(size x, size y), 1 #()), size# n(x, y, z) -> +#(size x, size y), size# n(x, y, z) -> size# x, size# n(x, y, z) -> size# y, wb# n(x, y, z) -> -#(size y, size z), wb# n(x, y, z) -> -#(size z, size y), wb# n(x, y, z) -> and#(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z)), wb# n(x, y, z) -> and#(wb y, wb z), wb# n(x, y, z) -> if#(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), wb# n(x, y, z) -> ge#(1 #(), -(size y, size z)), wb# n(x, y, z) -> ge#(1 #(), -(size z, size y)), wb# n(x, y, z) -> ge#(size y, size z), wb# n(x, y, z) -> size# y, wb# n(x, y, z) -> size# z, wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> wb# z} TRS: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} EDG: { (bs# n(x, y, z) -> ge#(min z, x), ge#(1 x, 1 y) -> ge#(x, y)) (bs# n(x, y, z) -> ge#(min z, x), ge#(1 x, 0 y) -> ge#(x, y)) (bs# n(x, y, z) -> ge#(min z, x), ge#(0 x, 1 y) -> ge#(y, x)) (bs# n(x, y, z) -> ge#(min z, x), ge#(0 x, 1 y) -> not# ge(y, x)) (bs# n(x, y, z) -> ge#(min z, x), ge#(0 x, 0 y) -> ge#(x, y)) (bs# n(x, y, z) -> ge#(min z, x), ge#(#(), 0 x) -> ge#(#(), x)) (bs# n(x, y, z) -> min# z, min# n(x, y, z) -> min# y) (wb# n(x, y, z) -> size# z, size# n(x, y, z) -> size# y) (wb# n(x, y, z) -> size# z, size# n(x, y, z) -> size# x) (wb# n(x, y, z) -> size# z, size# n(x, y, z) -> +#(size x, size y)) (wb# n(x, y, z) -> size# z, size# n(x, y, z) -> +#(+(size x, size y), 1 #())) (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)) (bs# n(x, y, z) -> max# y, max# n(x, y, z) -> max# z) (size# n(x, y, z) -> size# y, size# n(x, y, z) -> size# y) (size# n(x, y, z) -> size# y, size# n(x, y, z) -> size# x) (size# n(x, y, z) -> size# y, size# n(x, y, z) -> +#(size x, size y)) (size# n(x, y, z) -> size# y, size# n(x, y, z) -> +#(+(size x, size y), 1 #())) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> wb# z) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> wb# y) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> size# z) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> size# y) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> ge#(size y, size z)) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> ge#(1 #(), -(size z, size y))) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> ge#(1 #(), -(size y, size z))) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> if#(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y)))) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> and#(wb y, wb z)) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> and#(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> -#(size z, size y)) (wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> -#(size y, size z)) (ge#(#(), 0 x) -> ge#(#(), 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)) (+#(x, +(y, z)) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(x, +(y, z)) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (+#(x, +(y, z)) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(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), +#(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)) (+#(0 x, 1 y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(0 x, 1 y) -> +#(x, y), +#(x, +(y, z)) -> +#(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), +#(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)) (+#(1 x, 1 y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(1 x, 1 y) -> +#(x, y), +#(x, +(y, z)) -> +#(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)) (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)) (wb# n(x, y, z) -> ge#(1 #(), -(size y, size z)), ge#(1 x, 1 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(1 #(), -(size y, size z)), ge#(1 x, 0 y) -> ge#(x, y)) (size# n(x, y, z) -> +#(size x, size y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (size# n(x, y, z) -> +#(size x, size y), +#(1 x, 1 y) -> +#(x, y)) (size# n(x, y, z) -> +#(size x, size y), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (size# n(x, y, z) -> +#(size x, size y), +#(1 x, 0 y) -> +#(x, y)) (size# n(x, y, z) -> +#(size x, size y), +#(0 x, 1 y) -> +#(x, y)) (size# n(x, y, z) -> +#(size x, size y), +#(0 x, 0 y) -> +#(x, y)) (size# n(x, y, z) -> +#(size x, size y), +#(0 x, 0 y) -> 0# +(x, y)) (size# n(x, y, z) -> +#(size x, size y), +#(x, +(y, z)) -> +#(+(x, y), z)) (size# n(x, y, z) -> +#(size x, size y), +#(x, +(y, z)) -> +#(x, y)) (wb# n(x, y, z) -> -#(size z, size y), -#(1 x, 1 y) -> -#(x, y)) (wb# n(x, y, z) -> -#(size z, size y), -#(1 x, 1 y) -> 0# -(x, y)) (wb# n(x, y, z) -> -#(size z, size y), -#(1 x, 0 y) -> -#(x, y)) (wb# n(x, y, z) -> -#(size z, size y), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (wb# n(x, y, z) -> -#(size z, size y), -#(0 x, 1 y) -> -#(x, y)) (wb# n(x, y, z) -> -#(size z, size y), -#(0 x, 0 y) -> -#(x, y)) (wb# n(x, y, z) -> -#(size z, size y), -#(0 x, 0 y) -> 0# -(x, y)) (wb# n(x, y, z) -> ge#(size y, size z), ge#(1 x, 1 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(size y, size z), ge#(1 x, 0 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(size y, size z), ge#(0 x, 1 y) -> ge#(y, x)) (wb# n(x, y, z) -> ge#(size y, size z), ge#(0 x, 1 y) -> not# ge(y, x)) (wb# n(x, y, z) -> ge#(size y, size z), ge#(0 x, 0 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(size y, size z), ge#(#(), 0 x) -> ge#(#(), x)) (size# n(x, y, z) -> size# x, size# n(x, y, z) -> size# y) (size# n(x, y, z) -> size# x, size# n(x, y, z) -> size# x) (size# n(x, y, z) -> size# x, size# n(x, y, z) -> +#(size x, size y)) (size# n(x, y, z) -> size# x, size# n(x, y, z) -> +#(+(size x, size y), 1 #())) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, 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), +#(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 #())) (wb# n(x, y, z) -> -#(size y, size z), -#(0 x, 0 y) -> 0# -(x, y)) (wb# n(x, y, z) -> -#(size y, size z), -#(0 x, 0 y) -> -#(x, y)) (wb# n(x, y, z) -> -#(size y, size z), -#(0 x, 1 y) -> -#(x, y)) (wb# n(x, y, z) -> -#(size y, size z), -#(0 x, 1 y) -> -#(-(x, y), 1 #())) (wb# n(x, y, z) -> -#(size y, size z), -#(1 x, 0 y) -> -#(x, y)) (wb# n(x, y, z) -> -#(size y, size z), -#(1 x, 1 y) -> 0# -(x, y)) (wb# n(x, y, z) -> -#(size y, size z), -#(1 x, 1 y) -> -#(x, y)) (bs# n(x, y, z) -> ge#(x, max y), ge#(#(), 0 x) -> ge#(#(), x)) (bs# n(x, y, z) -> ge#(x, max y), ge#(0 x, 0 y) -> ge#(x, y)) (bs# n(x, y, z) -> ge#(x, max y), ge#(0 x, 1 y) -> not# ge(y, x)) (bs# n(x, y, z) -> ge#(x, max y), ge#(0 x, 1 y) -> ge#(y, x)) (bs# n(x, y, z) -> ge#(x, max y), ge#(1 x, 0 y) -> ge#(x, y)) (bs# n(x, y, z) -> ge#(x, max y), ge#(1 x, 1 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(1 #(), -(size z, size y)), ge#(1 x, 0 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(1 #(), -(size z, size y)), ge#(1 x, 1 y) -> ge#(x, y)) (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)) (-#(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), +#(x, +(y, z)) -> +#(x, y)) (+#(1 x, 0 y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(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), +#(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), +#(x, +(y, z)) -> +#(x, y)) (+#(0 x, 0 y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(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), +#(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 #())) (size# n(x, y, z) -> +#(+(size x, size y), 1 #()), +#(0 x, 1 y) -> +#(x, y)) (size# n(x, y, z) -> +#(+(size x, size y), 1 #()), +#(1 x, 1 y) -> 0# +(+(x, y), 1 #())) (size# n(x, y, z) -> +#(+(size x, size y), 1 #()), +#(1 x, 1 y) -> +#(x, y)) (size# n(x, y, z) -> +#(+(size x, size y), 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 #()), +#(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 #())) (wb# n(x, y, z) -> size# y, size# n(x, y, z) -> +#(+(size x, size y), 1 #())) (wb# n(x, y, z) -> size# y, size# n(x, y, z) -> +#(size x, size y)) (wb# n(x, y, z) -> size# y, size# n(x, y, z) -> size# x) (wb# n(x, y, z) -> size# y, size# n(x, y, z) -> size# y) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> and#(and(ge(x, max y), ge(min z, x)), and(bs y, bs z))) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> and#(ge(x, max y), ge(min z, x))) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> and#(bs y, bs z)) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> ge#(x, max y)) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> ge#(min z, x)) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> min# z) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> max# y) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> bs# y) (bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> bs# z) (min# n(x, y, z) -> min# y, min# n(x, y, z) -> min# y) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> -#(size y, size z)) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> -#(size z, size y)) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> and#(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> and#(wb y, wb z)) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> if#(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y)))) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> ge#(1 #(), -(size y, size z))) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> ge#(1 #(), -(size z, size y))) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> ge#(size y, size z)) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> size# y) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> size# z) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> wb# y) (wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> wb# z) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> and#(and(ge(x, max y), ge(min z, x)), and(bs y, bs z))) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> and#(ge(x, max y), ge(min z, x))) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> and#(bs y, bs z)) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> ge#(x, max y)) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> ge#(min z, x)) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> min# z) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> max# y) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> bs# y) (bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> bs# z) (max# n(x, y, z) -> max# z, max# n(x, y, z) -> max# z) } SCCS (9): Scc: {wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> wb# z} Scc: {size# n(x, y, z) -> size# x, size# n(x, y, z) -> size# y} Scc: {bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> bs# z} Scc: {max# n(x, y, z) -> max# z} Scc: {min# n(x, y, z) -> min# 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: {-#(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: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())} SCC (2): Strict: {wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> wb# z} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(wb#) = 0 Strict: {wb# n(x, y, z) -> wb# z} EDG: {(wb# n(x, y, z) -> wb# z, wb# n(x, y, z) -> wb# z)} SCCS (1): Scc: {wb# n(x, y, z) -> wb# z} SCC (1): Strict: {wb# n(x, y, z) -> wb# z} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(wb#) = 0 Strict: {} Qed SCC (2): Strict: {size# n(x, y, z) -> size# x, size# n(x, y, z) -> size# y} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(size#) = 0 Strict: {size# n(x, y, z) -> size# y} EDG: {(size# n(x, y, z) -> size# y, size# n(x, y, z) -> size# y)} SCCS (1): Scc: {size# n(x, y, z) -> size# y} SCC (1): Strict: {size# n(x, y, z) -> size# y} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(size#) = 0 Strict: {} Qed SCC (2): Strict: {bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> bs# z} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(bs#) = 0 Strict: {bs# n(x, y, z) -> bs# z} EDG: {(bs# n(x, y, z) -> bs# z, bs# n(x, y, z) -> bs# z)} SCCS (1): Scc: {bs# n(x, y, z) -> bs# z} SCC (1): Strict: {bs# n(x, y, z) -> bs# z} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(bs#) = 0 Strict: {} Qed SCC (1): Strict: {max# n(x, y, z) -> max# z} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(max#) = 0 Strict: {} Qed SCC (1): Strict: {min# n(x, y, z) -> min# y} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(min#) = 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, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 1, [n](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = x0, [not](x0) = x0 + 1, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = 0, [max](x0) = x0 + 1, [bs](x0) = x0 + 1, [size](x0) = 1, [wb](x0) = 0, [#] = 1, [true] = 1, [false] = 0, [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, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} SPSC: Simple Projection: pi(ge#) = 1 Strict: {} Qed SCC (1): Strict: {ge#(#(), 0 x) -> ge#(#(), x)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} 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, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [n](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0, [and](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + x1 + 1, [0](x0) = x0 + 1, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = 0, [max](x0) = x0 + 1, [bs](x0) = x0 + 1, [size](x0) = x0 + 1, [wb](x0) = x0 + 1, [#] = 1, [true] = 1, [false] = 1, [-#](x0, x1) = x0 + 1 Strict: -#(1 x, 1 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(1 x, 0 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(0 x, 1 y) -> -#(-(x, y), 1 #()) 2 + 1x + 0y >= 1 + 1x + 0y -#(0 x, 1 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(0 x, 0 y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: Qed SCC (7): Strict: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [n](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1, [-](x0, x1) = 0, [and](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0, [0](x0) = x0 + 1, [1](x0) = x0, [not](x0) = x0 + 1, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = 0, [max](x0) = x0 + 1, [bs](x0) = x0 + 1, [size](x0) = x0 + 1, [wb](x0) = x0 + 1, [#] = 0, [true] = 1, [false] = 1, [+#](x0, x1) = x0 Strict: +#(1 x, 1 y) -> +#(+(x, y), 1 #()) 0 + 0x + 1y >= 0 + 0x + 0y +#(1 x, 1 y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(1 x, 0 y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +#(0 x, 1 y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(0 x, 0 y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +#(x, +(y, z)) -> +#(+(x, y), z) 0 + 0x + 1y + 1z >= 0 + 0x + 0y + 1z +#(x, +(y, z)) -> +#(x, y) 0 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: EDG: {(+#(x, +(y, z)) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())) (+#(x, +(y, z)) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(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), +#(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)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(0 x, 1 y) -> +#(x, y)) (+#(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 #())) (+#(0 x, 1 y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(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), +#(1 x, 1 y) -> +#(x, y)) (+#(0 x, 1 y) -> +#(x, y), +#(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 #()), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))} SCCS (1): Scc: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())} SCC (5): Strict: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0, [n](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = 0, [and](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = 0, [1](x0) = x0, [not](x0) = x0 + 1, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = x0 + 1, [max](x0) = x0 + 1, [bs](x0) = 0, [size](x0) = x0 + 1, [wb](x0) = x0 + 1, [#] = 0, [true] = 1, [false] = 1, [+#](x0, x1) = x0 Strict: +#(1 x, 1 y) -> +#(+(x, y), 1 #()) 0 + 0x + 1y >= 0 + 0x + 0y +#(1 x, 1 y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(0 x, 1 y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(x, +(y, z)) -> +#(+(x, y), z) 1 + 0x + 1y + 1z >= 0 + 0x + 0y + 1z +#(x, +(y, z)) -> +#(x, y) 1 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: EDG: {(+#(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), +#(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, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(x, y), +#(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 #()), +#(1 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))} SCCS (1): Scc: {+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())} SCC (3): Strict: {+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #())} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [n](x0, x1, x2) = 1, [+](x0, x1) = 0, [-](x0, x1) = 0, [and](x0, x1) = 0, [ge](x0, x1) = x0 + x1 + 1, [0](x0) = 0, [1](x0) = x0 + 1, [not](x0) = 0, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = x0 + 1, [max](x0) = x0 + 1, [bs](x0) = x0 + 1, [size](x0) = x0 + 1, [wb](x0) = x0 + 1, [#] = 0, [true] = 1, [false] = 1, [+#](x0, x1) = x0 Strict: +#(1 x, 1 y) -> +#(+(x, y), 1 #()) 1 + 0x + 1y >= 1 + 0x + 0y +#(1 x, 1 y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +#(0 x, 1 y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: EDG: {(+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))} SCCS (1): Scc: {+#(1 x, 1 y) -> +#(+(x, y), 1 #())} SCC (1): Strict: {+#(1 x, 1 y) -> +#(+(x, y), 1 #())} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(#(), x) -> x, +(0 x, 0 y) -> 0 +(x, y), +(0 x, 1 y) -> 1 +(x, y), +(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 true() -> false(), not false() -> true(), and(x, true()) -> x, and(x, false()) -> false(), if(true(), x, y) -> x, if(false(), x, y) -> 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), val l x -> x, val n(x, y, z) -> x, min l x -> x, min n(x, y, z) -> min y, max l x -> x, max n(x, y, z) -> max z, bs l x -> true(), bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)), size l x -> 1 #(), size n(x, y, z) -> +(+(size x, size y), 1 #()), wb l x -> true(), wb n(x, y, z) -> and(if(ge(size y, size z), ge(1 #(), -(size y, size z)), ge(1 #(), -(size z, size y))), and(wb y, wb z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [n](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1, [-](x0, x1) = 0, [and](x0, x1) = x0 + 1, [ge](x0, x1) = 0, [0](x0) = x0, [1](x0) = x0 + 1, [not](x0) = x0 + 1, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = x0 + 1, [max](x0) = x0 + 1, [bs](x0) = x0 + 1, [size](x0) = 0, [wb](x0) = x0 + 1, [#] = 0, [true] = 1, [false] = 1, [+#](x0, x1) = x0 + x1 + 1 Strict: +#(1 x, 1 y) -> +#(+(x, y), 1 #()) 3 + 1x + 1y >= 2 + 1x + 1y Weak: Qed