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