MAYBE *** Computating Strongly Quasi-Reducible Parts *** TRS: [ +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?y,?x)), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] Constructors: {0,s} Defined function symbols: {+} Constructor subsystem: [ ] Rule part & Conj Part: [ +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?y,?x)) ] [ +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] *** Ground Confluence Check by Rewriting Induction *** Sort: {Nat} Signature: [ + : Nat,Nat -> Nat, s : Nat -> Nat, 0 : Nat ] Rule Part: [ +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?y,?x)) ] Conjecture Part: [ +(+(?x,?x),?x) = +(?x,+(?x,?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: [ +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?y,?x)) ] Conjectures: [ +(+(?x,?x),?x) = +(?x,+(?x,?x)) ] STEP 0 ES: [ +(+(?x,?x),?x) = +(?x,+(?x,?x)) ] HS: [ ] ES0: [ +(+(?x,?x),?x) = +(?x,+(?x,?x)) ] HS0: [ ] ES1: [ +(+(?x,?x),?x) = +(?x,+(?x,?x)) ] HS1: [ ] Expand +(+(?x,?x),?x) = +(?x,+(?x,?x)) [ +(0,0) = +(0,+(0,0)), +(s(+(s(?x_2),?x_2)),s(?x_2)) = +(s(?x_2),+(s(?x_2),s(?x_2))) ] ES2: [ 0 = +(0,+(0,0)), s(s(s(+(?x_2,+(?x_2,?x_2))))) = +(s(?x_2),+(s(?x_2),s(?x_2))) ] HS2: [ +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] STEP 1 ES: [ 0 = +(0,+(0,0)), s(s(s(+(?x_2,+(?x_2,?x_2))))) = +(s(?x_2),+(s(?x_2),s(?x_2))) ] HS: [ +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES0: [ 0 = 0, s(s(s(+(?x_2,+(?x_2,?x_2))))) = s(s(+(?x_2,s(+(?x_2,?x_2))))) ] HS0: [ +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES1: [ s(s(s(+(?x_2,+(?x_2,?x_2))))) = s(s(+(?x_2,s(+(?x_2,?x_2))))) ] HS1: [ +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] Expand s(s(+(?x_2,s(+(?x_2,?x_2))))) = s(s(s(+(?x_2,+(?x_2,?x_2))))) [ s(s(s(+(0,0)))) = s(s(s(+(0,+(0,0))))), s(s(s(+(s(+(s(?x_2),s(?x_2))),?x_2)))) = s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))) ] ES2: [ s(s(s(0))) = s(s(s(+(0,+(0,0))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) = s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))) ] HS2: [ s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] STEP 2 ES: [ s(s(s(0))) = s(s(s(+(0,+(0,0))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) = s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))) ] HS: [ s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES0: [ s(s(s(0))) = s(s(s(0))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) = s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))) ] HS0: [ s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES1: [ s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) = s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))) ] HS1: [ s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] Expand s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) = s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))) [ s(s(s(s(s(s(+(0,0))))))) = s(s(s(s(s(s(+(0,+(0,0)))))))), s(s(s(s(s(+(s(s(+(s(?x_2),s(?x_2)))),?x_2)))))) = s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))) ] ES2: [ s(s(s(s(s(s(0)))))) = s(s(s(s(s(s(+(0,+(0,0)))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) = s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))) ] HS2: [ s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] STEP 3 ES: [ s(s(s(s(s(s(0)))))) = s(s(s(s(s(s(+(0,+(0,0)))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) = s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))) ] HS: [ s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES0: [ s(s(s(s(s(s(0)))))) = s(s(s(s(s(s(0)))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) = s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))) ] HS0: [ s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES1: [ s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) = s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))) ] HS1: [ s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] Expand s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) = s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))) [ s(s(s(s(s(s(s(s(s(+(0,0)))))))))) = s(s(s(s(s(s(s(s(s(+(0,+(0,0))))))))))), s(s(s(s(s(s(s(+(s(s(s(+(s(?x_2),s(?x_2))))),?x_2)))))))) = s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))))))))) ] ES2: [ s(s(s(s(s(s(s(s(s(0))))))))) = s(s(s(s(s(s(s(s(s(+(0,+(0,0))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) = s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))))))))) ] HS2: [ s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] STEP 4 ES: [ s(s(s(s(s(s(s(s(s(0))))))))) = s(s(s(s(s(s(s(s(s(+(0,+(0,0))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) = s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))))))))) ] HS: [ s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES0: [ s(s(s(s(s(s(s(s(s(0))))))))) = s(s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))) ] HS0: [ s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES1: [ s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))) ] HS1: [ s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] Expand s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))) [ s(s(s(s(s(s(s(s(s(s(s(s(+(0,0))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0)))))))))))))), s(s(s(s(s(s(s(s(s(+(s(s(s(s(+(s(?x_2),s(?x_2)))))),?x_2)))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))))))))) ] ES2: [ s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0)))))))))))))), s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))))))))) ] HS2: [ s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] STEP 5 ES: [ s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0)))))))))))))), s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))))))))) ] HS: [ s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES0: [ s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))) ] HS0: [ s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES1: [ s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))) ] HS1: [ s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] Expand s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))) [ s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,0)))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0))))))))))))))))), s(s(s(s(s(s(s(s(s(s(s(+(s(s(s(s(s(+(s(?x_2),s(?x_2))))))),?x_2)))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))))))))))))))) ] ES2: [ s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0))))))))))))))))), s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(+(?x_2,?x_2)))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))))))))))))))) ] HS2: [ s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] STEP 6 ES: [ s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0))))))))))))))))), s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(+(?x_2,?x_2)))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2)))))))))))))))))) ] HS: [ s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES0: [ s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))), s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(+(?x_2,?x_2)))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))))))))) ] HS0: [ s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] ES1: [ s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(+(?x_2,?x_2)))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))))))))) ] HS1: [ s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] Expand s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(+(?x_2,?x_2)))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))))))))) [ s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,0))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0)))))))))))))))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(+(s(s(s(s(s(s(+(s(?x_2),s(?x_2)))))))),?x_2)))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))))))))))))))) ] ES2: [ s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0)))))))))))))))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(s(+(?x_2,?x_2))))))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))))))))))))))) ] HS2: [ s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(+(?x_2,?x_2)))))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))))))))), s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] STEP 7 ES: [ s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(0,+(0,0)))))))))))))))))))), s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(s(+(?x_2,?x_2))))))))))))))))))))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(s(?x_2),+(s(?x_2),s(?x_2))))))))))))))))))))) ] HS: [ s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(s(+(?x_2,?x_2)))))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))))))))), s(s(s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(s(+(?x_2,?x_2))))))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))))))))), s(s(s(s(s(s(s(s(+(?x_2,s(s(s(s(+(?x_2,?x_2)))))))))))))) -> s(s(s(s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))))))))), s(s(s(s(s(s(+(?x_2,s(s(s(+(?x_2,?x_2))))))))))) -> s(s(s(s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2))))))))))), s(s(s(s(+(?x_2,s(s(+(?x_2,?x_2)))))))) -> s(s(s(s(s(s(+(?x_2,+(?x_2,?x_2)))))))), s(s(+(?x_2,s(+(?x_2,?x_2))))) -> s(s(s(+(?x_2,+(?x_2,?x_2))))), +(+(?x,?x),?x) -> +(?x,+(?x,?x)) ] rewriting induction stopped because of timeout. examples/additions/plus8.trs: Failure(unknown) (5001 msec.)