YES Time: 0.022284 TRS: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} DP: DP: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)} TRS: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} UR: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} EDG: {(plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z)) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4))) (plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4))} STATUS: arrows: 0.000000 SCCS (1): Scc: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)} SCC (5): Strict: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4)} Weak: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + 1, [s](x0) = 0, [plus#](x0, x1) = x0 Strict: plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X2, X4) 2 + 0X1 + 0X3 + 0X2 + 1X4 >= 0 + 0X2 + 1X4 plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X3, plus(X2, X4)) 2 + 0X1 + 0X3 + 0X2 + 1X4 >= 1 + 0X3 + 0X2 + 1X4 plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))) 2 + 0X1 + 0X3 + 0X2 + 1X4 >= 2 + 0X1 + 0X3 + 0X2 + 1X4 plus#(s X, plus(Y, Z)) -> plus#(s s Y, Z) 1 + 0X + 0Y + 1Z >= 0 + 0Y + 1Z plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)) 1 + 0X + 0Y + 1Z >= 1 + 0X + 0Y + 1Z Weak: plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4))) 3 + 0X1 + 0X3 + 0X2 + 1X4 >= 3 + 0X1 + 0X3 + 0X2 + 1X4 plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)) 2 + 0X + 0Y + 1Z >= 2 + 0X + 0Y + 1Z SCCS (1): Scc: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))} SCC (2): Strict: { plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)), plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4)))} Weak: { plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)), plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [plus#](x0, x1) = x0 Strict: plus#(s X1, plus(X2, plus(X3, X4))) -> plus#(X1, plus(X3, plus(X2, X4))) 1 + 1X1 + 0X3 + 0X2 + 0X4 >= 0 + 1X1 + 0X3 + 0X2 + 0X4 plus#(s X, plus(Y, Z)) -> plus#(X, plus(s s Y, Z)) 1 + 1X + 0Y + 0Z >= 0 + 1X + 0Y + 0Z Weak: plus(s X1, plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4))) 1 + 1X1 + 1X3 + 1X2 + 1X4 >= 0 + 1X1 + 1X3 + 1X2 + 1X4 plus(s X, plus(Y, Z)) -> plus(X, plus(s s Y, Z)) 1 + 1X + 1Y + 1Z >= 2 + 1X + 1Y + 1Z Qed