MAYBE Time: 0.102906 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))} Open SCC (5): Strict: {-#(0 x, 0 y) -> -#(x, y), -#(0 x, 1 y) -> -#(x, y), -#(0 x, 1 y) -> -#(-(x, y), 1 #()), -#(1 x, 0 y) -> -#(x, y), -#(1 x, 1 y) -> -#(x, y)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(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))} Open 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))} Open 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))} Open 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))} Open 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))} Open 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))} Open SCC (4): Strict: {ge#(0 x, 0 y) -> ge#(x, y), ge#(0 x, 1 y) -> ge#(y, x), ge#(1 x, 0 y) -> ge#(x, y), ge#(1 x, 1 y) -> ge#(x, y)} Weak: { 0 #() -> #(), +(x, #()) -> x, +(x, +(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))} Open 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))} Open