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) = 3x0 + 2x0x0 + 2, [+](x0, x1) = x0 + x1, [*](x0, x1) = x0 + x1 + 2x1x0 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)) = 3x + 2x*y + y + 1 >= 2x + 2x*y + y = +(x,*(x,y)) *(s(x),y) = x + 2x*y + 3y + 1 >= x + 2x*y + 2y = +(*(x,y),y) *(x,y) = x + 2x*y + y >= x + 2x*y + y = *(y,x) sq(x) = 3x + 2x*x + 2 >= 2x + 2x*x = *(x,x) sq(s(x)) = 7x + 2x*x + 7 >= 4x + 2x*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))), +(*(x701,x701),s(+(x701,x701))) = *(s(x701),s(x701)) 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,x621),x622)) <-0|1[]- +(x,+(y,+(x621,x622))) -0|[]-> +(+(x,y),+(x621,x622)) +(+(+(x,y),x624),x625) <-0|[]- +(+(x,y),+(x624,x625)) -1|[]-> +(x,+(y,+(x624,x625))) +(+(+(x,x627),x628),z) <-0|0[]- +(+(x,+(x627,x628)),z) -1|[]-> +(x,+(+(x627,x628),z)) +(+(x,x630),x631) <-0|[]- +(x,+(x630,x631)) -2|[]-> +(+(x630,x631),x) +(+(s(x),x633),x634) <-0|[]- +(s(x),+(x633,x634)) -3|[]-> +(x,s(+(x633,x634))) +(x635,+(x636,+(y,z))) <-1|[]- +(+(x635,x636),+(y,z)) -0|[]-> +(+(+(x635,x636),y),z) +(x,+(x638,+(x639,z))) <-1|1[]- +(x,+(+(x638,x639),z)) -0|[]-> +(+(x,+(x638,x639)),z) +(+(x641,+(x642,y)),z) <-1|0[]- +(+(+(x641,x642),y),z) -1|[]-> +(+(x641,x642),+(y,z)) +(x644,+(x645,y)) <-1|[]- +(+(x644,x645),y) -2|[]-> +(y,+(x644,x645)) +(x647,+(x648,s(y))) <-1|[]- +(+(x647,x648),s(y)) -4|[]-> +(s(+(x647,x648)),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) +(x662,s(+(y,z))) <-3|[]- +(s(x662),+(y,z)) -0|[]-> +(+(s(x662),y),z) +(x,+(x664,s(z))) <-3|1[]- +(x,+(s(x664),z)) -0|[]-> +(+(x,s(x664)),z) +(+(x666,s(y)),z) <-3|0[]- +(+(s(x666),y),z) -1|[]-> +(s(x666),+(y,z)) +(x668,s(y)) <-3|[]- +(s(x668),y) -2|[]-> +(y,s(x668)) +(x670,s(s(y))) <-3|[]- +(s(x670),s(y)) -4|[]-> +(s(s(x670)),y) +(x,+(s(y),x673)) <-4|1[]- +(x,+(y,s(x673))) -0|[]-> +(+(x,y),s(x673)) +(s(+(x,y)),x675) <-4|[]- +(+(x,y),s(x675)) -1|[]-> +(x,+(y,s(x675))) +(+(s(x),x677),z) <-4|0[]- +(+(x,s(x677)),z) -1|[]-> +(x,+(s(x677),z)) +(s(x),x679) <-4|[]- +(x,s(x679)) -2|[]-> +(s(x679),x) +(s(s(x)),x681) <-4|[]- +(s(x),s(x681)) -3|[]-> +(x,s(s(x681))) +(s(x),*(s(x),x683)) <-5|[]- *(s(x),s(x683)) -6|[]-> +(*(x,s(x683)),s(x683)) +(x,*(x,x685)) <-5|[]- *(x,s(x685)) -7|[]-> *(s(x685),x) +(*(x686,s(y)),s(y)) <-6|[]- *(s(x686),s(y)) -5|[]-> +(s(x686),*(s(x686),y)) +(*(x688,y),y) <-6|[]- *(s(x688),y) -7|[]-> *(y,s(x688)) *(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 + 2, [+](x0, x1) = x0 + x1, [*](x0, x1) = 2x0 + 2x1 + x0x0 + 2x1x0 + x1x1 orientation: *(x,s(y)) = 6x + x*x + 2x*y + 6y + y*y + 8 >= 3x + x*x + 2x*y + 2y + y*y = +(x,*(x,y)) *(s(x),y) = 6x + x*x + 2x*y + 6y + y*y + 8 >= 2x + x*x + 2x*y + 3y + y*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 + 2 >= x + y + 2 = +(x,s(y)) +(x,s(y)) = x + y + 2 >= x + y + 2 = +(s(x),y) *(x,y) = 2x + x*x + 2x*y + 2y + y*y >= 2x + x*x + 2x*y + 2y + y*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,+(x621,x622))) -> +(x,+(+(y,x621),x622)) +(x,+(y,+(x621,x622))) -> +(+(x,y),+(x621,x622)) +(x,+(+(y,x621),x622)) -> +(x,+(y,+(x621,x622))) +(+(x,y),+(x621,x622)) -> +(x,+(y,+(x621,x622))) +(+(x,y),+(x624,x625)) -> +(+(+(x,y),x624),x625) +(+(x,y),+(x624,x625)) -> +(x,+(y,+(x624,x625))) +(+(+(x,y),x624),x625) -> +(+(x,y),+(x624,x625)) +(x,+(y,+(x624,x625))) -> +(+(x,y),+(x624,x625)) +(+(x,+(x627,x628)),z) -> +(+(+(x,x627),x628),z) +(+(x,+(x627,x628)),z) -> +(x,+(+(x627,x628),z)) +(+(+(x,x627),x628),z) -> +(+(x,+(x627,x628)),z) +(x,+(+(x627,x628),z)) -> +(+(x,+(x627,x628)),z) +(x,+(x630,x631)) -> +(+(x,x630),x631) +(x,+(x630,x631)) -> +(+(x630,x631),x) +(+(x,x630),x631) -> +(x,+(x630,x631)) +(+(x630,x631),x) -> +(x,+(x630,x631)) +(s(x),+(x633,x634)) -> +(+(s(x),x633),x634) +(s(x),+(x633,x634)) -> +(x,s(+(x633,x634))) +(+(s(x),x633),x634) -> +(s(x),+(x633,x634)) +(x,s(+(x633,x634))) -> +(s(x),+(x633,x634)) +(+(x635,x636),+(y,z)) -> +(x635,+(x636,+(y,z))) +(+(x635,x636),+(y,z)) -> +(+(+(x635,x636),y),z) +(x635,+(x636,+(y,z))) -> +(+(x635,x636),+(y,z)) +(+(+(x635,x636),y),z) -> +(+(x635,x636),+(y,z)) +(x,+(+(x638,x639),z)) -> +(x,+(x638,+(x639,z))) +(x,+(+(x638,x639),z)) -> +(+(x,+(x638,x639)),z) +(x,+(x638,+(x639,z))) -> +(x,+(+(x638,x639),z)) +(+(x,+(x638,x639)),z) -> +(x,+(+(x638,x639),z)) +(+(+(x641,x642),y),z) -> +(+(x641,+(x642,y)),z) +(+(+(x641,x642),y),z) -> +(+(x641,x642),+(y,z)) +(+(x641,+(x642,y)),z) -> +(+(+(x641,x642),y),z) +(+(x641,x642),+(y,z)) -> +(+(+(x641,x642),y),z) +(+(x644,x645),y) -> +(x644,+(x645,y)) +(+(x644,x645),y) -> +(y,+(x644,x645)) +(x644,+(x645,y)) -> +(+(x644,x645),y) +(y,+(x644,x645)) -> +(+(x644,x645),y) +(+(x647,x648),s(y)) -> +(x647,+(x648,s(y))) +(+(x647,x648),s(y)) -> +(s(+(x647,x648)),y) +(x647,+(x648,s(y))) -> +(+(x647,x648),s(y)) +(s(+(x647,x648)),y) -> +(+(x647,x648),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(x662),+(y,z)) -> +(x662,s(+(y,z))) +(s(x662),+(y,z)) -> +(+(s(x662),y),z) +(x662,s(+(y,z))) -> +(s(x662),+(y,z)) +(+(s(x662),y),z) -> +(s(x662),+(y,z)) +(x,+(s(x664),z)) -> +(x,+(x664,s(z))) +(x,+(s(x664),z)) -> +(+(x,s(x664)),z) +(x,+(x664,s(z))) -> +(x,+(s(x664),z)) +(+(x,s(x664)),z) -> +(x,+(s(x664),z)) +(+(s(x666),y),z) -> +(+(x666,s(y)),z) +(+(s(x666),y),z) -> +(s(x666),+(y,z)) +(+(x666,s(y)),z) -> +(+(s(x666),y),z) +(s(x666),+(y,z)) -> +(+(s(x666),y),z) +(s(x668),y) -> +(x668,s(y)) +(s(x668),y) -> +(y,s(x668)) +(x668,s(y)) -> +(s(y),x668) +(y,s(x668)) -> +(s(y),x668) +(x668,s(y)) -> +(s(x668),y) +(y,s(x668)) -> +(s(x668),y) +(s(x670),s(y)) -> +(x670,s(s(y))) +(s(x670),s(y)) -> +(s(s(x670)),y) +(x670,s(s(y))) -> +(s(x670),s(y)) +(s(s(x670)),y) -> +(s(x670),s(y)) +(x,+(y,s(x673))) -> +(x,+(s(y),x673)) +(x,+(y,s(x673))) -> +(+(x,y),s(x673)) +(x,+(s(y),x673)) -> +(x,+(y,s(x673))) +(+(x,y),s(x673)) -> +(x,+(y,s(x673))) +(+(x,y),s(x675)) -> +(s(+(x,y)),x675) +(+(x,y),s(x675)) -> +(x,+(y,s(x675))) +(s(+(x,y)),x675) -> +(+(x,y),s(x675)) +(x,+(y,s(x675))) -> +(+(x,y),s(x675)) +(+(x,s(x677)),z) -> +(+(s(x),x677),z) +(+(x,s(x677)),z) -> +(x,+(s(x677),z)) +(+(s(x),x677),z) -> +(+(x,s(x677)),z) +(x,+(s(x677),z)) -> +(+(x,s(x677)),z) +(x,s(x679)) -> +(s(x),x679) +(x,s(x679)) -> +(s(x679),x) +(s(x),x679) -> +(x679,s(x)) +(s(x679),x) -> +(x679,s(x)) +(s(x),x679) -> +(x,s(x679)) +(s(x679),x) -> +(x,s(x679)) +(s(x),s(x681)) -> +(s(s(x)),x681) +(s(x),s(x681)) -> +(x,s(s(x681))) +(s(s(x)),x681) -> +(s(x),s(x681)) +(x,s(s(x681))) -> +(s(x),s(x681)) *(s(x),s(x683)) -> +(s(x),*(s(x),x683)) *(s(x),s(x683)) -> +(*(x,s(x683)),s(x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(s(x),*(x,x683)),x683) +(+(s(x),*(x,x683)),x683) -> +(+(x,s(*(x,x683))),x683) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(x,+(*(x,x683),s(x683))) +(x,+(*(x,x683),s(x683))) -> +(x,+(s(*(x,x683)),x683)) +(x,+(s(*(x,x683)),x683)) -> +(+(x,s(*(x,x683))),x683) +(s(x),*(s(x),x683)) -> +(*(s(x),x683),s(x)) +(*(s(x),x683),s(x)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x),x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(+(*(x,x683),x),s(x683)) +(+(*(x,x683),x),s(x683)) -> +(*(x,x683),+(x,s(x683))) +(*(x,x683),+(x,s(x683))) -> +(*(x,x683),+(s(x),x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x),x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(+(*(x,x683),x),s(x683)) +(+(*(x,x683),x),s(x683)) -> +(*(x,x683),+(x,s(x683))) +(*(x,x683),+(x,s(x683))) -> +(*(x,x683),+(s(x),x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(s(x),*(x,x683)),x683) +(+(s(x),*(x,x683)),x683) -> +(+(*(x,x683),s(x)),x683) +(+(*(x,x683),s(x)),x683) -> +(*(x,x683),+(s(x),x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(+(*(x,x683),x),s(x683)) +(+(*(x,x683),x),s(x683)) -> +(*(x,x683),+(x,s(x683))) +(*(x,x683),+(x,s(x683))) -> +(*(x,x683),+(s(x),x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(s(x),+(x683,*(x,x683))) +(s(x),+(x683,*(x,x683))) -> +(+(s(x),x683),*(x,x683)) +(+(s(x),x683),*(x,x683)) -> +(*(x,x683),+(s(x),x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(+(*(x,x683),x),s(x683)) +(+(*(x,x683),x),s(x683)) -> +(*(x,x683),+(x,s(x683))) +(*(x,x683),+(x,s(x683))) -> +(*(x,x683),+(s(x),x683)) +(s(x),*(s(x),x683)) -> +(*(s(x),x683),s(x)) +(*(s(x),x683),s(x)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(s(x683),*(x,s(x683))) +(s(x683),*(x,s(x683))) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(*(s(x),x683),s(x)) +(*(s(x),x683),s(x)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(s(x683),*(x,s(x683))) +(s(x683),*(x,s(x683))) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(s(x),*(x,x683)),x683) +(+(s(x),*(x,x683)),x683) -> +(x683,+(s(x),*(x,x683))) +(x683,+(s(x),*(x,x683))) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(s(x683),*(x,s(x683))) +(s(x683),*(x,s(x683))) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(s(x),*(x,x683)),x683) +(+(s(x),*(x,x683)),x683) -> +(x683,+(s(x),*(x,x683))) +(x683,+(s(x),*(x,x683))) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(s(x),+(x683,*(x,x683))) +(s(x),+(x683,*(x,x683))) -> +(+(s(x),x683),*(x,x683)) +(+(s(x),x683),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(s(x683),*(x,s(x683))) +(s(x683),*(x,s(x683))) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(s(x),+(x683,*(x,x683))) +(s(x),+(x683,*(x,x683))) -> +(+(s(x),x683),*(x,x683)) +(+(s(x),x683),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x683,s(x)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(*(s(x),x683),s(x)) +(*(s(x),x683),s(x)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(s(x683),*(x,s(x683))) +(s(x683),*(x,s(x683))) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(*(s(x),x683),s(x)) +(*(s(x),x683),s(x)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(*(s(x),x683),s(x)) +(*(s(x),x683),s(x)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(x,+(*(x,x683),s(x683))) +(x,+(*(x,x683),s(x683))) -> +(+(*(x,x683),s(x683)),x) +(+(*(x,x683),s(x683)),x) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(*(s(x),x683),s(x)) +(*(s(x),x683),s(x)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(+(*(x,x683),x),s(x683)) +(+(*(x,x683),x),s(x683)) -> +(*(x,x683),+(x,s(x683))) +(*(x,x683),+(x,s(x683))) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(s(x683),*(x,s(x683))) +(s(x683),*(x,s(x683))) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(x,+(*(x,x683),s(x683))) +(x,+(*(x,x683),s(x683))) -> +(+(*(x,x683),s(x683)),x) +(+(*(x,x683),s(x683)),x) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(*(x,x683),x683),s(x)) +(+(*(x,x683),x683),s(x)) -> +(*(x,x683),+(x683,s(x))) +(*(x,x683),+(x683,s(x))) -> +(*(x,x683),+(s(x683),x)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(+(*(x,x683),x),s(x683)) +(+(*(x,x683),x),s(x683)) -> +(*(x,x683),+(x,s(x683))) +(*(x,x683),+(x,s(x683))) -> +(*(x,x683),+(s(x683),x)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(+(s(x),*(x,x683)),x683) +(+(s(x),*(x,x683)),x683) -> +(+(x,s(*(x,x683))),x683) +(+(x,s(*(x,x683))),x683) -> +(x,+(s(*(x,x683)),x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(x,+(*(x,x683),s(x683))) +(x,+(*(x,x683),s(x683))) -> +(x,+(s(*(x,x683)),x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(s(x),+(x683,*(x,x683))) +(s(x),+(x683,*(x,x683))) -> +(+(s(x),x683),*(x,x683)) +(+(s(x),x683),*(x,x683)) -> +(+(x,s(x683)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(s(x683),*(x,s(x683))) +(s(x683),*(x,s(x683))) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x,s(x683)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(s(x),+(x683,*(x,x683))) +(s(x),+(x683,*(x,x683))) -> +(+(s(x),x683),*(x,x683)) +(+(s(x),x683),*(x,x683)) -> +(+(x,s(x683)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(s(x683),+(x,*(x,x683))) +(s(x683),+(x,*(x,x683))) -> +(+(s(x683),x),*(x,x683)) +(+(s(x683),x),*(x,x683)) -> +(+(x,s(x683)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(s(x),+(x683,*(x,x683))) +(s(x),+(x683,*(x,x683))) -> +(+(s(x),x683),*(x,x683)) +(+(s(x),x683),*(x,x683)) -> +(+(x,s(x683)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(x,+(*(x,x683),s(x683))) +(x,+(*(x,x683),s(x683))) -> +(x,+(s(x683),*(x,x683))) +(x,+(s(x683),*(x,x683))) -> +(+(x,s(x683)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),+(*(x,x683),x683)) +(s(x),+(*(x,x683),x683)) -> +(s(x),+(x683,*(x,x683))) +(s(x),+(x683,*(x,x683))) -> +(+(s(x),x683),*(x,x683)) +(+(s(x),x683),*(x,x683)) -> +(+(x,s(x683)),*(x,x683)) +(*(x,s(x683)),s(x683)) -> +(+(x,*(x,x683)),s(x683)) +(+(x,*(x,x683)),s(x683)) -> +(+(*(x,x683),x),s(x683)) +(+(*(x,x683),x),s(x683)) -> +(*(x,x683),+(x,s(x683))) +(*(x,x683),+(x,s(x683))) -> +(+(x,s(x683)),*(x,x683)) +(s(x),*(s(x),x683)) -> +(s(x),*(x683,s(x))) +(s(x),*(x683,s(x))) -> +(s(x),+(x683,*(x683,x))) +(s(x),+(x683,*(x683,x))) -> +(+(s(x),x683),*(x683,x)) +(+(s(x),x683),*(x683,x)) -> +(*(x683,x),+(s(x),x683)) +(*(x,s(x683)),s(x683)) -> +(*(s(x683),x),s(x683)) +(*(s(x683),x),s(x683)) -> +(+(*(x683,x),x),s(x683)) +(+(*(x683,x),x),s(x683)) -> +(*(x683,x),+(x,s(x683))) +(*(x683,x),+(x,s(x683))) -> +(*(x683,x),+(s(x),x683)) +(s(x),*(s(x),x683)) -> +(s(x),*(x683,s(x))) +(s(x),*(x683,s(x))) -> +(s(x),+(x683,*(x683,x))) +(s(x),+(x683,*(x683,x))) -> +(+(s(x),x683),*(x683,x)) +(+(s(x),x683),*(x683,x)) -> +(+(x,s(x683)),*(x683,x)) +(*(x,s(x683)),s(x683)) -> +(*(s(x683),x),s(x683)) +(*(s(x683),x),s(x683)) -> +(+(*(x683,x),x),s(x683)) +(+(*(x683,x),x),s(x683)) -> +(*(x683,x),+(x,s(x683))) +(*(x683,x),+(x,s(x683))) -> +(+(x,s(x683)),*(x683,x)) *(x,s(x685)) -> +(x,*(x,x685)) *(x,s(x685)) -> *(s(x685),x) *(s(x685),x) -> *(x,s(x685)) *(x,s(x685)) -> +(x,*(x,x685)) +(x,*(x,x685)) -> +(*(x,x685),x) *(s(x685),x) -> +(*(x685,x),x) +(*(x685,x),x) -> +(*(x,x685),x) +(x,*(x,x685)) -> +(x,*(x685,x)) *(s(x685),x) -> +(*(x685,x),x) +(*(x685,x),x) -> +(x,*(x685,x)) +(x,*(x,x685)) -> +(*(x,x685),x) +(*(x,x685),x) -> +(*(x685,x),x) *(s(x685),x) -> +(*(x685,x),x) +(x,*(x,x685)) -> +(x,*(x685,x)) +(x,*(x685,x)) -> +(*(x685,x),x) *(s(x685),x) -> +(*(x685,x),x) *(s(x686),s(y)) -> +(*(x686,s(y)),s(y)) *(s(x686),s(y)) -> +(s(x686),*(s(x686),y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(x686,+(*(x686,y),s(y))) +(x686,+(*(x686,y),s(y))) -> +(x686,+(s(*(x686,y)),y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(s(x686),*(x686,y)),y) +(+(s(x686),*(x686,y)),y) -> +(+(x686,s(*(x686,y))),y) +(+(x686,s(*(x686,y))),y) -> +(x686,+(s(*(x686,y)),y)) +(*(x686,s(y)),s(y)) -> +(s(y),*(x686,s(y))) +(s(y),*(x686,s(y))) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(x686,s(y)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(s(x686),+(y,*(x686,y))) +(s(x686),+(y,*(x686,y))) -> +(+(s(x686),y),*(x686,y)) +(+(s(x686),y),*(x686,y)) -> +(+(x686,s(y)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(x686,s(y)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(s(x686),+(y,*(x686,y))) +(s(x686),+(y,*(x686,y))) -> +(+(s(x686),y),*(x686,y)) +(+(s(x686),y),*(x686,y)) -> +(+(x686,s(y)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(x686,+(*(x686,y),s(y))) +(x686,+(*(x686,y),s(y))) -> +(x686,+(s(y),*(x686,y))) +(x686,+(s(y),*(x686,y))) -> +(+(x686,s(y)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(s(x686),+(y,*(x686,y))) +(s(x686),+(y,*(x686,y))) -> +(+(s(x686),y),*(x686,y)) +(+(s(x686),y),*(x686,y)) -> +(+(x686,s(y)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(+(*(x686,y),x686),s(y)) +(+(*(x686,y),x686),s(y)) -> +(*(x686,y),+(x686,s(y))) +(*(x686,y),+(x686,s(y))) -> +(+(x686,s(y)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(s(x686),+(y,*(x686,y))) +(s(x686),+(y,*(x686,y))) -> +(+(s(x686),y),*(x686,y)) +(+(s(x686),y),*(x686,y)) -> +(+(x686,s(y)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(s(y),*(x686,s(y))) +(s(y),*(x686,s(y))) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(*(s(x686),y),s(x686)) +(*(s(x686),y),s(x686)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(s(y),*(x686,s(y))) +(s(y),*(x686,s(y))) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(*(s(x686),y),s(x686)) +(*(s(x686),y),s(x686)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(x686,+(*(x686,y),s(y))) +(x686,+(*(x686,y),s(y))) -> +(+(*(x686,y),s(y)),x686) +(+(*(x686,y),s(y)),x686) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(*(s(x686),y),s(x686)) +(*(s(x686),y),s(x686)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(x686,+(*(x686,y),s(y))) +(x686,+(*(x686,y),s(y))) -> +(+(*(x686,y),s(y)),x686) +(+(*(x686,y),s(y)),x686) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(+(*(x686,y),x686),s(y)) +(+(*(x686,y),x686),s(y)) -> +(*(x686,y),+(x686,s(y))) +(*(x686,y),+(x686,s(y))) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(*(s(x686),y),s(x686)) +(*(s(x686),y),s(x686)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(+(*(x686,y),x686),s(y)) +(+(*(x686,y),x686),s(y)) -> +(*(x686,y),+(x686,s(y))) +(*(x686,y),+(x686,s(y))) -> +(*(x686,y),+(s(y),x686)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(y),x686)) +(*(x686,s(y)),s(y)) -> +(s(y),*(x686,s(y))) +(s(y),*(x686,s(y))) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(*(s(x686),y),s(x686)) +(*(s(x686),y),s(x686)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(s(y),*(x686,s(y))) +(s(y),*(x686,s(y))) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(s(y),*(x686,s(y))) +(s(y),*(x686,s(y))) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(s(x686),*(x686,y)),y) +(+(s(x686),*(x686,y)),y) -> +(y,+(s(x686),*(x686,y))) +(y,+(s(x686),*(x686,y))) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(s(y),*(x686,s(y))) +(s(y),*(x686,s(y))) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(s(x686),+(y,*(x686,y))) +(s(x686),+(y,*(x686,y))) -> +(+(s(x686),y),*(x686,y)) +(+(s(x686),y),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(*(s(x686),y),s(x686)) +(*(s(x686),y),s(x686)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(s(x686),*(x686,y)),y) +(+(s(x686),*(x686,y)),y) -> +(y,+(s(x686),*(x686,y))) +(y,+(s(x686),*(x686,y))) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(s(y),+(x686,*(x686,y))) +(s(y),+(x686,*(x686,y))) -> +(+(s(y),x686),*(x686,y)) +(+(s(y),x686),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(s(x686),+(y,*(x686,y))) +(s(x686),+(y,*(x686,y))) -> +(+(s(x686),y),*(x686,y)) +(+(s(x686),y),*(x686,y)) -> +(+(y,s(x686)),*(x686,y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(x686,+(*(x686,y),s(y))) +(x686,+(*(x686,y),s(y))) -> +(x686,+(s(*(x686,y)),y)) +(x686,+(s(*(x686,y)),y)) -> +(+(x686,s(*(x686,y))),y) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(s(x686),*(x686,y)),y) +(+(s(x686),*(x686,y)),y) -> +(+(x686,s(*(x686,y))),y) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(+(*(x686,y),x686),s(y)) +(+(*(x686,y),x686),s(y)) -> +(*(x686,y),+(x686,s(y))) +(*(x686,y),+(x686,s(y))) -> +(*(x686,y),+(s(x686),y)) +(s(x686),*(s(x686),y)) -> +(*(s(x686),y),s(x686)) +(*(s(x686),y),s(x686)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(x686),y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(+(*(x686,y),x686),s(y)) +(+(*(x686,y),x686),s(y)) -> +(*(x686,y),+(x686,s(y))) +(*(x686,y),+(x686,s(y))) -> +(*(x686,y),+(s(x686),y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(*(x686,y),y),s(x686)) +(+(*(x686,y),y),s(x686)) -> +(*(x686,y),+(y,s(x686))) +(*(x686,y),+(y,s(x686))) -> +(*(x686,y),+(s(x686),y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(+(*(x686,y),x686),s(y)) +(+(*(x686,y),x686),s(y)) -> +(*(x686,y),+(x686,s(y))) +(*(x686,y),+(x686,s(y))) -> +(*(x686,y),+(s(x686),y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(+(s(x686),*(x686,y)),y) +(+(s(x686),*(x686,y)),y) -> +(+(*(x686,y),s(x686)),y) +(+(*(x686,y),s(x686)),y) -> +(*(x686,y),+(s(x686),y)) +(*(x686,s(y)),s(y)) -> +(+(x686,*(x686,y)),s(y)) +(+(x686,*(x686,y)),s(y)) -> +(+(*(x686,y),x686),s(y)) +(+(*(x686,y),x686),s(y)) -> +(*(x686,y),+(x686,s(y))) +(*(x686,y),+(x686,s(y))) -> +(*(x686,y),+(s(x686),y)) +(s(x686),*(s(x686),y)) -> +(s(x686),+(*(x686,y),y)) +(s(x686),+(*(x686,y),y)) -> +(s(x686),+(y,*(x686,y))) +(s(x686),+(y,*(x686,y))) -> +(+(s(x686),y),*(x686,y)) +(+(s(x686),y),*(x686,y)) -> +(*(x686,y),+(s(x686),y)) +(*(x686,s(y)),s(y)) -> +(*(s(y),x686),s(y)) +(*(s(y),x686),s(y)) -> +(+(*(y,x686),x686),s(y)) +(+(*(y,x686),x686),s(y)) -> +(*(y,x686),+(x686,s(y))) +(*(y,x686),+(x686,s(y))) -> +(+(x686,s(y)),*(y,x686)) +(s(x686),*(s(x686),y)) -> +(s(x686),*(y,s(x686))) +(s(x686),*(y,s(x686))) -> +(s(x686),+(y,*(y,x686))) +(s(x686),+(y,*(y,x686))) -> +(+(s(x686),y),*(y,x686)) +(+(s(x686),y),*(y,x686)) -> +(+(x686,s(y)),*(y,x686)) +(*(x686,s(y)),s(y)) -> +(*(s(y),x686),s(y)) +(*(s(y),x686),s(y)) -> +(+(*(y,x686),x686),s(y)) +(+(*(y,x686),x686),s(y)) -> +(*(y,x686),+(x686,s(y))) +(*(y,x686),+(x686,s(y))) -> +(*(y,x686),+(s(x686),y)) +(s(x686),*(s(x686),y)) -> +(s(x686),*(y,s(x686))) +(s(x686),*(y,s(x686))) -> +(s(x686),+(y,*(y,x686))) +(s(x686),+(y,*(y,x686))) -> +(+(s(x686),y),*(y,x686)) +(+(s(x686),y),*(y,x686)) -> +(*(y,x686),+(s(x686),y)) *(s(x688),y) -> +(*(x688,y),y) *(s(x688),y) -> *(y,s(x688)) *(y,s(x688)) -> *(s(x688),y) *(s(x688),y) -> +(*(x688,y),y) +(*(x688,y),y) -> +(y,*(x688,y)) *(y,s(x688)) -> +(y,*(y,x688)) +(y,*(y,x688)) -> +(y,*(x688,y)) +(*(x688,y),y) -> +(*(y,x688),y) *(y,s(x688)) -> +(y,*(y,x688)) +(y,*(y,x688)) -> +(*(y,x688),y) +(*(x688,y),y) -> +(y,*(x688,y)) +(y,*(x688,y)) -> +(y,*(y,x688)) *(y,s(x688)) -> +(y,*(y,x688)) +(*(x688,y),y) -> +(*(y,x688),y) +(*(y,x688),y) -> +(y,*(y,x688)) *(y,s(x688)) -> +(y,*(y,x688)) *(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,x621),x622)) <-0|1[==1,==0]- +(x,+(y,+(x621,x622))) -0| [==1,==0]-> +(+(x,y),+(x621,x622)) joins (1): +(x,+(+(y,x621),x622)) -1|1[==1,==0]-> +(x,+(y,+(x621,x622))) +(+(x,y),+(x621,x622)) -1|[==1,==0]-> +(x,+(y,+(x621,x622))) peak: +(+(+(x,y),x624),x625) <-0|[==1,==0]- +(+(x,y),+(x624,x625)) -1| [==1,==0]-> +(x,+(y,+(x624,x625))) joins (1): +(+(+(x,y),x624),x625) -1|[==1,==0]-> +(+(x,y),+(x624,x625)) +(x,+(y,+(x624,x625))) -0|[==1,==0]-> +(+(x,y),+(x624,x625)) peak: +(+(+(x,x627),x628),z) <-0|0[==1,==0]- +(+(x,+(x627,x628)),z) -1| [==1,==0]-> +(x,+(+(x627,x628),z)) joins (1): +(+(+(x,x627),x628),z) -1|0[==1,==0]-> +(+(x,+(x627,x628)),z) +(x,+(+(x627,x628),z)) -0|[==1,==0]-> +(+(x,+(x627,x628)),z) peak: +(+(x,x630),x631) <-0|[==1,==0]- +(x,+(x630,x631)) -2|[==1,==0]-> +(+(x630,x631),x) joins (1): +(+(x,x630),x631) -1|[==1,==0]-> +(x,+(x630,x631)) +(+(x630,x631),x) -2|[==1,==0]-> +(x,+(x630,x631)) peak: +(+(s(x),x633),x634) <-0|[==1,==0]- +(s(x),+(x633,x634)) -3| [==1,==0]-> +(x,s(+(x633,x634))) joins (1): +(+(s(x),x633),x634) -1|[==1,==0]-> +(s(x),+(x633,x634)) +(x,s(+(x633,x634))) -4|[==1,==0]-> +(s(x),+(x633,x634)) peak: +(x635,+(x636,+(y,z))) <-1|[==1,==0]- +(+(x635,x636),+(y,z)) -0| [==1,==0]-> +(+(+(x635,x636),y),z) joins (1): +(x635,+(x636,+(y,z))) -0|[==1,==0]-> +(+(x635,x636),+(y,z)) +(+(+(x635,x636),y),z) -1|[==1,==0]-> +(+(x635,x636),+(y,z)) peak: +(x,+(x638,+(x639,z))) <-1|1[==1,==0]- +(x,+(+(x638,x639),z)) -0| [==1,==0]-> +(+(x,+(x638,x639)),z) joins (1): +(x,+(x638,+(x639,z))) -0|1[==1,==0]-> +(x,+(+(x638,x639),z)) +(+(x,+(x638,x639)),z) -1|[==1,==0]-> +(x,+(+(x638,x639),z)) peak: +(+(x641,+(x642,y)),z) <-1|0[==1,==0]- +(+(+(x641,x642),y),z) -1| [==1,==0]-> +(+(x641,x642),+(y,z)) joins (1): +(+(x641,+(x642,y)),z) -0|0[==1,==0]-> +(+(+(x641,x642),y),z) +(+(x641,x642),+(y,z)) -0|[==1,==0]-> +(+(+(x641,x642),y),z) peak: +(x644,+(x645,y)) <-1|[==1,==0]- +(+(x644,x645),y) -2|[==1,==0]-> +(y,+(x644,x645)) joins (1): +(x644,+(x645,y)) -0|[==1,==0]-> +(+(x644,x645),y) +(y,+(x644,x645)) -2|[==1,==0]-> +(+(x644,x645),y) peak: +(x647,+(x648,s(y))) <-1|[==1,==0]- +(+(x647,x648),s(y)) -4| [==1,==0]-> +(s(+(x647,x648)),y) joins (1): +(x647,+(x648,s(y))) -0|[==1,==0]-> +(+(x647,x648),s(y)) +(s(+(x647,x648)),y) -3|[==1,==0]-> +(+(x647,x648),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: +(x662,s(+(y,z))) <-3|[==1,==0]- +(s(x662),+(y,z)) -0|[==1,==0]-> +(+(s(x662),y),z) joins (1): +(x662,s(+(y,z))) -4|[==1,==0]-> +(s(x662),+(y,z)) +(+(s(x662),y),z) -1|[==1,==0]-> +(s(x662),+(y,z)) peak: +(x,+(x664,s(z))) <-3|1[==1,==0]- +(x,+(s(x664),z)) -0|[==1,==0]-> +(+(x,s(x664)),z) joins (1): +(x,+(x664,s(z))) -4|1[==1,==0]-> +(x,+(s(x664),z)) +(+(x,s(x664)),z) -1|[==1,==0]-> +(x,+(s(x664),z)) peak: +(+(x666,s(y)),z) <-3|0[==1,==0]- +(+(s(x666),y),z) -1|[==1,==0]-> +(s(x666),+(y,z)) joins (1): +(+(x666,s(y)),z) -4|0[==1,==0]-> +(+(s(x666),y),z) +(s(x666),+(y,z)) -0|[==1,==0]-> +(+(s(x666),y),z) peak: +(x668,s(y)) <-3|[==1,==0]- +(s(x668),y) -2|[==1,==0]-> +(y,s(x668)) joins (1): +(x668,s(y)) -2|[==1,==0]-> +(s(y),x668) +(y,s(x668)) -4|[==1,==0]-> +(s(y),x668) peak: +(x670,s(s(y))) <-3|[==1,==0]- +(s(x670),s(y)) -4|[==1,==0]-> +(s(s(x670)),y) joins (1): +(x670,s(s(y))) -4|[==1,==0]-> +(s(x670),s(y)) +(s(s(x670)),y) -3|[==1,==0]-> +(s(x670),s(y)) peak: +(x,+(s(y),x673)) <-4|1[==1,==0]- +(x,+(y,s(x673))) -0|[==1,==0]-> +(+(x,y),s(x673)) joins (1): +(x,+(s(y),x673)) -3|1[==1,==0]-> +(x,+(y,s(x673))) +(+(x,y),s(x673)) -1|[==1,==0]-> +(x,+(y,s(x673))) peak: +(s(+(x,y)),x675) <-4|[==1,==0]- +(+(x,y),s(x675)) -1|[==1,==0]-> +(x,+(y,s(x675))) joins (1): +(s(+(x,y)),x675) -3|[==1,==0]-> +(+(x,y),s(x675)) +(x,+(y,s(x675))) -0|[==1,==0]-> +(+(x,y),s(x675)) peak: +(+(s(x),x677),z) <-4|0[==1,==0]- +(+(x,s(x677)),z) -1|[==1,==0]-> +(x,+(s(x677),z)) joins (1): +(+(s(x),x677),z) -3|0[==1,==0]-> +(+(x,s(x677)),z) +(x,+(s(x677),z)) -0|[==1,==0]-> +(+(x,s(x677)),z) peak: +(s(x),x679) <-4|[==1,==0]- +(x,s(x679)) -2|[==1,==0]-> +(s(x679),x) joins (1): +(s(x),x679) -2|[==1,==0]-> +(x679,s(x)) +(s(x679),x) -3|[==1,==0]-> +(x679,s(x)) peak: +(s(s(x)),x681) <-4|[==1,==0]- +(s(x),s(x681)) -3|[==1,==0]-> +(x,s(s(x681))) joins (1): +(s(s(x)),x681) -3|[==1,==0]-> +(s(x),s(x681)) +(x,s(s(x681))) -4|[==1,==0]-> +(s(x),s(x681)) peak: +(s(x),*(s(x),x683)) <-5|[==1,=?1]- *(s(x),s(x683)) -6|[ ==1,>=0]-> +(*(x,s(x683)),s(x683)) joins (1): +(s(x),*(s(x),x683)) -6|1[==1,>=0]-> +(s(x),+(*(x,x683),x683)) -0|[==1,>=0]-> +(+(s(x),*(x,x683)),x683) -3|0[==1,>=0]-> +(+(x,s(*(x,x683))),x683) +(*(x,s(x683)),s(x683)) -5|0[==1,=?1]-> +(+(x,*(x,x683)),s(x683)) -1|[==1,>=0]-> +(x,+(*(x,x683),s(x683))) -4|1[==1,>=0]-> +(x,+(s(*(x,x683)),x683)) -0| [==1,>=0]-> +(+(x,s(*(x,x683))),x683) peak: +(x,*(x,x685)) <-5|[==1,=>1]- *(x,s(x685)) -7|[==1,?=9]-> *(s(x685),x) joins (1): +(x,*(x,x685)) -7|1[==1,?=9]-> +(x,*(x685,x)) *(s(x685),x) -6|[==1,>>0]-> +(*(x685,x),x) -2|[==1,>>0]-> +(x,*(x685,x)) peak: +(*(x686,s(y)),s(y)) <-6|[==1,=>0]- *(s(x686),s(y)) -5|[ ==1,?=1]-> +(s(x686),*(s(x686),y)) joins (1): +(*(x686,s(y)),s(y)) -5|0[==1,?=1]-> +(+(x686,*(x686,y)),s(y)) -1|[==1,=>0]-> +(x686,+(*(x686,y),s(y))) -4|1[==1,=>0]-> +(x686,+(s(*(x686,y)),y)) +(s(x686),*(s(x686),y)) -6|1[==1,=>0]-> +(s(x686),+(*(x686,y),y)) -0|[==1,=>0]-> +(+(s(x686),*(x686,y)),y) -3|0[==1,=>0]-> +(+(x686,s(*(x686,y))),y) -1| [==1,=>0]-> +(x686,+(s(*(x686,y)),y)) peak: +(*(x688,y),y) <-6|[==1,=>0]- *(s(x688),y) -7|[==1,?=9]-> *(y,s(x688)) joins (1): +(*(x688,y),y) -7|0[==1,?=9]-> +(*(y,x688),y) *(y,s(x688)) -5|[==1,?>1]-> +(y,*(y,x688)) -2|[==1,=>0]-> +(*(y,x688),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