Runtime Complexity TRS:
The TRS R consists of the following rules:

plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


plus'(plus'(X, Y), Z) → plus'(X, plus'(Y, Z))
times'(X, s'(Y)) → plus'(X, times'(Y, X))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
plus'(plus'(X, Y), Z) → plus'(X, plus'(Y, Z))
times'(X, s'(Y)) → plus'(X, times'(Y, X))

Types:
plus' :: s' → s' → s'
times' :: s' → s' → s'
s' :: s' → s'
_hole_s'1 :: s'
_gen_s'2 :: Nat → s'

Heuristically decided to analyse the following defined symbols:
plus', times'

They will be analysed ascendingly in the following order:
plus' < times'

Rules:
plus'(plus'(X, Y), Z) → plus'(X, plus'(Y, Z))
times'(X, s'(Y)) → plus'(X, times'(Y, X))

Types:
plus' :: s' → s' → s'
times' :: s' → s' → s'
s' :: s' → s'
_hole_s'1 :: s'
_gen_s'2 :: Nat → s'

Generator Equations:
_gen_s'2(0) ⇔ _hole_s'1
_gen_s'2(+(x, 1)) ⇔ s'(_gen_s'2(x))

The following defined symbols remain to be analysed:
plus', times'

They will be analysed ascendingly in the following order:
plus' < times'

Could not prove a rewrite lemma for the defined symbol plus'.

Rules:
plus'(plus'(X, Y), Z) → plus'(X, plus'(Y, Z))
times'(X, s'(Y)) → plus'(X, times'(Y, X))

Types:
plus' :: s' → s' → s'
times' :: s' → s' → s'
s' :: s' → s'
_hole_s'1 :: s'
_gen_s'2 :: Nat → s'

Generator Equations:
_gen_s'2(0) ⇔ _hole_s'1
_gen_s'2(+(x, 1)) ⇔ s'(_gen_s'2(x))

The following defined symbols remain to be analysed:
times'

Could not prove a rewrite lemma for the defined symbol times'.

Rules:
plus'(plus'(X, Y), Z) → plus'(X, plus'(Y, Z))
times'(X, s'(Y)) → plus'(X, times'(Y, X))

Types:
plus' :: s' → s' → s'
times' :: s' → s' → s'
s' :: s' → s'
_hole_s'1 :: s'
_gen_s'2 :: Nat → s'

Generator Equations:
_gen_s'2(0) ⇔ _hole_s'1
_gen_s'2(+(x, 1)) ⇔ s'(_gen_s'2(x))

No more defined symbols left to analyse.