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 (to relative problem): strict: +(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))) weak: original 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))) critical peaks: Polynomial Interpretation Processor: dimension: 1 interpretation: [s](x0) = x0 + 1, [sq](x0) = 3x0x0 + 2, [+](x0, x1) = x0 + x1, [*](x0, x1) = x0x0 + x1x0 + x1x1 orientation: +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z)) +(x,y) = x + y >= x + y = +(y,x) +(s(x),y) = x + y + 1 >= x + y + 1 = +(x,s(y)) +(x,s(y)) = x + y + 1 >= x + y + 1 = +(s(x),y) *(x,s(y)) = x + x*x + x*y + 2y + y*y + 1 >= x + x*x + x*y + y*y = +(x,*(x,y)) *(s(x),y) = 2x + x*x + x*y + y + y*y + 1 >= x*x + x*y + y + y*y = +(*(x,y),y) *(x,y) = x*x + x*y + y*y >= x*x + x*y + y*y = *(y,x) sq(x) = 3x*x + 2 >= 3x*x = *(x,x) sq(s(x)) = 6x + 3x*x + 5 >= 2x + 3x*x + 1 = +(*(x,x),s(+(x,x))) problem: strict: +(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,y) -> *(y,x) weak: original 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))) KH confluence processor Split input TRS into two TRSs S and T: TRS S: +(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) TRS T: sq(x) -> *(x,x) sq(s(x)) -> +(*(x,x),s(+(x,x))) As established above, T/S is terminating. T is strongly non-overlapping on S and S is strongly non-overlapping on T We get the following critical pairs, which are also S-critical pairs: *(s(x),s(x)) = +(*(x,x),s(+(x,x))), +(*(x4667,x4667),s(+(x4667,x4667))) = *(s(x4667),s(x4667)) all these critical pairs are joinable with S union T. Please install theorem prover 'Prover9' and 'Mace4' for handling more TRSs. All S-critical pairs are joinable. We have to check confluence of S. Church Rosser Transformation Processor (star): strict: *(1)(x709) -> +(0)(*(1)(x709)) *(1)(x709) -> +(1)(x709) *(0)(x710) -> +(0)(x710) *(0)(x710) -> +(1)(*(0)(x710)) weak: *(0)(x706) -> *(1)(x706) *(1)(x707) -> *(0)(x707) *(0)(s(0)(x708)) -> +(0)(*(0)(x708)) *(1)(s(0)(x711)) -> +(1)(*(1)(x711)) +(0)(x712) -> +(0)(s(0)(x712)) +(1)(s(0)(x713)) -> +(1)(x713) +(0)(s(0)(x714)) -> +(0)(x714) +(1)(x715) -> +(1)(s(0)(x715)) +(0)(x716) -> +(1)(x716) +(1)(x717) -> +(0)(x717) +(0)(+(0)(x718)) -> +(0)(x718) +(0)(+(1)(x719)) -> +(1)(+(0)(x719)) +(1)(x720) -> +(1)(+(1)(x720)) +(0)(x721) -> +(0)(+(0)(x721)) +(1)(+(0)(x722)) -> +(0)(+(1)(x722)) +(1)(+(1)(x723)) -> +(1)(x723) critical peaks: 32 +(x,+(+(y,x633),x634)) <-0|1[]- +(x,+(y,+(x633,x634))) -0|[]-> +(+(x,y),+(x633,x634)) +(+(+(x,y),x636),x637) <-0|[]- +(+(x,y),+(x636,x637)) -1|[]-> +(x,+(y,+(x636,x637))) +(+(+(x,x639),x640),z) <-0|0[]- +(+(x,+(x639,x640)),z) -1|[]-> +(x,+(+(x639,x640),z)) +(+(x,x642),x643) <-0|[]- +(x,+(x642,x643)) -2|[]-> +(+(x642,x643),x) +(+(s(x),x645),x646) <-0|[]- +(s(x),+(x645,x646)) -3|[]-> +(x,s(+(x645,x646))) +(x647,+(x648,+(y,z))) <-1|[]- +(+(x647,x648),+(y,z)) -0|[]-> +(+(+(x647,x648),y),z) +(x,+(x650,+(x651,z))) <-1|1[]- +(x,+(+(x650,x651),z)) -0|[]-> +(+(x,+(x650,x651)),z) +(+(x653,+(x654,y)),z) <-1|0[]- +(+(+(x653,x654),y),z) -1|[]-> +(+(x653,x654),+(y,z)) +(x656,+(x657,y)) <-1|[]- +(+(x656,x657),y) -2|[]-> +(y,+(x656,x657)) +(x659,+(x660,s(y))) <-1|[]- +(+(x659,x660),s(y)) -4|[]-> +(s(+(x659,x660)),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) +(x674,s(+(y,z))) <-3|[]- +(s(x674),+(y,z)) -0|[]-> +(+(s(x674),y),z) +(x,+(x676,s(z))) <-3|1[]- +(x,+(s(x676),z)) -0|[]-> +(+(x,s(x676)),z) +(+(x678,s(y)),z) <-3|0[]- +(+(s(x678),y),z) -1|[]-> +(s(x678),+(y,z)) +(x680,s(y)) <-3|[]- +(s(x680),y) -2|[]-> +(y,s(x680)) +(x682,s(s(y))) <-3|[]- +(s(x682),s(y)) -4|[]-> +(s(s(x682)),y) +(x,+(s(y),x685)) <-4|1[]- +(x,+(y,s(x685))) -0|[]-> +(+(x,y),s(x685)) +(s(+(x,y)),x687) <-4|[]- +(+(x,y),s(x687)) -1|[]-> +(x,+(y,s(x687))) +(+(s(x),x689),z) <-4|0[]- +(+(x,s(x689)),z) -1|[]-> +(x,+(s(x689),z)) +(s(x),x691) <-4|[]- +(x,s(x691)) -2|[]-> +(s(x691),x) +(s(s(x)),x693) <-4|[]- +(s(x),s(x693)) -3|[]-> +(x,s(s(x693))) +(s(x),*(s(x),x695)) <-5|[]- *(s(x),s(x695)) -6|[]-> +(*(x,s(x695)),s(x695)) +(x,*(x,x697)) <-5|[]- *(x,s(x697)) -7|[]-> *(s(x697),x) +(*(x698,s(y)),s(y)) <-6|[]- *(s(x698),s(y)) -5|[]-> +(s(x698),*(s(x698),y)) +(*(x700,y),y) <-6|[]- *(s(x700),y) -7|[]-> *(y,s(x700)) *(s(y),x) <-7|[]- *(x,s(y)) -5|[]-> +(x,*(x,y)) *(y,s(x)) <-7|[]- *(s(x),y) -6|[]-> +(*(x,y),y) Matrix Interpretation Processor: dim=1, star lab=right interpretation: [*(0)](x0) = 2x0 + 1, [+(1)](x0) = x0, [*(1)](x0) = 2x0 + 1, [+(0)](x0) = x0, [s(0)](x0) = x0 orientation: *(1)(x709) = 2x709 + 1 >= 2x709 + 1 = +(0)(*(1)(x709)) *(1)(x709) = 2x709 + 1 >= x709 = +(1)(x709) *(0)(x710) = 2x710 + 1 >= x710 = +(0)(x710) *(0)(x710) = 2x710 + 1 >= 2x710 + 1 = +(1)(*(0)(x710)) *(0)(x706) = 2x706 + 1 >= 2x706 + 1 = *(1)(x706) *(1)(x707) = 2x707 + 1 >= 2x707 + 1 = *(0)(x707) *(0)(s(0)(x708)) = 2x708 + 1 >= 2x708 + 1 = +(0)(*(0)(x708)) *(1)(s(0)(x711)) = 2x711 + 1 >= 2x711 + 1 = +(1)(*(1)(x711)) +(0)(x712) = x712 >= x712 = +(0)(s(0)(x712)) +(1)(s(0)(x713)) = x713 >= x713 = +(1)(x713) +(0)(s(0)(x714)) = x714 >= x714 = +(0)(x714) +(1)(x715) = x715 >= x715 = +(1)(s(0)(x715)) +(0)(x716) = x716 >= x716 = +(1)(x716) +(1)(x717) = x717 >= x717 = +(0)(x717) +(0)(+(0)(x718)) = x718 >= x718 = +(0)(x718) +(0)(+(1)(x719)) = x719 >= x719 = +(1)(+(0)(x719)) +(1)(x720) = x720 >= x720 = +(1)(+(1)(x720)) +(0)(x721) = x721 >= x721 = +(0)(+(0)(x721)) +(1)(+(0)(x722)) = x722 >= x722 = +(0)(+(1)(x722)) +(1)(+(1)(x723)) = x723 >= x723 = +(1)(x723) problem: strict: *(1)(x709) -> +(0)(*(1)(x709)) *(0)(x710) -> +(1)(*(0)(x710)) weak: *(0)(x706) -> *(1)(x706) *(1)(x707) -> *(0)(x707) *(0)(s(0)(x708)) -> +(0)(*(0)(x708)) *(1)(s(0)(x711)) -> +(1)(*(1)(x711)) +(0)(x712) -> +(0)(s(0)(x712)) +(1)(s(0)(x713)) -> +(1)(x713) +(0)(s(0)(x714)) -> +(0)(x714) +(1)(x715) -> +(1)(s(0)(x715)) +(0)(x716) -> +(1)(x716) +(1)(x717) -> +(0)(x717) +(0)(+(0)(x718)) -> +(0)(x718) +(0)(+(1)(x719)) -> +(1)(+(0)(x719)) +(1)(x720) -> +(1)(+(1)(x720)) +(0)(x721) -> +(0)(+(0)(x721)) +(1)(+(0)(x722)) -> +(0)(+(1)(x722)) +(1)(+(1)(x723)) -> +(1)(x723) Matrix Interpretation Processor: dim=2, star lab=right interpretation: [2 2] [*(0)](x0) = [0 1]x0, [1 0] [+(1)](x0) = [0 0]x0, [2 2] [*(1)](x0) = [0 1]x0, [1 0] [+(0)](x0) = [0 0]x0, [0] [s(0)](x0) = x0 + [1] orientation: [2 2] [2 2] *(1)(x709) = [0 1]x709 >= [0 0]x709 = +(0)(*(1)(x709)) [2 2] [2 2] *(0)(x710) = [0 1]x710 >= [0 0]x710 = +(1)(*(0)(x710)) [2 2] [2 2] *(0)(x706) = [0 1]x706 >= [0 1]x706 = *(1)(x706) [2 2] [2 2] *(1)(x707) = [0 1]x707 >= [0 1]x707 = *(0)(x707) [2 2] [2] [2 2] *(0)(s(0)(x708)) = [0 1]x708 + [1] >= [0 0]x708 = +(0)(*(0)(x708)) [2 2] [2] [2 2] *(1)(s(0)(x711)) = [0 1]x711 + [1] >= [0 0]x711 = +(1)(*(1)(x711)) [1 0] [1 0] +(0)(x712) = [0 0]x712 >= [0 0]x712 = +(0)(s(0)(x712)) [1 0] [1 0] +(1)(s(0)(x713)) = [0 0]x713 >= [0 0]x713 = +(1)(x713) [1 0] [1 0] +(0)(s(0)(x714)) = [0 0]x714 >= [0 0]x714 = +(0)(x714) [1 0] [1 0] +(1)(x715) = [0 0]x715 >= [0 0]x715 = +(1)(s(0)(x715)) [1 0] [1 0] +(0)(x716) = [0 0]x716 >= [0 0]x716 = +(1)(x716) [1 0] [1 0] +(1)(x717) = [0 0]x717 >= [0 0]x717 = +(0)(x717) [1 0] [1 0] +(0)(+(0)(x718)) = [0 0]x718 >= [0 0]x718 = +(0)(x718) [1 0] [1 0] +(0)(+(1)(x719)) = [0 0]x719 >= [0 0]x719 = +(1)(+(0)(x719)) [1 0] [1 0] +(1)(x720) = [0 0]x720 >= [0 0]x720 = +(1)(+(1)(x720)) [1 0] [1 0] +(0)(x721) = [0 0]x721 >= [0 0]x721 = +(0)(+(0)(x721)) [1 0] [1 0] +(1)(+(0)(x722)) = [0 0]x722 >= [0 0]x722 = +(0)(+(1)(x722)) [1 0] [1 0] +(1)(+(1)(x723)) = [0 0]x723 >= [0 0]x723 = +(1)(x723) problem: strict: *(1)(x709) -> +(0)(*(1)(x709)) *(0)(x710) -> +(1)(*(0)(x710)) weak: *(0)(x706) -> *(1)(x706) *(1)(x707) -> *(0)(x707) +(0)(x712) -> +(0)(s(0)(x712)) +(1)(s(0)(x713)) -> +(1)(x713) +(0)(s(0)(x714)) -> +(0)(x714) +(1)(x715) -> +(1)(s(0)(x715)) +(0)(x716) -> +(1)(x716) +(1)(x717) -> +(0)(x717) +(0)(+(0)(x718)) -> +(0)(x718) +(0)(+(1)(x719)) -> +(1)(+(0)(x719)) +(1)(x720) -> +(1)(+(1)(x720)) +(0)(x721) -> +(0)(+(0)(x721)) +(1)(+(0)(x722)) -> +(0)(+(1)(x722)) +(1)(+(1)(x723)) -> +(1)(x723) Shift Processor (**) lab=left: strict: weak: Shift Processor lab=left (dd): strict: +(x,+(y,+(x633,x634))) -> +(x,+(+(y,x633),x634)) +(x,+(y,+(x633,x634))) -> +(+(x,y),+(x633,x634)) +(x,+(+(y,x633),x634)) -> +(x,+(y,+(x633,x634))) +(+(x,y),+(x633,x634)) -> +(x,+(y,+(x633,x634))) +(+(x,y),+(x636,x637)) -> +(+(+(x,y),x636),x637) +(+(x,y),+(x636,x637)) -> +(x,+(y,+(x636,x637))) +(+(+(x,y),x636),x637) -> +(+(x,y),+(x636,x637)) +(x,+(y,+(x636,x637))) -> +(+(x,y),+(x636,x637)) +(+(x,+(x639,x640)),z) -> +(+(+(x,x639),x640),z) +(+(x,+(x639,x640)),z) -> +(x,+(+(x639,x640),z)) +(+(+(x,x639),x640),z) -> +(+(x,+(x639,x640)),z) +(x,+(+(x639,x640),z)) -> +(+(x,+(x639,x640)),z) +(x,+(x642,x643)) -> +(+(x,x642),x643) +(x,+(x642,x643)) -> +(+(x642,x643),x) +(+(x,x642),x643) -> +(x,+(x642,x643)) +(+(x642,x643),x) -> +(x,+(x642,x643)) +(s(x),+(x645,x646)) -> +(+(s(x),x645),x646) +(s(x),+(x645,x646)) -> +(x,s(+(x645,x646))) +(+(s(x),x645),x646) -> +(s(x),+(x645,x646)) +(x,s(+(x645,x646))) -> +(s(x),+(x645,x646)) +(+(x647,x648),+(y,z)) -> +(x647,+(x648,+(y,z))) +(+(x647,x648),+(y,z)) -> +(+(+(x647,x648),y),z) +(x647,+(x648,+(y,z))) -> +(+(x647,x648),+(y,z)) +(+(+(x647,x648),y),z) -> +(+(x647,x648),+(y,z)) +(x,+(+(x650,x651),z)) -> +(x,+(x650,+(x651,z))) +(x,+(+(x650,x651),z)) -> +(+(x,+(x650,x651)),z) +(x,+(x650,+(x651,z))) -> +(x,+(+(x650,x651),z)) +(+(x,+(x650,x651)),z) -> +(x,+(+(x650,x651),z)) +(+(+(x653,x654),y),z) -> +(+(x653,+(x654,y)),z) +(+(+(x653,x654),y),z) -> +(+(x653,x654),+(y,z)) +(+(x653,+(x654,y)),z) -> +(+(+(x653,x654),y),z) +(+(x653,x654),+(y,z)) -> +(+(+(x653,x654),y),z) +(+(x656,x657),y) -> +(x656,+(x657,y)) +(+(x656,x657),y) -> +(y,+(x656,x657)) +(x656,+(x657,y)) -> +(+(x656,x657),y) +(y,+(x656,x657)) -> +(+(x656,x657),y) +(+(x659,x660),s(y)) -> +(x659,+(x660,s(y))) +(+(x659,x660),s(y)) -> +(s(+(x659,x660)),y) +(x659,+(x660,s(y))) -> +(+(x659,x660),s(y)) +(s(+(x659,x660)),y) -> +(+(x659,x660),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(x674),+(y,z)) -> +(x674,s(+(y,z))) +(s(x674),+(y,z)) -> +(+(s(x674),y),z) +(x674,s(+(y,z))) -> +(s(x674),+(y,z)) +(+(s(x674),y),z) -> +(s(x674),+(y,z)) +(x,+(s(x676),z)) -> +(x,+(x676,s(z))) +(x,+(s(x676),z)) -> +(+(x,s(x676)),z) +(x,+(x676,s(z))) -> +(x,+(s(x676),z)) +(+(x,s(x676)),z) -> +(x,+(s(x676),z)) +(+(s(x678),y),z) -> +(+(x678,s(y)),z) +(+(s(x678),y),z) -> +(s(x678),+(y,z)) +(+(x678,s(y)),z) -> +(+(s(x678),y),z) +(s(x678),+(y,z)) -> +(+(s(x678),y),z) +(s(x680),y) -> +(x680,s(y)) +(s(x680),y) -> +(y,s(x680)) +(x680,s(y)) -> +(s(y),x680) +(y,s(x680)) -> +(s(y),x680) +(x680,s(y)) -> +(s(x680),y) +(y,s(x680)) -> +(s(x680),y) +(s(x682),s(y)) -> +(x682,s(s(y))) +(s(x682),s(y)) -> +(s(s(x682)),y) +(x682,s(s(y))) -> +(s(x682),s(y)) +(s(s(x682)),y) -> +(s(x682),s(y)) +(x,+(y,s(x685))) -> +(x,+(s(y),x685)) +(x,+(y,s(x685))) -> +(+(x,y),s(x685)) +(x,+(s(y),x685)) -> +(x,+(y,s(x685))) +(+(x,y),s(x685)) -> +(x,+(y,s(x685))) +(+(x,y),s(x687)) -> +(s(+(x,y)),x687) +(+(x,y),s(x687)) -> +(x,+(y,s(x687))) +(s(+(x,y)),x687) -> +(+(x,y),s(x687)) +(x,+(y,s(x687))) -> +(+(x,y),s(x687)) +(+(x,s(x689)),z) -> +(+(s(x),x689),z) +(+(x,s(x689)),z) -> +(x,+(s(x689),z)) +(+(s(x),x689),z) -> +(+(x,s(x689)),z) +(x,+(s(x689),z)) -> +(+(x,s(x689)),z) +(x,s(x691)) -> +(s(x),x691) +(x,s(x691)) -> +(s(x691),x) +(s(x),x691) -> +(x691,s(x)) +(s(x691),x) -> +(x691,s(x)) +(s(x),x691) -> +(x,s(x691)) +(s(x691),x) -> +(x,s(x691)) +(s(x),s(x693)) -> +(s(s(x)),x693) +(s(x),s(x693)) -> +(x,s(s(x693))) +(s(s(x)),x693) -> +(s(x),s(x693)) +(x,s(s(x693))) -> +(s(x),s(x693)) *(s(x),s(x695)) -> +(s(x),*(s(x),x695)) *(s(x),s(x695)) -> +(*(x,s(x695)),s(x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(s(x),*(x,x695)),x695) +(+(s(x),*(x,x695)),x695) -> +(+(x,s(*(x,x695))),x695) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(x,+(*(x,x695),s(x695))) +(x,+(*(x,x695),s(x695))) -> +(x,+(s(*(x,x695)),x695)) +(x,+(s(*(x,x695)),x695)) -> +(+(x,s(*(x,x695))),x695) +(s(x),*(s(x),x695)) -> +(*(s(x),x695),s(x)) +(*(s(x),x695),s(x)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x),x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(+(*(x,x695),x),s(x695)) +(+(*(x,x695),x),s(x695)) -> +(*(x,x695),+(x,s(x695))) +(*(x,x695),+(x,s(x695))) -> +(*(x,x695),+(s(x),x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x),x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(+(*(x,x695),x),s(x695)) +(+(*(x,x695),x),s(x695)) -> +(*(x,x695),+(x,s(x695))) +(*(x,x695),+(x,s(x695))) -> +(*(x,x695),+(s(x),x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(s(x),*(x,x695)),x695) +(+(s(x),*(x,x695)),x695) -> +(+(*(x,x695),s(x)),x695) +(+(*(x,x695),s(x)),x695) -> +(*(x,x695),+(s(x),x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(+(*(x,x695),x),s(x695)) +(+(*(x,x695),x),s(x695)) -> +(*(x,x695),+(x,s(x695))) +(*(x,x695),+(x,s(x695))) -> +(*(x,x695),+(s(x),x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(s(x),+(x695,*(x,x695))) +(s(x),+(x695,*(x,x695))) -> +(+(s(x),x695),*(x,x695)) +(+(s(x),x695),*(x,x695)) -> +(*(x,x695),+(s(x),x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(+(*(x,x695),x),s(x695)) +(+(*(x,x695),x),s(x695)) -> +(*(x,x695),+(x,s(x695))) +(*(x,x695),+(x,s(x695))) -> +(*(x,x695),+(s(x),x695)) +(s(x),*(s(x),x695)) -> +(*(s(x),x695),s(x)) +(*(s(x),x695),s(x)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(s(x695),*(x,s(x695))) +(s(x695),*(x,s(x695))) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(*(s(x),x695),s(x)) +(*(s(x),x695),s(x)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(s(x695),*(x,s(x695))) +(s(x695),*(x,s(x695))) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(s(x),*(x,x695)),x695) +(+(s(x),*(x,x695)),x695) -> +(x695,+(s(x),*(x,x695))) +(x695,+(s(x),*(x,x695))) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(s(x695),*(x,s(x695))) +(s(x695),*(x,s(x695))) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(s(x),*(x,x695)),x695) +(+(s(x),*(x,x695)),x695) -> +(x695,+(s(x),*(x,x695))) +(x695,+(s(x),*(x,x695))) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(s(x),+(x695,*(x,x695))) +(s(x),+(x695,*(x,x695))) -> +(+(s(x),x695),*(x,x695)) +(+(s(x),x695),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(s(x695),*(x,s(x695))) +(s(x695),*(x,s(x695))) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(s(x),+(x695,*(x,x695))) +(s(x),+(x695,*(x,x695))) -> +(+(s(x),x695),*(x,x695)) +(+(s(x),x695),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x695,s(x)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(*(s(x),x695),s(x)) +(*(s(x),x695),s(x)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(s(x695),*(x,s(x695))) +(s(x695),*(x,s(x695))) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(*(s(x),x695),s(x)) +(*(s(x),x695),s(x)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(*(s(x),x695),s(x)) +(*(s(x),x695),s(x)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(x,+(*(x,x695),s(x695))) +(x,+(*(x,x695),s(x695))) -> +(+(*(x,x695),s(x695)),x) +(+(*(x,x695),s(x695)),x) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(*(s(x),x695),s(x)) +(*(s(x),x695),s(x)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(+(*(x,x695),x),s(x695)) +(+(*(x,x695),x),s(x695)) -> +(*(x,x695),+(x,s(x695))) +(*(x,x695),+(x,s(x695))) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(s(x695),*(x,s(x695))) +(s(x695),*(x,s(x695))) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(x,+(*(x,x695),s(x695))) +(x,+(*(x,x695),s(x695))) -> +(+(*(x,x695),s(x695)),x) +(+(*(x,x695),s(x695)),x) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(*(x,x695),x695),s(x)) +(+(*(x,x695),x695),s(x)) -> +(*(x,x695),+(x695,s(x))) +(*(x,x695),+(x695,s(x))) -> +(*(x,x695),+(s(x695),x)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(+(*(x,x695),x),s(x695)) +(+(*(x,x695),x),s(x695)) -> +(*(x,x695),+(x,s(x695))) +(*(x,x695),+(x,s(x695))) -> +(*(x,x695),+(s(x695),x)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(+(s(x),*(x,x695)),x695) +(+(s(x),*(x,x695)),x695) -> +(+(x,s(*(x,x695))),x695) +(+(x,s(*(x,x695))),x695) -> +(x,+(s(*(x,x695)),x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(x,+(*(x,x695),s(x695))) +(x,+(*(x,x695),s(x695))) -> +(x,+(s(*(x,x695)),x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(s(x),+(x695,*(x,x695))) +(s(x),+(x695,*(x,x695))) -> +(+(s(x),x695),*(x,x695)) +(+(s(x),x695),*(x,x695)) -> +(+(x,s(x695)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(s(x695),*(x,s(x695))) +(s(x695),*(x,s(x695))) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x,s(x695)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(s(x),+(x695,*(x,x695))) +(s(x),+(x695,*(x,x695))) -> +(+(s(x),x695),*(x,x695)) +(+(s(x),x695),*(x,x695)) -> +(+(x,s(x695)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(s(x695),+(x,*(x,x695))) +(s(x695),+(x,*(x,x695))) -> +(+(s(x695),x),*(x,x695)) +(+(s(x695),x),*(x,x695)) -> +(+(x,s(x695)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(s(x),+(x695,*(x,x695))) +(s(x),+(x695,*(x,x695))) -> +(+(s(x),x695),*(x,x695)) +(+(s(x),x695),*(x,x695)) -> +(+(x,s(x695)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(x,+(*(x,x695),s(x695))) +(x,+(*(x,x695),s(x695))) -> +(x,+(s(x695),*(x,x695))) +(x,+(s(x695),*(x,x695))) -> +(+(x,s(x695)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),+(*(x,x695),x695)) +(s(x),+(*(x,x695),x695)) -> +(s(x),+(x695,*(x,x695))) +(s(x),+(x695,*(x,x695))) -> +(+(s(x),x695),*(x,x695)) +(+(s(x),x695),*(x,x695)) -> +(+(x,s(x695)),*(x,x695)) +(*(x,s(x695)),s(x695)) -> +(+(x,*(x,x695)),s(x695)) +(+(x,*(x,x695)),s(x695)) -> +(+(*(x,x695),x),s(x695)) +(+(*(x,x695),x),s(x695)) -> +(*(x,x695),+(x,s(x695))) +(*(x,x695),+(x,s(x695))) -> +(+(x,s(x695)),*(x,x695)) +(s(x),*(s(x),x695)) -> +(s(x),*(x695,s(x))) +(s(x),*(x695,s(x))) -> +(s(x),+(x695,*(x695,x))) +(s(x),+(x695,*(x695,x))) -> +(+(s(x),x695),*(x695,x)) +(+(s(x),x695),*(x695,x)) -> +(*(x695,x),+(s(x),x695)) +(*(x,s(x695)),s(x695)) -> +(*(s(x695),x),s(x695)) +(*(s(x695),x),s(x695)) -> +(+(*(x695,x),x),s(x695)) +(+(*(x695,x),x),s(x695)) -> +(*(x695,x),+(x,s(x695))) +(*(x695,x),+(x,s(x695))) -> +(*(x695,x),+(s(x),x695)) +(s(x),*(s(x),x695)) -> +(s(x),*(x695,s(x))) +(s(x),*(x695,s(x))) -> +(s(x),+(x695,*(x695,x))) +(s(x),+(x695,*(x695,x))) -> +(+(s(x),x695),*(x695,x)) +(+(s(x),x695),*(x695,x)) -> +(+(x,s(x695)),*(x695,x)) +(*(x,s(x695)),s(x695)) -> +(*(s(x695),x),s(x695)) +(*(s(x695),x),s(x695)) -> +(+(*(x695,x),x),s(x695)) +(+(*(x695,x),x),s(x695)) -> +(*(x695,x),+(x,s(x695))) +(*(x695,x),+(x,s(x695))) -> +(+(x,s(x695)),*(x695,x)) *(x,s(x697)) -> +(x,*(x,x697)) *(x,s(x697)) -> *(s(x697),x) *(s(x697),x) -> *(x,s(x697)) *(x,s(x697)) -> +(x,*(x,x697)) +(x,*(x,x697)) -> +(*(x,x697),x) *(s(x697),x) -> +(*(x697,x),x) +(*(x697,x),x) -> +(*(x,x697),x) +(x,*(x,x697)) -> +(x,*(x697,x)) *(s(x697),x) -> +(*(x697,x),x) +(*(x697,x),x) -> +(x,*(x697,x)) +(x,*(x,x697)) -> +(*(x,x697),x) +(*(x,x697),x) -> +(*(x697,x),x) *(s(x697),x) -> +(*(x697,x),x) +(x,*(x,x697)) -> +(x,*(x697,x)) +(x,*(x697,x)) -> +(*(x697,x),x) *(s(x697),x) -> +(*(x697,x),x) *(s(x698),s(y)) -> +(*(x698,s(y)),s(y)) *(s(x698),s(y)) -> +(s(x698),*(s(x698),y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(x698,+(*(x698,y),s(y))) +(x698,+(*(x698,y),s(y))) -> +(x698,+(s(*(x698,y)),y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(s(x698),*(x698,y)),y) +(+(s(x698),*(x698,y)),y) -> +(+(x698,s(*(x698,y))),y) +(+(x698,s(*(x698,y))),y) -> +(x698,+(s(*(x698,y)),y)) +(*(x698,s(y)),s(y)) -> +(s(y),*(x698,s(y))) +(s(y),*(x698,s(y))) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(x698,s(y)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(s(x698),+(y,*(x698,y))) +(s(x698),+(y,*(x698,y))) -> +(+(s(x698),y),*(x698,y)) +(+(s(x698),y),*(x698,y)) -> +(+(x698,s(y)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(x698,s(y)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(s(x698),+(y,*(x698,y))) +(s(x698),+(y,*(x698,y))) -> +(+(s(x698),y),*(x698,y)) +(+(s(x698),y),*(x698,y)) -> +(+(x698,s(y)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(x698,+(*(x698,y),s(y))) +(x698,+(*(x698,y),s(y))) -> +(x698,+(s(y),*(x698,y))) +(x698,+(s(y),*(x698,y))) -> +(+(x698,s(y)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(s(x698),+(y,*(x698,y))) +(s(x698),+(y,*(x698,y))) -> +(+(s(x698),y),*(x698,y)) +(+(s(x698),y),*(x698,y)) -> +(+(x698,s(y)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(+(*(x698,y),x698),s(y)) +(+(*(x698,y),x698),s(y)) -> +(*(x698,y),+(x698,s(y))) +(*(x698,y),+(x698,s(y))) -> +(+(x698,s(y)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(s(x698),+(y,*(x698,y))) +(s(x698),+(y,*(x698,y))) -> +(+(s(x698),y),*(x698,y)) +(+(s(x698),y),*(x698,y)) -> +(+(x698,s(y)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(s(y),*(x698,s(y))) +(s(y),*(x698,s(y))) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(*(s(x698),y),s(x698)) +(*(s(x698),y),s(x698)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(s(y),*(x698,s(y))) +(s(y),*(x698,s(y))) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(*(s(x698),y),s(x698)) +(*(s(x698),y),s(x698)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(x698,+(*(x698,y),s(y))) +(x698,+(*(x698,y),s(y))) -> +(+(*(x698,y),s(y)),x698) +(+(*(x698,y),s(y)),x698) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(*(s(x698),y),s(x698)) +(*(s(x698),y),s(x698)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(x698,+(*(x698,y),s(y))) +(x698,+(*(x698,y),s(y))) -> +(+(*(x698,y),s(y)),x698) +(+(*(x698,y),s(y)),x698) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(+(*(x698,y),x698),s(y)) +(+(*(x698,y),x698),s(y)) -> +(*(x698,y),+(x698,s(y))) +(*(x698,y),+(x698,s(y))) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(*(s(x698),y),s(x698)) +(*(s(x698),y),s(x698)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(+(*(x698,y),x698),s(y)) +(+(*(x698,y),x698),s(y)) -> +(*(x698,y),+(x698,s(y))) +(*(x698,y),+(x698,s(y))) -> +(*(x698,y),+(s(y),x698)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(y),x698)) +(*(x698,s(y)),s(y)) -> +(s(y),*(x698,s(y))) +(s(y),*(x698,s(y))) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(*(s(x698),y),s(x698)) +(*(s(x698),y),s(x698)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(s(y),*(x698,s(y))) +(s(y),*(x698,s(y))) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(s(y),*(x698,s(y))) +(s(y),*(x698,s(y))) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(s(x698),*(x698,y)),y) +(+(s(x698),*(x698,y)),y) -> +(y,+(s(x698),*(x698,y))) +(y,+(s(x698),*(x698,y))) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(s(y),*(x698,s(y))) +(s(y),*(x698,s(y))) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(s(x698),+(y,*(x698,y))) +(s(x698),+(y,*(x698,y))) -> +(+(s(x698),y),*(x698,y)) +(+(s(x698),y),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(*(s(x698),y),s(x698)) +(*(s(x698),y),s(x698)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(s(x698),*(x698,y)),y) +(+(s(x698),*(x698,y)),y) -> +(y,+(s(x698),*(x698,y))) +(y,+(s(x698),*(x698,y))) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(s(y),+(x698,*(x698,y))) +(s(y),+(x698,*(x698,y))) -> +(+(s(y),x698),*(x698,y)) +(+(s(y),x698),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(s(x698),+(y,*(x698,y))) +(s(x698),+(y,*(x698,y))) -> +(+(s(x698),y),*(x698,y)) +(+(s(x698),y),*(x698,y)) -> +(+(y,s(x698)),*(x698,y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(x698,+(*(x698,y),s(y))) +(x698,+(*(x698,y),s(y))) -> +(x698,+(s(*(x698,y)),y)) +(x698,+(s(*(x698,y)),y)) -> +(+(x698,s(*(x698,y))),y) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(s(x698),*(x698,y)),y) +(+(s(x698),*(x698,y)),y) -> +(+(x698,s(*(x698,y))),y) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(+(*(x698,y),x698),s(y)) +(+(*(x698,y),x698),s(y)) -> +(*(x698,y),+(x698,s(y))) +(*(x698,y),+(x698,s(y))) -> +(*(x698,y),+(s(x698),y)) +(s(x698),*(s(x698),y)) -> +(*(s(x698),y),s(x698)) +(*(s(x698),y),s(x698)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(x698),y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(+(*(x698,y),x698),s(y)) +(+(*(x698,y),x698),s(y)) -> +(*(x698,y),+(x698,s(y))) +(*(x698,y),+(x698,s(y))) -> +(*(x698,y),+(s(x698),y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(*(x698,y),y),s(x698)) +(+(*(x698,y),y),s(x698)) -> +(*(x698,y),+(y,s(x698))) +(*(x698,y),+(y,s(x698))) -> +(*(x698,y),+(s(x698),y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(+(*(x698,y),x698),s(y)) +(+(*(x698,y),x698),s(y)) -> +(*(x698,y),+(x698,s(y))) +(*(x698,y),+(x698,s(y))) -> +(*(x698,y),+(s(x698),y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(+(s(x698),*(x698,y)),y) +(+(s(x698),*(x698,y)),y) -> +(+(*(x698,y),s(x698)),y) +(+(*(x698,y),s(x698)),y) -> +(*(x698,y),+(s(x698),y)) +(*(x698,s(y)),s(y)) -> +(+(x698,*(x698,y)),s(y)) +(+(x698,*(x698,y)),s(y)) -> +(+(*(x698,y),x698),s(y)) +(+(*(x698,y),x698),s(y)) -> +(*(x698,y),+(x698,s(y))) +(*(x698,y),+(x698,s(y))) -> +(*(x698,y),+(s(x698),y)) +(s(x698),*(s(x698),y)) -> +(s(x698),+(*(x698,y),y)) +(s(x698),+(*(x698,y),y)) -> +(s(x698),+(y,*(x698,y))) +(s(x698),+(y,*(x698,y))) -> +(+(s(x698),y),*(x698,y)) +(+(s(x698),y),*(x698,y)) -> +(*(x698,y),+(s(x698),y)) +(*(x698,s(y)),s(y)) -> +(*(s(y),x698),s(y)) +(*(s(y),x698),s(y)) -> +(+(*(y,x698),x698),s(y)) +(+(*(y,x698),x698),s(y)) -> +(*(y,x698),+(x698,s(y))) +(*(y,x698),+(x698,s(y))) -> +(+(x698,s(y)),*(y,x698)) +(s(x698),*(s(x698),y)) -> +(s(x698),*(y,s(x698))) +(s(x698),*(y,s(x698))) -> +(s(x698),+(y,*(y,x698))) +(s(x698),+(y,*(y,x698))) -> +(+(s(x698),y),*(y,x698)) +(+(s(x698),y),*(y,x698)) -> +(+(x698,s(y)),*(y,x698)) +(*(x698,s(y)),s(y)) -> +(*(s(y),x698),s(y)) +(*(s(y),x698),s(y)) -> +(+(*(y,x698),x698),s(y)) +(+(*(y,x698),x698),s(y)) -> +(*(y,x698),+(x698,s(y))) +(*(y,x698),+(x698,s(y))) -> +(*(y,x698),+(s(x698),y)) +(s(x698),*(s(x698),y)) -> +(s(x698),*(y,s(x698))) +(s(x698),*(y,s(x698))) -> +(s(x698),+(y,*(y,x698))) +(s(x698),+(y,*(y,x698))) -> +(+(s(x698),y),*(y,x698)) +(+(s(x698),y),*(y,x698)) -> +(*(y,x698),+(s(x698),y)) *(s(x700),y) -> +(*(x700,y),y) *(s(x700),y) -> *(y,s(x700)) *(y,s(x700)) -> *(s(x700),y) *(s(x700),y) -> +(*(x700,y),y) +(*(x700,y),y) -> +(y,*(x700,y)) *(y,s(x700)) -> +(y,*(y,x700)) +(y,*(y,x700)) -> +(y,*(x700,y)) +(*(x700,y),y) -> +(*(y,x700),y) *(y,s(x700)) -> +(y,*(y,x700)) +(y,*(y,x700)) -> +(*(y,x700),y) +(*(x700,y),y) -> +(y,*(x700,y)) +(y,*(x700,y)) -> +(y,*(y,x700)) *(y,s(x700)) -> +(y,*(y,x700)) +(*(x700,y),y) -> +(*(y,x700),y) +(*(y,x700),y) -> +(y,*(y,x700)) *(y,s(x700)) -> +(y,*(y,x700)) *(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) 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) 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): 0 *(x,y) -> *(y,x): 9 Decreasing Processor: The following diagrams are decreasing: peak: +(x,+(+(y,x633),x634)) <-0|1[==1,==0,==0,==0]- +(x,+(y,+(x633,x634))) -0| [==1,==0,==0,==0]-> +(+(x,y),+(x633,x634)) joins (1): +(x,+(+(y,x633),x634)) -1|1[==1,==0,==0,==0]-> +(x,+(y,+(x633,x634))) +(+(x,y),+(x633,x634)) -1|[==1,==0,==0,==0]-> +(x,+(y,+(x633,x634))) peak: +(+(+(x,y),x636),x637) <-0|[==1,==0,==0,==0]- +(+(x,y),+(x636,x637)) -1| [==1,==0,==0,==0]-> +(x,+(y,+(x636,x637))) joins (1): +(+(+(x,y),x636),x637) -1|[==1,==0,==0,==0]-> +(+(x,y),+(x636,x637)) +(x,+(y,+(x636,x637))) -0|[==1,==0,==0,==0]-> +(+(x,y),+(x636,x637)) peak: +(+(+(x,x639),x640),z) <-0|0[==1,==0,==0,==0]- +(+(x,+(x639,x640)),z) -1| [==1,==0,==0,==0]-> +(x,+(+(x639,x640),z)) joins (1): +(+(+(x,x639),x640),z) -1|0[==1,==0,==0,==0]-> +(+(x,+(x639,x640)),z) +(x,+(+(x639,x640),z)) -0|[==1,==0,==0,==0]-> +(+(x,+(x639,x640)),z) peak: +(+(x,x642),x643) <-0|[==1,==0,==0,==0]- +(x,+(x642,x643)) -2| [==1,==0,==0,==0]-> +(+(x642,x643),x) joins (1): +(+(x,x642),x643) -1|[==1,==0,==0,==0]-> +(x,+(x642,x643)) +(+(x642,x643),x) -2|[==1,==0,==0,==0]-> +(x,+(x642,x643)) peak: +(+(s(x),x645),x646) <-0|[==1,==0,==0,==0]- +(s(x),+(x645,x646)) -3| [==1,==0,==0,==0]-> +(x,s(+(x645,x646))) joins (1): +(+(s(x),x645),x646) -1|[==1,==0,==0,==0]-> +(s(x),+(x645,x646)) +(x,s(+(x645,x646))) -4|[==1,==0,==0,==0]-> +(s(x),+(x645,x646)) peak: +(x647,+(x648,+(y,z))) <-1|[==1,==0,==0,==0]- +(+(x647,x648),+(y,z)) -0| [==1,==0,==0,==0]-> +(+(+(x647,x648),y),z) joins (1): +(x647,+(x648,+(y,z))) -0|[==1,==0,==0,==0]-> +(+(x647,x648),+(y,z)) +(+(+(x647,x648),y),z) -1|[==1,==0,==0,==0]-> +(+(x647,x648),+(y,z)) peak: +(x,+(x650,+(x651,z))) <-1|1[==1,==0,==0,==0]- +(x,+(+(x650,x651),z)) -0| [==1,==0,==0,==0]-> +(+(x,+(x650,x651)),z) joins (1): +(x,+(x650,+(x651,z))) -0|1[==1,==0,==0,==0]-> +(x,+(+(x650,x651),z)) +(+(x,+(x650,x651)),z) -1|[==1,==0,==0,==0]-> +(x,+(+(x650,x651),z)) peak: +(+(x653,+(x654,y)),z) <-1|0[==1,==0,==0,==0]- +(+(+(x653,x654),y),z) -1| [==1,==0,==0,==0]-> +(+(x653,x654),+(y,z)) joins (1): +(+(x653,+(x654,y)),z) -0|0[==1,==0,==0,==0]-> +(+(+(x653,x654),y),z) +(+(x653,x654),+(y,z)) -0|[==1,==0,==0,==0]-> +(+(+(x653,x654),y),z) peak: +(x656,+(x657,y)) <-1|[==1,==0,==0,==0]- +(+(x656,x657),y) -2| [==1,==0,==0,==0]-> +(y,+(x656,x657)) joins (1): +(x656,+(x657,y)) -0|[==1,==0,==0,==0]-> +(+(x656,x657),y) +(y,+(x656,x657)) -2|[==1,==0,==0,==0]-> +(+(x656,x657),y) peak: +(x659,+(x660,s(y))) <-1|[==1,==0,==0,==0]- +(+(x659,x660),s(y)) -4| [==1,==0,==0,==0]-> +(s(+(x659,x660)),y) joins (1): +(x659,+(x660,s(y))) -0|[==1,==0,==0,==0]-> +(+(x659,x660),s(y)) +(s(+(x659,x660)),y) -3|[==1,==0,==0,==0]-> +(+(x659,x660),s(y)) peak: +(+(y,z),x) <-2|[==1,==0,==0,==0]- +(x,+(y,z)) -0|[==1,==0,==0,==0]-> +(+(x,y),z) joins (1): +(+(y,z),x) -2|[==1,==0,==0,==0]-> +(x,+(y,z)) +(+(x,y),z) -1|[==1,==0,==0,==0]-> +(x,+(y,z)) peak: +(x,+(z,y)) <-2|1[==1,==0,==0,==0]- +(x,+(y,z)) -0|[==1,==0,==0,==0]-> +(+(x,y),z) joins (1): +(x,+(z,y)) -2|1[==1,==0,==0,==0]-> +(x,+(y,z)) +(+(x,y),z) -1|[==1,==0,==0,==0]-> +(x,+(y,z)) peak: +(z,+(x,y)) <-2|[==1,==0,==0,==0]- +(+(x,y),z) -1|[==1,==0,==0,==0]-> +(x,+(y,z)) joins (1): +(z,+(x,y)) -2|[==1,==0,==0,==0]-> +(+(x,y),z) +(x,+(y,z)) -0|[==1,==0,==0,==0]-> +(+(x,y),z) peak: +(+(y,x),z) <-2|0[==1,==0,==0,==0]- +(+(x,y),z) -1|[==1,==0,==0,==0]-> +(x,+(y,z)) joins (1): +(+(y,x),z) -2|0[==1,==0,==0,==0]-> +(+(x,y),z) +(x,+(y,z)) -0|[==1,==0,==0,==0]-> +(+(x,y),z) peak: +(y,s(x)) <-2|[==1,==0,==0,==0]- +(s(x),y) -3|[==1,==0,==0,==0]-> +(x,s(y)) joins (1): +(y,s(x)) -2|[==1,==0,==0,==0]-> +(s(x),y) +(x,s(y)) -4|[==1,==0,==0,==0]-> +(s(x),y) peak: +(s(y),x) <-2|[==1,==0,==0,==0]- +(x,s(y)) -4|[==1,==0,==0,==0]-> +(s(x),y) joins (1): +(s(y),x) -2|[==1,==0,==0,==0]-> +(x,s(y)) +(s(x),y) -3|[==1,==0,==0,==0]-> +(x,s(y)) peak: +(x674,s(+(y,z))) <-3|[==1,==0,==0,==0]- +(s(x674),+(y,z)) -0| [==1,==0,==0,==0]-> +(+(s(x674),y),z) joins (1): +(x674,s(+(y,z))) -4|[==1,==0,==0,==0]-> +(s(x674),+(y,z)) +(+(s(x674),y),z) -1|[==1,==0,==0,==0]-> +(s(x674),+(y,z)) peak: +(x,+(x676,s(z))) <-3|1[==1,==0,==0,==0]- +(x,+(s(x676),z)) -0| [==1,==0,==0,==0]-> +(+(x,s(x676)),z) joins (1): +(x,+(x676,s(z))) -4|1[==1,==0,==0,==0]-> +(x,+(s(x676),z)) +(+(x,s(x676)),z) -1|[==1,==0,==0,==0]-> +(x,+(s(x676),z)) peak: +(+(x678,s(y)),z) <-3|0[==1,==0,==0,==0]- +(+(s(x678),y),z) -1| [==1,==0,==0,==0]-> +(s(x678),+(y,z)) joins (1): +(+(x678,s(y)),z) -4|0[==1,==0,==0,==0]-> +(+(s(x678),y),z) +(s(x678),+(y,z)) -0|[==1,==0,==0,==0]-> +(+(s(x678),y),z) peak: +(x680,s(y)) <-3|[==1,==0,==0,==0]- +(s(x680),y) -2|[==1,==0,==0,==0]-> +(y,s(x680)) joins (1): +(x680,s(y)) -2|[==1,==0,==0,==0]-> +(s(y),x680) +(y,s(x680)) -4|[==1,==0,==0,==0]-> +(s(y),x680) peak: +(x682,s(s(y))) <-3|[==1,==0,==0,==0]- +(s(x682),s(y)) -4| [==1,==0,==0,==0]-> +(s(s(x682)),y) joins (1): +(x682,s(s(y))) -4|[==1,==0,==0,==0]-> +(s(x682),s(y)) +(s(s(x682)),y) -3|[==1,==0,==0,==0]-> +(s(x682),s(y)) peak: +(x,+(s(y),x685)) <-4|1[==1,==0,==0,==0]- +(x,+(y,s(x685))) -0| [==1,==0,==0,==0]-> +(+(x,y),s(x685)) joins (1): +(x,+(s(y),x685)) -3|1[==1,==0,==0,==0]-> +(x,+(y,s(x685))) +(+(x,y),s(x685)) -1|[==1,==0,==0,==0]-> +(x,+(y,s(x685))) peak: +(s(+(x,y)),x687) <-4|[==1,==0,==0,==0]- +(+(x,y),s(x687)) -1| [==1,==0,==0,==0]-> +(x,+(y,s(x687))) joins (1): +(s(+(x,y)),x687) -3|[==1,==0,==0,==0]-> +(+(x,y),s(x687)) +(x,+(y,s(x687))) -0|[==1,==0,==0,==0]-> +(+(x,y),s(x687)) peak: +(+(s(x),x689),z) <-4|0[==1,==0,==0,==0]- +(+(x,s(x689)),z) -1| [==1,==0,==0,==0]-> +(x,+(s(x689),z)) joins (1): +(+(s(x),x689),z) -3|0[==1,==0,==0,==0]-> +(+(x,s(x689)),z) +(x,+(s(x689),z)) -0|[==1,==0,==0,==0]-> +(+(x,s(x689)),z) peak: +(s(x),x691) <-4|[==1,==0,==0,==0]- +(x,s(x691)) -2|[==1,==0,==0,==0]-> +(s(x691),x) joins (1): +(s(x),x691) -2|[==1,==0,==0,==0]-> +(x691,s(x)) +(s(x691),x) -3|[==1,==0,==0,==0]-> +(x691,s(x)) peak: +(s(s(x)),x693) <-4|[==1,==0,==0,==0]- +(s(x),s(x693)) -3| [==1,==0,==0,==0]-> +(x,s(s(x693))) joins (1): +(s(s(x)),x693) -3|[==1,==0,==0,==0]-> +(s(x),s(x693)) +(x,s(s(x693))) -4|[==1,==0,==0,==0]-> +(s(x),s(x693)) peak: +(s(x),*(s(x),x695)) <-5|[==1,==0,==0,=?1]- *(s(x),s(x695)) -6| [==1,==0,==0,>=0]-> +(*(x,s(x695)),s(x695)) joins (1): +(s(x),*(s(x),x695)) -6|1[==1,==0,==0,>=0]-> +(s(x),+(*(x,x695),x695)) -0| [==1,==0,==0,>=0]-> +(+(s(x),*(x,x695)),x695) -3|0[==1,==0,==0,>=0]-> +(+(x,s(*(x,x695))),x695) +(*(x,s(x695)),s(x695)) -5|0[==1,==0,==0,=?1]-> +(+(x,*(x,x695)),s(x695)) -1| [==1,==0,==0,>=0]-> +(x,+(*(x,x695),s(x695))) -4|1[==1,==0,==0,>=0]-> +(x,+(s(*(x,x695)),x695)) -0| [==1,==0,==0,>=0]-> +(+(x,s(*(x,x695))),x695) peak: +(x,*(x,x697)) <-5|[==1,==0,==0,=>1]- *(x,s(x697)) -7|[ ==1,==0,==0,?=9]-> *(s(x697),x) joins (1): +(x,*(x,x697)) -7|1[==1,==0,==0,?=9]-> +(x,*(x697,x)) *(s(x697),x) -6|[==1,==0,==0,>>0]-> +(*(x697,x),x) -2|[ ==1,==0,==0,>>0]-> +(x,*(x697,x)) peak: +(*(x698,s(y)),s(y)) <-6|[==1,==0,==0,=>0]- *(s(x698),s(y)) -5| [==1,==0,==0,?=1]-> +(s(x698),*(s(x698),y)) joins (1): +(*(x698,s(y)),s(y)) -5|0[==1,==0,==0,?=1]-> +(+(x698,*(x698,y)),s(y)) -1| [==1,==0,==0,=>0]-> +(x698,+(*(x698,y),s(y))) -4|1[==1,==0,==0,=>0]-> +(x698,+(s(*(x698,y)),y)) +(s(x698),*(s(x698),y)) -6|1[==1,==0,==0,=>0]-> +(s(x698),+(*(x698,y),y)) -0| [==1,==0,==0,=>0]-> +(+(s(x698),*(x698,y)),y) -3|0[==1,==0,==0,=>0]-> +(+(x698,s(*(x698,y))),y) -1| [==1,==0,==0,=>0]-> +(x698,+(s(*(x698,y)),y)) peak: +(*(x700,y),y) <-6|[==1,==0,==0,=>0]- *(s(x700),y) -7|[ ==1,==0,==0,?=9]-> *(y,s(x700)) joins (1): +(*(x700,y),y) -7|0[==1,==0,==0,?=9]-> +(*(y,x700),y) *(y,s(x700)) -5|[==1,==0,==0,?>1]-> +(y,*(y,x700)) -2|[ ==1,==0,==0,=>0]-> +(*(y,x700),y) peak: *(s(y),x) <-7|[==1,==0,==0,=?9]- *(x,s(y)) -5|[==1,==0,==0,>=1]-> +(x,*(x,y)) joins (1): *(s(y),x) -6|[==1,==0,==0,>>0]-> +(*(y,x),x) +(x,*(x,y)) -2|[==1,==0,==0,>>0]-> +(*(x,y),x) -7|0[==1,==0,==0,=?9]-> +(*(y,x),x) peak: *(y,s(x)) <-7|[==1,==0,==0,=?9]- *(s(x),y) -6|[==1,==0,==0,>=0]-> +(*(x,y),y) joins (1): *(y,s(x)) -5|[==1,==0,==0,>?1]-> +(y,*(y,x)) +(*(x,y),y) -7|0[==1,==0,==0,=?9]-> +(*(y,x),y) -2|[==1,==0,==0,>=0]-> +(y,*(y,x)) Qed