YES 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))), +(*(x713,x713),s(+(x713,x713))) = *(s(x713),s(x713)) 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 (dup): strict: *(x,s(y)) -> +(x,*(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,y) -> *(y,x) 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) Polynomial Interpretation Processor: dimension: 1 interpretation: [s](x0) = x0 + 1, [+](x0, x1) = x0 + x1, [*](x0, x1) = 2x0 + 2x1 + 2x0x0 + 2x1x0 + 2x1x1 orientation: *(x,s(y)) = 4x + 2x*x + 2x*y + 6y + 2y*y + 4 >= 3x + 2x*x + 2x*y + 2y + 2y*y = +(x,*(x,y)) *(s(x),y) = 6x + 2x*x + 2x*y + 4y + 2y*y + 4 >= 2x + 2x*x + 2x*y + 3y + 2y*y = +(*(x,y),y) +(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,y) = 2x + 2x*x + 2x*y + 2y + 2y*y >= 2x + 2x*x + 2x*y + 2y + 2y*y = *(y,x) problem: strict: 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,y) -> *(y,x) Shift Processor (no label): 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]- +(x,+(y,+(x633,x634))) -0| [==1,==0]-> +(+(x,y),+(x633,x634)) joins (1): +(x,+(+(y,x633),x634)) -1|1[==1,==0]-> +(x,+(y,+(x633,x634))) +(+(x,y),+(x633,x634)) -1|[==1,==0]-> +(x,+(y,+(x633,x634))) peak: +(+(+(x,y),x636),x637) <-0|[==1,==0]- +(+(x,y),+(x636,x637)) -1| [==1,==0]-> +(x,+(y,+(x636,x637))) joins (1): +(+(+(x,y),x636),x637) -1|[==1,==0]-> +(+(x,y),+(x636,x637)) +(x,+(y,+(x636,x637))) -0|[==1,==0]-> +(+(x,y),+(x636,x637)) peak: +(+(+(x,x639),x640),z) <-0|0[==1,==0]- +(+(x,+(x639,x640)),z) -1| [==1,==0]-> +(x,+(+(x639,x640),z)) joins (1): +(+(+(x,x639),x640),z) -1|0[==1,==0]-> +(+(x,+(x639,x640)),z) +(x,+(+(x639,x640),z)) -0|[==1,==0]-> +(+(x,+(x639,x640)),z) peak: +(+(x,x642),x643) <-0|[==1,==0]- +(x,+(x642,x643)) -2|[==1,==0]-> +(+(x642,x643),x) joins (1): +(+(x,x642),x643) -1|[==1,==0]-> +(x,+(x642,x643)) +(+(x642,x643),x) -2|[==1,==0]-> +(x,+(x642,x643)) peak: +(+(s(x),x645),x646) <-0|[==1,==0]- +(s(x),+(x645,x646)) -3| [==1,==0]-> +(x,s(+(x645,x646))) joins (1): +(+(s(x),x645),x646) -1|[==1,==0]-> +(s(x),+(x645,x646)) +(x,s(+(x645,x646))) -4|[==1,==0]-> +(s(x),+(x645,x646)) peak: +(x647,+(x648,+(y,z))) <-1|[==1,==0]- +(+(x647,x648),+(y,z)) -0| [==1,==0]-> +(+(+(x647,x648),y),z) joins (1): +(x647,+(x648,+(y,z))) -0|[==1,==0]-> +(+(x647,x648),+(y,z)) +(+(+(x647,x648),y),z) -1|[==1,==0]-> +(+(x647,x648),+(y,z)) peak: +(x,+(x650,+(x651,z))) <-1|1[==1,==0]- +(x,+(+(x650,x651),z)) -0| [==1,==0]-> +(+(x,+(x650,x651)),z) joins (1): +(x,+(x650,+(x651,z))) -0|1[==1,==0]-> +(x,+(+(x650,x651),z)) +(+(x,+(x650,x651)),z) -1|[==1,==0]-> +(x,+(+(x650,x651),z)) peak: +(+(x653,+(x654,y)),z) <-1|0[==1,==0]- +(+(+(x653,x654),y),z) -1| [==1,==0]-> +(+(x653,x654),+(y,z)) joins (1): +(+(x653,+(x654,y)),z) -0|0[==1,==0]-> +(+(+(x653,x654),y),z) +(+(x653,x654),+(y,z)) -0|[==1,==0]-> +(+(+(x653,x654),y),z) peak: +(x656,+(x657,y)) <-1|[==1,==0]- +(+(x656,x657),y) -2|[==1,==0]-> +(y,+(x656,x657)) joins (1): +(x656,+(x657,y)) -0|[==1,==0]-> +(+(x656,x657),y) +(y,+(x656,x657)) -2|[==1,==0]-> +(+(x656,x657),y) peak: +(x659,+(x660,s(y))) <-1|[==1,==0]- +(+(x659,x660),s(y)) -4| [==1,==0]-> +(s(+(x659,x660)),y) joins (1): +(x659,+(x660,s(y))) -0|[==1,==0]-> +(+(x659,x660),s(y)) +(s(+(x659,x660)),y) -3|[==1,==0]-> +(+(x659,x660),s(y)) peak: +(+(y,z),x) <-2|[==1,==0]- +(x,+(y,z)) -0|[==1,==0]-> +(+(x,y),z) joins (1): +(+(y,z),x) -2|[==1,==0]-> +(x,+(y,z)) +(+(x,y),z) -1|[==1,==0]-> +(x,+(y,z)) peak: +(x,+(z,y)) <-2|1[==1,==0]- +(x,+(y,z)) -0|[==1,==0]-> +(+(x,y),z) joins (1): +(x,+(z,y)) -2|1[==1,==0]-> +(x,+(y,z)) +(+(x,y),z) -1|[==1,==0]-> +(x,+(y,z)) peak: +(z,+(x,y)) <-2|[==1,==0]- +(+(x,y),z) -1|[==1,==0]-> +(x,+(y,z)) joins (1): +(z,+(x,y)) -2|[==1,==0]-> +(+(x,y),z) +(x,+(y,z)) -0|[==1,==0]-> +(+(x,y),z) peak: +(+(y,x),z) <-2|0[==1,==0]- +(+(x,y),z) -1|[==1,==0]-> +(x,+(y,z)) joins (1): +(+(y,x),z) -2|0[==1,==0]-> +(+(x,y),z) +(x,+(y,z)) -0|[==1,==0]-> +(+(x,y),z) peak: +(y,s(x)) <-2|[==1,==0]- +(s(x),y) -3|[==1,==0]-> +(x,s(y)) joins (1): +(y,s(x)) -2|[==1,==0]-> +(s(x),y) +(x,s(y)) -4|[==1,==0]-> +(s(x),y) peak: +(s(y),x) <-2|[==1,==0]- +(x,s(y)) -4|[==1,==0]-> +(s(x),y) joins (1): +(s(y),x) -2|[==1,==0]-> +(x,s(y)) +(s(x),y) -3|[==1,==0]-> +(x,s(y)) peak: +(x674,s(+(y,z))) <-3|[==1,==0]- +(s(x674),+(y,z)) -0|[==1,==0]-> +(+(s(x674),y),z) joins (1): +(x674,s(+(y,z))) -4|[==1,==0]-> +(s(x674),+(y,z)) +(+(s(x674),y),z) -1|[==1,==0]-> +(s(x674),+(y,z)) peak: +(x,+(x676,s(z))) <-3|1[==1,==0]- +(x,+(s(x676),z)) -0|[==1,==0]-> +(+(x,s(x676)),z) joins (1): +(x,+(x676,s(z))) -4|1[==1,==0]-> +(x,+(s(x676),z)) +(+(x,s(x676)),z) -1|[==1,==0]-> +(x,+(s(x676),z)) peak: +(+(x678,s(y)),z) <-3|0[==1,==0]- +(+(s(x678),y),z) -1|[==1,==0]-> +(s(x678),+(y,z)) joins (1): +(+(x678,s(y)),z) -4|0[==1,==0]-> +(+(s(x678),y),z) +(s(x678),+(y,z)) -0|[==1,==0]-> +(+(s(x678),y),z) peak: +(x680,s(y)) <-3|[==1,==0]- +(s(x680),y) -2|[==1,==0]-> +(y,s(x680)) joins (1): +(x680,s(y)) -2|[==1,==0]-> +(s(y),x680) +(y,s(x680)) -4|[==1,==0]-> +(s(y),x680) peak: +(x682,s(s(y))) <-3|[==1,==0]- +(s(x682),s(y)) -4|[==1,==0]-> +(s(s(x682)),y) joins (1): +(x682,s(s(y))) -4|[==1,==0]-> +(s(x682),s(y)) +(s(s(x682)),y) -3|[==1,==0]-> +(s(x682),s(y)) peak: +(x,+(s(y),x685)) <-4|1[==1,==0]- +(x,+(y,s(x685))) -0|[==1,==0]-> +(+(x,y),s(x685)) joins (1): +(x,+(s(y),x685)) -3|1[==1,==0]-> +(x,+(y,s(x685))) +(+(x,y),s(x685)) -1|[==1,==0]-> +(x,+(y,s(x685))) peak: +(s(+(x,y)),x687) <-4|[==1,==0]- +(+(x,y),s(x687)) -1|[==1,==0]-> +(x,+(y,s(x687))) joins (1): +(s(+(x,y)),x687) -3|[==1,==0]-> +(+(x,y),s(x687)) +(x,+(y,s(x687))) -0|[==1,==0]-> +(+(x,y),s(x687)) peak: +(+(s(x),x689),z) <-4|0[==1,==0]- +(+(x,s(x689)),z) -1|[==1,==0]-> +(x,+(s(x689),z)) joins (1): +(+(s(x),x689),z) -3|0[==1,==0]-> +(+(x,s(x689)),z) +(x,+(s(x689),z)) -0|[==1,==0]-> +(+(x,s(x689)),z) peak: +(s(x),x691) <-4|[==1,==0]- +(x,s(x691)) -2|[==1,==0]-> +(s(x691),x) joins (1): +(s(x),x691) -2|[==1,==0]-> +(x691,s(x)) +(s(x691),x) -3|[==1,==0]-> +(x691,s(x)) peak: +(s(s(x)),x693) <-4|[==1,==0]- +(s(x),s(x693)) -3|[==1,==0]-> +(x,s(s(x693))) joins (1): +(s(s(x)),x693) -3|[==1,==0]-> +(s(x),s(x693)) +(x,s(s(x693))) -4|[==1,==0]-> +(s(x),s(x693)) peak: +(s(x),*(s(x),x695)) <-5|[==1,=?1]- *(s(x),s(x695)) -6|[ ==1,>=0]-> +(*(x,s(x695)),s(x695)) joins (1): +(s(x),*(s(x),x695)) -6|1[==1,>=0]-> +(s(x),+(*(x,x695),x695)) -0|[==1,>=0]-> +(+(s(x),*(x,x695)),x695) -3|0[==1,>=0]-> +(+(x,s(*(x,x695))),x695) +(*(x,s(x695)),s(x695)) -5|0[==1,=?1]-> +(+(x,*(x,x695)),s(x695)) -1|[==1,>=0]-> +(x,+(*(x,x695),s(x695))) -4|1[==1,>=0]-> +(x,+(s(*(x,x695)),x695)) -0| [==1,>=0]-> +(+(x,s(*(x,x695))),x695) peak: +(x,*(x,x697)) <-5|[==1,=>1]- *(x,s(x697)) -7|[==1,?=9]-> *(s(x697),x) joins (1): +(x,*(x,x697)) -7|1[==1,?=9]-> +(x,*(x697,x)) *(s(x697),x) -6|[==1,>>0]-> +(*(x697,x),x) -2|[==1,>>0]-> +(x,*(x697,x)) peak: +(*(x698,s(y)),s(y)) <-6|[==1,=>0]- *(s(x698),s(y)) -5|[ ==1,?=1]-> +(s(x698),*(s(x698),y)) joins (1): +(*(x698,s(y)),s(y)) -5|0[==1,?=1]-> +(+(x698,*(x698,y)),s(y)) -1|[==1,=>0]-> +(x698,+(*(x698,y),s(y))) -4|1[==1,=>0]-> +(x698,+(s(*(x698,y)),y)) +(s(x698),*(s(x698),y)) -6|1[==1,=>0]-> +(s(x698),+(*(x698,y),y)) -0|[==1,=>0]-> +(+(s(x698),*(x698,y)),y) -3|0[==1,=>0]-> +(+(x698,s(*(x698,y))),y) -1| [==1,=>0]-> +(x698,+(s(*(x698,y)),y)) peak: +(*(x700,y),y) <-6|[==1,=>0]- *(s(x700),y) -7|[==1,?=9]-> *(y,s(x700)) joins (1): +(*(x700,y),y) -7|0[==1,?=9]-> +(*(y,x700),y) *(y,s(x700)) -5|[==1,?>1]-> +(y,*(y,x700)) -2|[==1,=>0]-> +(*(y,x700),y) peak: *(s(y),x) <-7|[==1,=?9]- *(x,s(y)) -5|[==1,>=1]-> +(x,*(x,y)) joins (1): *(s(y),x) -6|[==1,>>0]-> +(*(y,x),x) +(x,*(x,y)) -2|[==1,>>0]-> +(*(x,y),x) -7|0[==1,=?9]-> +(*(y,x),x) peak: *(y,s(x)) <-7|[==1,=?9]- *(s(x),y) -6|[==1,>=0]-> +(*(x,y),y) joins (1): *(y,s(x)) -5|[==1,>?1]-> +(y,*(y,x)) +(*(x,y),y) -7|0[==1,=?9]-> +(*(y,x),y) -2|[==1,>=0]-> +(y,*(y,x)) Qed