Problem: +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) +(s(x),y) -> +(x,s(y)) +(x,s(y)) -> +(s(x),y) *(x,s(y)) -> +(x,*(x,y)) *(s(x),y) -> +(*(x,y),y) *(x,y) -> *(y,x) sq(x) -> *(x,x) sq(s(x)) -> +(*(x,x),s(+(x,x))) Proof: Church Rosser Transformation Processor (star): strict: sq(0)(s(0)(x)) -> +(0)(*(0)(x)) sq(0)(s(0)(x)) -> +(0)(*(1)(x)) sq(0)(s(0)(x)) -> +(1)(s(0)(+(0)(x))) sq(0)(s(0)(x)) -> +(1)(s(0)(+(1)(x))) sq(0)(x) -> *(0)(x) sq(0)(x) -> *(1)(x) *(1)(y) -> +(0)(*(1)(y)) *(1)(y) -> +(1)(y) *(0)(x) -> +(0)(x) *(0)(x) -> +(1)(*(0)(x)) weak: *(0)(x) -> *(1)(x) *(1)(y) -> *(0)(y) *(0)(s(0)(x)) -> +(0)(*(0)(x)) *(1)(s(0)(y)) -> +(1)(*(1)(y)) +(0)(x) -> +(0)(s(0)(x)) +(1)(s(0)(y)) -> +(1)(y) +(0)(s(0)(x)) -> +(0)(x) +(1)(y) -> +(1)(s(0)(y)) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) +(0)(+(0)(x)) -> +(0)(x) +(0)(+(1)(y)) -> +(1)(+(0)(y)) +(1)(z) -> +(1)(+(1)(z)) +(0)(x) -> +(0)(+(0)(x)) +(1)(+(0)(y)) -> +(0)(+(1)(y)) +(1)(+(1)(z)) -> +(1)(z) critical peaks: 34 +(x,+(+(y,x344),x345)) <-0|1[]- +(x,+(y,+(x344,x345))) -0|[]-> +(+(x,y),+(x344,x345)) +(+(+(x,y),x347),x348) <-0|[]- +(+(x,y),+(x347,x348)) -1|[]-> +(x,+(y,+(x347,x348))) +(+(+(x,x350),x351),z) <-0|0[]- +(+(x,+(x350,x351)),z) -1|[]-> +(x,+(+(x350,x351),z)) +(+(x,x353),x354) <-0|[]- +(x,+(x353,x354)) -2|[]-> +(+(x353,x354),x) +(+(s(x),x356),x357) <-0|[]- +(s(x),+(x356,x357)) -3|[]-> +(x,s(+(x356,x357))) +(x358,+(x359,+(y,z))) <-1|[]- +(+(x358,x359),+(y,z)) -0|[]-> +(+(+(x358,x359),y),z) +(x,+(x361,+(x362,z))) <-1|1[]- +(x,+(+(x361,x362),z)) -0|[]-> +(+(x,+(x361,x362)),z) +(+(x364,+(x365,y)),z) <-1|0[]- +(+(+(x364,x365),y),z) -1|[]-> +(+(x364,x365),+(y,z)) +(x367,+(x368,y)) <-1|[]- +(+(x367,x368),y) -2|[]-> +(y,+(x367,x368)) +(x370,+(x371,s(y))) <-1|[]- +(+(x370,x371),s(y)) -4|[]-> +(s(+(x370,x371)),y) +(+(y,z),x) <-2|[]- +(x,+(y,z)) -0|[]-> +(+(x,y),z) +(x,+(z,y)) <-2|1[]- +(x,+(y,z)) -0|[]-> +(+(x,y),z) +(z,+(x,y)) <-2|[]- +(+(x,y),z) -1|[]-> +(x,+(y,z)) +(+(y,x),z) <-2|0[]- +(+(x,y),z) -1|[]-> +(x,+(y,z)) +(y,s(x)) <-2|[]- +(s(x),y) -3|[]-> +(x,s(y)) +(s(y),x) <-2|[]- +(x,s(y)) -4|[]-> +(s(x),y) +(x385,s(+(y,z))) <-3|[]- +(s(x385),+(y,z)) -0|[]-> +(+(s(x385),y),z) +(x,+(x387,s(z))) <-3|1[]- +(x,+(s(x387),z)) -0|[]-> +(+(x,s(x387)),z) +(+(x389,s(y)),z) <-3|0[]- +(+(s(x389),y),z) -1|[]-> +(s(x389),+(y,z)) +(x391,s(y)) <-3|[]- +(s(x391),y) -2|[]-> +(y,s(x391)) +(x393,s(s(y))) <-3|[]- +(s(x393),s(y)) -4|[]-> +(s(s(x393)),y) +(x,+(s(y),x396)) <-4|1[]- +(x,+(y,s(x396))) -0|[]-> +(+(x,y),s(x396)) +(s(+(x,y)),x398) <-4|[]- +(+(x,y),s(x398)) -1|[]-> +(x,+(y,s(x398))) +(+(s(x),x400),z) <-4|0[]- +(+(x,s(x400)),z) -1|[]-> +(x,+(s(x400),z)) +(s(x),x402) <-4|[]- +(x,s(x402)) -2|[]-> +(s(x402),x) +(s(s(x)),x404) <-4|[]- +(s(x),s(x404)) -3|[]-> +(x,s(s(x404))) +(s(x),*(s(x),x406)) <-5|[]- *(s(x),s(x406)) -6|[]-> +(*(x,s(x406)),s(x406)) +(x,*(x,x408)) <-5|[]- *(x,s(x408)) -7|[]-> *(s(x408),x) +(*(x409,s(y)),s(y)) <-6|[]- *(s(x409),s(y)) -5|[]-> +(s(x409),*(s(x409),y)) +(*(x411,y),y) <-6|[]- *(s(x411),y) -7|[]-> *(y,s(x411)) *(s(y),x) <-7|[]- *(x,s(y)) -5|[]-> +(x,*(x,y)) *(y,s(x)) <-7|[]- *(s(x),y) -6|[]-> +(*(x,y),y) *(s(x),s(x)) <-8|[]- sq(s(x)) -9|[]-> +(*(x,x),s(+(x,x))) +(*(x418,x418),s(+(x418,x418))) <-9|[]- sq(s(x418)) -8|[]-> *(s(x418),s(x418)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [+(1)](x0) = x0, [*(1)](x0) = x0, [*(0)](x0) = x0, [+(0)](x0) = x0, [s(0)](x0) = x0, [sq(0)](x0) = x0 + 3 orientation: sq(0)(s(0)(x)) = x + 3 >= x = +(0)(*(0)(x)) sq(0)(s(0)(x)) = x + 3 >= x = +(0)(*(1)(x)) sq(0)(s(0)(x)) = x + 3 >= x = +(1)(s(0)(+(0)(x))) sq(0)(s(0)(x)) = x + 3 >= x = +(1)(s(0)(+(1)(x))) sq(0)(x) = x + 3 >= x = *(0)(x) sq(0)(x) = x + 3 >= x = *(1)(x) *(1)(y) = y >= y = +(0)(*(1)(y)) *(1)(y) = y >= y = +(1)(y) *(0)(x) = x >= x = +(0)(x) *(0)(x) = x >= x = +(1)(*(0)(x)) *(0)(x) = x >= x = *(1)(x) *(1)(y) = y >= y = *(0)(y) *(0)(s(0)(x)) = x >= x = +(0)(*(0)(x)) *(1)(s(0)(y)) = y >= y = +(1)(*(1)(y)) +(0)(x) = x >= x = +(0)(s(0)(x)) +(1)(s(0)(y)) = y >= y = +(1)(y) +(0)(s(0)(x)) = x >= x = +(0)(x) +(1)(y) = y >= y = +(1)(s(0)(y)) +(0)(x) = x >= x = +(1)(x) +(1)(y) = y >= y = +(0)(y) +(0)(+(0)(x)) = x >= x = +(0)(x) +(0)(+(1)(y)) = y >= y = +(1)(+(0)(y)) +(1)(z) = z >= z = +(1)(+(1)(z)) +(0)(x) = x >= x = +(0)(+(0)(x)) +(1)(+(0)(y)) = y >= y = +(0)(+(1)(y)) +(1)(+(1)(z)) = z >= z = +(1)(z) problem: strict: *(1)(y) -> +(0)(*(1)(y)) *(1)(y) -> +(1)(y) *(0)(x) -> +(0)(x) *(0)(x) -> +(1)(*(0)(x)) weak: *(0)(x) -> *(1)(x) *(1)(y) -> *(0)(y) *(0)(s(0)(x)) -> +(0)(*(0)(x)) *(1)(s(0)(y)) -> +(1)(*(1)(y)) +(0)(x) -> +(0)(s(0)(x)) +(1)(s(0)(y)) -> +(1)(y) +(0)(s(0)(x)) -> +(0)(x) +(1)(y) -> +(1)(s(0)(y)) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) +(0)(+(0)(x)) -> +(0)(x) +(0)(+(1)(y)) -> +(1)(+(0)(y)) +(1)(z) -> +(1)(+(1)(z)) +(0)(x) -> +(0)(+(0)(x)) +(1)(+(0)(y)) -> +(0)(+(1)(y)) +(1)(+(1)(z)) -> +(1)(z) Matrix Interpretation Processor: dim=1, lab=right interpretation: [+(1)](x0) = x0, [*(1)](x0) = x0 + 2, [*(0)](x0) = x0 + 2, [+(0)](x0) = x0, [s(0)](x0) = x0 orientation: *(1)(y) = y + 2 >= y + 2 = +(0)(*(1)(y)) *(1)(y) = y + 2 >= y = +(1)(y) *(0)(x) = x + 2 >= x = +(0)(x) *(0)(x) = x + 2 >= x + 2 = +(1)(*(0)(x)) *(0)(x) = x + 2 >= x + 2 = *(1)(x) *(1)(y) = y + 2 >= y + 2 = *(0)(y) *(0)(s(0)(x)) = x + 2 >= x + 2 = +(0)(*(0)(x)) *(1)(s(0)(y)) = y + 2 >= y + 2 = +(1)(*(1)(y)) +(0)(x) = x >= x = +(0)(s(0)(x)) +(1)(s(0)(y)) = y >= y = +(1)(y) +(0)(s(0)(x)) = x >= x = +(0)(x) +(1)(y) = y >= y = +(1)(s(0)(y)) +(0)(x) = x >= x = +(1)(x) +(1)(y) = y >= y = +(0)(y) +(0)(+(0)(x)) = x >= x = +(0)(x) +(0)(+(1)(y)) = y >= y = +(1)(+(0)(y)) +(1)(z) = z >= z = +(1)(+(1)(z)) +(0)(x) = x >= x = +(0)(+(0)(x)) +(1)(+(0)(y)) = y >= y = +(0)(+(1)(y)) +(1)(+(1)(z)) = z >= z = +(1)(z) problem: strict: *(1)(y) -> +(0)(*(1)(y)) *(0)(x) -> +(1)(*(0)(x)) weak: *(0)(x) -> *(1)(x) *(1)(y) -> *(0)(y) *(0)(s(0)(x)) -> +(0)(*(0)(x)) *(1)(s(0)(y)) -> +(1)(*(1)(y)) +(0)(x) -> +(0)(s(0)(x)) +(1)(s(0)(y)) -> +(1)(y) +(0)(s(0)(x)) -> +(0)(x) +(1)(y) -> +(1)(s(0)(y)) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) +(0)(+(0)(x)) -> +(0)(x) +(0)(+(1)(y)) -> +(1)(+(0)(y)) +(1)(z) -> +(1)(+(1)(z)) +(0)(x) -> +(0)(+(0)(x)) +(1)(+(0)(y)) -> +(0)(+(1)(y)) +(1)(+(1)(z)) -> +(1)(z) Matrix Interpretation Processor: dim=2, lab=right interpretation: [1 0] [+(1)](x0) = [2 0]x0, [1 1] [0] [*(1)](x0) = [2 2]x0 + [1], [1 1] [0] [*(0)](x0) = [2 2]x0 + [1], [1 0] [+(0)](x0) = [2 0]x0, [0] [s(0)](x0) = x0 + [1] orientation: [1 1] [0] [1 1] *(1)(y) = [2 2]y + [1] >= [2 2]y = +(0)(*(1)(y)) [1 1] [0] [1 1] *(0)(x) = [2 2]x + [1] >= [2 2]x = +(1)(*(0)(x)) [1 1] [0] [1 1] [0] *(0)(x) = [2 2]x + [1] >= [2 2]x + [1] = *(1)(x) [1 1] [0] [1 1] [0] *(1)(y) = [2 2]y + [1] >= [2 2]y + [1] = *(0)(y) [1 1] [1] [1 1] *(0)(s(0)(x)) = [2 2]x + [3] >= [2 2]x = +(0)(*(0)(x)) [1 1] [1] [1 1] *(1)(s(0)(y)) = [2 2]y + [3] >= [2 2]y = +(1)(*(1)(y)) [1 0] [1 0] +(0)(x) = [2 0]x >= [2 0]x = +(0)(s(0)(x)) [1 0] [1 0] +(1)(s(0)(y)) = [2 0]y >= [2 0]y = +(1)(y) [1 0] [1 0] +(0)(s(0)(x)) = [2 0]x >= [2 0]x = +(0)(x) [1 0] [1 0] +(1)(y) = [2 0]y >= [2 0]y = +(1)(s(0)(y)) [1 0] [1 0] +(0)(x) = [2 0]x >= [2 0]x = +(1)(x) [1 0] [1 0] +(1)(y) = [2 0]y >= [2 0]y = +(0)(y) [1 0] [1 0] +(0)(+(0)(x)) = [2 0]x >= [2 0]x = +(0)(x) [1 0] [1 0] +(0)(+(1)(y)) = [2 0]y >= [2 0]y = +(1)(+(0)(y)) [1 0] [1 0] +(1)(z) = [2 0]z >= [2 0]z = +(1)(+(1)(z)) [1 0] [1 0] +(0)(x) = [2 0]x >= [2 0]x = +(0)(+(0)(x)) [1 0] [1 0] +(1)(+(0)(y)) = [2 0]y >= [2 0]y = +(0)(+(1)(y)) [1 0] [1 0] +(1)(+(1)(z)) = [2 0]z >= [2 0]z = +(1)(z) problem: strict: *(1)(y) -> +(0)(*(1)(y)) *(0)(x) -> +(1)(*(0)(x)) weak: *(0)(x) -> *(1)(x) *(1)(y) -> *(0)(y) +(0)(x) -> +(0)(s(0)(x)) +(1)(s(0)(y)) -> +(1)(y) +(0)(s(0)(x)) -> +(0)(x) +(1)(y) -> +(1)(s(0)(y)) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) +(0)(+(0)(x)) -> +(0)(x) +(0)(+(1)(y)) -> +(1)(+(0)(y)) +(1)(z) -> +(1)(+(1)(z)) +(0)(x) -> +(0)(+(0)(x)) +(1)(+(0)(y)) -> +(0)(+(1)(y)) +(1)(+(1)(z)) -> +(1)(z) Shift Processor (**) lab=left: strict: weak: Shift Processor lab=left (dd): strict: +(x,+(y,+(x344,x345))) -> +(x,+(+(y,x344),x345)) +(x,+(y,+(x344,x345))) -> +(+(x,y),+(x344,x345)) +(x,+(+(y,x344),x345)) -> +(x,+(y,+(x344,x345))) +(+(x,y),+(x344,x345)) -> +(x,+(y,+(x344,x345))) +(+(x,y),+(x347,x348)) -> +(+(+(x,y),x347),x348) +(+(x,y),+(x347,x348)) -> +(x,+(y,+(x347,x348))) +(+(+(x,y),x347),x348) -> +(+(x,y),+(x347,x348)) +(x,+(y,+(x347,x348))) -> +(+(x,y),+(x347,x348)) +(+(x,+(x350,x351)),z) -> +(+(+(x,x350),x351),z) +(+(x,+(x350,x351)),z) -> +(x,+(+(x350,x351),z)) +(+(+(x,x350),x351),z) -> +(+(x,+(x350,x351)),z) +(x,+(+(x350,x351),z)) -> +(+(x,+(x350,x351)),z) +(x,+(x353,x354)) -> +(+(x,x353),x354) +(x,+(x353,x354)) -> +(+(x353,x354),x) +(+(x,x353),x354) -> +(x,+(x353,x354)) +(+(x353,x354),x) -> +(x,+(x353,x354)) +(s(x),+(x356,x357)) -> +(+(s(x),x356),x357) +(s(x),+(x356,x357)) -> +(x,s(+(x356,x357))) +(+(s(x),x356),x357) -> +(s(x),+(x356,x357)) +(x,s(+(x356,x357))) -> +(s(x),+(x356,x357)) +(+(x358,x359),+(y,z)) -> +(x358,+(x359,+(y,z))) +(+(x358,x359),+(y,z)) -> +(+(+(x358,x359),y),z) +(x358,+(x359,+(y,z))) -> +(+(x358,x359),+(y,z)) +(+(+(x358,x359),y),z) -> +(+(x358,x359),+(y,z)) +(x,+(+(x361,x362),z)) -> +(x,+(x361,+(x362,z))) +(x,+(+(x361,x362),z)) -> +(+(x,+(x361,x362)),z) +(x,+(x361,+(x362,z))) -> +(x,+(+(x361,x362),z)) +(+(x,+(x361,x362)),z) -> +(x,+(+(x361,x362),z)) +(+(+(x364,x365),y),z) -> +(+(x364,+(x365,y)),z) +(+(+(x364,x365),y),z) -> +(+(x364,x365),+(y,z)) +(+(x364,+(x365,y)),z) -> +(+(+(x364,x365),y),z) +(+(x364,x365),+(y,z)) -> +(+(+(x364,x365),y),z) +(+(x367,x368),y) -> +(x367,+(x368,y)) +(+(x367,x368),y) -> +(y,+(x367,x368)) +(x367,+(x368,y)) -> +(+(x367,x368),y) +(y,+(x367,x368)) -> +(+(x367,x368),y) +(+(x370,x371),s(y)) -> +(x370,+(x371,s(y))) +(+(x370,x371),s(y)) -> +(s(+(x370,x371)),y) +(x370,+(x371,s(y))) -> +(+(x370,x371),s(y)) +(s(+(x370,x371)),y) -> +(+(x370,x371),s(y)) +(x,+(y,z)) -> +(+(y,z),x) +(x,+(y,z)) -> +(+(x,y),z) +(+(y,z),x) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(x,+(z,y)) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(z,y)) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(+(x,y),z) -> +(z,+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) +(z,+(x,y)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(+(y,x),z) +(+(x,y),z) -> +(x,+(y,z)) +(+(y,x),z) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> +(x,s(y)) +(y,s(x)) -> +(s(x),y) +(x,s(y)) -> +(s(x),y) +(y,s(x)) -> +(s(y),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> +(s(x),y) +(s(y),x) -> +(x,s(y)) +(s(x),y) -> +(x,s(y)) +(s(y),x) -> +(y,s(x)) +(s(x),y) -> +(y,s(x)) +(s(x385),+(y,z)) -> +(x385,s(+(y,z))) +(s(x385),+(y,z)) -> +(+(s(x385),y),z) +(x385,s(+(y,z))) -> +(s(x385),+(y,z)) +(+(s(x385),y),z) -> +(s(x385),+(y,z)) +(x,+(s(x387),z)) -> +(x,+(x387,s(z))) +(x,+(s(x387),z)) -> +(+(x,s(x387)),z) +(x,+(x387,s(z))) -> +(x,+(s(x387),z)) +(+(x,s(x387)),z) -> +(x,+(s(x387),z)) +(+(s(x389),y),z) -> +(+(x389,s(y)),z) +(+(s(x389),y),z) -> +(s(x389),+(y,z)) +(+(x389,s(y)),z) -> +(+(s(x389),y),z) +(s(x389),+(y,z)) -> +(+(s(x389),y),z) +(s(x391),y) -> +(x391,s(y)) +(s(x391),y) -> +(y,s(x391)) +(x391,s(y)) -> +(s(y),x391) +(y,s(x391)) -> +(s(y),x391) +(x391,s(y)) -> +(s(x391),y) +(y,s(x391)) -> +(s(x391),y) +(s(x393),s(y)) -> +(x393,s(s(y))) +(s(x393),s(y)) -> +(s(s(x393)),y) +(x393,s(s(y))) -> +(s(x393),s(y)) +(s(s(x393)),y) -> +(s(x393),s(y)) +(x,+(y,s(x396))) -> +(x,+(s(y),x396)) +(x,+(y,s(x396))) -> +(+(x,y),s(x396)) +(x,+(s(y),x396)) -> +(x,+(y,s(x396))) +(+(x,y),s(x396)) -> +(x,+(y,s(x396))) +(+(x,y),s(x398)) -> +(s(+(x,y)),x398) +(+(x,y),s(x398)) -> +(x,+(y,s(x398))) +(s(+(x,y)),x398) -> +(+(x,y),s(x398)) +(x,+(y,s(x398))) -> +(+(x,y),s(x398)) +(+(x,s(x400)),z) -> +(+(s(x),x400),z) +(+(x,s(x400)),z) -> +(x,+(s(x400),z)) +(+(s(x),x400),z) -> +(+(x,s(x400)),z) +(x,+(s(x400),z)) -> +(+(x,s(x400)),z) +(x,s(x402)) -> +(s(x),x402) +(x,s(x402)) -> +(s(x402),x) +(s(x),x402) -> +(x402,s(x)) +(s(x402),x) -> +(x402,s(x)) +(s(x),x402) -> +(x,s(x402)) +(s(x402),x) -> +(x,s(x402)) +(s(x),s(x404)) -> +(s(s(x)),x404) +(s(x),s(x404)) -> +(x,s(s(x404))) +(s(s(x)),x404) -> +(s(x),s(x404)) +(x,s(s(x404))) -> +(s(x),s(x404)) *(s(x),s(x406)) -> +(s(x),*(s(x),x406)) *(s(x),s(x406)) -> +(*(x,s(x406)),s(x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(s(x),*(x,x406)),x406) +(+(s(x),*(x,x406)),x406) -> +(+(x,s(*(x,x406))),x406) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(x,+(*(x,x406),s(x406))) +(x,+(*(x,x406),s(x406))) -> +(x,+(s(*(x,x406)),x406)) +(x,+(s(*(x,x406)),x406)) -> +(+(x,s(*(x,x406))),x406) +(s(x),*(s(x),x406)) -> +(*(s(x),x406),s(x)) +(*(s(x),x406),s(x)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x),x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(+(*(x,x406),x),s(x406)) +(+(*(x,x406),x),s(x406)) -> +(*(x,x406),+(x,s(x406))) +(*(x,x406),+(x,s(x406))) -> +(*(x,x406),+(s(x),x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x),x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(+(*(x,x406),x),s(x406)) +(+(*(x,x406),x),s(x406)) -> +(*(x,x406),+(x,s(x406))) +(*(x,x406),+(x,s(x406))) -> +(*(x,x406),+(s(x),x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(s(x),*(x,x406)),x406) +(+(s(x),*(x,x406)),x406) -> +(+(*(x,x406),s(x)),x406) +(+(*(x,x406),s(x)),x406) -> +(*(x,x406),+(s(x),x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(+(*(x,x406),x),s(x406)) +(+(*(x,x406),x),s(x406)) -> +(*(x,x406),+(x,s(x406))) +(*(x,x406),+(x,s(x406))) -> +(*(x,x406),+(s(x),x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(s(x),+(x406,*(x,x406))) +(s(x),+(x406,*(x,x406))) -> +(+(s(x),x406),*(x,x406)) +(+(s(x),x406),*(x,x406)) -> +(*(x,x406),+(s(x),x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(+(*(x,x406),x),s(x406)) +(+(*(x,x406),x),s(x406)) -> +(*(x,x406),+(x,s(x406))) +(*(x,x406),+(x,s(x406))) -> +(*(x,x406),+(s(x),x406)) +(s(x),*(s(x),x406)) -> +(*(s(x),x406),s(x)) +(*(s(x),x406),s(x)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(s(x406),*(x,s(x406))) +(s(x406),*(x,s(x406))) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(*(s(x),x406),s(x)) +(*(s(x),x406),s(x)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(s(x406),*(x,s(x406))) +(s(x406),*(x,s(x406))) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(s(x),*(x,x406)),x406) +(+(s(x),*(x,x406)),x406) -> +(x406,+(s(x),*(x,x406))) +(x406,+(s(x),*(x,x406))) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(s(x406),*(x,s(x406))) +(s(x406),*(x,s(x406))) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(s(x),*(x,x406)),x406) +(+(s(x),*(x,x406)),x406) -> +(x406,+(s(x),*(x,x406))) +(x406,+(s(x),*(x,x406))) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(s(x),+(x406,*(x,x406))) +(s(x),+(x406,*(x,x406))) -> +(+(s(x),x406),*(x,x406)) +(+(s(x),x406),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(s(x406),*(x,s(x406))) +(s(x406),*(x,s(x406))) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(s(x),+(x406,*(x,x406))) +(s(x),+(x406,*(x,x406))) -> +(+(s(x),x406),*(x,x406)) +(+(s(x),x406),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x406,s(x)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(*(s(x),x406),s(x)) +(*(s(x),x406),s(x)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(s(x406),*(x,s(x406))) +(s(x406),*(x,s(x406))) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(*(s(x),x406),s(x)) +(*(s(x),x406),s(x)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(*(s(x),x406),s(x)) +(*(s(x),x406),s(x)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(x,+(*(x,x406),s(x406))) +(x,+(*(x,x406),s(x406))) -> +(+(*(x,x406),s(x406)),x) +(+(*(x,x406),s(x406)),x) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(*(s(x),x406),s(x)) +(*(s(x),x406),s(x)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(+(*(x,x406),x),s(x406)) +(+(*(x,x406),x),s(x406)) -> +(*(x,x406),+(x,s(x406))) +(*(x,x406),+(x,s(x406))) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(s(x406),*(x,s(x406))) +(s(x406),*(x,s(x406))) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(x,+(*(x,x406),s(x406))) +(x,+(*(x,x406),s(x406))) -> +(+(*(x,x406),s(x406)),x) +(+(*(x,x406),s(x406)),x) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(*(x,x406),x406),s(x)) +(+(*(x,x406),x406),s(x)) -> +(*(x,x406),+(x406,s(x))) +(*(x,x406),+(x406,s(x))) -> +(*(x,x406),+(s(x406),x)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(+(*(x,x406),x),s(x406)) +(+(*(x,x406),x),s(x406)) -> +(*(x,x406),+(x,s(x406))) +(*(x,x406),+(x,s(x406))) -> +(*(x,x406),+(s(x406),x)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(+(s(x),*(x,x406)),x406) +(+(s(x),*(x,x406)),x406) -> +(+(x,s(*(x,x406))),x406) +(+(x,s(*(x,x406))),x406) -> +(x,+(s(*(x,x406)),x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(x,+(*(x,x406),s(x406))) +(x,+(*(x,x406),s(x406))) -> +(x,+(s(*(x,x406)),x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(s(x),+(x406,*(x,x406))) +(s(x),+(x406,*(x,x406))) -> +(+(s(x),x406),*(x,x406)) +(+(s(x),x406),*(x,x406)) -> +(+(x,s(x406)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(s(x406),*(x,s(x406))) +(s(x406),*(x,s(x406))) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x,s(x406)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(s(x),+(x406,*(x,x406))) +(s(x),+(x406,*(x,x406))) -> +(+(s(x),x406),*(x,x406)) +(+(s(x),x406),*(x,x406)) -> +(+(x,s(x406)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(s(x406),+(x,*(x,x406))) +(s(x406),+(x,*(x,x406))) -> +(+(s(x406),x),*(x,x406)) +(+(s(x406),x),*(x,x406)) -> +(+(x,s(x406)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(s(x),+(x406,*(x,x406))) +(s(x),+(x406,*(x,x406))) -> +(+(s(x),x406),*(x,x406)) +(+(s(x),x406),*(x,x406)) -> +(+(x,s(x406)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(x,+(*(x,x406),s(x406))) +(x,+(*(x,x406),s(x406))) -> +(x,+(s(x406),*(x,x406))) +(x,+(s(x406),*(x,x406))) -> +(+(x,s(x406)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),+(*(x,x406),x406)) +(s(x),+(*(x,x406),x406)) -> +(s(x),+(x406,*(x,x406))) +(s(x),+(x406,*(x,x406))) -> +(+(s(x),x406),*(x,x406)) +(+(s(x),x406),*(x,x406)) -> +(+(x,s(x406)),*(x,x406)) +(*(x,s(x406)),s(x406)) -> +(+(x,*(x,x406)),s(x406)) +(+(x,*(x,x406)),s(x406)) -> +(+(*(x,x406),x),s(x406)) +(+(*(x,x406),x),s(x406)) -> +(*(x,x406),+(x,s(x406))) +(*(x,x406),+(x,s(x406))) -> +(+(x,s(x406)),*(x,x406)) +(s(x),*(s(x),x406)) -> +(s(x),*(x406,s(x))) +(s(x),*(x406,s(x))) -> +(s(x),+(x406,*(x406,x))) +(s(x),+(x406,*(x406,x))) -> +(+(s(x),x406),*(x406,x)) +(+(s(x),x406),*(x406,x)) -> +(*(x406,x),+(s(x),x406)) +(*(x,s(x406)),s(x406)) -> +(*(s(x406),x),s(x406)) +(*(s(x406),x),s(x406)) -> +(+(*(x406,x),x),s(x406)) +(+(*(x406,x),x),s(x406)) -> +(*(x406,x),+(x,s(x406))) +(*(x406,x),+(x,s(x406))) -> +(*(x406,x),+(s(x),x406)) +(s(x),*(s(x),x406)) -> +(s(x),*(x406,s(x))) +(s(x),*(x406,s(x))) -> +(s(x),+(x406,*(x406,x))) +(s(x),+(x406,*(x406,x))) -> +(+(s(x),x406),*(x406,x)) +(+(s(x),x406),*(x406,x)) -> +(+(x,s(x406)),*(x406,x)) +(*(x,s(x406)),s(x406)) -> +(*(s(x406),x),s(x406)) +(*(s(x406),x),s(x406)) -> +(+(*(x406,x),x),s(x406)) +(+(*(x406,x),x),s(x406)) -> +(*(x406,x),+(x,s(x406))) +(*(x406,x),+(x,s(x406))) -> +(+(x,s(x406)),*(x406,x)) *(x,s(x408)) -> +(x,*(x,x408)) *(x,s(x408)) -> *(s(x408),x) *(s(x408),x) -> *(x,s(x408)) *(x,s(x408)) -> +(x,*(x,x408)) +(x,*(x,x408)) -> +(*(x,x408),x) *(s(x408),x) -> +(*(x408,x),x) +(*(x408,x),x) -> +(*(x,x408),x) +(x,*(x,x408)) -> +(x,*(x408,x)) *(s(x408),x) -> +(*(x408,x),x) +(*(x408,x),x) -> +(x,*(x408,x)) +(x,*(x,x408)) -> +(*(x,x408),x) +(*(x,x408),x) -> +(*(x408,x),x) *(s(x408),x) -> +(*(x408,x),x) +(x,*(x,x408)) -> +(x,*(x408,x)) +(x,*(x408,x)) -> +(*(x408,x),x) *(s(x408),x) -> +(*(x408,x),x) *(s(x409),s(y)) -> +(*(x409,s(y)),s(y)) *(s(x409),s(y)) -> +(s(x409),*(s(x409),y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(x409,+(*(x409,y),s(y))) +(x409,+(*(x409,y),s(y))) -> +(x409,+(s(*(x409,y)),y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(s(x409),*(x409,y)),y) +(+(s(x409),*(x409,y)),y) -> +(+(x409,s(*(x409,y))),y) +(+(x409,s(*(x409,y))),y) -> +(x409,+(s(*(x409,y)),y)) +(*(x409,s(y)),s(y)) -> +(s(y),*(x409,s(y))) +(s(y),*(x409,s(y))) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(x409,s(y)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(s(x409),+(y,*(x409,y))) +(s(x409),+(y,*(x409,y))) -> +(+(s(x409),y),*(x409,y)) +(+(s(x409),y),*(x409,y)) -> +(+(x409,s(y)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(x409,s(y)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(s(x409),+(y,*(x409,y))) +(s(x409),+(y,*(x409,y))) -> +(+(s(x409),y),*(x409,y)) +(+(s(x409),y),*(x409,y)) -> +(+(x409,s(y)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(x409,+(*(x409,y),s(y))) +(x409,+(*(x409,y),s(y))) -> +(x409,+(s(y),*(x409,y))) +(x409,+(s(y),*(x409,y))) -> +(+(x409,s(y)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(s(x409),+(y,*(x409,y))) +(s(x409),+(y,*(x409,y))) -> +(+(s(x409),y),*(x409,y)) +(+(s(x409),y),*(x409,y)) -> +(+(x409,s(y)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(+(*(x409,y),x409),s(y)) +(+(*(x409,y),x409),s(y)) -> +(*(x409,y),+(x409,s(y))) +(*(x409,y),+(x409,s(y))) -> +(+(x409,s(y)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(s(x409),+(y,*(x409,y))) +(s(x409),+(y,*(x409,y))) -> +(+(s(x409),y),*(x409,y)) +(+(s(x409),y),*(x409,y)) -> +(+(x409,s(y)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(s(y),*(x409,s(y))) +(s(y),*(x409,s(y))) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(*(s(x409),y),s(x409)) +(*(s(x409),y),s(x409)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(s(y),*(x409,s(y))) +(s(y),*(x409,s(y))) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(*(s(x409),y),s(x409)) +(*(s(x409),y),s(x409)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(x409,+(*(x409,y),s(y))) +(x409,+(*(x409,y),s(y))) -> +(+(*(x409,y),s(y)),x409) +(+(*(x409,y),s(y)),x409) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(*(s(x409),y),s(x409)) +(*(s(x409),y),s(x409)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(x409,+(*(x409,y),s(y))) +(x409,+(*(x409,y),s(y))) -> +(+(*(x409,y),s(y)),x409) +(+(*(x409,y),s(y)),x409) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(+(*(x409,y),x409),s(y)) +(+(*(x409,y),x409),s(y)) -> +(*(x409,y),+(x409,s(y))) +(*(x409,y),+(x409,s(y))) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(*(s(x409),y),s(x409)) +(*(s(x409),y),s(x409)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(+(*(x409,y),x409),s(y)) +(+(*(x409,y),x409),s(y)) -> +(*(x409,y),+(x409,s(y))) +(*(x409,y),+(x409,s(y))) -> +(*(x409,y),+(s(y),x409)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(y),x409)) +(*(x409,s(y)),s(y)) -> +(s(y),*(x409,s(y))) +(s(y),*(x409,s(y))) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(*(s(x409),y),s(x409)) +(*(s(x409),y),s(x409)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(s(y),*(x409,s(y))) +(s(y),*(x409,s(y))) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(s(y),*(x409,s(y))) +(s(y),*(x409,s(y))) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(s(x409),*(x409,y)),y) +(+(s(x409),*(x409,y)),y) -> +(y,+(s(x409),*(x409,y))) +(y,+(s(x409),*(x409,y))) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(s(y),*(x409,s(y))) +(s(y),*(x409,s(y))) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(s(x409),+(y,*(x409,y))) +(s(x409),+(y,*(x409,y))) -> +(+(s(x409),y),*(x409,y)) +(+(s(x409),y),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(*(s(x409),y),s(x409)) +(*(s(x409),y),s(x409)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(s(x409),*(x409,y)),y) +(+(s(x409),*(x409,y)),y) -> +(y,+(s(x409),*(x409,y))) +(y,+(s(x409),*(x409,y))) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(s(y),+(x409,*(x409,y))) +(s(y),+(x409,*(x409,y))) -> +(+(s(y),x409),*(x409,y)) +(+(s(y),x409),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(s(x409),+(y,*(x409,y))) +(s(x409),+(y,*(x409,y))) -> +(+(s(x409),y),*(x409,y)) +(+(s(x409),y),*(x409,y)) -> +(+(y,s(x409)),*(x409,y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(x409,+(*(x409,y),s(y))) +(x409,+(*(x409,y),s(y))) -> +(x409,+(s(*(x409,y)),y)) +(x409,+(s(*(x409,y)),y)) -> +(+(x409,s(*(x409,y))),y) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(s(x409),*(x409,y)),y) +(+(s(x409),*(x409,y)),y) -> +(+(x409,s(*(x409,y))),y) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(+(*(x409,y),x409),s(y)) +(+(*(x409,y),x409),s(y)) -> +(*(x409,y),+(x409,s(y))) +(*(x409,y),+(x409,s(y))) -> +(*(x409,y),+(s(x409),y)) +(s(x409),*(s(x409),y)) -> +(*(s(x409),y),s(x409)) +(*(s(x409),y),s(x409)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(x409),y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(+(*(x409,y),x409),s(y)) +(+(*(x409,y),x409),s(y)) -> +(*(x409,y),+(x409,s(y))) +(*(x409,y),+(x409,s(y))) -> +(*(x409,y),+(s(x409),y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(*(x409,y),y),s(x409)) +(+(*(x409,y),y),s(x409)) -> +(*(x409,y),+(y,s(x409))) +(*(x409,y),+(y,s(x409))) -> +(*(x409,y),+(s(x409),y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(+(*(x409,y),x409),s(y)) +(+(*(x409,y),x409),s(y)) -> +(*(x409,y),+(x409,s(y))) +(*(x409,y),+(x409,s(y))) -> +(*(x409,y),+(s(x409),y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(+(s(x409),*(x409,y)),y) +(+(s(x409),*(x409,y)),y) -> +(+(*(x409,y),s(x409)),y) +(+(*(x409,y),s(x409)),y) -> +(*(x409,y),+(s(x409),y)) +(*(x409,s(y)),s(y)) -> +(+(x409,*(x409,y)),s(y)) +(+(x409,*(x409,y)),s(y)) -> +(+(*(x409,y),x409),s(y)) +(+(*(x409,y),x409),s(y)) -> +(*(x409,y),+(x409,s(y))) +(*(x409,y),+(x409,s(y))) -> +(*(x409,y),+(s(x409),y)) +(s(x409),*(s(x409),y)) -> +(s(x409),+(*(x409,y),y)) +(s(x409),+(*(x409,y),y)) -> +(s(x409),+(y,*(x409,y))) +(s(x409),+(y,*(x409,y))) -> +(+(s(x409),y),*(x409,y)) +(+(s(x409),y),*(x409,y)) -> +(*(x409,y),+(s(x409),y)) +(*(x409,s(y)),s(y)) -> +(*(s(y),x409),s(y)) +(*(s(y),x409),s(y)) -> +(+(*(y,x409),x409),s(y)) +(+(*(y,x409),x409),s(y)) -> +(*(y,x409),+(x409,s(y))) +(*(y,x409),+(x409,s(y))) -> +(+(x409,s(y)),*(y,x409)) +(s(x409),*(s(x409),y)) -> +(s(x409),*(y,s(x409))) +(s(x409),*(y,s(x409))) -> +(s(x409),+(y,*(y,x409))) +(s(x409),+(y,*(y,x409))) -> +(+(s(x409),y),*(y,x409)) +(+(s(x409),y),*(y,x409)) -> +(+(x409,s(y)),*(y,x409)) +(*(x409,s(y)),s(y)) -> +(*(s(y),x409),s(y)) +(*(s(y),x409),s(y)) -> +(+(*(y,x409),x409),s(y)) +(+(*(y,x409),x409),s(y)) -> +(*(y,x409),+(x409,s(y))) +(*(y,x409),+(x409,s(y))) -> +(*(y,x409),+(s(x409),y)) +(s(x409),*(s(x409),y)) -> +(s(x409),*(y,s(x409))) +(s(x409),*(y,s(x409))) -> +(s(x409),+(y,*(y,x409))) +(s(x409),+(y,*(y,x409))) -> +(+(s(x409),y),*(y,x409)) +(+(s(x409),y),*(y,x409)) -> +(*(y,x409),+(s(x409),y)) *(s(x411),y) -> +(*(x411,y),y) *(s(x411),y) -> *(y,s(x411)) *(y,s(x411)) -> *(s(x411),y) *(s(x411),y) -> +(*(x411,y),y) +(*(x411,y),y) -> +(y,*(x411,y)) *(y,s(x411)) -> +(y,*(y,x411)) +(y,*(y,x411)) -> +(y,*(x411,y)) +(*(x411,y),y) -> +(*(y,x411),y) *(y,s(x411)) -> +(y,*(y,x411)) +(y,*(y,x411)) -> +(*(y,x411),y) +(*(x411,y),y) -> +(y,*(x411,y)) +(y,*(x411,y)) -> +(y,*(y,x411)) *(y,s(x411)) -> +(y,*(y,x411)) +(*(x411,y),y) -> +(*(y,x411),y) +(*(y,x411),y) -> +(y,*(y,x411)) *(y,s(x411)) -> +(y,*(y,x411)) *(x,s(y)) -> *(s(y),x) *(x,s(y)) -> +(x,*(x,y)) *(s(y),x) -> +(*(y,x),x) +(x,*(x,y)) -> +(*(x,y),x) +(*(x,y),x) -> +(*(y,x),x) *(s(y),x) -> +(*(y,x),x) +(x,*(x,y)) -> +(x,*(y,x)) +(x,*(y,x)) -> +(*(y,x),x) *(s(y),x) -> +(*(y,x),x) +(*(y,x),x) -> +(x,*(y,x)) +(x,*(x,y)) -> +(x,*(y,x)) *(s(y),x) -> +(*(y,x),x) +(*(y,x),x) -> +(*(x,y),x) +(x,*(x,y)) -> +(*(x,y),x) *(s(y),x) -> *(x,s(y)) *(x,s(y)) -> +(x,*(x,y)) *(s(x),y) -> *(y,s(x)) *(s(x),y) -> +(*(x,y),y) *(y,s(x)) -> +(y,*(y,x)) +(*(x,y),y) -> +(y,*(x,y)) +(y,*(x,y)) -> +(y,*(y,x)) *(y,s(x)) -> +(y,*(y,x)) +(*(x,y),y) -> +(*(y,x),y) +(*(y,x),y) -> +(y,*(y,x)) *(y,s(x)) -> +(y,*(y,x)) +(y,*(y,x)) -> +(*(y,x),y) +(*(x,y),y) -> +(*(y,x),y) *(y,s(x)) -> +(y,*(y,x)) +(y,*(y,x)) -> +(y,*(x,y)) +(*(x,y),y) -> +(y,*(x,y)) *(y,s(x)) -> *(s(x),y) *(s(x),y) -> +(*(x,y),y) sq(s(x)) -> *(s(x),s(x)) sq(s(x)) -> +(*(x,x),s(+(x,x))) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) +(+(x,s(*(x,x))),x) -> +(+(s(x),*(x,x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(+(s(x),*(x,x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) +(+(x,s(*(x,x))),x) -> +(+(s(x),*(x,x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(+(s(x),*(x,x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(s(x),*(x,x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) +(+(x,s(*(x,x))),x) -> +(+(s(x),*(x,x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(s(x),*(x,x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(+(s(x),*(x,x)),x) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) +(x,+(s(*(x,x)),x)) -> +(x,+(*(x,x),s(x))) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(x,+(*(x,x),s(x))) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) +(x,+(s(*(x,x)),x)) -> +(x,+(*(x,x),s(x))) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(x,+(*(x,x),s(x))) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(*(x,x),s(x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) +(x,+(s(*(x,x)),x)) -> +(x,+(*(x,x),s(x))) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(*(x,x),s(x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(x,+(*(x,x),s(x))) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(+(*(x,x),s(x)),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(*(x,x),s(x)),x) +(+(*(x,x),s(x)),x) -> +(+(*(x,x),s(x)),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(x,+(s(x),*(x,x))) +(*(x,x),s(+(x,x))) -> +(s(+(x,x)),*(x,x)) +(s(+(x,x)),*(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(x,+(s(x),*(x,x))) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(x,+(s(x),*(x,x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(x,+(s(x),*(x,x))) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(x),*(x,x))) +(*(x,x),s(+(x,x))) -> +(s(+(x,x)),*(x,x)) +(s(+(x,x)),*(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(x,+(s(x),*(x,x))) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(x),*(x,x))) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(x,+(s(x),*(x,x))) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(x,s(*(x,x))),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(x,s(*(x,x))),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(x,s(*(x,x))),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(x,s(*(x,x))),x) +(*(x,x),s(+(x,x))) -> +(s(+(x,x)),*(x,x)) +(s(+(x,x)),*(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(+(x,s(*(x,x))),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(x,s(*(x,x))),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(+(x,s(*(x,x))),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(x,s(*(x,x))),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) +(+(x,s(*(x,x))),x) -> +(+(x,s(*(x,x))),x) *(s(x),s(x)) -> +(s(x),*(s(x),x)) +(s(x),*(s(x),x)) -> +(s(x),+(*(x,x),x)) +(s(x),+(*(x,x),x)) -> +(+(s(x),*(x,x)),x) +(+(s(x),*(x,x)),x) -> +(+(x,s(*(x,x))),x) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) +(x,+(s(*(x,x)),x)) -> +(+(x,s(*(x,x))),x) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(*(x,x)),x)) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(*(x,x)),x)) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(*(x,x)),x)) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(*(x,x)),x)) +(*(x,x),s(+(x,x))) -> +(s(+(x,x)),*(x,x)) +(s(+(x,x)),*(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(x,+(s(*(x,x)),x)) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(*(x,x)),x)) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(x,x),s(*(x,x))) +(+(x,x),s(*(x,x))) -> +(x,+(x,s(*(x,x)))) +(x,+(x,s(*(x,x)))) -> +(x,+(s(*(x,x)),x)) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(*(x,x)),x)) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(+(x,s(*(x,x))),x) +(+(x,s(*(x,x))),x) -> +(x,+(s(*(x,x)),x)) *(s(x),s(x)) -> +(*(x,s(x)),s(x)) +(*(x,s(x)),s(x)) -> +(+(x,*(x,x)),s(x)) +(+(x,*(x,x)),s(x)) -> +(x,+(*(x,x),s(x))) +(x,+(*(x,x),s(x))) -> +(x,+(s(*(x,x)),x)) +(*(x,x),s(+(x,x))) -> +(s(*(x,x)),+(x,x)) +(s(*(x,x)),+(x,x)) -> +(+(s(*(x,x)),x),x) +(+(s(*(x,x)),x),x) -> +(x,+(s(*(x,x)),x)) +(x,+(s(*(x,x)),x)) -> +(x,+(s(*(x,x)),x)) sq(s(x418)) -> +(*(x418,x418),s(+(x418,x418))) sq(s(x418)) -> *(s(x418),s(x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(x418,s(*(x418,x418))),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(x418,s(*(x418,x418))),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(x418,s(*(x418,x418))),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(+(x418,x418)),*(x418,x418)) +(s(+(x418,x418)),*(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(x418,s(*(x418,x418))),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(x418,s(*(x418,x418))),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) +(+(x418,s(*(x418,x418))),x418) -> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(x418,s(*(x418,x418))),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) +(x418,+(s(*(x418,x418)),x418)) -> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(x418,s(*(x418,x418))),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(*(x418,x418)),x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(*(x418,x418)),x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(*(x418,x418)),x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(+(x418,x418)),*(x418,x418)) +(s(+(x418,x418)),*(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(x418,+(s(*(x418,x418)),x418)) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(*(x418,x418)),x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(x418,+(s(*(x418,x418)),x418)) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(*(x418,x418)),x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) +(+(x418,s(*(x418,x418))),x418) -> +(x418,+(s(*(x418,x418)),x418)) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(*(x418,x418)),x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) +(x418,+(s(*(x418,x418)),x418)) -> +(x418,+(s(*(x418,x418)),x418)) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(*(x418,x418)),x418)) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(+(*(x418,x418),s(x418)),x418) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(+(*(x418,x418),s(x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(+(x418,x418)),*(x418,x418)) +(s(+(x418,x418)),*(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(x418,+(s(x418),*(x418,x418))) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(x418,+(s(x418),*(x418,x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(+(x418,x418)),*(x418,x418)) +(s(+(x418,x418)),*(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(x418,+(s(x418),*(x418,x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(x418),*(x418,x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(x418,+(s(x418),*(x418,x418))) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(x418,+(s(x418),*(x418,x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(x418,x418),s(*(x418,x418))) +(+(x418,x418),s(*(x418,x418))) -> +(x418,+(x418,s(*(x418,x418)))) +(x418,+(x418,s(*(x418,x418)))) -> +(x418,+(s(x418),*(x418,x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(s(x418),*(x418,x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) +(+(x418,s(*(x418,x418))),x418) -> +(+(s(x418),*(x418,x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) +(+(x418,s(*(x418,x418))),x418) -> +(+(s(x418),*(x418,x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(x418,s(*(x418,x418))),x418) +(+(x418,s(*(x418,x418))),x418) -> +(+(s(x418),*(x418,x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(s(x418),*(x418,x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(+(s(x418),*(x418,x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(+(s(x418),*(x418,x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(+(s(x418),*(x418,x418)),x418) *(s(x418),s(x418)) -> +(s(x418),*(s(x418),x418)) +(s(x418),*(s(x418),x418)) -> +(s(x418),+(*(x418,x418),x418)) +(s(x418),+(*(x418,x418),x418)) -> +(+(s(x418),*(x418,x418)),x418) +(+(s(x418),*(x418,x418)),x418) -> +(+(s(x418),*(x418,x418)),x418) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) +(x418,+(s(*(x418,x418)),x418)) -> +(x418,+(*(x418,x418),s(x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) +(x418,+(s(*(x418,x418)),x418)) -> +(x418,+(*(x418,x418),s(x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(x418,+(s(*(x418,x418)),x418)) +(x418,+(s(*(x418,x418)),x418)) -> +(x418,+(*(x418,x418),s(x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(*(x418,x418),s(x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(x418,+(*(x418,x418),s(x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(x418,+(*(x418,x418),s(x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(*(x418,x418),s(+(x418,x418))) -> +(s(*(x418,x418)),+(x418,x418)) +(s(*(x418,x418)),+(x418,x418)) -> +(+(s(*(x418,x418)),x418),x418) +(+(s(*(x418,x418)),x418),x418) -> +(+(*(x418,x418),s(x418)),x418) +(+(*(x418,x418),s(x418)),x418) -> +(x418,+(*(x418,x418),s(x418))) *(s(x418),s(x418)) -> +(*(x418,s(x418)),s(x418)) +(*(x418,s(x418)),s(x418)) -> +(+(x418,*(x418,x418)),s(x418)) +(+(x418,*(x418,x418)),s(x418)) -> +(x418,+(*(x418,x418),s(x418))) +(x418,+(*(x418,x418),s(x418))) -> +(x418,+(*(x418,x418),s(x418))) weak: +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) +(s(x),y) -> +(x,s(y)) +(x,s(y)) -> +(s(x),y) *(x,s(y)) -> +(x,*(x,y)) *(s(x),y) -> +(*(x,y),y) *(x,y) -> *(y,x) sq(x) -> *(x,x) sq(s(x)) -> +(*(x,x),s(+(x,x))) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): +(x,+(y,z)) -> +(+(x,y),z): 0 +(+(x,y),z) -> +(x,+(y,z)): 0 +(x,y) -> +(y,x): 0 +(s(x),y) -> +(x,s(y)): 0 +(x,s(y)) -> +(s(x),y): 0 *(x,s(y)) -> +(x,*(x,y)): 1 *(s(x),y) -> +(*(x,y),y): 1 *(x,y) -> *(y,x): 8 sq(x) -> *(x,x): 11 sq(s(x)) -> +(*(x,x),s(+(x,x))): 10 Decreasing Processor: The following diagrams are decreasing: peak: +(x,+(+(y,x344),x345)) <-0|1[1,0,0,0,0]- +(x,+(y,+(x344,x345))) -0| [1,0,0,0,0]-> +(+(x,y),+(x344,x345)) joins: +(x,+(+(y,x344),x345)) -1|1[1,0,0,0,0]-> +(x,+(y,+(x344,x345))) +(+(x,y),+(x344,x345)) -1|[1,0,0,0,0]-> +(x,+(y,+(x344,x345))) peak: +(+(+(x,y),x347),x348) <-0|[1,0,0,0,0]- +(+(x,y),+(x347,x348)) -1| [1,0,0,0,0]-> +(x,+(y,+(x347,x348))) joins: +(+(+(x,y),x347),x348) -1|[1,0,0,0,0]-> +(+(x,y),+(x347,x348)) +(x,+(y,+(x347,x348))) -0|[1,0,0,0,0]-> +(+(x,y),+(x347,x348)) peak: +(+(+(x,x350),x351),z) <-0|0[1,0,0,0,0]- +(+(x,+(x350,x351)),z) -1| [1,0,0,0,0]-> +(x,+(+(x350,x351),z)) joins: +(+(+(x,x350),x351),z) -1|0[1,0,0,0,0]-> +(+(x,+(x350,x351)),z) +(x,+(+(x350,x351),z)) -0|[1,0,0,0,0]-> +(+(x,+(x350,x351)),z) peak: +(+(x,x353),x354) <-0|[1,0,0,0,0]- +(x,+(x353,x354)) -2|[1,0,0,0,0]-> +(+(x353,x354),x) joins: +(+(x,x353),x354) -1|[1,0,0,0,0]-> +(x,+(x353,x354)) +(+(x353,x354),x) -2|[1,0,0,0,0]-> +(x,+(x353,x354)) peak: +(+(s(x),x356),x357) <-0|[1,0,0,0,0]- +(s(x),+(x356,x357)) -3| [1,0,0,0,0]-> +(x,s(+(x356,x357))) joins: +(+(s(x),x356),x357) -1|[1,0,0,0,0]-> +(s(x),+(x356,x357)) +(x,s(+(x356,x357))) -4|[1,0,0,0,0]-> +(s(x),+(x356,x357)) peak: +(x358,+(x359,+(y,z))) <-1|[1,0,0,0,0]- +(+(x358,x359),+(y,z)) -0| [1,0,0,0,0]-> +(+(+(x358,x359),y),z) joins: +(x358,+(x359,+(y,z))) -0|[1,0,0,0,0]-> +(+(x358,x359),+(y,z)) +(+(+(x358,x359),y),z) -1|[1,0,0,0,0]-> +(+(x358,x359),+(y,z)) peak: +(x,+(x361,+(x362,z))) <-1|1[1,0,0,0,0]- +(x,+(+(x361,x362),z)) -0| [1,0,0,0,0]-> +(+(x,+(x361,x362)),z) joins: +(x,+(x361,+(x362,z))) -0|1[1,0,0,0,0]-> +(x,+(+(x361,x362),z)) +(+(x,+(x361,x362)),z) -1|[1,0,0,0,0]-> +(x,+(+(x361,x362),z)) peak: +(+(x364,+(x365,y)),z) <-1|0[1,0,0,0,0]- +(+(+(x364,x365),y),z) -1| [1,0,0,0,0]-> +(+(x364,x365),+(y,z)) joins: +(+(x364,+(x365,y)),z) -0|0[1,0,0,0,0]-> +(+(+(x364,x365),y),z) +(+(x364,x365),+(y,z)) -0|[1,0,0,0,0]-> +(+(+(x364,x365),y),z) peak: +(x367,+(x368,y)) <-1|[1,0,0,0,0]- +(+(x367,x368),y) -2|[1,0,0,0,0]-> +(y,+(x367,x368)) joins: +(x367,+(x368,y)) -0|[1,0,0,0,0]-> +(+(x367,x368),y) +(y,+(x367,x368)) -2|[1,0,0,0,0]-> +(+(x367,x368),y) peak: +(x370,+(x371,s(y))) <-1|[1,0,0,0,0]- +(+(x370,x371),s(y)) -4| [1,0,0,0,0]-> +(s(+(x370,x371)),y) joins: +(x370,+(x371,s(y))) -0|[1,0,0,0,0]-> +(+(x370,x371),s(y)) +(s(+(x370,x371)),y) -3|[1,0,0,0,0]-> +(+(x370,x371),s(y)) peak: +(+(y,z),x) <-2|[1,0,0,0,0]- +(x,+(y,z)) -0|[1,0,0,0,0]-> +(+(x,y),z) joins: +(+(y,z),x) -2|[1,0,0,0,0]-> +(x,+(y,z)) +(+(x,y),z) -1|[1,0,0,0,0]-> +(x,+(y,z)) peak: +(x,+(z,y)) <-2|1[1,0,0,0,0]- +(x,+(y,z)) -0|[1,0,0,0,0]-> +(+(x,y),z) joins: +(x,+(z,y)) -2|1[1,0,0,0,0]-> +(x,+(y,z)) +(+(x,y),z) -1|[1,0,0,0,0]-> +(x,+(y,z)) peak: +(z,+(x,y)) <-2|[1,0,0,0,0]- +(+(x,y),z) -1|[1,0,0,0,0]-> +(x,+(y,z)) joins: +(z,+(x,y)) -2|[1,0,0,0,0]-> +(+(x,y),z) +(x,+(y,z)) -0|[1,0,0,0,0]-> +(+(x,y),z) peak: +(+(y,x),z) <-2|0[1,0,0,0,0]- +(+(x,y),z) -1|[1,0,0,0,0]-> +(x,+(y,z)) joins: +(+(y,x),z) -2|0[1,0,0,0,0]-> +(+(x,y),z) +(x,+(y,z)) -0|[1,0,0,0,0]-> +(+(x,y),z) peak: +(y,s(x)) <-2|[1,0,0,0,0]- +(s(x),y) -3|[1,0,0,0,0]-> +(x,s(y)) joins: +(y,s(x)) -2|[1,0,0,0,0]-> +(s(x),y) +(x,s(y)) -4|[1,0,0,0,0]-> +(s(x),y) peak: +(s(y),x) <-2|[1,0,0,0,0]- +(x,s(y)) -4|[1,0,0,0,0]-> +(s(x),y) joins: +(s(y),x) -2|[1,0,0,0,0]-> +(x,s(y)) +(s(x),y) -3|[1,0,0,0,0]-> +(x,s(y)) peak: +(x385,s(+(y,z))) <-3|[1,0,0,0,0]- +(s(x385),+(y,z)) -0|[1,0,0,0,0]-> +(+(s(x385),y),z) joins: +(x385,s(+(y,z))) -4|[1,0,0,0,0]-> +(s(x385),+(y,z)) +(+(s(x385),y),z) -1|[1,0,0,0,0]-> +(s(x385),+(y,z)) peak: +(x,+(x387,s(z))) <-3|1[1,0,0,0,0]- +(x,+(s(x387),z)) -0|[1,0,0,0,0]-> +(+(x,s(x387)),z) joins: +(x,+(x387,s(z))) -4|1[1,0,0,0,0]-> +(x,+(s(x387),z)) +(+(x,s(x387)),z) -1|[1,0,0,0,0]-> +(x,+(s(x387),z)) peak: +(+(x389,s(y)),z) <-3|0[1,0,0,0,0]- +(+(s(x389),y),z) -1|[1,0,0,0,0]-> +(s(x389),+(y,z)) joins: +(+(x389,s(y)),z) -4|0[1,0,0,0,0]-> +(+(s(x389),y),z) +(s(x389),+(y,z)) -0|[1,0,0,0,0]-> +(+(s(x389),y),z) peak: +(x391,s(y)) <-3|[1,0,0,0,0]- +(s(x391),y) -2|[1,0,0,0,0]-> +(y,s(x391)) joins: +(x391,s(y)) -2|[1,0,0,0,0]-> +(s(y),x391) +(y,s(x391)) -4|[1,0,0,0,0]-> +(s(y),x391) peak: +(x393,s(s(y))) <-3|[1,0,0,0,0]- +(s(x393),s(y)) -4|[1,0,0,0,0]-> +(s(s(x393)),y) joins: +(x393,s(s(y))) -4|[1,0,0,0,0]-> +(s(x393),s(y)) +(s(s(x393)),y) -3|[1,0,0,0,0]-> +(s(x393),s(y)) peak: +(x,+(s(y),x396)) <-4|1[1,0,0,0,0]- +(x,+(y,s(x396))) -0|[1,0,0,0,0]-> +(+(x,y),s(x396)) joins: +(x,+(s(y),x396)) -3|1[1,0,0,0,0]-> +(x,+(y,s(x396))) +(+(x,y),s(x396)) -1|[1,0,0,0,0]-> +(x,+(y,s(x396))) peak: +(s(+(x,y)),x398) <-4|[1,0,0,0,0]- +(+(x,y),s(x398)) -1|[1,0,0,0,0]-> +(x,+(y,s(x398))) joins: +(s(+(x,y)),x398) -3|[1,0,0,0,0]-> +(+(x,y),s(x398)) +(x,+(y,s(x398))) -0|[1,0,0,0,0]-> +(+(x,y),s(x398)) peak: +(+(s(x),x400),z) <-4|0[1,0,0,0,0]- +(+(x,s(x400)),z) -1|[1,0,0,0,0]-> +(x,+(s(x400),z)) joins: +(+(s(x),x400),z) -3|0[1,0,0,0,0]-> +(+(x,s(x400)),z) +(x,+(s(x400),z)) -0|[1,0,0,0,0]-> +(+(x,s(x400)),z) peak: +(s(x),x402) <-4|[1,0,0,0,0]- +(x,s(x402)) -2|[1,0,0,0,0]-> +(s(x402),x) joins: +(s(x),x402) -2|[1,0,0,0,0]-> +(x402,s(x)) +(s(x402),x) -3|[1,0,0,0,0]-> +(x402,s(x)) peak: +(s(s(x)),x404) <-4|[1,0,0,0,0]- +(s(x),s(x404)) -3|[1,0,0,0,0]-> +(x,s(s(x404))) joins: +(s(s(x)),x404) -3|[1,0,0,0,0]-> +(s(x),s(x404)) +(x,s(s(x404))) -4|[1,0,0,0,0]-> +(s(x),s(x404)) peak: +(s(x),*(s(x),x406)) <-5|[1,0,0,0,1]- *(s(x),s(x406)) -6|[ 1,0,0,0,1]-> +(*(x,s(x406)),s(x406)) joins: +(s(x),*(s(x),x406)) -6|1[1,0,0,0,1]-> +(s(x),+(*(x,x406),x406)) -0|[1,0,0,0,0]-> +(+(s(x),*(x,x406)),x406) -3|0[1,0,0,0,0]-> +(+(x,s(*(x,x406))),x406) +(*(x,s(x406)),s(x406)) -5|0[1,0,0,0,1]-> +(+(x,*(x,x406)),s(x406)) -1|[1,0,0,0,0]-> +(x,+(*(x,x406),s(x406))) -4|1[1,0,0,0,0]-> +(x,+(s(*(x,x406)),x406)) -0| [1,0,0,0,0]-> +(+(x,s(*(x,x406))),x406) peak: +(x,*(x,x408)) <-5|[1,0,0,0,1]- *(x,s(x408)) -7|[1,0,0,0,8]-> *(s(x408),x) joins: +(x,*(x,x408)) -7|1[1,0,0,0,8]-> +(x,*(x408,x)) *(s(x408),x) -6|[1,0,0,0,1]-> +(*(x408,x),x) -2|[1,0,0,0,0]-> +(x,*(x408,x)) peak: +(*(x409,s(y)),s(y)) <-6|[1,0,0,0,1]- *(s(x409),s(y)) -5|[ 1,0,0,0,1]-> +(s(x409),*(s(x409),y)) joins: +(*(x409,s(y)),s(y)) -5|0[1,0,0,0,1]-> +(+(x409,*(x409,y)),s(y)) -1|[1,0,0,0,0]-> +(x409,+(*(x409,y),s(y))) -4|1[1,0,0,0,0]-> +(x409,+(s(*(x409,y)),y)) +(s(x409),*(s(x409),y)) -6|1[1,0,0,0,1]-> +(s(x409),+(*(x409,y),y)) -0|[1,0,0,0,0]-> +(+(s(x409),*(x409,y)),y) -3|0[1,0,0,0,0]-> +(+(x409,s(*(x409,y))),y) -1| [1,0,0,0,0]-> +(x409,+(s(*(x409,y)),y)) peak: +(*(x411,y),y) <-6|[1,0,0,0,1]- *(s(x411),y) -7|[1,0,0,0,8]-> *(y,s(x411)) joins: +(*(x411,y),y) -7|0[1,0,0,0,8]-> +(*(y,x411),y) *(y,s(x411)) -5|[1,0,0,0,1]-> +(y,*(y,x411)) -2|[1,0,0,0,0]-> +(*(y,x411),y) peak: *(s(y),x) <-7|[1,0,0,0,8]- *(x,s(y)) -5|[1,0,0,0,1]-> +(x,*(x,y)) joins: *(s(y),x) -6|[1,0,0,0,1]-> +(*(y,x),x) +(x,*(x,y)) -2|[1,0,0,0,0]-> +(*(x,y),x) -7|0[1,0,0,0,8]-> +(*(y,x),x) peak: *(y,s(x)) <-7|[1,0,0,0,8]- *(s(x),y) -6|[1,0,0,0,1]-> +(*(x,y),y) joins: *(y,s(x)) -5|[1,0,0,0,1]-> +(y,*(y,x)) +(*(x,y),y) -2|[1,0,0,0,0]-> +(y,*(x,y)) -7|1[1,0,0,0,8]-> +(y,*(y,x)) peak: *(s(x),s(x)) <-8|[1,0,0,0,11]- sq(s(x)) -9|[1,0,0,0,10]-> +(*(x,x),s(+(x,x))) joins: *(s(x),s(x)) -5|[1,0,0,0,1]-> +(s(x),*(s(x),x)) -6|1[1,0,0,0,1]-> +(s(x),+(*(x,x),x)) -0|[1,0,0,0,0]-> +(+(s(x),*(x,x)),x) +(*(x,x),s(+(x,x))) -4|[1,0,0,0,0]-> +(s(*(x,x)),+(x,x)) -0|[1,0,0,0,0]-> +(+(s(*(x,x)),x),x) -2|0[1,0,0,0,0]-> +(+(x,s(*(x,x))),x) -4| 0[1,0,0,0,0]-> +(+(s(x),*(x,x)),x) peak: +(*(x418,x418),s(+(x418,x418))) <-9|[1,0,0,0,10]- sq(s(x418)) -8| [1,0,0,0,11]-> *(s(x418),s(x418)) joins: +(*(x418,x418),s(+(x418,x418))) -4|[1,0,0,0,0]-> +(s(*(x418,x418)),+(x418,x418)) -0| [1,0,0,0,0]-> +(+(s(*(x418,x418)),x418),x418) -2|0[1,0,0,0,0]-> +(+(x418,s(*(x418,x418))),x418) *(s(x418),s(x418)) -5|[1,0,0,0,1]-> +(s(x418),*(s(x418),x418)) -6|1[1,0,0,0,1]-> +(s(x418),+(*(x418,x418),x418)) -0|[1,0,0,0,0]-> +(+(s(x418),*(x418,x418)),x418) -3| 0[1,0,0,0,0]-> +(+(x418,s(*(x418,x418))),x418) Qed