Problem: not(T()) -> F() not(F()) -> T() or(x,T()) -> T() or(x,F()) -> x or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) and(x,T()) -> x and(x,F()) -> F() and(x,y) -> and(y,x) and(and(x,y),z) -> and(x,and(y,z)) imply(x,y) -> or(not(x),y) Proof: sorted: (order) 0:not(T()) -> F() not(F()) -> T() or(x,T()) -> T() or(x,F()) -> x or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) imply(x,y) -> or(not(x),y) 1:and(x,T()) -> x and(x,F()) -> F() and(x,y) -> and(y,x) and(and(x,y),z) -> and(x,and(y,z)) ----- sorts [1>3, 2>8, 2>9, 3>4, 3>5, 5>6, 6>7, 6>8, 6>9] sort attachment (non-strict) not : 6 -> 5 T : 9 F : 8 or : 3 x 3 -> 3 and : 2 x 2 -> 2 imply : 7 x 4 -> 1 ----- 0:not(T()) -> F() not(F()) -> T() or(x,T()) -> T() or(x,F()) -> x or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) imply(x,y) -> or(not(x),y) Commute Transformation Processor: not(T()) -> F() not(F()) -> T() or(x,T()) -> T() or(T(),x) -> T() or(x,F()) -> x or(F(),x) -> x or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) imply(x,y) -> or(not(x),y) Church Rosser Transformation Processor (dup): strict: weak: not(T()) -> F() not(F()) -> T() or(x,T()) -> T() or(T(),x) -> T() or(x,F()) -> x or(F(),x) -> x or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) imply(x,y) -> or(not(x),y) critical peaks: 44 T() <-2|[]- or(T(),T()) -3|[]-> T() T() <-2|[]- or(F(),T()) -5|[]-> T() T() <-2|[]- or(x,T()) -6|[]-> or(T(),x) T() <-2|[]- or(or(x,y),T()) -7|[]-> or(x,or(y,T())) or(T(),z) <-2|0[]- or(or(x,T()),z) -7|[]-> or(x,or(T(),z)) or(x,T()) <-2|1[]- or(x,or(y,T())) -8|[]-> or(or(x,y),T()) T() <-3|[]- or(T(),T()) -2|[]-> T() T() <-3|[]- or(T(),F()) -4|[]-> T() T() <-3|[]- or(T(),y) -6|[]-> or(y,T()) or(T(),z) <-3|0[]- or(or(T(),y),z) -7|[]-> or(T(),or(y,z)) T() <-3|[]- or(T(),or(y,z)) -8|[]-> or(or(T(),y),z) or(x,T()) <-3|1[]- or(x,or(T(),z)) -8|[]-> or(or(x,T()),z) T() <-4|[]- or(T(),F()) -3|[]-> T() F() <-4|[]- or(F(),F()) -5|[]-> F() x <-4|[]- or(x,F()) -6|[]-> or(F(),x) or(x,y) <-4|[]- or(or(x,y),F()) -7|[]-> or(x,or(y,F())) or(x,z) <-4|0[]- or(or(x,F()),z) -7|[]-> or(x,or(F(),z)) or(x,y) <-4|1[]- or(x,or(y,F())) -8|[]-> or(or(x,y),F()) T() <-5|[]- or(F(),T()) -2|[]-> T() F() <-5|[]- or(F(),F()) -4|[]-> F() y <-5|[]- or(F(),y) -6|[]-> or(y,F()) or(y,z) <-5|0[]- or(or(F(),y),z) -7|[]-> or(F(),or(y,z)) or(y,z) <-5|[]- or(F(),or(y,z)) -8|[]-> or(or(F(),y),z) or(x,z) <-5|1[]- or(x,or(F(),z)) -8|[]-> or(or(x,F()),z) or(T(),x) <-6|[]- or(x,T()) -2|[]-> T() or(x,T()) <-6|[]- or(T(),x) -3|[]-> T() or(F(),x) <-6|[]- or(x,F()) -4|[]-> x or(x,F()) <-6|[]- or(F(),x) -5|[]-> x or(z,or(x,y)) <-6|[]- or(or(x,y),z) -7|[]-> or(x,or(y,z)) or(or(y,x),z) <-6|0[]- or(or(x,y),z) -7|[]-> or(x,or(y,z)) or(or(y,z),x) <-6|[]- or(x,or(y,z)) -8|[]-> or(or(x,y),z) or(x,or(z,y)) <-6|1[]- or(x,or(y,z)) -8|[]-> or(or(x,y),z) or(x295,or(x296,T())) <-7|[]- or(or(x295,x296),T()) -2|[]-> T() or(x298,or(x299,F())) <-7|[]- or(or(x298,x299),F()) -4|[]-> or(x298,x299) or(x301,or(x302,y)) <-7|[]- or(or(x301,x302),y) -6|[]-> or(y,or(x301,x302)) or(or(x304,or(x305,y)),z) <-7|0[]- or(or(or(x304,x305),y),z) -7|[]-> or(or(x304,x305),or(y,z)) or(x307,or(x308,or(y,z))) <-7|[]- or(or(x307,x308),or(y,z)) -8|[]-> or(or(or(x307,x308),y),z) or(x,or(x310,or(x311,z))) <-7|1[]- or(x,or(or(x310,x311),z)) -8|[]-> or(or(x,or(x310,x311)),z) or(or(T(),x314),x315) <-8|[]- or(T(),or(x314,x315)) -3|[]-> T() or(or(F(),x317),x318) <-8|[]- or(F(),or(x317,x318)) -5|[]-> or(x317,x318) or(or(x,x320),x321) <-8|[]- or(x,or(x320,x321)) -6|[]-> or(or(x320,x321),x) or(or(or(x,y),x323),x324) <-8|[]- or(or(x,y),or(x323,x324)) -7|[]-> or(x,or(y,or(x323,x324))) or(or(or(x,x326),x327),z) <-8|0[]- or(or(x,or(x326,x327)),z) -7|[]-> or(x,or(or(x326,x327),z)) or(x,or(or(y,x329),x330)) <-8|1[]- or(x,or(y,or(x329,x330))) -8|[]-> or(or(x,y),or(x329,x330)) Polynomial Interpretation Processor: dimension: 1 interpretation: [imply](x0, x1) = x0 + 2x1 + 3x0x0 + 2x1x1 + 2, [or](x0, x1) = x0 + x1 + 1, [F] = 0, [not](x0) = x0 + 3x0x0, [T] = 0 orientation: not(T()) = 0 >= 0 = F() not(F()) = 0 >= 0 = T() or(x,T()) = x + 1 >= 0 = T() or(T(),x) = x + 1 >= 0 = T() or(x,F()) = x + 1 >= x = x or(F(),x) = x + 1 >= x = x or(x,y) = x + y + 1 >= x + y + 1 = or(y,x) or(or(x,y),z) = x + y + z + 2 >= x + y + z + 2 = or(x,or(y,z)) or(x,or(y,z)) = x + y + z + 2 >= x + y + z + 2 = or(or(x,y),z) imply(x,y) = x + 3x*x + 2y + 2y*y + 2 >= x + 3x*x + y + 1 = or(not(x),y) problem: strict: weak: not(T()) -> F() not(F()) -> T() or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) Polynomial Interpretation Processor: dimension: 1 interpretation: [or](x0, x1) = x0 + x1, [F] = 2, [not](x0) = 2x0x0 + 3, [T] = 0 orientation: not(T()) = 3 >= 2 = F() not(F()) = 11 >= 0 = T() or(x,y) = x + y >= x + y = or(y,x) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) problem: strict: weak: or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: or(T(),T()) -> T() or(T(),T()) -> T() or(F(),T()) -> T() or(F(),T()) -> T() or(x,T()) -> T() or(x,T()) -> or(T(),x) or(T(),x) -> T() or(or(x,y),T()) -> T() or(or(x,y),T()) -> or(x,or(y,T())) or(x,or(y,T())) -> or(x,T()) or(x,T()) -> T() or(x,or(y,T())) -> or(or(x,y),T()) or(or(x,y),T()) -> T() or(or(x,T()),z) -> or(T(),z) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,or(T(),z)) -> or(or(x,T()),z) or(or(x,T()),z) -> or(T(),z) or(T(),z) -> T() or(x,or(T(),z)) -> or(x,T()) or(x,T()) -> T() or(T(),z) -> or(z,T()) or(z,T()) -> T() or(x,or(T(),z)) -> or(x,T()) or(x,T()) -> T() or(x,or(y,T())) -> or(x,T()) or(x,or(y,T())) -> or(or(x,y),T()) or(x,T()) -> T() or(or(x,y),T()) -> T() or(T(),T()) -> T() or(T(),T()) -> T() or(T(),F()) -> T() or(T(),F()) -> T() or(T(),y) -> T() or(T(),y) -> or(y,T()) or(y,T()) -> T() or(or(T(),y),z) -> or(T(),z) or(or(T(),y),z) -> or(T(),or(y,z)) or(T(),z) -> T() or(T(),or(y,z)) -> T() or(T(),or(y,z)) -> T() or(T(),or(y,z)) -> or(or(T(),y),z) or(or(T(),y),z) -> or(T(),z) or(T(),z) -> T() or(or(T(),y),z) -> or(T(),or(y,z)) or(T(),or(y,z)) -> T() or(x,or(T(),z)) -> or(x,T()) or(x,or(T(),z)) -> or(or(x,T()),z) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,or(T(),z)) -> or(x,T()) or(x,T()) -> T() or(or(x,T()),z) -> or(T(),z) or(T(),z) -> T() or(x,T()) -> or(T(),x) or(T(),x) -> T() or(or(x,T()),z) -> or(T(),z) or(T(),z) -> T() or(T(),F()) -> T() or(T(),F()) -> T() or(F(),F()) -> F() or(F(),F()) -> F() or(x,F()) -> x or(x,F()) -> or(F(),x) or(F(),x) -> x or(or(x,y),F()) -> or(x,y) or(or(x,y),F()) -> or(x,or(y,F())) or(x,or(y,F())) -> or(x,y) or(or(x,F()),z) -> or(x,z) or(or(x,F()),z) -> or(x,or(F(),z)) or(x,or(F(),z)) -> or(x,z) or(x,or(y,F())) -> or(x,y) or(x,or(y,F())) -> or(or(x,y),F()) or(or(x,y),F()) -> or(x,y) or(F(),T()) -> T() or(F(),T()) -> T() or(F(),F()) -> F() or(F(),F()) -> F() or(F(),y) -> y or(F(),y) -> or(y,F()) or(y,F()) -> y or(or(F(),y),z) -> or(y,z) or(or(F(),y),z) -> or(F(),or(y,z)) or(F(),or(y,z)) -> or(y,z) or(F(),or(y,z)) -> or(y,z) or(F(),or(y,z)) -> or(or(F(),y),z) or(or(F(),y),z) -> or(y,z) or(x,or(F(),z)) -> or(x,z) or(x,or(F(),z)) -> or(or(x,F()),z) or(or(x,F()),z) -> or(x,z) or(x,T()) -> or(T(),x) or(x,T()) -> T() or(T(),x) -> T() or(T(),x) -> or(x,T()) or(T(),x) -> T() or(x,T()) -> T() or(x,F()) -> or(F(),x) or(x,F()) -> x or(F(),x) -> x or(F(),x) -> or(x,F()) or(F(),x) -> x or(x,F()) -> x or(or(x,y),z) -> or(z,or(x,y)) or(or(x,y),z) -> or(x,or(y,z)) or(z,or(x,y)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(or(x,y),z) -> or(or(y,x),z) or(or(x,y),z) -> or(x,or(y,z)) or(or(y,x),z) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(y,z),x) or(x,or(y,z)) -> or(or(x,y),z) or(or(y,z),x) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(x,or(z,y)) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(z,y)) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(or(x295,x296),T()) -> or(x295,or(x296,T())) or(or(x295,x296),T()) -> T() or(x295,or(x296,T())) -> or(x295,T()) or(x295,T()) -> T() or(x295,or(x296,T())) -> or(or(x295,x296),T()) or(or(x295,x296),T()) -> T() or(or(x298,x299),F()) -> or(x298,or(x299,F())) or(or(x298,x299),F()) -> or(x298,x299) or(x298,or(x299,F())) -> or(x298,x299) or(or(x301,x302),y) -> or(x301,or(x302,y)) or(or(x301,x302),y) -> or(y,or(x301,x302)) or(x301,or(x302,y)) -> or(or(x301,x302),y) or(y,or(x301,x302)) -> or(or(x301,x302),y) or(or(or(x304,x305),y),z) -> or(or(x304,or(x305,y)),z) or(or(or(x304,x305),y),z) -> or(or(x304,x305),or(y,z)) or(or(x304,or(x305,y)),z) -> or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) -> or(or(or(x304,x305),y),z) or(or(x307,x308),or(y,z)) -> or(x307,or(x308,or(y,z))) or(or(x307,x308),or(y,z)) -> or(or(or(x307,x308),y),z) or(x307,or(x308,or(y,z))) -> or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) -> or(or(x307,x308),or(y,z)) or(x,or(or(x310,x311),z)) -> or(x,or(x310,or(x311,z))) or(x,or(or(x310,x311),z)) -> or(or(x,or(x310,x311)),z) or(x,or(x310,or(x311,z))) -> or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) -> or(x,or(or(x310,x311),z)) or(T(),or(x314,x315)) -> or(or(T(),x314),x315) or(T(),or(x314,x315)) -> T() or(or(T(),x314),x315) -> or(T(),x315) or(T(),x315) -> T() or(or(T(),x314),x315) -> or(T(),or(x314,x315)) or(T(),or(x314,x315)) -> T() or(F(),or(x317,x318)) -> or(or(F(),x317),x318) or(F(),or(x317,x318)) -> or(x317,x318) or(or(F(),x317),x318) -> or(x317,x318) or(x,or(x320,x321)) -> or(or(x,x320),x321) or(x,or(x320,x321)) -> or(or(x320,x321),x) or(or(x,x320),x321) -> or(x,or(x320,x321)) or(or(x320,x321),x) -> or(x,or(x320,x321)) or(or(x,y),or(x323,x324)) -> or(or(or(x,y),x323),x324) or(or(x,y),or(x323,x324)) -> or(x,or(y,or(x323,x324))) or(or(or(x,y),x323),x324) -> or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) -> or(or(x,y),or(x323,x324)) or(or(x,or(x326,x327)),z) -> or(or(or(x,x326),x327),z) or(or(x,or(x326,x327)),z) -> or(x,or(or(x326,x327),z)) or(or(or(x,x326),x327),z) -> or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) -> or(or(x,or(x326,x327)),z) or(x,or(y,or(x329,x330))) -> or(x,or(or(y,x329),x330)) or(x,or(y,or(x329,x330))) -> or(or(x,y),or(x329,x330)) or(x,or(or(y,x329),x330)) -> or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) -> or(x,or(y,or(x329,x330))) weak: not(T()) -> F() not(F()) -> T() or(x,T()) -> T() or(T(),x) -> T() or(x,F()) -> x or(F(),x) -> x or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) imply(x,y) -> or(not(x),y) Polynomial Interpretation Processor: dimension: 1 interpretation: [imply](x0, x1) = 3x0 + x1 + x1x1 + 2, [or](x0, x1) = x0 + x1, [F] = 1, [not](x0) = 3x0 + 1, [T] = 0 orientation: or(T(),T()) = 0 >= 0 = T() or(T(),T()) = 0 >= 0 = T() or(F(),T()) = 1 >= 0 = T() or(F(),T()) = 1 >= 0 = T() or(x,T()) = x >= 0 = T() or(x,T()) = x >= x = or(T(),x) or(T(),x) = x >= 0 = T() or(or(x,y),T()) = x + y >= 0 = T() or(or(x,y),T()) = x + y >= x + y = or(x,or(y,T())) or(x,or(y,T())) = x + y >= x = or(x,T()) or(x,T()) = x >= 0 = T() or(x,or(y,T())) = x + y >= x + y = or(or(x,y),T()) or(or(x,y),T()) = x + y >= 0 = T() or(or(x,T()),z) = x + z >= z = or(T(),z) or(or(x,T()),z) = x + z >= x + z = or(x,or(T(),z)) or(x,or(T(),z)) = x + z >= x + z = or(or(x,T()),z) or(or(x,T()),z) = x + z >= z = or(T(),z) or(T(),z) = z >= 0 = T() or(x,or(T(),z)) = x + z >= x = or(x,T()) or(x,T()) = x >= 0 = T() or(T(),z) = z >= z = or(z,T()) or(z,T()) = z >= 0 = T() or(x,or(T(),z)) = x + z >= x = or(x,T()) or(x,T()) = x >= 0 = T() or(x,or(y,T())) = x + y >= x = or(x,T()) or(x,or(y,T())) = x + y >= x + y = or(or(x,y),T()) or(x,T()) = x >= 0 = T() or(or(x,y),T()) = x + y >= 0 = T() or(T(),T()) = 0 >= 0 = T() or(T(),T()) = 0 >= 0 = T() or(T(),F()) = 1 >= 0 = T() or(T(),F()) = 1 >= 0 = T() or(T(),y) = y >= 0 = T() or(T(),y) = y >= y = or(y,T()) or(y,T()) = y >= 0 = T() or(or(T(),y),z) = y + z >= z = or(T(),z) or(or(T(),y),z) = y + z >= y + z = or(T(),or(y,z)) or(T(),z) = z >= 0 = T() or(T(),or(y,z)) = y + z >= 0 = T() or(T(),or(y,z)) = y + z >= 0 = T() or(T(),or(y,z)) = y + z >= y + z = or(or(T(),y),z) or(or(T(),y),z) = y + z >= z = or(T(),z) or(T(),z) = z >= 0 = T() or(or(T(),y),z) = y + z >= y + z = or(T(),or(y,z)) or(T(),or(y,z)) = y + z >= 0 = T() or(x,or(T(),z)) = x + z >= x = or(x,T()) or(x,or(T(),z)) = x + z >= x + z = or(or(x,T()),z) or(or(x,T()),z) = x + z >= x + z = or(x,or(T(),z)) or(x,or(T(),z)) = x + z >= x = or(x,T()) or(x,T()) = x >= 0 = T() or(or(x,T()),z) = x + z >= z = or(T(),z) or(T(),z) = z >= 0 = T() or(x,T()) = x >= x = or(T(),x) or(T(),x) = x >= 0 = T() or(or(x,T()),z) = x + z >= z = or(T(),z) or(T(),z) = z >= 0 = T() or(T(),F()) = 1 >= 0 = T() or(T(),F()) = 1 >= 0 = T() or(F(),F()) = 2 >= 1 = F() or(F(),F()) = 2 >= 1 = F() or(x,F()) = x + 1 >= x = x or(x,F()) = x + 1 >= x + 1 = or(F(),x) or(F(),x) = x + 1 >= x = x or(or(x,y),F()) = x + y + 1 >= x + y = or(x,y) or(or(x,y),F()) = x + y + 1 >= x + y + 1 = or(x,or(y,F())) or(x,or(y,F())) = x + y + 1 >= x + y = or(x,y) or(or(x,F()),z) = x + z + 1 >= x + z = or(x,z) or(or(x,F()),z) = x + z + 1 >= x + z + 1 = or(x,or(F(),z)) or(x,or(F(),z)) = x + z + 1 >= x + z = or(x,z) or(x,or(y,F())) = x + y + 1 >= x + y = or(x,y) or(x,or(y,F())) = x + y + 1 >= x + y + 1 = or(or(x,y),F()) or(or(x,y),F()) = x + y + 1 >= x + y = or(x,y) or(F(),T()) = 1 >= 0 = T() or(F(),T()) = 1 >= 0 = T() or(F(),F()) = 2 >= 1 = F() or(F(),F()) = 2 >= 1 = F() or(F(),y) = y + 1 >= y = y or(F(),y) = y + 1 >= y + 1 = or(y,F()) or(y,F()) = y + 1 >= y = y or(or(F(),y),z) = y + z + 1 >= y + z = or(y,z) or(or(F(),y),z) = y + z + 1 >= y + z + 1 = or(F(),or(y,z)) or(F(),or(y,z)) = y + z + 1 >= y + z = or(y,z) or(F(),or(y,z)) = y + z + 1 >= y + z = or(y,z) or(F(),or(y,z)) = y + z + 1 >= y + z + 1 = or(or(F(),y),z) or(or(F(),y),z) = y + z + 1 >= y + z = or(y,z) or(x,or(F(),z)) = x + z + 1 >= x + z = or(x,z) or(x,or(F(),z)) = x + z + 1 >= x + z + 1 = or(or(x,F()),z) or(or(x,F()),z) = x + z + 1 >= x + z = or(x,z) or(x,T()) = x >= x = or(T(),x) or(x,T()) = x >= 0 = T() or(T(),x) = x >= 0 = T() or(T(),x) = x >= x = or(x,T()) or(T(),x) = x >= 0 = T() or(x,T()) = x >= 0 = T() or(x,F()) = x + 1 >= x + 1 = or(F(),x) or(x,F()) = x + 1 >= x = x or(F(),x) = x + 1 >= x = x or(F(),x) = x + 1 >= x + 1 = or(x,F()) or(F(),x) = x + 1 >= x = x or(x,F()) = x + 1 >= x = x or(or(x,y),z) = x + y + z >= x + y + z = or(z,or(x,y)) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(z,or(x,y)) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(or(x,y),z) = x + y + z >= x + y + z = or(or(y,x),z) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(y,x),z) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(y,z),x) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(or(y,z),x) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(x,or(y,z)) = x + y + z >= x + y + z = or(x,or(z,y)) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(z,y)) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(x295,x296),T()) = x295 + x296 >= x295 + x296 = or(x295,or(x296,T())) or(or(x295,x296),T()) = x295 + x296 >= 0 = T() or(x295,or(x296,T())) = x295 + x296 >= x295 = or(x295,T()) or(x295,T()) = x295 >= 0 = T() or(x295,or(x296,T())) = x295 + x296 >= x295 + x296 = or(or(x295,x296),T()) or(or(x295,x296),T()) = x295 + x296 >= 0 = T() or(or(x298,x299),F()) = x298 + x299 + 1 >= x298 + x299 + 1 = or(x298,or(x299,F())) or(or(x298,x299),F()) = x298 + x299 + 1 >= x298 + x299 = or(x298,x299) or(x298,or(x299,F())) = x298 + x299 + 1 >= x298 + x299 = or(x298,x299) or(or(x301,x302),y) = x301 + x302 + y >= x301 + x302 + y = or(x301,or(x302,y)) or(or(x301,x302),y) = x301 + x302 + y >= x301 + x302 + y = or(y,or(x301,x302)) or(x301,or(x302,y)) = x301 + x302 + y >= x301 + x302 + y = or(or(x301,x302),y) or(y,or(x301,x302)) = x301 + x302 + y >= x301 + x302 + y = or(or(x301,x302),y) or(or(or(x304,x305),y),z) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(x304,or(x305,y)),z) or(or(or(x304,x305),y),z) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(x304,x305),or(y,z)) or(or(x304,or(x305,y)),z) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(or(x304,x305),y),z) or(or(x307,x308),or(y,z)) = x307 + x308 + y + z >= x307 + x308 + y + z = or(x307,or(x308,or(y,z))) or(or(x307,x308),or(y,z)) = x307 + x308 + y + z >= x307 + x308 + y + z = or(or(or(x307,x308),y),z) or(x307,or(x308,or(y,z))) = x307 + x308 + y + z >= x307 + x308 + y + z = or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) = x307 + x308 + y + z >= x307 + x308 + y + z = or(or(x307,x308),or(y,z)) or(x,or(or(x310,x311),z)) = x + x310 + x311 + z >= x + x310 + x311 + z = or(x,or(x310,or(x311,z))) or(x,or(or(x310,x311),z)) = x + x310 + x311 + z >= x + x310 + x311 + z = or(or(x,or(x310,x311)),z) or(x,or(x310,or(x311,z))) = x + x310 + x311 + z >= x + x310 + x311 + z = or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) = x + x310 + x311 + z >= x + x310 + x311 + z = or(x,or(or(x310,x311),z)) or(T(),or(x314,x315)) = x314 + x315 >= x314 + x315 = or(or(T(),x314),x315) or(T(),or(x314,x315)) = x314 + x315 >= 0 = T() or(or(T(),x314),x315) = x314 + x315 >= x315 = or(T(),x315) or(T(),x315) = x315 >= 0 = T() or(or(T(),x314),x315) = x314 + x315 >= x314 + x315 = or(T(),or(x314,x315)) or(T(),or(x314,x315)) = x314 + x315 >= 0 = T() or(F(),or(x317,x318)) = x317 + x318 + 1 >= x317 + x318 + 1 = or(or(F(),x317),x318) or(F(),or(x317,x318)) = x317 + x318 + 1 >= x317 + x318 = or(x317,x318) or(or(F(),x317),x318) = x317 + x318 + 1 >= x317 + x318 = or(x317,x318) or(x,or(x320,x321)) = x + x320 + x321 >= x + x320 + x321 = or(or(x,x320),x321) or(x,or(x320,x321)) = x + x320 + x321 >= x + x320 + x321 = or(or(x320,x321),x) or(or(x,x320),x321) = x + x320 + x321 >= x + x320 + x321 = or(x,or(x320,x321)) or(or(x320,x321),x) = x + x320 + x321 >= x + x320 + x321 = or(x,or(x320,x321)) or(or(x,y),or(x323,x324)) = x + x323 + x324 + y >= x + x323 + x324 + y = or(or(or(x,y),x323),x324) or(or(x,y),or(x323,x324)) = x + x323 + x324 + y >= x + x323 + x324 + y = or(x,or(y,or(x323,x324))) or(or(or(x,y),x323),x324) = x + x323 + x324 + y >= x + x323 + x324 + y = or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) = x + x323 + x324 + y >= x + x323 + x324 + y = or(or(x,y),or(x323,x324)) or(or(x,or(x326,x327)),z) = x + x326 + x327 + z >= x + x326 + x327 + z = or(or(or(x,x326),x327),z) or(or(x,or(x326,x327)),z) = x + x326 + x327 + z >= x + x326 + x327 + z = or(x,or(or(x326,x327),z)) or(or(or(x,x326),x327),z) = x + x326 + x327 + z >= x + x326 + x327 + z = or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) = x + x326 + x327 + z >= x + x326 + x327 + z = or(or(x,or(x326,x327)),z) or(x,or(y,or(x329,x330))) = x + x329 + x330 + y >= x + x329 + x330 + y = or(x,or(or(y,x329),x330)) or(x,or(y,or(x329,x330))) = x + x329 + x330 + y >= x + x329 + x330 + y = or(or(x,y),or(x329,x330)) or(x,or(or(y,x329),x330)) = x + x329 + x330 + y >= x + x329 + x330 + y = or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) = x + x329 + x330 + y >= x + x329 + x330 + y = or(x,or(y,or(x329,x330))) not(T()) = 1 >= 1 = F() not(F()) = 4 >= 0 = T() or(x,y) = x + y >= x + y = or(y,x) imply(x,y) = 3x + y + y*y + 2 >= 3x + y + 1 = or(not(x),y) problem: strict: or(T(),T()) -> T() or(T(),T()) -> T() or(x,T()) -> T() or(x,T()) -> or(T(),x) or(T(),x) -> T() or(or(x,y),T()) -> T() or(or(x,y),T()) -> or(x,or(y,T())) or(x,or(y,T())) -> or(x,T()) or(x,T()) -> T() or(x,or(y,T())) -> or(or(x,y),T()) or(or(x,y),T()) -> T() or(or(x,T()),z) -> or(T(),z) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,or(T(),z)) -> or(or(x,T()),z) or(or(x,T()),z) -> or(T(),z) or(T(),z) -> T() or(x,or(T(),z)) -> or(x,T()) or(x,T()) -> T() or(T(),z) -> or(z,T()) or(z,T()) -> T() or(x,or(T(),z)) -> or(x,T()) or(x,T()) -> T() or(x,or(y,T())) -> or(x,T()) or(x,or(y,T())) -> or(or(x,y),T()) or(x,T()) -> T() or(or(x,y),T()) -> T() or(T(),T()) -> T() or(T(),T()) -> T() or(T(),y) -> T() or(T(),y) -> or(y,T()) or(y,T()) -> T() or(or(T(),y),z) -> or(T(),z) or(or(T(),y),z) -> or(T(),or(y,z)) or(T(),z) -> T() or(T(),or(y,z)) -> T() or(T(),or(y,z)) -> T() or(T(),or(y,z)) -> or(or(T(),y),z) or(or(T(),y),z) -> or(T(),z) or(T(),z) -> T() or(or(T(),y),z) -> or(T(),or(y,z)) or(T(),or(y,z)) -> T() or(x,or(T(),z)) -> or(x,T()) or(x,or(T(),z)) -> or(or(x,T()),z) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,or(T(),z)) -> or(x,T()) or(x,T()) -> T() or(or(x,T()),z) -> or(T(),z) or(T(),z) -> T() or(x,T()) -> or(T(),x) or(T(),x) -> T() or(or(x,T()),z) -> or(T(),z) or(T(),z) -> T() or(x,F()) -> or(F(),x) or(or(x,y),F()) -> or(x,or(y,F())) or(or(x,F()),z) -> or(x,or(F(),z)) or(x,or(y,F())) -> or(or(x,y),F()) or(F(),y) -> or(y,F()) or(or(F(),y),z) -> or(F(),or(y,z)) or(F(),or(y,z)) -> or(or(F(),y),z) or(x,or(F(),z)) -> or(or(x,F()),z) or(x,T()) -> or(T(),x) or(x,T()) -> T() or(T(),x) -> T() or(T(),x) -> or(x,T()) or(T(),x) -> T() or(x,T()) -> T() or(x,F()) -> or(F(),x) or(F(),x) -> or(x,F()) or(or(x,y),z) -> or(z,or(x,y)) or(or(x,y),z) -> or(x,or(y,z)) or(z,or(x,y)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(or(x,y),z) -> or(or(y,x),z) or(or(x,y),z) -> or(x,or(y,z)) or(or(y,x),z) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(y,z),x) or(x,or(y,z)) -> or(or(x,y),z) or(or(y,z),x) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(x,or(z,y)) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(z,y)) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(or(x295,x296),T()) -> or(x295,or(x296,T())) or(or(x295,x296),T()) -> T() or(x295,or(x296,T())) -> or(x295,T()) or(x295,T()) -> T() or(x295,or(x296,T())) -> or(or(x295,x296),T()) or(or(x295,x296),T()) -> T() or(or(x298,x299),F()) -> or(x298,or(x299,F())) or(or(x301,x302),y) -> or(x301,or(x302,y)) or(or(x301,x302),y) -> or(y,or(x301,x302)) or(x301,or(x302,y)) -> or(or(x301,x302),y) or(y,or(x301,x302)) -> or(or(x301,x302),y) or(or(or(x304,x305),y),z) -> or(or(x304,or(x305,y)),z) or(or(or(x304,x305),y),z) -> or(or(x304,x305),or(y,z)) or(or(x304,or(x305,y)),z) -> or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) -> or(or(or(x304,x305),y),z) or(or(x307,x308),or(y,z)) -> or(x307,or(x308,or(y,z))) or(or(x307,x308),or(y,z)) -> or(or(or(x307,x308),y),z) or(x307,or(x308,or(y,z))) -> or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) -> or(or(x307,x308),or(y,z)) or(x,or(or(x310,x311),z)) -> or(x,or(x310,or(x311,z))) or(x,or(or(x310,x311),z)) -> or(or(x,or(x310,x311)),z) or(x,or(x310,or(x311,z))) -> or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) -> or(x,or(or(x310,x311),z)) or(T(),or(x314,x315)) -> or(or(T(),x314),x315) or(T(),or(x314,x315)) -> T() or(or(T(),x314),x315) -> or(T(),x315) or(T(),x315) -> T() or(or(T(),x314),x315) -> or(T(),or(x314,x315)) or(T(),or(x314,x315)) -> T() or(F(),or(x317,x318)) -> or(or(F(),x317),x318) or(x,or(x320,x321)) -> or(or(x,x320),x321) or(x,or(x320,x321)) -> or(or(x320,x321),x) or(or(x,x320),x321) -> or(x,or(x320,x321)) or(or(x320,x321),x) -> or(x,or(x320,x321)) or(or(x,y),or(x323,x324)) -> or(or(or(x,y),x323),x324) or(or(x,y),or(x323,x324)) -> or(x,or(y,or(x323,x324))) or(or(or(x,y),x323),x324) -> or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) -> or(or(x,y),or(x323,x324)) or(or(x,or(x326,x327)),z) -> or(or(or(x,x326),x327),z) or(or(x,or(x326,x327)),z) -> or(x,or(or(x326,x327),z)) or(or(or(x,x326),x327),z) -> or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) -> or(or(x,or(x326,x327)),z) or(x,or(y,or(x329,x330))) -> or(x,or(or(y,x329),x330)) or(x,or(y,or(x329,x330))) -> or(or(x,y),or(x329,x330)) or(x,or(or(y,x329),x330)) -> or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) -> or(x,or(y,or(x329,x330))) weak: not(T()) -> F() or(x,T()) -> T() or(T(),x) -> T() or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) Matrix Interpretation Processor: dim=1 interpretation: [or](x0, x1) = x0 + x1 + 2, [F] = 7, [not](x0) = x0 + 1, [T] = 6 orientation: or(T(),T()) = 14 >= 6 = T() or(T(),T()) = 14 >= 6 = T() or(x,T()) = x + 8 >= 6 = T() or(x,T()) = x + 8 >= x + 8 = or(T(),x) or(T(),x) = x + 8 >= 6 = T() or(or(x,y),T()) = x + y + 10 >= 6 = T() or(or(x,y),T()) = x + y + 10 >= x + y + 10 = or(x,or(y,T())) or(x,or(y,T())) = x + y + 10 >= x + 8 = or(x,T()) or(x,T()) = x + 8 >= 6 = T() or(x,or(y,T())) = x + y + 10 >= x + y + 10 = or(or(x,y),T()) or(or(x,y),T()) = x + y + 10 >= 6 = T() or(or(x,T()),z) = x + z + 10 >= z + 8 = or(T(),z) or(or(x,T()),z) = x + z + 10 >= x + z + 10 = or(x,or(T(),z)) or(x,or(T(),z)) = x + z + 10 >= x + z + 10 = or(or(x,T()),z) or(or(x,T()),z) = x + z + 10 >= z + 8 = or(T(),z) or(T(),z) = z + 8 >= 6 = T() or(x,or(T(),z)) = x + z + 10 >= x + 8 = or(x,T()) or(x,T()) = x + 8 >= 6 = T() or(T(),z) = z + 8 >= z + 8 = or(z,T()) or(z,T()) = z + 8 >= 6 = T() or(x,or(T(),z)) = x + z + 10 >= x + 8 = or(x,T()) or(x,T()) = x + 8 >= 6 = T() or(x,or(y,T())) = x + y + 10 >= x + 8 = or(x,T()) or(x,or(y,T())) = x + y + 10 >= x + y + 10 = or(or(x,y),T()) or(x,T()) = x + 8 >= 6 = T() or(or(x,y),T()) = x + y + 10 >= 6 = T() or(T(),T()) = 14 >= 6 = T() or(T(),T()) = 14 >= 6 = T() or(T(),y) = y + 8 >= 6 = T() or(T(),y) = y + 8 >= y + 8 = or(y,T()) or(y,T()) = y + 8 >= 6 = T() or(or(T(),y),z) = y + z + 10 >= z + 8 = or(T(),z) or(or(T(),y),z) = y + z + 10 >= y + z + 10 = or(T(),or(y,z)) or(T(),z) = z + 8 >= 6 = T() or(T(),or(y,z)) = y + z + 10 >= 6 = T() or(T(),or(y,z)) = y + z + 10 >= 6 = T() or(T(),or(y,z)) = y + z + 10 >= y + z + 10 = or(or(T(),y),z) or(or(T(),y),z) = y + z + 10 >= z + 8 = or(T(),z) or(T(),z) = z + 8 >= 6 = T() or(or(T(),y),z) = y + z + 10 >= y + z + 10 = or(T(),or(y,z)) or(T(),or(y,z)) = y + z + 10 >= 6 = T() or(x,or(T(),z)) = x + z + 10 >= x + 8 = or(x,T()) or(x,or(T(),z)) = x + z + 10 >= x + z + 10 = or(or(x,T()),z) or(or(x,T()),z) = x + z + 10 >= x + z + 10 = or(x,or(T(),z)) or(x,or(T(),z)) = x + z + 10 >= x + 8 = or(x,T()) or(x,T()) = x + 8 >= 6 = T() or(or(x,T()),z) = x + z + 10 >= z + 8 = or(T(),z) or(T(),z) = z + 8 >= 6 = T() or(x,T()) = x + 8 >= x + 8 = or(T(),x) or(T(),x) = x + 8 >= 6 = T() or(or(x,T()),z) = x + z + 10 >= z + 8 = or(T(),z) or(T(),z) = z + 8 >= 6 = T() or(x,F()) = x + 9 >= x + 9 = or(F(),x) or(or(x,y),F()) = x + y + 11 >= x + y + 11 = or(x,or(y,F())) or(or(x,F()),z) = x + z + 11 >= x + z + 11 = or(x,or(F(),z)) or(x,or(y,F())) = x + y + 11 >= x + y + 11 = or(or(x,y),F()) or(F(),y) = y + 9 >= y + 9 = or(y,F()) or(or(F(),y),z) = y + z + 11 >= y + z + 11 = or(F(),or(y,z)) or(F(),or(y,z)) = y + z + 11 >= y + z + 11 = or(or(F(),y),z) or(x,or(F(),z)) = x + z + 11 >= x + z + 11 = or(or(x,F()),z) or(x,T()) = x + 8 >= x + 8 = or(T(),x) or(x,T()) = x + 8 >= 6 = T() or(T(),x) = x + 8 >= 6 = T() or(T(),x) = x + 8 >= x + 8 = or(x,T()) or(T(),x) = x + 8 >= 6 = T() or(x,T()) = x + 8 >= 6 = T() or(x,F()) = x + 9 >= x + 9 = or(F(),x) or(F(),x) = x + 9 >= x + 9 = or(x,F()) or(or(x,y),z) = x + y + z + 4 >= x + y + z + 4 = or(z,or(x,y)) or(or(x,y),z) = x + y + z + 4 >= x + y + z + 4 = or(x,or(y,z)) or(z,or(x,y)) = x + y + z + 4 >= x + y + z + 4 = or(or(x,y),z) or(x,or(y,z)) = x + y + z + 4 >= x + y + z + 4 = or(or(x,y),z) or(or(x,y),z) = x + y + z + 4 >= x + y + z + 4 = or(or(y,x),z) or(or(x,y),z) = x + y + z + 4 >= x + y + z + 4 = or(x,or(y,z)) or(or(y,x),z) = x + y + z + 4 >= x + y + z + 4 = or(or(x,y),z) or(x,or(y,z)) = x + y + z + 4 >= x + y + z + 4 = or(or(x,y),z) or(x,or(y,z)) = x + y + z + 4 >= x + y + z + 4 = or(or(y,z),x) or(x,or(y,z)) = x + y + z + 4 >= x + y + z + 4 = or(or(x,y),z) or(or(y,z),x) = x + y + z + 4 >= x + y + z + 4 = or(x,or(y,z)) or(or(x,y),z) = x + y + z + 4 >= x + y + z + 4 = or(x,or(y,z)) or(x,or(y,z)) = x + y + z + 4 >= x + y + z + 4 = or(x,or(z,y)) or(x,or(y,z)) = x + y + z + 4 >= x + y + z + 4 = or(or(x,y),z) or(x,or(z,y)) = x + y + z + 4 >= x + y + z + 4 = or(x,or(y,z)) or(or(x,y),z) = x + y + z + 4 >= x + y + z + 4 = or(x,or(y,z)) or(or(x295,x296),T()) = x295 + x296 + 10 >= x295 + x296 + 10 = or(x295,or(x296,T())) or(or(x295,x296),T()) = x295 + x296 + 10 >= 6 = T() or(x295,or(x296,T())) = x295 + x296 + 10 >= x295 + 8 = or(x295,T()) or(x295,T()) = x295 + 8 >= 6 = T() or(x295,or(x296,T())) = x295 + x296 + 10 >= x295 + x296 + 10 = or(or(x295,x296),T()) or(or(x295,x296),T()) = x295 + x296 + 10 >= 6 = T() or(or(x298,x299),F()) = x298 + x299 + 11 >= x298 + x299 + 11 = or(x298,or(x299,F())) or(or(x301,x302),y) = x301 + x302 + y + 4 >= x301 + x302 + y + 4 = or(x301,or(x302,y)) or(or(x301,x302),y) = x301 + x302 + y + 4 >= x301 + x302 + y + 4 = or(y,or(x301,x302)) or(x301,or(x302,y)) = x301 + x302 + y + 4 >= x301 + x302 + y + 4 = or(or(x301,x302),y) or(y,or(x301,x302)) = x301 + x302 + y + 4 >= x301 + x302 + y + 4 = or(or(x301,x302),y) or(or(or(x304,x305),y),z) = x304 + x305 + y + z + 6 >= x304 + x305 + y + z + 6 = or(or(x304,or(x305,y)),z) or(or(or(x304,x305),y),z) = x304 + x305 + y + z + 6 >= x304 + x305 + y + z + 6 = or(or(x304,x305),or(y,z)) or(or(x304,or(x305,y)),z) = x304 + x305 + y + z + 6 >= x304 + x305 + y + z + 6 = or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) = x304 + x305 + y + z + 6 >= x304 + x305 + y + z + 6 = or(or(or(x304,x305),y),z) or(or(x307,x308),or(y,z)) = x307 + x308 + y + z + 6 >= x307 + x308 + y + z + 6 = or(x307,or(x308,or(y,z))) or(or(x307,x308),or(y,z)) = x307 + x308 + y + z + 6 >= x307 + x308 + y + z + 6 = or(or(or(x307,x308),y),z) or(x307,or(x308,or(y,z))) = x307 + x308 + y + z + 6 >= x307 + x308 + y + z + 6 = or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) = x307 + x308 + y + z + 6 >= x307 + x308 + y + z + 6 = or(or(x307,x308),or(y,z)) or(x,or(or(x310,x311),z)) = x + x310 + x311 + z + 6 >= x + x310 + x311 + z + 6 = or(x,or(x310,or(x311,z))) or(x,or(or(x310,x311),z)) = x + x310 + x311 + z + 6 >= x + x310 + x311 + z + 6 = or(or(x,or(x310,x311)),z) or(x,or(x310,or(x311,z))) = x + x310 + x311 + z + 6 >= x + x310 + x311 + z + 6 = or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) = x + x310 + x311 + z + 6 >= x + x310 + x311 + z + 6 = or(x,or(or(x310,x311),z)) or(T(),or(x314,x315)) = x314 + x315 + 10 >= x314 + x315 + 10 = or(or(T(),x314),x315) or(T(),or(x314,x315)) = x314 + x315 + 10 >= 6 = T() or(or(T(),x314),x315) = x314 + x315 + 10 >= x315 + 8 = or(T(),x315) or(T(),x315) = x315 + 8 >= 6 = T() or(or(T(),x314),x315) = x314 + x315 + 10 >= x314 + x315 + 10 = or(T(),or(x314,x315)) or(T(),or(x314,x315)) = x314 + x315 + 10 >= 6 = T() or(F(),or(x317,x318)) = x317 + x318 + 11 >= x317 + x318 + 11 = or(or(F(),x317),x318) or(x,or(x320,x321)) = x + x320 + x321 + 4 >= x + x320 + x321 + 4 = or(or(x,x320),x321) or(x,or(x320,x321)) = x + x320 + x321 + 4 >= x + x320 + x321 + 4 = or(or(x320,x321),x) or(or(x,x320),x321) = x + x320 + x321 + 4 >= x + x320 + x321 + 4 = or(x,or(x320,x321)) or(or(x320,x321),x) = x + x320 + x321 + 4 >= x + x320 + x321 + 4 = or(x,or(x320,x321)) or(or(x,y),or(x323,x324)) = x + x323 + x324 + y + 6 >= x + x323 + x324 + y + 6 = or(or(or(x,y),x323),x324) or(or(x,y),or(x323,x324)) = x + x323 + x324 + y + 6 >= x + x323 + x324 + y + 6 = or(x,or(y,or(x323,x324))) or(or(or(x,y),x323),x324) = x + x323 + x324 + y + 6 >= x + x323 + x324 + y + 6 = or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) = x + x323 + x324 + y + 6 >= x + x323 + x324 + y + 6 = or(or(x,y),or(x323,x324)) or(or(x,or(x326,x327)),z) = x + x326 + x327 + z + 6 >= x + x326 + x327 + z + 6 = or(or(or(x,x326),x327),z) or(or(x,or(x326,x327)),z) = x + x326 + x327 + z + 6 >= x + x326 + x327 + z + 6 = or(x,or(or(x326,x327),z)) or(or(or(x,x326),x327),z) = x + x326 + x327 + z + 6 >= x + x326 + x327 + z + 6 = or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) = x + x326 + x327 + z + 6 >= x + x326 + x327 + z + 6 = or(or(x,or(x326,x327)),z) or(x,or(y,or(x329,x330))) = x + x329 + x330 + y + 6 >= x + x329 + x330 + y + 6 = or(x,or(or(y,x329),x330)) or(x,or(y,or(x329,x330))) = x + x329 + x330 + y + 6 >= x + x329 + x330 + y + 6 = or(or(x,y),or(x329,x330)) or(x,or(or(y,x329),x330)) = x + x329 + x330 + y + 6 >= x + x329 + x330 + y + 6 = or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) = x + x329 + x330 + y + 6 >= x + x329 + x330 + y + 6 = or(x,or(y,or(x329,x330))) not(T()) = 7 >= 7 = F() or(x,y) = x + y + 2 >= x + y + 2 = or(y,x) problem: strict: or(x,T()) -> or(T(),x) or(or(x,y),T()) -> or(x,or(y,T())) or(x,or(y,T())) -> or(or(x,y),T()) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,or(T(),z)) -> or(or(x,T()),z) or(T(),z) -> or(z,T()) or(x,or(y,T())) -> or(or(x,y),T()) or(T(),y) -> or(y,T()) or(or(T(),y),z) -> or(T(),or(y,z)) or(T(),or(y,z)) -> or(or(T(),y),z) or(or(T(),y),z) -> or(T(),or(y,z)) or(x,or(T(),z)) -> or(or(x,T()),z) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,T()) -> or(T(),x) or(x,F()) -> or(F(),x) or(or(x,y),F()) -> or(x,or(y,F())) or(or(x,F()),z) -> or(x,or(F(),z)) or(x,or(y,F())) -> or(or(x,y),F()) or(F(),y) -> or(y,F()) or(or(F(),y),z) -> or(F(),or(y,z)) or(F(),or(y,z)) -> or(or(F(),y),z) or(x,or(F(),z)) -> or(or(x,F()),z) or(x,T()) -> or(T(),x) or(T(),x) -> or(x,T()) or(x,F()) -> or(F(),x) or(F(),x) -> or(x,F()) or(or(x,y),z) -> or(z,or(x,y)) or(or(x,y),z) -> or(x,or(y,z)) or(z,or(x,y)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(or(x,y),z) -> or(or(y,x),z) or(or(x,y),z) -> or(x,or(y,z)) or(or(y,x),z) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(y,z),x) or(x,or(y,z)) -> or(or(x,y),z) or(or(y,z),x) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(x,or(z,y)) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(z,y)) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(or(x295,x296),T()) -> or(x295,or(x296,T())) or(x295,or(x296,T())) -> or(or(x295,x296),T()) or(or(x298,x299),F()) -> or(x298,or(x299,F())) or(or(x301,x302),y) -> or(x301,or(x302,y)) or(or(x301,x302),y) -> or(y,or(x301,x302)) or(x301,or(x302,y)) -> or(or(x301,x302),y) or(y,or(x301,x302)) -> or(or(x301,x302),y) or(or(or(x304,x305),y),z) -> or(or(x304,or(x305,y)),z) or(or(or(x304,x305),y),z) -> or(or(x304,x305),or(y,z)) or(or(x304,or(x305,y)),z) -> or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) -> or(or(or(x304,x305),y),z) or(or(x307,x308),or(y,z)) -> or(x307,or(x308,or(y,z))) or(or(x307,x308),or(y,z)) -> or(or(or(x307,x308),y),z) or(x307,or(x308,or(y,z))) -> or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) -> or(or(x307,x308),or(y,z)) or(x,or(or(x310,x311),z)) -> or(x,or(x310,or(x311,z))) or(x,or(or(x310,x311),z)) -> or(or(x,or(x310,x311)),z) or(x,or(x310,or(x311,z))) -> or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) -> or(x,or(or(x310,x311),z)) or(T(),or(x314,x315)) -> or(or(T(),x314),x315) or(or(T(),x314),x315) -> or(T(),or(x314,x315)) or(F(),or(x317,x318)) -> or(or(F(),x317),x318) or(x,or(x320,x321)) -> or(or(x,x320),x321) or(x,or(x320,x321)) -> or(or(x320,x321),x) or(or(x,x320),x321) -> or(x,or(x320,x321)) or(or(x320,x321),x) -> or(x,or(x320,x321)) or(or(x,y),or(x323,x324)) -> or(or(or(x,y),x323),x324) or(or(x,y),or(x323,x324)) -> or(x,or(y,or(x323,x324))) or(or(or(x,y),x323),x324) -> or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) -> or(or(x,y),or(x323,x324)) or(or(x,or(x326,x327)),z) -> or(or(or(x,x326),x327),z) or(or(x,or(x326,x327)),z) -> or(x,or(or(x326,x327),z)) or(or(or(x,x326),x327),z) -> or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) -> or(or(x,or(x326,x327)),z) or(x,or(y,or(x329,x330))) -> or(x,or(or(y,x329),x330)) or(x,or(y,or(x329,x330))) -> or(or(x,y),or(x329,x330)) or(x,or(or(y,x329),x330)) -> or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) -> or(x,or(y,or(x329,x330))) weak: not(T()) -> F() or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) Polynomial Interpretation Processor: dimension: 1 interpretation: [or](x0, x1) = x0 + x1, [F] = 0, [not](x0) = x0 + 1, [T] = 0 orientation: or(x,T()) = x >= x = or(T(),x) or(or(x,y),T()) = x + y >= x + y = or(x,or(y,T())) or(x,or(y,T())) = x + y >= x + y = or(or(x,y),T()) or(or(x,T()),z) = x + z >= x + z = or(x,or(T(),z)) or(x,or(T(),z)) = x + z >= x + z = or(or(x,T()),z) or(T(),z) = z >= z = or(z,T()) or(x,or(y,T())) = x + y >= x + y = or(or(x,y),T()) or(T(),y) = y >= y = or(y,T()) or(or(T(),y),z) = y + z >= y + z = or(T(),or(y,z)) or(T(),or(y,z)) = y + z >= y + z = or(or(T(),y),z) or(or(T(),y),z) = y + z >= y + z = or(T(),or(y,z)) or(x,or(T(),z)) = x + z >= x + z = or(or(x,T()),z) or(or(x,T()),z) = x + z >= x + z = or(x,or(T(),z)) or(x,T()) = x >= x = or(T(),x) or(x,F()) = x >= x = or(F(),x) or(or(x,y),F()) = x + y >= x + y = or(x,or(y,F())) or(or(x,F()),z) = x + z >= x + z = or(x,or(F(),z)) or(x,or(y,F())) = x + y >= x + y = or(or(x,y),F()) or(F(),y) = y >= y = or(y,F()) or(or(F(),y),z) = y + z >= y + z = or(F(),or(y,z)) or(F(),or(y,z)) = y + z >= y + z = or(or(F(),y),z) or(x,or(F(),z)) = x + z >= x + z = or(or(x,F()),z) or(x,T()) = x >= x = or(T(),x) or(T(),x) = x >= x = or(x,T()) or(x,F()) = x >= x = or(F(),x) or(F(),x) = x >= x = or(x,F()) or(or(x,y),z) = x + y + z >= x + y + z = or(z,or(x,y)) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(z,or(x,y)) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(or(x,y),z) = x + y + z >= x + y + z = or(or(y,x),z) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(y,x),z) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(y,z),x) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(or(y,z),x) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(x,or(y,z)) = x + y + z >= x + y + z = or(x,or(z,y)) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(x,or(z,y)) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(x,y),z) = x + y + z >= x + y + z = or(x,or(y,z)) or(or(x295,x296),T()) = x295 + x296 >= x295 + x296 = or(x295,or(x296,T())) or(x295,or(x296,T())) = x295 + x296 >= x295 + x296 = or(or(x295,x296),T()) or(or(x298,x299),F()) = x298 + x299 >= x298 + x299 = or(x298,or(x299,F())) or(or(x301,x302),y) = x301 + x302 + y >= x301 + x302 + y = or(x301,or(x302,y)) or(or(x301,x302),y) = x301 + x302 + y >= x301 + x302 + y = or(y,or(x301,x302)) or(x301,or(x302,y)) = x301 + x302 + y >= x301 + x302 + y = or(or(x301,x302),y) or(y,or(x301,x302)) = x301 + x302 + y >= x301 + x302 + y = or(or(x301,x302),y) or(or(or(x304,x305),y),z) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(x304,or(x305,y)),z) or(or(or(x304,x305),y),z) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(x304,x305),or(y,z)) or(or(x304,or(x305,y)),z) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) = x304 + x305 + y + z >= x304 + x305 + y + z = or(or(or(x304,x305),y),z) or(or(x307,x308),or(y,z)) = x307 + x308 + y + z >= x307 + x308 + y + z = or(x307,or(x308,or(y,z))) or(or(x307,x308),or(y,z)) = x307 + x308 + y + z >= x307 + x308 + y + z = or(or(or(x307,x308),y),z) or(x307,or(x308,or(y,z))) = x307 + x308 + y + z >= x307 + x308 + y + z = or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) = x307 + x308 + y + z >= x307 + x308 + y + z = or(or(x307,x308),or(y,z)) or(x,or(or(x310,x311),z)) = x + x310 + x311 + z >= x + x310 + x311 + z = or(x,or(x310,or(x311,z))) or(x,or(or(x310,x311),z)) = x + x310 + x311 + z >= x + x310 + x311 + z = or(or(x,or(x310,x311)),z) or(x,or(x310,or(x311,z))) = x + x310 + x311 + z >= x + x310 + x311 + z = or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) = x + x310 + x311 + z >= x + x310 + x311 + z = or(x,or(or(x310,x311),z)) or(T(),or(x314,x315)) = x314 + x315 >= x314 + x315 = or(or(T(),x314),x315) or(or(T(),x314),x315) = x314 + x315 >= x314 + x315 = or(T(),or(x314,x315)) or(F(),or(x317,x318)) = x317 + x318 >= x317 + x318 = or(or(F(),x317),x318) or(x,or(x320,x321)) = x + x320 + x321 >= x + x320 + x321 = or(or(x,x320),x321) or(x,or(x320,x321)) = x + x320 + x321 >= x + x320 + x321 = or(or(x320,x321),x) or(or(x,x320),x321) = x + x320 + x321 >= x + x320 + x321 = or(x,or(x320,x321)) or(or(x320,x321),x) = x + x320 + x321 >= x + x320 + x321 = or(x,or(x320,x321)) or(or(x,y),or(x323,x324)) = x + x323 + x324 + y >= x + x323 + x324 + y = or(or(or(x,y),x323),x324) or(or(x,y),or(x323,x324)) = x + x323 + x324 + y >= x + x323 + x324 + y = or(x,or(y,or(x323,x324))) or(or(or(x,y),x323),x324) = x + x323 + x324 + y >= x + x323 + x324 + y = or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) = x + x323 + x324 + y >= x + x323 + x324 + y = or(or(x,y),or(x323,x324)) or(or(x,or(x326,x327)),z) = x + x326 + x327 + z >= x + x326 + x327 + z = or(or(or(x,x326),x327),z) or(or(x,or(x326,x327)),z) = x + x326 + x327 + z >= x + x326 + x327 + z = or(x,or(or(x326,x327),z)) or(or(or(x,x326),x327),z) = x + x326 + x327 + z >= x + x326 + x327 + z = or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) = x + x326 + x327 + z >= x + x326 + x327 + z = or(or(x,or(x326,x327)),z) or(x,or(y,or(x329,x330))) = x + x329 + x330 + y >= x + x329 + x330 + y = or(x,or(or(y,x329),x330)) or(x,or(y,or(x329,x330))) = x + x329 + x330 + y >= x + x329 + x330 + y = or(or(x,y),or(x329,x330)) or(x,or(or(y,x329),x330)) = x + x329 + x330 + y >= x + x329 + x330 + y = or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) = x + x329 + x330 + y >= x + x329 + x330 + y = or(x,or(y,or(x329,x330))) not(T()) = 1 >= 0 = F() or(x,y) = x + y >= x + y = or(y,x) problem: strict: or(x,T()) -> or(T(),x) or(or(x,y),T()) -> or(x,or(y,T())) or(x,or(y,T())) -> or(or(x,y),T()) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,or(T(),z)) -> or(or(x,T()),z) or(T(),z) -> or(z,T()) or(x,or(y,T())) -> or(or(x,y),T()) or(T(),y) -> or(y,T()) or(or(T(),y),z) -> or(T(),or(y,z)) or(T(),or(y,z)) -> or(or(T(),y),z) or(or(T(),y),z) -> or(T(),or(y,z)) or(x,or(T(),z)) -> or(or(x,T()),z) or(or(x,T()),z) -> or(x,or(T(),z)) or(x,T()) -> or(T(),x) or(x,F()) -> or(F(),x) or(or(x,y),F()) -> or(x,or(y,F())) or(or(x,F()),z) -> or(x,or(F(),z)) or(x,or(y,F())) -> or(or(x,y),F()) or(F(),y) -> or(y,F()) or(or(F(),y),z) -> or(F(),or(y,z)) or(F(),or(y,z)) -> or(or(F(),y),z) or(x,or(F(),z)) -> or(or(x,F()),z) or(x,T()) -> or(T(),x) or(T(),x) -> or(x,T()) or(x,F()) -> or(F(),x) or(F(),x) -> or(x,F()) or(or(x,y),z) -> or(z,or(x,y)) or(or(x,y),z) -> or(x,or(y,z)) or(z,or(x,y)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(or(x,y),z) -> or(or(y,x),z) or(or(x,y),z) -> or(x,or(y,z)) or(or(y,x),z) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(y,z)) -> or(or(y,z),x) or(x,or(y,z)) -> or(or(x,y),z) or(or(y,z),x) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(x,or(z,y)) or(x,or(y,z)) -> or(or(x,y),z) or(x,or(z,y)) -> or(x,or(y,z)) or(or(x,y),z) -> or(x,or(y,z)) or(or(x295,x296),T()) -> or(x295,or(x296,T())) or(x295,or(x296,T())) -> or(or(x295,x296),T()) or(or(x298,x299),F()) -> or(x298,or(x299,F())) or(or(x301,x302),y) -> or(x301,or(x302,y)) or(or(x301,x302),y) -> or(y,or(x301,x302)) or(x301,or(x302,y)) -> or(or(x301,x302),y) or(y,or(x301,x302)) -> or(or(x301,x302),y) or(or(or(x304,x305),y),z) -> or(or(x304,or(x305,y)),z) or(or(or(x304,x305),y),z) -> or(or(x304,x305),or(y,z)) or(or(x304,or(x305,y)),z) -> or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) -> or(or(or(x304,x305),y),z) or(or(x307,x308),or(y,z)) -> or(x307,or(x308,or(y,z))) or(or(x307,x308),or(y,z)) -> or(or(or(x307,x308),y),z) or(x307,or(x308,or(y,z))) -> or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) -> or(or(x307,x308),or(y,z)) or(x,or(or(x310,x311),z)) -> or(x,or(x310,or(x311,z))) or(x,or(or(x310,x311),z)) -> or(or(x,or(x310,x311)),z) or(x,or(x310,or(x311,z))) -> or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) -> or(x,or(or(x310,x311),z)) or(T(),or(x314,x315)) -> or(or(T(),x314),x315) or(or(T(),x314),x315) -> or(T(),or(x314,x315)) or(F(),or(x317,x318)) -> or(or(F(),x317),x318) or(x,or(x320,x321)) -> or(or(x,x320),x321) or(x,or(x320,x321)) -> or(or(x320,x321),x) or(or(x,x320),x321) -> or(x,or(x320,x321)) or(or(x320,x321),x) -> or(x,or(x320,x321)) or(or(x,y),or(x323,x324)) -> or(or(or(x,y),x323),x324) or(or(x,y),or(x323,x324)) -> or(x,or(y,or(x323,x324))) or(or(or(x,y),x323),x324) -> or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) -> or(or(x,y),or(x323,x324)) or(or(x,or(x326,x327)),z) -> or(or(or(x,x326),x327),z) or(or(x,or(x326,x327)),z) -> or(x,or(or(x326,x327),z)) or(or(or(x,x326),x327),z) -> or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) -> or(or(x,or(x326,x327)),z) or(x,or(y,or(x329,x330))) -> or(x,or(or(y,x329),x330)) or(x,or(y,or(x329,x330))) -> or(or(x,y),or(x329,x330)) or(x,or(or(y,x329),x330)) -> or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) -> or(x,or(y,or(x329,x330))) weak: or(x,y) -> or(y,x) or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: T() <-2|[1]- or(T(),T()) -3|[1]-> T() joins: peak: T() <-2|[1]- or(F(),T()) -5|[1]-> T() joins: peak: T() <-2|[1]- or(x,T()) -6|[1]-> or(T(),x) joins: or(T(),x) -3|[1]-> T() peak: T() <-2|[1]- or(or(x,y),T()) -7|[1]-> or(x,or(y,T())) joins: or(x,or(y,T())) -2|1[1]-> or(x,T()) -2|[0]-> T() peak: or(T(),z) <-2|0[1]- or(or(x,T()),z) -7|[1]-> or(x,or(T(),z)) joins: or(T(),z) -3|[0]-> T() or(x,or(T(),z)) -3|1[1]-> or(x,T()) -2|[0]-> T() peak: or(x,T()) <-2|1[1]- or(x,or(y,T())) -8|[1]-> or(or(x,y),T()) joins: or(x,T()) -2|[0]-> T() or(or(x,y),T()) -2|[1]-> T() peak: T() <-3|[1]- or(T(),T()) -2|[1]-> T() joins: peak: T() <-3|[1]- or(T(),F()) -4|[1]-> T() joins: peak: T() <-3|[1]- or(T(),y) -6|[1]-> or(y,T()) joins: or(y,T()) -2|[1]-> T() peak: or(T(),z) <-3|0[1]- or(or(T(),y),z) -7|[1]-> or(T(),or(y,z)) joins: or(T(),z) -3|[0]-> T() or(T(),or(y,z)) -3|[1]-> T() peak: T() <-3|[1]- or(T(),or(y,z)) -8|[1]-> or(or(T(),y),z) joins: or(or(T(),y),z) -3|0[1]-> or(T(),z) -3|[0]-> T() peak: or(x,T()) <-3|1[1]- or(x,or(T(),z)) -8|[1]-> or(or(x,T()),z) joins: or(x,T()) -2|[0]-> T() or(or(x,T()),z) -2|0[1]-> or(T(),z) -3|[0]-> T() peak: T() <-4|[1]- or(T(),F()) -3|[1]-> T() joins: peak: F() <-4|[1]- or(F(),F()) -5|[1]-> F() joins: peak: x <-4|[1]- or(x,F()) -6|[1]-> or(F(),x) joins: or(F(),x) -5|[1]-> x peak: or(x,y) <-4|[1]- or(or(x,y),F()) -7|[1]-> or(x,or(y,F())) joins: or(x,or(y,F())) -4|1[1]-> or(x,y) peak: or(x,z) <-4|0[1]- or(or(x,F()),z) -7|[1]-> or(x,or(F(),z)) joins: or(x,or(F(),z)) -5|1[1]-> or(x,z) peak: or(x,y) <-4|1[1]- or(x,or(y,F())) -8|[1]-> or(or(x,y),F()) joins: or(or(x,y),F()) -4|[1]-> or(x,y) peak: T() <-5|[1]- or(F(),T()) -2|[1]-> T() joins: peak: F() <-5|[1]- or(F(),F()) -4|[1]-> F() joins: peak: y <-5|[1]- or(F(),y) -6|[1]-> or(y,F()) joins: or(y,F()) -4|[1]-> y peak: or(y,z) <-5|0[1]- or(or(F(),y),z) -7|[1]-> or(F(),or(y,z)) joins: or(F(),or(y,z)) -5|[1]-> or(y,z) peak: or(y,z) <-5|[1]- or(F(),or(y,z)) -8|[1]-> or(or(F(),y),z) joins: or(or(F(),y),z) -5|0[1]-> or(y,z) peak: or(x,z) <-5|1[1]- or(x,or(F(),z)) -8|[1]-> or(or(x,F()),z) joins: or(or(x,F()),z) -4|0[1]-> or(x,z) peak: or(T(),x) <-6|[1]- or(x,T()) -2|[1]-> T() joins: or(T(),x) -3|[1]-> T() peak: or(x,T()) <-6|[1]- or(T(),x) -3|[1]-> T() joins: or(x,T()) -2|[1]-> T() peak: or(F(),x) <-6|[1]- or(x,F()) -4|[1]-> x joins: or(F(),x) -5|[1]-> x peak: or(x,F()) <-6|[1]- or(F(),x) -5|[1]-> x joins: or(x,F()) -4|[1]-> x peak: or(z,or(x,y)) <-6|[1]- or(or(x,y),z) -7|[1]-> or(x,or(y,z)) joins: or(z,or(x,y)) -6|[1]-> or(or(x,y),z) or(x,or(y,z)) -8|[1]-> or(or(x,y),z) peak: or(or(y,x),z) <-6|0[1]- or(or(x,y),z) -7|[1]-> or(x,or(y,z)) joins: or(or(y,x),z) -6|0[1]-> or(or(x,y),z) or(x,or(y,z)) -8|[1]-> or(or(x,y),z) peak: or(or(y,z),x) <-6|[1]- or(x,or(y,z)) -8|[1]-> or(or(x,y),z) joins: or(or(y,z),x) -6|[1]-> or(x,or(y,z)) or(or(x,y),z) -7|[1]-> or(x,or(y,z)) peak: or(x,or(z,y)) <-6|1[1]- or(x,or(y,z)) -8|[1]-> or(or(x,y),z) joins: or(x,or(z,y)) -6|1[1]-> or(x,or(y,z)) or(or(x,y),z) -7|[1]-> or(x,or(y,z)) peak: or(x295,or(x296,T())) <-7|[1]- or(or(x295,x296),T()) -2|[1]-> T() joins: or(x295,or(x296,T())) -2|1[1]-> or(x295,T()) -2|[0]-> T() peak: or(x298,or(x299,F())) <-7|[1]- or(or(x298,x299),F()) -4|[1]-> or(x298,x299) joins: or(x298,or(x299,F())) -4|1[1]-> or(x298,x299) peak: or(x301,or(x302,y)) <-7|[1]- or(or(x301,x302),y) -6|[1]-> or(y,or(x301,x302)) joins: or(x301,or(x302,y)) -8|[1]-> or(or(x301,x302),y) or(y,or(x301,x302)) -6|[1]-> or(or(x301,x302),y) peak: or(or(x304,or(x305,y)),z) <-7|0[1]- or(or(or(x304,x305),y),z) -7| [1]-> or(or(x304,x305),or(y,z)) joins: or(or(x304,or(x305,y)),z) -8|0[1]-> or(or(or(x304,x305),y),z) or(or(x304,x305),or(y,z)) -8|[1]-> or(or(or(x304,x305),y),z) peak: or(x307,or(x308,or(y,z))) <-7|[1]- or(or(x307,x308),or(y,z)) -8| [1]-> or(or(or(x307,x308),y),z) joins: or(x307,or(x308,or(y,z))) -8|[1]-> or(or(x307,x308),or(y,z)) or(or(or(x307,x308),y),z) -7|[1]-> or(or(x307,x308),or(y,z)) peak: or(x,or(x310,or(x311,z))) <-7|1[1]- or(x,or(or(x310,x311),z)) -8| [1]-> or(or(x,or(x310,x311)),z) joins: or(x,or(x310,or(x311,z))) -8|1[1]-> or(x,or(or(x310,x311),z)) or(or(x,or(x310,x311)),z) -7|[1]-> or(x,or(or(x310,x311),z)) peak: or(or(T(),x314),x315) <-8|[1]- or(T(),or(x314,x315)) -3|[1]-> T() joins: or(or(T(),x314),x315) -3|0[1]-> or(T(),x315) -3|[0]-> T() peak: or(or(F(),x317),x318) <-8|[1]- or(F(),or(x317,x318)) -5|[1]-> or(x317,x318) joins: or(or(F(),x317),x318) -5|0[1]-> or(x317,x318) peak: or(or(x,x320),x321) <-8|[1]- or(x,or(x320,x321)) -6|[1]-> or(or(x320,x321),x) joins: or(or(x,x320),x321) -7|[1]-> or(x,or(x320,x321)) or(or(x320,x321),x) -6|[1]-> or(x,or(x320,x321)) peak: or(or(or(x,y),x323),x324) <-8|[1]- or(or(x,y),or(x323,x324)) -7| [1]-> or(x,or(y,or(x323,x324))) joins: or(or(or(x,y),x323),x324) -7|[1]-> or(or(x,y),or(x323,x324)) or(x,or(y,or(x323,x324))) -8|[1]-> or(or(x,y),or(x323,x324)) peak: or(or(or(x,x326),x327),z) <-8|0[1]- or(or(x,or(x326,x327)),z) -7| [1]-> or(x,or(or(x326,x327),z)) joins: or(or(or(x,x326),x327),z) -7|0[1]-> or(or(x,or(x326,x327)),z) or(x,or(or(x326,x327),z)) -8|[1]-> or(or(x,or(x326,x327)),z) peak: or(x,or(or(y,x329),x330)) <-8|1[1]- or(x,or(y,or(x329,x330))) -8| [1]-> or(or(x,y),or(x329,x330)) joins: or(x,or(or(y,x329),x330)) -7|1[1]-> or(x,or(y,or(x329,x330))) or(or(x,y),or(x329,x330)) -7|[1]-> or(x,or(y,or(x329,x330))) Qed 1:and(x,T()) -> x and(x,F()) -> F() and(x,y) -> and(y,x) and(and(x,y),z) -> and(x,and(y,z)) Commute Transformation Processor: and(x,T()) -> x and(T(),x) -> x and(x,F()) -> F() and(F(),x) -> F() and(x,y) -> and(y,x) and(and(x,y),z) -> and(x,and(y,z)) and(x,and(y,z)) -> and(and(x,y),z) Church Rosser Transformation Processor (dup): strict: weak: and(x,T()) -> x and(T(),x) -> x and(x,F()) -> F() and(F(),x) -> F() and(x,y) -> and(y,x) and(and(x,y),z) -> and(x,and(y,z)) and(x,and(y,z)) -> and(and(x,y),z) critical peaks: 44 T() <-0|[]- and(T(),T()) -1|[]-> T() F() <-0|[]- and(F(),T()) -3|[]-> F() x <-0|[]- and(x,T()) -4|[]-> and(T(),x) and(x,y) <-0|[]- and(and(x,y),T()) -5|[]-> and(x,and(y,T())) and(x,z) <-0|0[]- and(and(x,T()),z) -5|[]-> and(x,and(T(),z)) and(x,y) <-0|1[]- and(x,and(y,T())) -6|[]-> and(and(x,y),T()) T() <-1|[]- and(T(),T()) -0|[]-> T() F() <-1|[]- and(T(),F()) -2|[]-> F() y <-1|[]- and(T(),y) -4|[]-> and(y,T()) and(y,z) <-1|0[]- and(and(T(),y),z) -5|[]-> and(T(),and(y,z)) and(y,z) <-1|[]- and(T(),and(y,z)) -6|[]-> and(and(T(),y),z) and(x,z) <-1|1[]- and(x,and(T(),z)) -6|[]-> and(and(x,T()),z) F() <-2|[]- and(T(),F()) -1|[]-> F() F() <-2|[]- and(F(),F()) -3|[]-> F() F() <-2|[]- and(x,F()) -4|[]-> and(F(),x) F() <-2|[]- and(and(x,y),F()) -5|[]-> and(x,and(y,F())) and(F(),z) <-2|0[]- and(and(x,F()),z) -5|[]-> and(x,and(F(),z)) and(x,F()) <-2|1[]- and(x,and(y,F())) -6|[]-> and(and(x,y),F()) F() <-3|[]- and(F(),T()) -0|[]-> F() F() <-3|[]- and(F(),F()) -2|[]-> F() F() <-3|[]- and(F(),y) -4|[]-> and(y,F()) and(F(),z) <-3|0[]- and(and(F(),y),z) -5|[]-> and(F(),and(y,z)) F() <-3|[]- and(F(),and(y,z)) -6|[]-> and(and(F(),y),z) and(x,F()) <-3|1[]- and(x,and(F(),z)) -6|[]-> and(and(x,F()),z) and(T(),x) <-4|[]- and(x,T()) -0|[]-> x and(x,T()) <-4|[]- and(T(),x) -1|[]-> x and(F(),x) <-4|[]- and(x,F()) -2|[]-> F() and(x,F()) <-4|[]- and(F(),x) -3|[]-> F() and(z,and(x,y)) <-4|[]- and(and(x,y),z) -5|[]-> and(x,and(y,z)) and(and(y,x),z) <-4|0[]- and(and(x,y),z) -5|[]-> and(x,and(y,z)) and(and(y,z),x) <-4|[]- and(x,and(y,z)) -6|[]-> and(and(x,y),z) and(x,and(z,y)) <-4|1[]- and(x,and(y,z)) -6|[]-> and(and(x,y),z) and(x527,and(x528,T())) <-5|[]- and(and(x527,x528),T()) -0|[]-> and(x527,x528) and(x530,and(x531,F())) <-5|[]- and(and(x530,x531),F()) -2|[]-> F() and(x533,and(x534,y)) <-5|[]- and(and(x533,x534),y) -4|[]-> and(y,and(x533,x534)) and(and(x536,and(x537,y)),z) <-5|0[]- and(and(and(x536,x537),y),z) -5| []-> and(and(x536,x537),and(y,z)) and(x539,and(x540,and(y,z))) <-5|[]- and(and(x539,x540),and(y,z)) -6| []-> and(and(and(x539,x540),y),z) and(x,and(x542,and(x543,z))) <-5|1[]- and(x,and(and(x542,x543),z)) -6| []-> and(and(x,and(x542,x543)),z) and(and(T(),x546),x547) <-6|[]- and(T(),and(x546,x547)) -1|[]-> and(x546,x547) and(and(F(),x549),x550) <-6|[]- and(F(),and(x549,x550)) -3|[]-> F() and(and(x,x552),x553) <-6|[]- and(x,and(x552,x553)) -4|[]-> and(and(x552,x553),x) and(and(and(x,y),x555),x556) <-6|[]- and(and(x,y),and(x555,x556)) -5| []-> and(x,and(y,and(x555,x556))) and(and(and(x,x558),x559),z) <-6|0[]- and(and(x,and(x558,x559)),z) -5| []-> and(x,and(and(x558,x559),z)) and(x,and(and(y,x561),x562)) <-6|1[]- and(x,and(y,and(x561,x562))) -6| []-> and(and(x,y),and(x561,x562)) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: and(T(),T()) -> T() and(T(),T()) -> T() and(F(),T()) -> F() and(F(),T()) -> F() and(x,T()) -> x and(x,T()) -> and(T(),x) and(T(),x) -> x and(and(x,y),T()) -> and(x,y) and(and(x,y),T()) -> and(x,and(y,T())) and(x,and(y,T())) -> and(x,y) and(and(x,T()),z) -> and(x,z) and(and(x,T()),z) -> and(x,and(T(),z)) and(x,and(T(),z)) -> and(x,z) and(x,and(y,T())) -> and(x,y) and(x,and(y,T())) -> and(and(x,y),T()) and(and(x,y),T()) -> and(x,y) and(T(),T()) -> T() and(T(),T()) -> T() and(T(),F()) -> F() and(T(),F()) -> F() and(T(),y) -> y and(T(),y) -> and(y,T()) and(y,T()) -> y and(and(T(),y),z) -> and(y,z) and(and(T(),y),z) -> and(T(),and(y,z)) and(T(),and(y,z)) -> and(y,z) and(T(),and(y,z)) -> and(y,z) and(T(),and(y,z)) -> and(and(T(),y),z) and(and(T(),y),z) -> and(y,z) and(x,and(T(),z)) -> and(x,z) and(x,and(T(),z)) -> and(and(x,T()),z) and(and(x,T()),z) -> and(x,z) and(T(),F()) -> F() and(T(),F()) -> F() and(F(),F()) -> F() and(F(),F()) -> F() and(x,F()) -> F() and(x,F()) -> and(F(),x) and(F(),x) -> F() and(and(x,y),F()) -> F() and(and(x,y),F()) -> and(x,and(y,F())) and(x,and(y,F())) -> and(x,F()) and(x,F()) -> F() and(x,and(y,F())) -> and(and(x,y),F()) and(and(x,y),F()) -> F() and(and(x,F()),z) -> and(F(),z) and(and(x,F()),z) -> and(x,and(F(),z)) and(x,and(F(),z)) -> and(and(x,F()),z) and(and(x,F()),z) -> and(F(),z) and(F(),z) -> F() and(x,and(F(),z)) -> and(x,F()) and(x,F()) -> F() and(F(),z) -> and(z,F()) and(z,F()) -> F() and(x,and(F(),z)) -> and(x,F()) and(x,F()) -> F() and(x,and(y,F())) -> and(x,F()) and(x,and(y,F())) -> and(and(x,y),F()) and(x,F()) -> F() and(and(x,y),F()) -> F() and(F(),T()) -> F() and(F(),T()) -> F() and(F(),F()) -> F() and(F(),F()) -> F() and(F(),y) -> F() and(F(),y) -> and(y,F()) and(y,F()) -> F() and(and(F(),y),z) -> and(F(),z) and(and(F(),y),z) -> and(F(),and(y,z)) and(F(),z) -> F() and(F(),and(y,z)) -> F() and(F(),and(y,z)) -> F() and(F(),and(y,z)) -> and(and(F(),y),z) and(and(F(),y),z) -> and(F(),z) and(F(),z) -> F() and(and(F(),y),z) -> and(F(),and(y,z)) and(F(),and(y,z)) -> F() and(x,and(F(),z)) -> and(x,F()) and(x,and(F(),z)) -> and(and(x,F()),z) and(and(x,F()),z) -> and(x,and(F(),z)) and(x,and(F(),z)) -> and(x,F()) and(x,F()) -> F() and(and(x,F()),z) -> and(F(),z) and(F(),z) -> F() and(x,F()) -> and(F(),x) and(F(),x) -> F() and(and(x,F()),z) -> and(F(),z) and(F(),z) -> F() and(x,T()) -> and(T(),x) and(x,T()) -> x and(T(),x) -> x and(T(),x) -> and(x,T()) and(T(),x) -> x and(x,T()) -> x and(x,F()) -> and(F(),x) and(x,F()) -> F() and(F(),x) -> F() and(F(),x) -> and(x,F()) and(F(),x) -> F() and(x,F()) -> F() and(and(x,y),z) -> and(z,and(x,y)) and(and(x,y),z) -> and(x,and(y,z)) and(z,and(x,y)) -> and(and(x,y),z) and(x,and(y,z)) -> and(and(x,y),z) and(and(x,y),z) -> and(and(y,x),z) and(and(x,y),z) -> and(x,and(y,z)) and(and(y,x),z) -> and(and(x,y),z) and(x,and(y,z)) -> and(and(x,y),z) and(x,and(y,z)) -> and(and(y,z),x) and(x,and(y,z)) -> and(and(x,y),z) and(and(y,z),x) -> and(x,and(y,z)) and(and(x,y),z) -> and(x,and(y,z)) and(x,and(y,z)) -> and(x,and(z,y)) and(x,and(y,z)) -> and(and(x,y),z) and(x,and(z,y)) -> and(x,and(y,z)) and(and(x,y),z) -> and(x,and(y,z)) and(and(x527,x528),T()) -> and(x527,and(x528,T())) and(and(x527,x528),T()) -> and(x527,x528) and(x527,and(x528,T())) -> and(x527,x528) and(and(x530,x531),F()) -> and(x530,and(x531,F())) and(and(x530,x531),F()) -> F() and(x530,and(x531,F())) -> and(x530,F()) and(x530,F()) -> F() and(x530,and(x531,F())) -> and(and(x530,x531),F()) and(and(x530,x531),F()) -> F() and(and(x533,x534),y) -> and(x533,and(x534,y)) and(and(x533,x534),y) -> and(y,and(x533,x534)) and(x533,and(x534,y)) -> and(and(x533,x534),y) and(y,and(x533,x534)) -> and(and(x533,x534),y) and(and(and(x536,x537),y),z) -> and(and(x536,and(x537,y)),z) and(and(and(x536,x537),y),z) -> and(and(x536,x537),and(y,z)) and(and(x536,and(x537,y)),z) -> and(and(and(x536,x537),y),z) and(and(x536,x537),and(y,z)) -> and(and(and(x536,x537),y),z) and(and(x539,x540),and(y,z)) -> and(x539,and(x540,and(y,z))) and(and(x539,x540),and(y,z)) -> and(and(and(x539,x540),y),z) and(x539,and(x540,and(y,z))) -> and(and(x539,x540),and(y,z)) and(and(and(x539,x540),y),z) -> and(and(x539,x540),and(y,z)) and(x,and(and(x542,x543),z)) -> and(x,and(x542,and(x543,z))) and(x,and(and(x542,x543),z)) -> and(and(x,and(x542,x543)),z) and(x,and(x542,and(x543,z))) -> and(x,and(and(x542,x543),z)) and(and(x,and(x542,x543)),z) -> and(x,and(and(x542,x543),z)) and(T(),and(x546,x547)) -> and(and(T(),x546),x547) and(T(),and(x546,x547)) -> and(x546,x547) and(and(T(),x546),x547) -> and(x546,x547) and(F(),and(x549,x550)) -> and(and(F(),x549),x550) and(F(),and(x549,x550)) -> F() and(and(F(),x549),x550) -> and(F(),x550) and(F(),x550) -> F() and(and(F(),x549),x550) -> and(F(),and(x549,x550)) and(F(),and(x549,x550)) -> F() and(x,and(x552,x553)) -> and(and(x,x552),x553) and(x,and(x552,x553)) -> and(and(x552,x553),x) and(and(x,x552),x553) -> and(x,and(x552,x553)) and(and(x552,x553),x) -> and(x,and(x552,x553)) and(and(x,y),and(x555,x556)) -> and(and(and(x,y),x555),x556) and(and(x,y),and(x555,x556)) -> and(x,and(y,and(x555,x556))) and(and(and(x,y),x555),x556) -> and(and(x,y),and(x555,x556)) and(x,and(y,and(x555,x556))) -> and(and(x,y),and(x555,x556)) and(and(x,and(x558,x559)),z) -> and(and(and(x,x558),x559),z) and(and(x,and(x558,x559)),z) -> and(x,and(and(x558,x559),z)) and(and(and(x,x558),x559),z) -> and(and(x,and(x558,x559)),z) and(x,and(and(x558,x559),z)) -> and(and(x,and(x558,x559)),z) and(x,and(y,and(x561,x562))) -> and(x,and(and(y,x561),x562)) and(x,and(y,and(x561,x562))) -> and(and(x,y),and(x561,x562)) and(x,and(and(y,x561),x562)) -> and(x,and(y,and(x561,x562))) and(and(x,y),and(x561,x562)) -> and(x,and(y,and(x561,x562))) weak: and(x,T()) -> x and(T(),x) -> x and(x,F()) -> F() and(F(),x) -> F() and(x,y) -> and(y,x) and(and(x,y),z) -> and(x,and(y,z)) and(x,and(y,z)) -> and(and(x,y),z) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): and(x,T()) -> x: 0 and(T(),x) -> x: 0 and(x,F()) -> F(): 0 and(F(),x) -> F(): 4 and(x,y) -> and(y,x): 6 and(and(x,y),z) -> and(x,and(y,z)): 6 and(x,and(y,z)) -> and(and(x,y),z): 6 Decreasing Processor: The following diagrams are decreasing: peak: T() <-0|[1,0]- and(T(),T()) -1|[1,0]-> T() joins: peak: F() <-0|[1,0]- and(F(),T()) -3|[1,4]-> F() joins: peak: x <-0|[1,0]- and(x,T()) -4|[1,6]-> and(T(),x) joins: and(T(),x) -1|[1,0]-> x peak: and(x,y) <-0|[1,0]- and(and(x,y),T()) -5|[1,6]-> and(x,and(y,T())) joins: and(x,and(y,T())) -0|1[1,0]-> and(x,y) peak: and(x,z) <-0|0[1,0]- and(and(x,T()),z) -5|[1,6]-> and(x,and(T(),z)) joins: and(x,and(T(),z)) -1|1[1,0]-> and(x,z) peak: and(x,y) <-0|1[1,0]- and(x,and(y,T())) -6|[1,6]-> and(and(x,y),T()) joins: and(and(x,y),T()) -0|[1,0]-> and(x,y) peak: T() <-1|[1,0]- and(T(),T()) -0|[1,0]-> T() joins: peak: F() <-1|[1,0]- and(T(),F()) -2|[1,0]-> F() joins: peak: y <-1|[1,0]- and(T(),y) -4|[1,6]-> and(y,T()) joins: and(y,T()) -0|[1,0]-> y peak: and(y,z) <-1|0[1,0]- and(and(T(),y),z) -5|[1,6]-> and(T(),and(y,z)) joins: and(T(),and(y,z)) -1|[1,0]-> and(y,z) peak: and(y,z) <-1|[1,0]- and(T(),and(y,z)) -6|[1,6]-> and(and(T(),y),z) joins: and(and(T(),y),z) -1|0[1,0]-> and(y,z) peak: and(x,z) <-1|1[1,0]- and(x,and(T(),z)) -6|[1,6]-> and(and(x,T()),z) joins: and(and(x,T()),z) -0|0[1,0]-> and(x,z) peak: F() <-2|[1,0]- and(T(),F()) -1|[1,0]-> F() joins: peak: F() <-2|[1,0]- and(F(),F()) -3|[1,4]-> F() joins: peak: F() <-2|[1,0]- and(x,F()) -4|[1,6]-> and(F(),x) joins: and(F(),x) -3|[1,4]-> F() peak: F() <-2|[1,0]- and(and(x,y),F()) -5|[1,6]-> and(x,and(y,F())) joins: and(x,and(y,F())) -2|1[1,0]-> and(x,F()) -2|[1,0]-> F() peak: and(F(),z) <-2|0[1,0]- and(and(x,F()),z) -5|[1,6]-> and(x,and(F(),z)) joins: and(F(),z) -3|[1,4]-> F() and(x,and(F(),z)) -3|1[1,4]-> and(x,F()) -2|[1,0]-> F() peak: and(x,F()) <-2|1[1,0]- and(x,and(y,F())) -6|[1,6]-> and(and(x,y),F()) joins: and(x,F()) -2|[1,0]-> F() and(and(x,y),F()) -2|[1,0]-> F() peak: F() <-3|[1,4]- and(F(),T()) -0|[1,0]-> F() joins: peak: F() <-3|[1,4]- and(F(),F()) -2|[1,0]-> F() joins: peak: F() <-3|[1,4]- and(F(),y) -4|[1,6]-> and(y,F()) joins: and(y,F()) -2|[1,0]-> F() peak: and(F(),z) <-3|0[1,4]- and(and(F(),y),z) -5|[1,6]-> and(F(),and(y,z)) joins: and(F(),z) -3|[1,4]-> F() and(F(),and(y,z)) -3|[1,4]-> F() peak: F() <-3|[1,4]- and(F(),and(y,z)) -6|[1,6]-> and(and(F(),y),z) joins: and(and(F(),y),z) -3|0[1,4]-> and(F(),z) -3|[1,4]-> F() peak: and(x,F()) <-3|1[1,4]- and(x,and(F(),z)) -6|[1,6]-> and(and(x,F()),z) joins: and(x,F()) -2|[1,0]-> F() and(and(x,F()),z) -2|0[1,0]-> and(F(),z) -3|[1,4]-> F() peak: and(T(),x) <-4|[1,6]- and(x,T()) -0|[1,0]-> x joins: and(T(),x) -1|[1,0]-> x peak: and(x,T()) <-4|[1,6]- and(T(),x) -1|[1,0]-> x joins: and(x,T()) -0|[1,0]-> x peak: and(F(),x) <-4|[1,6]- and(x,F()) -2|[1,0]-> F() joins: and(F(),x) -3|[1,4]-> F() peak: and(x,F()) <-4|[1,6]- and(F(),x) -3|[1,4]-> F() joins: and(x,F()) -2|[1,0]-> F() peak: and(z,and(x,y)) <-4|[1,6]- and(and(x,y),z) -5|[1,6]-> and(x,and(y,z)) joins: and(z,and(x,y)) -4|[1,6]-> and(and(x,y),z) and(x,and(y,z)) -6|[1,6]-> and(and(x,y),z) peak: and(and(y,x),z) <-4|0[1,6]- and(and(x,y),z) -5|[1,6]-> and(x,and(y,z)) joins: and(and(y,x),z) -4|0[1,6]-> and(and(x,y),z) and(x,and(y,z)) -6|[1,6]-> and(and(x,y),z) peak: and(and(y,z),x) <-4|[1,6]- and(x,and(y,z)) -6|[1,6]-> and(and(x,y),z) joins: and(and(y,z),x) -4|[1,6]-> and(x,and(y,z)) and(and(x,y),z) -5|[1,6]-> and(x,and(y,z)) peak: and(x,and(z,y)) <-4|1[1,6]- and(x,and(y,z)) -6|[1,6]-> and(and(x,y),z) joins: and(x,and(z,y)) -4|1[1,6]-> and(x,and(y,z)) and(and(x,y),z) -5|[1,6]-> and(x,and(y,z)) peak: and(x527,and(x528,T())) <-5|[1,6]- and(and(x527,x528),T()) -0|[1,0]-> and(x527,x528) joins: and(x527,and(x528,T())) -0|1[1,0]-> and(x527,x528) peak: and(x530,and(x531,F())) <-5|[1,6]- and(and(x530,x531),F()) -2|[1,0]-> F() joins: and(x530,and(x531,F())) -2|1[1,0]-> and(x530,F()) -2|[1,0]-> F() peak: and(x533,and(x534,y)) <-5|[1,6]- and(and(x533,x534),y) -4|[1,6]-> and(y,and(x533,x534)) joins: and(x533,and(x534,y)) -6|[1,6]-> and(and(x533,x534),y) and(y,and(x533,x534)) -4|[1,6]-> and(and(x533,x534),y) peak: and(and(x536,and(x537,y)),z) <-5|0[1,6]- and(and(and(x536,x537),y),z) -5| [1,6]-> and(and(x536,x537),and(y,z)) joins: and(and(x536,and(x537,y)),z) -6|0[1,6]-> and(and(and(x536,x537),y),z) and(and(x536,x537),and(y,z)) -6|[1,6]-> and(and(and(x536,x537),y),z) peak: and(x539,and(x540,and(y,z))) <-5|[1,6]- and(and(x539,x540),and(y,z)) -6| [1,6]-> and(and(and(x539,x540),y),z) joins: and(x539,and(x540,and(y,z))) -6|[1,6]-> and(and(x539,x540),and(y,z)) and(and(and(x539,x540),y),z) -5|[1,6]-> and(and(x539,x540),and(y,z)) peak: and(x,and(x542,and(x543,z))) <-5|1[1,6]- and(x,and(and(x542,x543),z)) -6| [1,6]-> and(and(x,and(x542,x543)),z) joins: and(x,and(x542,and(x543,z))) -6|1[1,6]-> and(x,and(and(x542,x543),z)) and(and(x,and(x542,x543)),z) -5|[1,6]-> and(x,and(and(x542,x543),z)) peak: and(and(T(),x546),x547) <-6|[1,6]- and(T(),and(x546,x547)) -1|[1,0]-> and(x546,x547) joins: and(and(T(),x546),x547) -1|0[1,0]-> and(x546,x547) peak: and(and(F(),x549),x550) <-6|[1,6]- and(F(),and(x549,x550)) -3|[1,4]-> F() joins: and(and(F(),x549),x550) -3|0[1,4]-> and(F(),x550) -3|[1,4]-> F() peak: and(and(x,x552),x553) <-6|[1,6]- and(x,and(x552,x553)) -4|[1,6]-> and(and(x552,x553),x) joins: and(and(x,x552),x553) -5|[1,6]-> and(x,and(x552,x553)) and(and(x552,x553),x) -4|[1,6]-> and(x,and(x552,x553)) peak: and(and(and(x,y),x555),x556) <-6|[1,6]- and(and(x,y),and(x555,x556)) -5| [1,6]-> and(x,and(y,and(x555,x556))) joins: and(and(and(x,y),x555),x556) -5|[1,6]-> and(and(x,y),and(x555,x556)) and(x,and(y,and(x555,x556))) -6|[1,6]-> and(and(x,y),and(x555,x556)) peak: and(and(and(x,x558),x559),z) <-6|0[1,6]- and(and(x,and(x558,x559)),z) -5| [1,6]-> and(x,and(and(x558,x559),z)) joins: and(and(and(x,x558),x559),z) -5|0[1,6]-> and(and(x,and(x558,x559)),z) and(x,and(and(x558,x559),z)) -6|[1,6]-> and(and(x,and(x558,x559)),z) peak: and(x,and(and(y,x561),x562)) <-6|1[1,6]- and(x,and(y,and(x561,x562))) -6| [1,6]-> and(and(x,y),and(x561,x562)) joins: and(x,and(and(y,x561),x562)) -5|1[1,6]-> and(x,and(y,and(x561,x562))) and(and(x,y),and(x561,x562)) -5|[1,6]-> and(x,and(y,and(x561,x562))) Qed