(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
+(x1, x2)  =  +(x1, x2)
0  =  0
s(x1)  =  s(x1)
p(x1)  =  p(x1)
minus(x1)  =  x1
*(x1, x2)  =  *(x1, x2)

Recursive path order with status [RPO].
Quasi-Precedence:

*₂ > +₂ > [s₁, p₁]

Status:

+₂: multiset
0: multiset
s₁: multiset
p₁: multiset
*₂: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:

minus₁ > p₁ > 0 > s₁

and weight map:

0=1
minus_1=2
s_1=1
p_1=1

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.