YES (ignored inputs)COMMENT translated from Cops 191 *** Computating Strongly Quasi-Reducible Parts *** TRS: [ +(0,?y) -> ?y, +(?x,0) -> ?x, +(s(?x),?y) -> s(+(?y,?x)), +(?x,s(?y)) -> s(+(?y,?x)), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(?x,?y) -> +(?y,?x) ] Constructors: {0,s} Defined function symbols: {+} Constructor subsystem: [ ] Rule part & Conj Part: [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?y,?x)) ] [ +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?y,?x)), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(?x,?y) -> +(?y,?x) ] Rule part & Conj Part: [ +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?y,?x)) ] [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?y,?x)), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(?x,?y) -> +(?y,?x) ] *** Ground Confluence Check by Rewriting Induction *** Sort: {Nat} Signature: [ + : Nat,Nat -> Nat, 0 : Nat, s : Nat -> Nat ] Rule Part: [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?y,?x)) ] Conjecture Part: [ +(0,?y) = ?y, +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(?x,?y) = +(?y,?x) ] Precedence (by weight): {(+,3),(0,2),(s,0)} Rule part is confluent. R0 is ground confluent. Check conj part consists of inductive theorems of R0. Rules: [ +(?x,0) -> ?x, +(?x,s(?y)) -> s(+(?y,?x)) ] Conjectures: [ +(0,?y) = ?y, +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(?x,?y) = +(?y,?x) ] STEP 0 ES: [ +(0,?y) = ?y, +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(?x,?y) = +(?y,?x) ] HS: [ ] ES0: [ +(0,?y) = ?y, +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(?x,?y) = +(?y,?x) ] HS0: [ ] ES1: [ +(0,?y) = ?y, +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(?x,?y) = +(?y,?x) ] HS1: [ ] Expand +(0,?y) = ?y [ 0 = 0, s(+(?y_2,0)) = s(?y_2) ] ES2: [ 0 = 0, s(?y_2) = s(?y_2), +(?x,?y) = +(?y,?x), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(s(?x),?y) = s(+(?y,?x)) ] HS2: [ +(0,?y) -> ?y ] STEP 1 ES: [ 0 = 0, s(?y_2) = s(?y_2), +(?x,?y) = +(?y,?x), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(s(?x),?y) = s(+(?y,?x)) ] HS: [ +(0,?y) -> ?y ] ES0: [ 0 = 0, s(?y_2) = s(?y_2), +(?x,?y) = +(?y,?x), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(s(?x),?y) = s(+(?y,?x)) ] HS0: [ +(0,?y) -> ?y ] ES1: [ +(?x,?y) = +(?y,?x), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(s(?x),?y) = s(+(?y,?x)) ] HS1: [ +(0,?y) -> ?y ] Expand +(?x,?y) = +(?y,?x) [ ?x_1 = +(0,?x_1), s(+(?y_2,?x_2)) = +(s(?y_2),?x_2) ] ES2: [ ?x_1 = +(0,?x_1), s(+(?y_2,?x_2)) = +(s(?y_2),?x_2), +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z) ] HS2: [ +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] STEP 2 ES: [ ?x_1 = +(0,?x_1), s(+(?y_2,?x_2)) = +(s(?y_2),?x_2), +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z) ] HS: [ +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES0: [ ?x_1 = ?x_1, s(+(?y_2,?x_2)) = +(s(?y_2),?x_2), +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z) ] HS0: [ +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES1: [ s(+(?y_2,?x_2)) = +(s(?y_2),?x_2), +(s(?x),?y) = s(+(?y,?x)), +(?x,+(?y,?z)) = +(+(?x,?y),?z) ] HS1: [ +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] Expand +(s(?y_2),?x_2) = s(+(?y_2,?x_2)) [ s(?y) = s(+(?y,0)), s(+(?y_2,s(?y))) = s(+(?y,s(?y_2))) ] ES2: [ s(?y) = s(+(?y,0)), s(s(+(?y,?y_2))) = s(+(?y,s(?y_2))), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(s(?x),?y) = s(+(?y,?x)) ] HS2: [ +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] STEP 3 ES: [ s(?y) = s(+(?y,0)), s(s(+(?y,?y_2))) = s(+(?y,s(?y_2))), +(?x,+(?y,?z)) = +(+(?x,?y),?z), +(s(?x),?y) = s(+(?y,?x)) ] HS: [ +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES0: [ s(?y) = s(?y), s(s(+(?y,?y_2))) = s(s(+(?y_2,?y))), +(?x,+(?y,?z)) = +(+(?x,?y),?z), s(+(?x,?y)) = s(+(?y,?x)) ] HS0: [ +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES1: [ +(?x,+(?y,?z)) = +(+(?x,?y),?z) ] HS1: [ +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] Expand +(?x,+(?y,?z)) = +(+(?x,?y),?z) [ +(?x,?x_1) = +(+(?x,?x_1),0), +(?x,s(+(?y_2,?x_2))) = +(+(?x,?x_2),s(?y_2)) ] ES2: [ +(?x,?x_1) = +(+(?x,?x_1),0), s(+(+(?y_2,?x_2),?x)) = +(+(?x,?x_2),s(?y_2)) ] HS2: [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] STEP 4 ES: [ +(?x,?x_1) = +(+(?x,?x_1),0), s(+(+(?y_2,?x_2),?x)) = +(+(?x,?x_2),s(?y_2)) ] HS: [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES0: [ +(?x,?x_1) = +(?x,?x_1), s(+(+(?y_2,?x_2),?x)) = s(+(?y_2,+(?x,?x_2))) ] HS0: [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES1: [ s(+(+(?y_2,?x_2),?x)) = s(+(?y_2,+(?x,?x_2))) ] HS1: [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] Expand s(+(+(?y_2,?x_2),?x)) = s(+(?y_2,+(?x,?x_2))) [ s(+(?x_3,?x)) = s(+(?x_3,+(?x,0))), s(+(s(+(?y_4,?x_4)),?x)) = s(+(?x_4,+(?x,s(?y_4)))) ] ES2: [ s(+(?x_3,?x)) = s(+(?x_3,+(?x,0))), s(s(+(+(?y_4,?x_4),?x))) = s(+(?x_4,+(?x,s(?y_4)))) ] HS2: [ s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] STEP 5 ES: [ s(+(?x_3,?x)) = s(+(?x_3,+(?x,0))), s(s(+(+(?y_4,?x_4),?x))) = s(+(?x_4,+(?x,s(?y_4)))) ] HS: [ s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES0: [ s(+(?x_3,?x)) = s(+(?x_3,?x)), s(s(+(+(?y_4,?x_4),?x))) = s(s(+(+(?y_4,?x),?x_4))) ] HS0: [ s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES1: [ s(s(+(+(?y_4,?x_4),?x))) = s(s(+(+(?y_4,?x),?x_4))) ] HS1: [ s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] Expand s(s(+(+(?y_4,?x_4),?x))) = s(s(+(+(?y_4,?x),?x_4))) [ s(s(+(?x_5,?x))) = s(s(+(+(?x_5,?x),0))), s(s(+(s(+(?y_6,?x_6)),?x))) = s(s(+(+(?x_6,?x),s(?y_6)))) ] ES2: [ s(s(+(?x_5,?x))) = s(s(+(+(?x_5,?x),0))), s(s(s(+(+(?y_6,?x_6),?x)))) = s(s(+(+(?x_6,?x),s(?y_6)))) ] HS2: [ s(s(+(+(?y_4,?x_4),?x))) -> s(s(+(+(?y_4,?x),?x_4))), s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] STEP 6 ES: [ s(s(+(?x_5,?x))) = s(s(+(+(?x_5,?x),0))), s(s(s(+(+(?y_6,?x_6),?x)))) = s(s(+(+(?x_6,?x),s(?y_6)))) ] HS: [ s(s(+(+(?y_4,?x_4),?x))) -> s(s(+(+(?y_4,?x),?x_4))), s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES0: [ s(s(+(?x_5,?x))) = s(s(+(?x_5,?x))), s(s(s(+(+(?y_6,?x_6),?x)))) = s(s(s(+(?y_6,+(?x_6,?x))))) ] HS0: [ s(s(+(+(?y_4,?x_4),?x))) -> s(s(+(+(?y_4,?x),?x_4))), s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] ES1: [ ] HS1: [ s(s(+(+(?y_4,?x_4),?x))) -> s(s(+(+(?y_4,?x),?x_4))), s(+(+(?y_2,?x_2),?x)) -> s(+(?y_2,+(?x,?x_2))), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(s(?y_2),?x_2) -> s(+(?y_2,?x_2)), +(?x,?y) -> +(?y,?x), +(0,?y) -> ?y ] Conj part consisits of inductive theorems of R0. examples/fromCops/cr/191.trs: Success(GCR) (8 msec.)