Problem: or(T(),x) -> T() or(F(),x) -> x or(or(x,y),z) -> or(x,or(y,z)) or(x,y) -> or(y,x) Proof: Commute Transformation Processor: or(T(),x) -> T() or(x,T()) -> T() or(F(),x) -> x or(x,F()) -> x or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) or(x,y) -> or(y,x) Church Rosser Transformation Processor (dup): strict: weak: or(T(),x) -> T() or(x,T()) -> T() or(F(),x) -> x or(x,F()) -> x or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) or(x,y) -> or(y,x) critical peaks: 44 T() <-0|[]- or(T(),T()) -1|[]-> T() T() <-0|[]- or(T(),F()) -3|[]-> T() or(T(),z) <-0|0[]- or(or(T(),y),z) -4|[]-> or(T(),or(y,z)) T() <-0|[]- or(T(),or(y,z)) -5|[]-> or(or(T(),y),z) or(x,T()) <-0|1[]- or(x,or(T(),z)) -5|[]-> or(or(x,T()),z) T() <-0|[]- or(T(),y) -6|[]-> or(y,T()) T() <-1|[]- or(T(),T()) -0|[]-> T() T() <-1|[]- or(F(),T()) -2|[]-> T() T() <-1|[]- or(or(x,y),T()) -4|[]-> or(x,or(y,T())) or(T(),z) <-1|0[]- or(or(x,T()),z) -4|[]-> or(x,or(T(),z)) or(x,T()) <-1|1[]- or(x,or(y,T())) -5|[]-> or(or(x,y),T()) T() <-1|[]- or(x,T()) -6|[]-> or(T(),x) T() <-2|[]- or(F(),T()) -1|[]-> T() F() <-2|[]- or(F(),F()) -3|[]-> F() or(y,z) <-2|0[]- or(or(F(),y),z) -4|[]-> or(F(),or(y,z)) or(y,z) <-2|[]- or(F(),or(y,z)) -5|[]-> or(or(F(),y),z) or(x,z) <-2|1[]- or(x,or(F(),z)) -5|[]-> or(or(x,F()),z) y <-2|[]- or(F(),y) -6|[]-> or(y,F()) T() <-3|[]- or(T(),F()) -0|[]-> T() F() <-3|[]- or(F(),F()) -2|[]-> F() or(x,y) <-3|[]- or(or(x,y),F()) -4|[]-> or(x,or(y,F())) or(x,z) <-3|0[]- or(or(x,F()),z) -4|[]-> or(x,or(F(),z)) or(x,y) <-3|1[]- or(x,or(y,F())) -5|[]-> or(or(x,y),F()) x <-3|[]- or(x,F()) -6|[]-> or(F(),x) or(x183,or(x184,T())) <-4|[]- or(or(x183,x184),T()) -1|[]-> T() or(x186,or(x187,F())) <-4|[]- or(or(x186,x187),F()) -3|[]-> or(x186,x187) or(or(x189,or(x190,y)),z) <-4|0[]- or(or(or(x189,x190),y),z) -4|[]-> or(or(x189,x190),or(y,z)) or(x192,or(x193,or(y,z))) <-4|[]- or(or(x192,x193),or(y,z)) -5|[]-> or(or(or(x192,x193),y),z) or(x,or(x195,or(x196,z))) <-4|1[]- or(x,or(or(x195,x196),z)) -5|[]-> or(or(x,or(x195,x196)),z) or(x198,or(x199,y)) <-4|[]- or(or(x198,x199),y) -6|[]-> or(y,or(x198,x199)) or(or(T(),x202),x203) <-5|[]- or(T(),or(x202,x203)) -0|[]-> T() or(or(F(),x205),x206) <-5|[]- or(F(),or(x205,x206)) -2|[]-> or(x205,x206) or(or(or(x,y),x208),x209) <-5|[]- or(or(x,y),or(x208,x209)) -4|[]-> or(x,or(y,or(x208,x209))) or(or(or(x,x211),x212),z) <-5|0[]- or(or(x,or(x211,x212)),z) -4|[]-> or(x,or(or(x211,x212),z)) or(x,or(or(y,x214),x215)) <-5|1[]- or(x,or(y,or(x214,x215))) -5|[]-> or(or(x,y),or(x214,x215)) or(or(x,x217),x218) <-5|[]- or(x,or(x217,x218)) -6|[]-> or(or(x217,x218),x) or(x,T()) <-6|[]- or(T(),x) -0|[]-> T() or(T(),x) <-6|[]- or(x,T()) -1|[]-> T() or(x,F()) <-6|[]- or(F(),x) -2|[]-> x or(F(),x) <-6|[]- or(x,F()) -3|[]-> x or(z,or(x,y)) <-6|[]- or(or(x,y),z) -4|[]-> or(x,or(y,z)) or(or(y,x),z) <-6|0[]- or(or(x,y),z) -4|[]-> or(x,or(y,z)) or(or(y,z),x) <-6|[]- or(x,or(y,z)) -5|[]-> or(or(x,y),z) or(x,or(z,y)) <-6|1[]- or(x,or(y,z)) -5|[]-> or(or(x,y),z) Polynomial Interpretation Processor: dimension: 1 interpretation: [F] = 1, [or](x0, x1) = x0 + x1, [T] = 0 orientation: or(T(),x) = x >= 0 = T() or(x,T()) = x >= 0 = T() 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(x,or(y,z)) or(x,or(y,z)) = x + y + z >= x + y + z = or(or(x,y),z) or(x,y) = x + y >= x + y = or(y,x) problem: strict: weak: or(T(),x) -> T() or(x,T()) -> T() or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) or(x,y) -> or(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [or](x0, x1) = x0 + x1 + 2, [T] = 1 orientation: or(T(),x) = x + 3 >= 1 = T() or(x,T()) = x + 3 >= 1 = T() 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(or(x,y),z) or(x,y) = x + y + 2 >= x + y + 2 = or(y,x) problem: strict: weak: or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) or(x,y) -> or(y,x) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: or(T(),T()) -> T() or(T(),T()) -> T() or(T(),F()) -> T() or(T(),F()) -> 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(),y) -> T() or(T(),y) -> or(y,T()) or(y,T()) -> T() or(T(),T()) -> T() or(T(),T()) -> T() or(F(),T()) -> T() or(F(),T()) -> 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(x,T()) -> T() or(x,T()) -> or(T(),x) or(T(),x) -> T() or(F(),T()) -> T() or(F(),T()) -> T() or(F(),F()) -> F() or(F(),F()) -> F() 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(F(),y) -> y or(F(),y) -> or(y,F()) or(y,F()) -> y or(T(),F()) -> T() or(T(),F()) -> T() or(F(),F()) -> F() or(F(),F()) -> F() 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(x,F()) -> x or(x,F()) -> or(F(),x) or(F(),x) -> x or(or(x183,x184),T()) -> or(x183,or(x184,T())) or(or(x183,x184),T()) -> T() or(x183,or(x184,T())) -> or(x183,T()) or(x183,T()) -> T() or(x183,or(x184,T())) -> or(or(x183,x184),T()) or(or(x183,x184),T()) -> T() or(or(x186,x187),F()) -> or(x186,or(x187,F())) or(or(x186,x187),F()) -> or(x186,x187) or(x186,or(x187,F())) -> or(x186,x187) or(or(or(x189,x190),y),z) -> or(or(x189,or(x190,y)),z) or(or(or(x189,x190),y),z) -> or(or(x189,x190),or(y,z)) or(or(x189,or(x190,y)),z) -> or(or(or(x189,x190),y),z) or(or(x189,x190),or(y,z)) -> or(or(or(x189,x190),y),z) or(or(x192,x193),or(y,z)) -> or(x192,or(x193,or(y,z))) or(or(x192,x193),or(y,z)) -> or(or(or(x192,x193),y),z) or(x192,or(x193,or(y,z))) -> or(or(x192,x193),or(y,z)) or(or(or(x192,x193),y),z) -> or(or(x192,x193),or(y,z)) or(x,or(or(x195,x196),z)) -> or(x,or(x195,or(x196,z))) or(x,or(or(x195,x196),z)) -> or(or(x,or(x195,x196)),z) or(x,or(x195,or(x196,z))) -> or(x,or(or(x195,x196),z)) or(or(x,or(x195,x196)),z) -> or(x,or(or(x195,x196),z)) or(or(x198,x199),y) -> or(x198,or(x199,y)) or(or(x198,x199),y) -> or(y,or(x198,x199)) or(x198,or(x199,y)) -> or(or(x198,x199),y) or(y,or(x198,x199)) -> or(or(x198,x199),y) or(T(),or(x202,x203)) -> or(or(T(),x202),x203) or(T(),or(x202,x203)) -> T() or(or(T(),x202),x203) -> or(T(),x203) or(T(),x203) -> T() or(or(T(),x202),x203) -> or(T(),or(x202,x203)) or(T(),or(x202,x203)) -> T() or(F(),or(x205,x206)) -> or(or(F(),x205),x206) or(F(),or(x205,x206)) -> or(x205,x206) or(or(F(),x205),x206) -> or(x205,x206) or(or(x,y),or(x208,x209)) -> or(or(or(x,y),x208),x209) or(or(x,y),or(x208,x209)) -> or(x,or(y,or(x208,x209))) or(or(or(x,y),x208),x209) -> or(or(x,y),or(x208,x209)) or(x,or(y,or(x208,x209))) -> or(or(x,y),or(x208,x209)) or(or(x,or(x211,x212)),z) -> or(or(or(x,x211),x212),z) or(or(x,or(x211,x212)),z) -> or(x,or(or(x211,x212),z)) or(or(or(x,x211),x212),z) -> or(or(x,or(x211,x212)),z) or(x,or(or(x211,x212),z)) -> or(or(x,or(x211,x212)),z) or(x,or(y,or(x214,x215))) -> or(x,or(or(y,x214),x215)) or(x,or(y,or(x214,x215))) -> or(or(x,y),or(x214,x215)) or(x,or(or(y,x214),x215)) -> or(x,or(y,or(x214,x215))) or(or(x,y),or(x214,x215)) -> or(x,or(y,or(x214,x215))) or(x,or(x217,x218)) -> or(or(x,x217),x218) or(x,or(x217,x218)) -> or(or(x217,x218),x) or(or(x,x217),x218) -> or(x,or(x217,x218)) or(or(x217,x218),x) -> or(x,or(x217,x218)) or(T(),x) -> or(x,T()) or(T(),x) -> T() or(x,T()) -> T() or(x,T()) -> or(T(),x) or(x,T()) -> T() or(T(),x) -> T() or(F(),x) -> or(x,F()) or(F(),x) -> x or(x,F()) -> x or(x,F()) -> or(F(),x) or(x,F()) -> x or(F(),x) -> 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)) weak: or(T(),x) -> T() or(x,T()) -> T() or(F(),x) -> x or(x,F()) -> x or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) or(x,y) -> or(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [F] = 0, [or](x0, x1) = x0 + x1 + 1, [T] = 1 orientation: or(T(),T()) = 3 >= 1 = T() or(T(),T()) = 3 >= 1 = T() or(T(),F()) = 2 >= 1 = T() or(T(),F()) = 2 >= 1 = T() or(or(T(),y),z) = y + z + 3 >= z + 2 = or(T(),z) or(or(T(),y),z) = y + z + 3 >= y + z + 3 = or(T(),or(y,z)) or(T(),z) = z + 2 >= 1 = T() or(T(),or(y,z)) = y + z + 3 >= 1 = T() or(T(),or(y,z)) = y + z + 3 >= 1 = T() or(T(),or(y,z)) = y + z + 3 >= y + z + 3 = or(or(T(),y),z) or(or(T(),y),z) = y + z + 3 >= z + 2 = or(T(),z) or(T(),z) = z + 2 >= 1 = T() or(or(T(),y),z) = y + z + 3 >= y + z + 3 = or(T(),or(y,z)) or(T(),or(y,z)) = y + z + 3 >= 1 = T() or(x,or(T(),z)) = x + z + 3 >= x + 2 = or(x,T()) or(x,or(T(),z)) = x + z + 3 >= x + z + 3 = or(or(x,T()),z) or(or(x,T()),z) = x + z + 3 >= x + z + 3 = or(x,or(T(),z)) or(x,or(T(),z)) = x + z + 3 >= x + 2 = or(x,T()) or(x,T()) = x + 2 >= 1 = T() or(or(x,T()),z) = x + z + 3 >= z + 2 = or(T(),z) or(T(),z) = z + 2 >= 1 = T() or(x,T()) = x + 2 >= x + 2 = or(T(),x) or(T(),x) = x + 2 >= 1 = T() or(or(x,T()),z) = x + z + 3 >= z + 2 = or(T(),z) or(T(),z) = z + 2 >= 1 = T() or(T(),y) = y + 2 >= 1 = T() or(T(),y) = y + 2 >= y + 2 = or(y,T()) or(y,T()) = y + 2 >= 1 = T() or(T(),T()) = 3 >= 1 = T() or(T(),T()) = 3 >= 1 = T() or(F(),T()) = 2 >= 1 = T() or(F(),T()) = 2 >= 1 = T() or(or(x,y),T()) = x + y + 3 >= 1 = T() or(or(x,y),T()) = x + y + 3 >= x + y + 3 = or(x,or(y,T())) or(x,or(y,T())) = x + y + 3 >= x + 2 = or(x,T()) or(x,T()) = x + 2 >= 1 = T() or(x,or(y,T())) = x + y + 3 >= x + y + 3 = or(or(x,y),T()) or(or(x,y),T()) = x + y + 3 >= 1 = T() or(or(x,T()),z) = x + z + 3 >= z + 2 = or(T(),z) or(or(x,T()),z) = x + z + 3 >= x + z + 3 = or(x,or(T(),z)) or(x,or(T(),z)) = x + z + 3 >= x + z + 3 = or(or(x,T()),z) or(or(x,T()),z) = x + z + 3 >= z + 2 = or(T(),z) or(T(),z) = z + 2 >= 1 = T() or(x,or(T(),z)) = x + z + 3 >= x + 2 = or(x,T()) or(x,T()) = x + 2 >= 1 = T() or(T(),z) = z + 2 >= z + 2 = or(z,T()) or(z,T()) = z + 2 >= 1 = T() or(x,or(T(),z)) = x + z + 3 >= x + 2 = or(x,T()) or(x,T()) = x + 2 >= 1 = T() or(x,or(y,T())) = x + y + 3 >= x + 2 = or(x,T()) or(x,or(y,T())) = x + y + 3 >= x + y + 3 = or(or(x,y),T()) or(x,T()) = x + 2 >= 1 = T() or(or(x,y),T()) = x + y + 3 >= 1 = T() or(x,T()) = x + 2 >= 1 = T() or(x,T()) = x + 2 >= x + 2 = or(T(),x) or(T(),x) = x + 2 >= 1 = T() or(F(),T()) = 2 >= 1 = T() or(F(),T()) = 2 >= 1 = T() or(F(),F()) = 1 >= 0 = F() or(F(),F()) = 1 >= 0 = F() or(or(F(),y),z) = y + z + 2 >= y + z + 1 = or(y,z) or(or(F(),y),z) = y + z + 2 >= y + z + 2 = or(F(),or(y,z)) or(F(),or(y,z)) = y + z + 2 >= y + z + 1 = or(y,z) or(F(),or(y,z)) = y + z + 2 >= y + z + 1 = or(y,z) or(F(),or(y,z)) = y + z + 2 >= y + z + 2 = or(or(F(),y),z) or(or(F(),y),z) = y + z + 2 >= y + z + 1 = or(y,z) or(x,or(F(),z)) = x + z + 2 >= x + z + 1 = or(x,z) or(x,or(F(),z)) = x + z + 2 >= x + z + 2 = or(or(x,F()),z) or(or(x,F()),z) = x + z + 2 >= x + z + 1 = or(x,z) 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(T(),F()) = 2 >= 1 = T() or(T(),F()) = 2 >= 1 = T() or(F(),F()) = 1 >= 0 = F() or(F(),F()) = 1 >= 0 = F() or(or(x,y),F()) = x + y + 2 >= x + y + 1 = or(x,y) or(or(x,y),F()) = x + y + 2 >= x + y + 2 = or(x,or(y,F())) or(x,or(y,F())) = x + y + 2 >= x + y + 1 = or(x,y) or(or(x,F()),z) = x + z + 2 >= x + z + 1 = or(x,z) or(or(x,F()),z) = x + z + 2 >= x + z + 2 = or(x,or(F(),z)) or(x,or(F(),z)) = x + z + 2 >= x + z + 1 = or(x,z) or(x,or(y,F())) = x + y + 2 >= x + y + 1 = or(x,y) or(x,or(y,F())) = x + y + 2 >= x + y + 2 = or(or(x,y),F()) or(or(x,y),F()) = x + y + 2 >= x + y + 1 = or(x,y) 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(x183,x184),T()) = x183 + x184 + 3 >= x183 + x184 + 3 = or(x183,or(x184,T())) or(or(x183,x184),T()) = x183 + x184 + 3 >= 1 = T() or(x183,or(x184,T())) = x183 + x184 + 3 >= x183 + 2 = or(x183,T()) or(x183,T()) = x183 + 2 >= 1 = T() or(x183,or(x184,T())) = x183 + x184 + 3 >= x183 + x184 + 3 = or(or(x183,x184),T()) or(or(x183,x184),T()) = x183 + x184 + 3 >= 1 = T() or(or(x186,x187),F()) = x186 + x187 + 2 >= x186 + x187 + 2 = or(x186,or(x187,F())) or(or(x186,x187),F()) = x186 + x187 + 2 >= x186 + x187 + 1 = or(x186,x187) or(x186,or(x187,F())) = x186 + x187 + 2 >= x186 + x187 + 1 = or(x186,x187) or(or(or(x189,x190),y),z) = x189 + x190 + y + z + 3 >= x189 + x190 + y + z + 3 = or(or(x189,or(x190,y)),z) or(or(or(x189,x190),y),z) = x189 + x190 + y + z + 3 >= x189 + x190 + y + z + 3 = or(or(x189,x190),or(y,z)) or(or(x189,or(x190,y)),z) = x189 + x190 + y + z + 3 >= x189 + x190 + y + z + 3 = or(or(or(x189,x190),y),z) or(or(x189,x190),or(y,z)) = x189 + x190 + y + z + 3 >= x189 + x190 + y + z + 3 = or(or(or(x189,x190),y),z) or(or(x192,x193),or(y,z)) = x192 + x193 + y + z + 3 >= x192 + x193 + y + z + 3 = or(x192,or(x193,or(y,z))) or(or(x192,x193),or(y,z)) = x192 + x193 + y + z + 3 >= x192 + x193 + y + z + 3 = or(or(or(x192,x193),y),z) or(x192,or(x193,or(y,z))) = x192 + x193 + y + z + 3 >= x192 + x193 + y + z + 3 = or(or(x192,x193),or(y,z)) or(or(or(x192,x193),y),z) = x192 + x193 + y + z + 3 >= x192 + x193 + y + z + 3 = or(or(x192,x193),or(y,z)) or(x,or(or(x195,x196),z)) = x + x195 + x196 + z + 3 >= x + x195 + x196 + z + 3 = or(x,or(x195,or(x196,z))) or(x,or(or(x195,x196),z)) = x + x195 + x196 + z + 3 >= x + x195 + x196 + z + 3 = or(or(x,or(x195,x196)),z) or(x,or(x195,or(x196,z))) = x + x195 + x196 + z + 3 >= x + x195 + x196 + z + 3 = or(x,or(or(x195,x196),z)) or(or(x,or(x195,x196)),z) = x + x195 + x196 + z + 3 >= x + x195 + x196 + z + 3 = or(x,or(or(x195,x196),z)) or(or(x198,x199),y) = x198 + x199 + y + 2 >= x198 + x199 + y + 2 = or(x198,or(x199,y)) or(or(x198,x199),y) = x198 + x199 + y + 2 >= x198 + x199 + y + 2 = or(y,or(x198,x199)) or(x198,or(x199,y)) = x198 + x199 + y + 2 >= x198 + x199 + y + 2 = or(or(x198,x199),y) or(y,or(x198,x199)) = x198 + x199 + y + 2 >= x198 + x199 + y + 2 = or(or(x198,x199),y) or(T(),or(x202,x203)) = x202 + x203 + 3 >= x202 + x203 + 3 = or(or(T(),x202),x203) or(T(),or(x202,x203)) = x202 + x203 + 3 >= 1 = T() or(or(T(),x202),x203) = x202 + x203 + 3 >= x203 + 2 = or(T(),x203) or(T(),x203) = x203 + 2 >= 1 = T() or(or(T(),x202),x203) = x202 + x203 + 3 >= x202 + x203 + 3 = or(T(),or(x202,x203)) or(T(),or(x202,x203)) = x202 + x203 + 3 >= 1 = T() or(F(),or(x205,x206)) = x205 + x206 + 2 >= x205 + x206 + 2 = or(or(F(),x205),x206) or(F(),or(x205,x206)) = x205 + x206 + 2 >= x205 + x206 + 1 = or(x205,x206) or(or(F(),x205),x206) = x205 + x206 + 2 >= x205 + x206 + 1 = or(x205,x206) or(or(x,y),or(x208,x209)) = x + x208 + x209 + y + 3 >= x + x208 + x209 + y + 3 = or(or(or(x,y),x208),x209) or(or(x,y),or(x208,x209)) = x + x208 + x209 + y + 3 >= x + x208 + x209 + y + 3 = or(x,or(y,or(x208,x209))) or(or(or(x,y),x208),x209) = x + x208 + x209 + y + 3 >= x + x208 + x209 + y + 3 = or(or(x,y),or(x208,x209)) or(x,or(y,or(x208,x209))) = x + x208 + x209 + y + 3 >= x + x208 + x209 + y + 3 = or(or(x,y),or(x208,x209)) or(or(x,or(x211,x212)),z) = x + x211 + x212 + z + 3 >= x + x211 + x212 + z + 3 = or(or(or(x,x211),x212),z) or(or(x,or(x211,x212)),z) = x + x211 + x212 + z + 3 >= x + x211 + x212 + z + 3 = or(x,or(or(x211,x212),z)) or(or(or(x,x211),x212),z) = x + x211 + x212 + z + 3 >= x + x211 + x212 + z + 3 = or(or(x,or(x211,x212)),z) or(x,or(or(x211,x212),z)) = x + x211 + x212 + z + 3 >= x + x211 + x212 + z + 3 = or(or(x,or(x211,x212)),z) or(x,or(y,or(x214,x215))) = x + x214 + x215 + y + 3 >= x + x214 + x215 + y + 3 = or(x,or(or(y,x214),x215)) or(x,or(y,or(x214,x215))) = x + x214 + x215 + y + 3 >= x + x214 + x215 + y + 3 = or(or(x,y),or(x214,x215)) or(x,or(or(y,x214),x215)) = x + x214 + x215 + y + 3 >= x + x214 + x215 + y + 3 = or(x,or(y,or(x214,x215))) or(or(x,y),or(x214,x215)) = x + x214 + x215 + y + 3 >= x + x214 + x215 + y + 3 = or(x,or(y,or(x214,x215))) or(x,or(x217,x218)) = x + x217 + x218 + 2 >= x + x217 + x218 + 2 = or(or(x,x217),x218) or(x,or(x217,x218)) = x + x217 + x218 + 2 >= x + x217 + x218 + 2 = or(or(x217,x218),x) or(or(x,x217),x218) = x + x217 + x218 + 2 >= x + x217 + x218 + 2 = or(x,or(x217,x218)) or(or(x217,x218),x) = x + x217 + x218 + 2 >= x + x217 + x218 + 2 = or(x,or(x217,x218)) or(T(),x) = x + 2 >= x + 2 = or(x,T()) or(T(),x) = x + 2 >= 1 = T() or(x,T()) = x + 2 >= 1 = T() or(x,T()) = x + 2 >= x + 2 = or(T(),x) or(x,T()) = x + 2 >= 1 = T() or(T(),x) = x + 2 >= 1 = T() 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(x,F()) = x + 1 >= x + 1 = or(F(),x) or(x,F()) = x + 1 >= x = x or(F(),x) = x + 1 >= x = x or(or(x,y),z) = x + y + z + 2 >= x + y + z + 2 = or(z,or(x,y)) or(or(x,y),z) = x + y + z + 2 >= x + y + z + 2 = or(x,or(y,z)) or(z,or(x,y)) = x + y + z + 2 >= x + y + z + 2 = or(or(x,y),z) or(x,or(y,z)) = x + y + z + 2 >= x + y + z + 2 = or(or(x,y),z) or(or(x,y),z) = x + y + z + 2 >= x + y + z + 2 = or(or(y,x),z) or(or(x,y),z) = x + y + z + 2 >= x + y + z + 2 = or(x,or(y,z)) or(or(y,x),z) = x + y + z + 2 >= x + y + z + 2 = or(or(x,y),z) or(x,or(y,z)) = x + y + z + 2 >= x + y + z + 2 = or(or(x,y),z) or(x,or(y,z)) = x + y + z + 2 >= x + y + z + 2 = or(or(y,z),x) or(x,or(y,z)) = x + y + z + 2 >= x + y + z + 2 = or(or(x,y),z) or(or(y,z),x) = x + y + z + 2 >= x + y + z + 2 = or(x,or(y,z)) 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(x,or(z,y)) or(x,or(y,z)) = x + y + z + 2 >= x + y + z + 2 = or(or(x,y),z) or(x,or(z,y)) = x + y + z + 2 >= x + y + z + 2 = or(x,or(y,z)) or(or(x,y),z) = x + y + z + 2 >= x + y + z + 2 = or(x,or(y,z)) or(x,y) = x + y + 1 >= x + y + 1 = or(y,x) problem: strict: 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(T(),y) -> or(y,T()) 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(x,T()) -> or(T(),x) 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(F(),y) -> or(y,F()) 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(x,F()) -> or(F(),x) or(or(x183,x184),T()) -> or(x183,or(x184,T())) or(x183,or(x184,T())) -> or(or(x183,x184),T()) or(or(x186,x187),F()) -> or(x186,or(x187,F())) or(or(or(x189,x190),y),z) -> or(or(x189,or(x190,y)),z) or(or(or(x189,x190),y),z) -> or(or(x189,x190),or(y,z)) or(or(x189,or(x190,y)),z) -> or(or(or(x189,x190),y),z) or(or(x189,x190),or(y,z)) -> or(or(or(x189,x190),y),z) or(or(x192,x193),or(y,z)) -> or(x192,or(x193,or(y,z))) or(or(x192,x193),or(y,z)) -> or(or(or(x192,x193),y),z) or(x192,or(x193,or(y,z))) -> or(or(x192,x193),or(y,z)) or(or(or(x192,x193),y),z) -> or(or(x192,x193),or(y,z)) or(x,or(or(x195,x196),z)) -> or(x,or(x195,or(x196,z))) or(x,or(or(x195,x196),z)) -> or(or(x,or(x195,x196)),z) or(x,or(x195,or(x196,z))) -> or(x,or(or(x195,x196),z)) or(or(x,or(x195,x196)),z) -> or(x,or(or(x195,x196),z)) or(or(x198,x199),y) -> or(x198,or(x199,y)) or(or(x198,x199),y) -> or(y,or(x198,x199)) or(x198,or(x199,y)) -> or(or(x198,x199),y) or(y,or(x198,x199)) -> or(or(x198,x199),y) or(T(),or(x202,x203)) -> or(or(T(),x202),x203) or(or(T(),x202),x203) -> or(T(),or(x202,x203)) or(F(),or(x205,x206)) -> or(or(F(),x205),x206) or(or(x,y),or(x208,x209)) -> or(or(or(x,y),x208),x209) or(or(x,y),or(x208,x209)) -> or(x,or(y,or(x208,x209))) or(or(or(x,y),x208),x209) -> or(or(x,y),or(x208,x209)) or(x,or(y,or(x208,x209))) -> or(or(x,y),or(x208,x209)) or(or(x,or(x211,x212)),z) -> or(or(or(x,x211),x212),z) or(or(x,or(x211,x212)),z) -> or(x,or(or(x211,x212),z)) or(or(or(x,x211),x212),z) -> or(or(x,or(x211,x212)),z) or(x,or(or(x211,x212),z)) -> or(or(x,or(x211,x212)),z) or(x,or(y,or(x214,x215))) -> or(x,or(or(y,x214),x215)) or(x,or(y,or(x214,x215))) -> or(or(x,y),or(x214,x215)) or(x,or(or(y,x214),x215)) -> or(x,or(y,or(x214,x215))) or(or(x,y),or(x214,x215)) -> or(x,or(y,or(x214,x215))) or(x,or(x217,x218)) -> or(or(x,x217),x218) or(x,or(x217,x218)) -> or(or(x217,x218),x) or(or(x,x217),x218) -> or(x,or(x217,x218)) or(or(x217,x218),x) -> or(x,or(x217,x218)) or(T(),x) -> or(x,T()) or(x,T()) -> or(T(),x) or(F(),x) -> or(x,F()) or(x,F()) -> or(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)) weak: or(or(x,y),z) -> or(x,or(y,z)) or(x,or(y,z)) -> or(or(x,y),z) or(x,y) -> or(y,x) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: T() <-0|[1]- or(T(),T()) -1|[1]-> T() joins: peak: T() <-0|[1]- or(T(),F()) -3|[1]-> T() joins: peak: or(T(),z) <-0|0[1]- or(or(T(),y),z) -4|[1]-> or(T(),or(y,z)) joins: or(T(),z) -0|[0]-> T() or(T(),or(y,z)) -0|[1]-> T() peak: T() <-0|[1]- or(T(),or(y,z)) -5|[1]-> or(or(T(),y),z) joins: or(or(T(),y),z) -0|0[1]-> or(T(),z) -0|[0]-> T() peak: or(x,T()) <-0|1[1]- or(x,or(T(),z)) -5|[1]-> or(or(x,T()),z) joins: or(x,T()) -1|[0]-> T() or(or(x,T()),z) -1|0[1]-> or(T(),z) -0|[0]-> T() peak: T() <-0|[1]- or(T(),y) -6|[1]-> or(y,T()) joins: or(y,T()) -1|[1]-> T() peak: T() <-1|[1]- or(T(),T()) -0|[1]-> T() joins: peak: T() <-1|[1]- or(F(),T()) -2|[1]-> T() joins: peak: T() <-1|[1]- or(or(x,y),T()) -4|[1]-> or(x,or(y,T())) joins: or(x,or(y,T())) -1|1[1]-> or(x,T()) -1|[0]-> T() peak: or(T(),z) <-1|0[1]- or(or(x,T()),z) -4|[1]-> or(x,or(T(),z)) joins: or(T(),z) -0|[0]-> T() or(x,or(T(),z)) -0|1[1]-> or(x,T()) -1|[0]-> T() peak: or(x,T()) <-1|1[1]- or(x,or(y,T())) -5|[1]-> or(or(x,y),T()) joins: or(x,T()) -1|[0]-> T() or(or(x,y),T()) -1|[1]-> T() peak: T() <-1|[1]- or(x,T()) -6|[1]-> or(T(),x) joins: or(T(),x) -0|[1]-> T() peak: T() <-2|[1]- or(F(),T()) -1|[1]-> T() joins: peak: F() <-2|[1]- or(F(),F()) -3|[1]-> F() joins: peak: or(y,z) <-2|0[1]- or(or(F(),y),z) -4|[1]-> or(F(),or(y,z)) joins: or(F(),or(y,z)) -2|[1]-> or(y,z) peak: or(y,z) <-2|[1]- or(F(),or(y,z)) -5|[1]-> or(or(F(),y),z) joins: or(or(F(),y),z) -2|0[1]-> or(y,z) peak: or(x,z) <-2|1[1]- or(x,or(F(),z)) -5|[1]-> or(or(x,F()),z) joins: or(or(x,F()),z) -3|0[1]-> or(x,z) peak: y <-2|[1]- or(F(),y) -6|[1]-> or(y,F()) joins: or(y,F()) -3|[1]-> y peak: T() <-3|[1]- or(T(),F()) -0|[1]-> T() joins: peak: F() <-3|[1]- or(F(),F()) -2|[1]-> F() joins: peak: or(x,y) <-3|[1]- or(or(x,y),F()) -4|[1]-> or(x,or(y,F())) joins: or(x,or(y,F())) -3|1[1]-> or(x,y) peak: or(x,z) <-3|0[1]- or(or(x,F()),z) -4|[1]-> or(x,or(F(),z)) joins: or(x,or(F(),z)) -2|1[1]-> or(x,z) peak: or(x,y) <-3|1[1]- or(x,or(y,F())) -5|[1]-> or(or(x,y),F()) joins: or(or(x,y),F()) -3|[1]-> or(x,y) peak: x <-3|[1]- or(x,F()) -6|[1]-> or(F(),x) joins: or(F(),x) -2|[1]-> x peak: or(x183,or(x184,T())) <-4|[1]- or(or(x183,x184),T()) -1|[1]-> T() joins: or(x183,or(x184,T())) -1|1[1]-> or(x183,T()) -1|[0]-> T() peak: or(x186,or(x187,F())) <-4|[1]- or(or(x186,x187),F()) -3|[1]-> or(x186,x187) joins: or(x186,or(x187,F())) -3|1[1]-> or(x186,x187) peak: or(or(x189,or(x190,y)),z) <-4|0[1]- or(or(or(x189,x190),y),z) -4| [1]-> or(or(x189,x190),or(y,z)) joins: or(or(x189,or(x190,y)),z) -5|0[1]-> or(or(or(x189,x190),y),z) or(or(x189,x190),or(y,z)) -5|[1]-> or(or(or(x189,x190),y),z) peak: or(x192,or(x193,or(y,z))) <-4|[1]- or(or(x192,x193),or(y,z)) -5| [1]-> or(or(or(x192,x193),y),z) joins: or(x192,or(x193,or(y,z))) -5|[1]-> or(or(x192,x193),or(y,z)) or(or(or(x192,x193),y),z) -4|[1]-> or(or(x192,x193),or(y,z)) peak: or(x,or(x195,or(x196,z))) <-4|1[1]- or(x,or(or(x195,x196),z)) -5| [1]-> or(or(x,or(x195,x196)),z) joins: or(x,or(x195,or(x196,z))) -5|1[1]-> or(x,or(or(x195,x196),z)) or(or(x,or(x195,x196)),z) -4|[1]-> or(x,or(or(x195,x196),z)) peak: or(x198,or(x199,y)) <-4|[1]- or(or(x198,x199),y) -6|[1]-> or(y,or(x198,x199)) joins: or(x198,or(x199,y)) -5|[1]-> or(or(x198,x199),y) or(y,or(x198,x199)) -6|[1]-> or(or(x198,x199),y) peak: or(or(T(),x202),x203) <-5|[1]- or(T(),or(x202,x203)) -0|[1]-> T() joins: or(or(T(),x202),x203) -0|0[1]-> or(T(),x203) -0|[0]-> T() peak: or(or(F(),x205),x206) <-5|[1]- or(F(),or(x205,x206)) -2|[1]-> or(x205,x206) joins: or(or(F(),x205),x206) -2|0[1]-> or(x205,x206) peak: or(or(or(x,y),x208),x209) <-5|[1]- or(or(x,y),or(x208,x209)) -4| [1]-> or(x,or(y,or(x208,x209))) joins: or(or(or(x,y),x208),x209) -4|[1]-> or(or(x,y),or(x208,x209)) or(x,or(y,or(x208,x209))) -5|[1]-> or(or(x,y),or(x208,x209)) peak: or(or(or(x,x211),x212),z) <-5|0[1]- or(or(x,or(x211,x212)),z) -4| [1]-> or(x,or(or(x211,x212),z)) joins: or(or(or(x,x211),x212),z) -4|0[1]-> or(or(x,or(x211,x212)),z) or(x,or(or(x211,x212),z)) -5|[1]-> or(or(x,or(x211,x212)),z) peak: or(x,or(or(y,x214),x215)) <-5|1[1]- or(x,or(y,or(x214,x215))) -5| [1]-> or(or(x,y),or(x214,x215)) joins: or(x,or(or(y,x214),x215)) -4|1[1]-> or(x,or(y,or(x214,x215))) or(or(x,y),or(x214,x215)) -4|[1]-> or(x,or(y,or(x214,x215))) peak: or(or(x,x217),x218) <-5|[1]- or(x,or(x217,x218)) -6|[1]-> or(or(x217,x218),x) joins: or(or(x,x217),x218) -4|[1]-> or(x,or(x217,x218)) or(or(x217,x218),x) -6|[1]-> or(x,or(x217,x218)) peak: or(x,T()) <-6|[1]- or(T(),x) -0|[1]-> T() joins: or(x,T()) -1|[1]-> T() peak: or(T(),x) <-6|[1]- or(x,T()) -1|[1]-> T() joins: or(T(),x) -0|[1]-> T() peak: or(x,F()) <-6|[1]- or(F(),x) -2|[1]-> x joins: or(x,F()) -3|[1]-> x peak: or(F(),x) <-6|[1]- or(x,F()) -3|[1]-> x joins: or(F(),x) -2|[1]-> x peak: or(z,or(x,y)) <-6|[1]- or(or(x,y),z) -4|[1]-> or(x,or(y,z)) joins: or(z,or(x,y)) -6|[1]-> or(or(x,y),z) or(x,or(y,z)) -5|[1]-> or(or(x,y),z) peak: or(or(y,x),z) <-6|0[1]- or(or(x,y),z) -4|[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)) -5|[1]-> or(or(x,y),z) peak: or(or(y,z),x) <-6|[1]- or(x,or(y,z)) -5|[1]-> or(or(x,y),z) joins: or(or(y,z),x) -6|[1]-> or(x,or(y,z)) or(or(x,y),z) -4|[1]-> or(x,or(y,z)) peak: or(x,or(z,y)) <-6|1[1]- or(x,or(y,z)) -5|[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) -4|[1]-> or(x,or(y,z)) Qed