average(s(x), y) → average(x, s(y))
average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0
average(0, s(0)) → 0
average(0, s(s(0))) → s(0)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')
Infered types.
Rules:
average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')
Types:
average' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'
Heuristically decided to analyse the following defined symbols:
average'
Rules:
average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')
Types:
average' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'
Generator Equations:
_gen_s':0'2(0) ⇔ 0'
_gen_s':0'2(+(x, 1)) ⇔ s'(_gen_s':0'2(x))
The following defined symbols remain to be analysed:
average'
Could not prove a rewrite lemma for the defined symbol average'.
The following conjecture could not be proven:
average'(_gen_s':0'2(+(1, _n4)), _gen_s':0'2(b)) →? _*3
Rules:
average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')
Types:
average' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'
Generator Equations:
_gen_s':0'2(0) ⇔ 0'
_gen_s':0'2(+(x, 1)) ⇔ s'(_gen_s':0'2(x))
No more defined symbols left to analyse.