YES Time: 0.749428 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))} UR: { 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), 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)), a(w, v) -> w, a(w, v) -> v} 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#(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, 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 #()), -#(1 x, 0 y) -> -#(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)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 0 y) -> -#(x, y)) (-#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(0 x, 0 y) -> 0# -(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)) (wb# n(x, y, z) -> ge#(1 #(), -(size y, size z)), ge#(0 x, 1 y) -> ge#(y, x)) (wb# n(x, y, z) -> ge#(1 #(), -(size y, size z)), ge#(0 x, 1 y) -> not# ge(y, x)) (wb# n(x, y, z) -> ge#(1 #(), -(size y, size z)), ge#(0 x, 0 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(1 #(), -(size y, size z)), ge#(#(), 0 x) -> ge#(#(), x)) (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#(#(), 0 x) -> ge#(#(), x)) (wb# n(x, y, z) -> ge#(1 #(), -(size z, size y)), ge#(0 x, 0 y) -> ge#(x, y)) (wb# n(x, y, z) -> ge#(1 #(), -(size z, size y)), ge#(0 x, 1 y) -> not# ge(y, x)) (wb# n(x, y, z) -> ge#(1 #(), -(size z, size y)), ge#(0 x, 1 y) -> ge#(y, x)) (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 #()), +#(x, +(y, z)) -> +#(x, y)) (size# n(x, y, z) -> +#(+(size x, size y), 1 #()), +#(x, +(y, z)) -> +#(+(x, y), z)) (size# n(x, y, z) -> +#(+(size x, size y), 1 #()), +#(0 x, 0 y) -> 0# +(x, y)) (size# n(x, y, z) -> +#(+(size x, size y), 1 #()), +#(0 x, 0 y) -> +#(x, y)) (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, 0 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 #()), +#(x, +(y, z)) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 0 y) -> 0# +(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 0 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y)) (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 0 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) } 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) } 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) } 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) } STATUS: arrows: 0.905873 SCCS (9): Scc: {wb# n(x, y, z) -> wb# y, wb# n(x, y, z) -> wb# z} 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: {size# n(x, y, z) -> size# x, size# n(x, y, z) -> size# 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: {bs# n(x, y, z) -> bs# y, bs# n(x, y, z) -> bs# z} Scc: {min# n(x, y, z) -> min# y} Scc: {max# n(x, y, z) -> max# z} 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 (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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [n](x0, x1, x2) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = 0, [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) = 0, [#] = 1, [true] = 1, [false] = 1, [wb#](x0) = x0 Strict: wb# n(x, y, z) -> wb# z 1 + 0x + 1y + 1z >= 0 + 1z wb# n(x, y, z) -> wb# y 1 + 0x + 1y + 1z >= 0 + 1y Weak: 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)) 0 + 0x + 0y + 0z >= 2 + 0y + 0z wb l x -> true() 0 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 0 + 0x + 0y + 0z >= 2 + 0x + 0y size l x -> 1 #() 0 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 1y + 1z >= 3 + 0x + 0y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 1y + 1z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 1y + 1z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 1y + 1z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 0x >= 1 and(x, true()) -> x 2 + 0x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(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, +(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: 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)) 2 + 0x + 0y + 0z >= 4 + 1y + 1z wb l x -> true() 2 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 2 + 0x + 0y + 0z >= 6 + 1x + 1y size l x -> 1 #() 2 + 0x >= 2 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 0z >= 8 + 2x + 2y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 0 + 0x + 0y + 0z >= 0 + 0y min l x -> x 0 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x ge(1 x, 1 y) -> ge(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge(1 x, 0 y) -> ge(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge(0 x, 1 y) -> not ge(y, x) 3 + 1x + 1y >= 2 + 1x + 1y ge(0 x, 0 y) -> ge(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge(#(), 1 x) -> false() 3 + 1x >= 1 ge(#(), 0 x) -> ge(#(), x) 3 + 1x >= 2 + 1x ge(x, #()) -> true() 2 + 1x >= 1 if(false(), x, y) -> y 0 + 0x + 0y >= 1y if(true(), x, y) -> x 0 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 1x >= 1 and(x, true()) -> x 2 + 1x >= 1x not false() -> true() 2 >= 1 not true() -> false() 2 >= 1 -(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 #()) 3 + 1x + 1y >= 5 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [n](x0, x1, x2) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = 0, [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) = 0, [#] = 1, [true] = 1, [false] = 1, [size#](x0) = x0 Strict: size# n(x, y, z) -> size# y 1 + 1x + 1y + 0z >= 0 + 1y size# n(x, y, z) -> size# x 1 + 1x + 1y + 0z >= 0 + 1x Weak: 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)) 0 + 0x + 0y + 0z >= 2 + 0y + 0z wb l x -> true() 0 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 0 + 0x + 0y + 0z >= 2 + 0x + 0y size l x -> 1 #() 0 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 1x + 1y + 0z >= 3 + 0x + 0y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 1x + 1y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 1x + 1y + 0z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 1x + 1y + 0z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 0x >= 1 and(x, true()) -> x 2 + 0x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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: 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)) 2 + 0x + 0y + 0z >= 6 + 2y + 1z wb l x -> true() 2 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 2 + 0x + 0y + 0z >= 2 + 1x + 1y size l x -> 1 #() 2 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 0z >= 5 + 1x + 1y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 0 + 0x + 0y + 0z >= 0 + 0y min l x -> x 0 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x ge(1 x, 1 y) -> ge(x, y) 0 + 1x + 0y >= 0 + 1x + 0y ge(1 x, 0 y) -> ge(x, y) 0 + 1x + 0y >= 0 + 1x + 0y ge(0 x, 1 y) -> not ge(y, x) 1 + 1x + 0y >= 1 + 0x + 1y ge(0 x, 0 y) -> ge(x, y) 1 + 1x + 0y >= 0 + 1x + 0y ge(#(), 1 x) -> false() 0 + 0x >= 1 ge(#(), 0 x) -> ge(#(), x) 0 + 0x >= 0 + 0x ge(x, #()) -> true() 0 + 1x >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 1x >= 1 and(x, true()) -> x 2 + 1x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 + 1x + 1y >= 1 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 1 + 1x + 1y >= 0 + 1x + 1y +(0 x, 1 y) -> 1 +(x, y) 1 + 1x + 1y >= 0 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(#(), x) -> x 0 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +(x, #()) -> x 0 + 1x >= 1x 0 #() -> #() 1 >= 0 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: 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)) 2 + 0x + 0y + 0z >= 6 + 2y + 1z wb l x -> true() 2 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 2 + 0x + 0y + 0z >= 4 + 1x + 1y size l x -> 1 #() 2 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 0 + 0x + 0y + 0z >= 6 + 1x + 0y + 1z bs l x -> true() 0 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 0y + 0z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x ge(1 x, 1 y) -> ge(x, y) 1 + 1x + 0y >= 1 + 1x + 0y ge(1 x, 0 y) -> ge(x, y) 1 + 1x + 0y >= 1 + 1x + 0y ge(0 x, 1 y) -> not ge(y, x) 1 + 0x + 0y >= 2 + 0x + 1y ge(0 x, 0 y) -> ge(x, y) 1 + 0x + 0y >= 1 + 1x + 0y ge(#(), 1 x) -> false() 1 + 0x >= 1 ge(#(), 0 x) -> ge(#(), x) 1 + 0x >= 1 + 0x ge(x, #()) -> true() 1 + 1x >= 1 if(false(), x, y) -> y 1 + 0x + 0y >= 1y if(true(), x, y) -> x 1 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 1x >= 1 and(x, true()) -> x 2 + 1x >= 1x not false() -> true() 2 >= 1 not true() -> false() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 0 + 0x + 0y >= 0 + 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 >= 0 + 0x + 0y -(#(), x) -> #() 0 + 0x >= 0 -(x, #()) -> x 0 + 0x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 1 + 1x + 1y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 1 + 1x + 0y >= 1 + 1x + 1y +(0 x, 1 y) -> 1 +(x, y) 1 + 0x + 1y >= 1 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 1 + 0x + 0y >= 0 + 0x + 0y +(#(), x) -> x 1 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 1 + 1x >= 1x 0 #() -> #() 0 >= 0 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: 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)) 2 + 0x + 0y + 0z >= 0 + 0y + 0z wb l x -> true() 2 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 2 + 0x + 0y + 0z >= 0 + 0x + 0y size l x -> 1 #() 2 + 0x >= 1 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 0y + 0z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x ge(1 x, 1 y) -> ge(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge(1 x, 0 y) -> ge(x, y) 2 + 1x + 0y >= 1 + 1x + 1y ge(0 x, 1 y) -> not ge(y, x) 2 + 0x + 1y >= 0 + 0x + 0y ge(0 x, 0 y) -> ge(x, y) 1 + 0x + 0y >= 1 + 1x + 1y ge(#(), 1 x) -> false() 2 + 1x >= 1 ge(#(), 0 x) -> ge(#(), x) 1 + 0x >= 1 + 1x ge(x, #()) -> true() 1 + 1x >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 0 + 0x >= 1 and(x, true()) -> x 0 + 0x >= 1x not false() -> true() 0 >= 1 not true() -> false() 0 >= 1 -(1 x, 1 y) -> 0 -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(1 x, 0 y) -> 1 -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 0 + 0x + 0y >= 1 + 0x + 0y -(0 x, 0 y) -> 0 -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(#(), x) -> #() 0 + 0x >= 0 -(x, #()) -> x 0 + 0x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 0 + 0x + 0y >= 0 + 0x + 0y +(1 x, 0 y) -> 1 +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(0 x, 1 y) -> 1 +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(0 x, 0 y) -> 0 +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(#(), x) -> x 0 + 0x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z +(x, #()) -> x 0 + 0x >= 1x 0 #() -> #() 0 >= 0 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: 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)) 2 + 0x + 0y + 0z >= 3 + 0y + 1z wb l x -> true() 2 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 0 + 0x + 0y + 0z >= 1 + 0x + 0y size l x -> 1 #() 0 + 0x >= 1 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 0z >= 3 + 0x + 0y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 0y + 0z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 0x >= 1 and(x, true()) -> x 2 + 0x >= 1x not false() -> true() 2 >= 1 not true() -> false() 2 >= 1 -(1 x, 1 y) -> 0 -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(1 x, 0 y) -> 1 -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(0 x, 1 y) -> 1 -(-(x, y), 1 #()) 0 + 0x + 0y >= 1 + 0x + 0y -(0 x, 0 y) -> 0 -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(#(), x) -> #() 0 + 0x >= 0 -(x, #()) -> x 0 + 0x >= 1x +(1 x, 1 y) -> 0 +(+(x, y), 1 #()) 2 + 1x + 1y >= 1 + 1x + 1y +(1 x, 0 y) -> 1 +(x, y) 1 + 1x + 1y >= 1 + 1x + 1y +(0 x, 1 y) -> 1 +(x, y) 1 + 1x + 1y >= 1 + 1x + 1y +(0 x, 0 y) -> 0 +(x, y) 0 + 1x + 1y >= 0 + 1x + 1y +(#(), x) -> x 0 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +(x, #()) -> x 0 + 1x >= 1x 0 #() -> #() 0 >= 0 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [n](x0, x1, x2) = x0 + x1 + 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = 0, [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) = 0, [#] = 1, [true] = 1, [false] = 1, [bs#](x0) = x0 Strict: bs# n(x, y, z) -> bs# z 1 + 0x + 1y + 1z >= 0 + 1z bs# n(x, y, z) -> bs# y 1 + 0x + 1y + 1z >= 0 + 1y Weak: 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)) 0 + 0x + 0y + 0z >= 2 + 0y + 0z wb l x -> true() 0 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 0 + 0x + 0y + 0z >= 2 + 0x + 0y size l x -> 1 #() 0 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 1y + 1z >= 3 + 0x + 0y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 1y + 1z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 1y + 1z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 1y + 1z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 0x >= 1 and(x, true()) -> x 2 + 0x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1 + 1, [n](x0, x1, x2) = x0 + 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) = 0, [not](x0) = x0 + 1, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = x0 + 1, [max](x0) = 0, [bs](x0) = x0 + 1, [size](x0) = x0 + 1, [wb](x0) = 0, [#] = 1, [true] = 1, [false] = 1, [min#](x0) = x0 Strict: min# n(x, y, z) -> min# y 1 + 0x + 1y + 0z >= 0 + 1y Weak: 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)) 0 + 0x + 0y + 0z >= 9 + 1y + 2z wb l x -> true() 0 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 2 + 0x + 1y + 0z >= 4 + 1x + 1y size l x -> 1 #() 2 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 1y + 0z >= 7 + 1x + 1y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 0 + 0x + 0y + 0z >= 0 + 0z max l x -> x 0 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 1y + 0z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 1y + 0z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 1x + 0y >= 1y if(true(), x, y) -> x 2 + 1x + 0y >= 1x and(x, false()) -> false() 2 + 1x >= 1 and(x, true()) -> x 2 + 1x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1 + 1, [n](x0, x1, x2) = x0 + 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) = 0, [not](x0) = x0 + 1, [val](x0) = x0 + 1, [l](x0) = 1, [min](x0) = x0 + 1, [max](x0) = 0, [bs](x0) = x0 + 1, [size](x0) = x0 + 1, [wb](x0) = x0 + 1, [#] = 1, [true] = 1, [false] = 1, [max#](x0) = x0 Strict: max# n(x, y, z) -> max# z 1 + 0x + 0y + 1z >= 0 + 1z Weak: 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)) 2 + 0x + 0y + 1z >= 11 + 2y + 3z wb l x -> true() 2 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 2 + 0x + 0y + 1z >= 4 + 1x + 1y size l x -> 1 #() 2 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 1z >= 7 + 1x + 1y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 0 + 0x + 0y + 0z >= 0 + 0z max l x -> x 0 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 0y + 1z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 1z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 1x + 0y >= 1y if(true(), x, y) -> x 2 + 1x + 0y >= 1x and(x, false()) -> false() 2 + 1x >= 1 and(x, true()) -> x 2 + 1x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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: 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)) 0 + 0x + 0y + 0z >= 3 + 0y + 0z wb l x -> true() 0 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 1 + 0x + 0y + 0z >= 5 + 0x + 0y size l x -> 1 #() 1 + 0x >= 1 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 0z >= 7 + 1x + 1y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 0 + 0x + 0y + 0z >= 0 + 0y min l x -> x 0 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x ge(1 x, 1 y) -> ge(x, y) 1 + 1x + 0y >= 1 + 1x + 0y ge(1 x, 0 y) -> ge(x, y) 1 + 1x + 0y >= 1 + 1x + 0y ge(0 x, 1 y) -> not ge(y, x) 2 + 1x + 0y >= 2 + 0x + 1y ge(0 x, 0 y) -> ge(x, y) 2 + 1x + 0y >= 1 + 1x + 0y ge(#(), 1 x) -> false() 2 + 0x >= 0 ge(#(), 0 x) -> ge(#(), x) 2 + 0x >= 2 + 0x ge(x, #()) -> true() 1 + 1x >= 1 if(false(), x, y) -> y 1 + 0x + 0y >= 1y if(true(), x, y) -> x 1 + 0x + 0y >= 1x and(x, false()) -> false() 1 + 1x >= 0 and(x, true()) -> x 2 + 1x >= 1x not false() -> true() 1 >= 1 not true() -> false() 2 >= 0 -(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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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))} 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 + 1, [-](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [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) = 1, [wb](x0) = 0, [#] = 1, [true] = 1, [false] = 1, [ge#](x0, x1) = x0 Strict: ge#(1 x, 1 y) -> ge#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: 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)) 0 + 0x + 0y + 0z >= 5 + 0y + 0z wb l x -> true() 0 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 1 + 0x + 0y + 0z >= 6 + 0x + 0y size l x -> 1 #() 1 + 0x >= 2 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 0z >= 8 + 1x + 2y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 0y + 0z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 1x >= 1 and(x, true()) -> x 2 + 1x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 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))} 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 + 1, [-](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + 1, [0](x0) = x0 + 1, [1](x0) = 0, [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) = x0 + 1, [wb](x0) = x0 + 1, [#] = 1, [true] = 1, [false] = 1, [ge#](x0, x1) = x0 + 1 Strict: ge#(#(), 0 x) -> ge#(#(), x) 2 + 1x >= 1 + 1x Weak: 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)) 2 + 0x + 0y + 0z >= 3 + 0y + 1z wb l x -> true() 2 + 0x >= 1 size n(x, y, z) -> +(+(size x, size y), 1 #()) 2 + 0x + 0y + 0z >= 4 + 1x + 1y size l x -> 1 #() 2 + 0x >= 0 bs n(x, y, z) -> and(and(ge(x, max y), ge(min z, x)), and(bs y, bs z)) 2 + 0x + 0y + 0z >= 3 + 0x + 0y + 1z bs l x -> true() 2 + 0x >= 1 max n(x, y, z) -> max z 2 + 0x + 0y + 0z >= 1 + 1z max l x -> x 2 + 0x >= 1x min n(x, y, z) -> min y 2 + 0x + 0y + 0z >= 1 + 1y min l x -> x 2 + 0x >= 1x val n(x, y, z) -> x 2 + 0x + 0y + 0z >= 1x val l x -> x 2 + 0x >= 1x 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(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x and(x, false()) -> false() 2 + 0x >= 1 and(x, true()) -> x 2 + 0x >= 1x not false() -> true() 2 >= 1 not true() -> false() 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 +(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, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, #()) -> x 2 + 1x >= 1x 0 #() -> #() 2 >= 1 Qed