perfectp(0) → false
perfectp(s(x)) → f(x, s(0), s(x), s(x))
f(0, y, 0, u) → true
f(0, y, s(z), u) → false
f(s(x), 0, z, u) → f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) → if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
perfectp'(0') → false'
perfectp'(s'(x)) → f'(x, s'(0'), s'(x), s'(x))
f'(0', y, 0', u) → true'
f'(0', y, s'(z), u) → false'
f'(s'(x), 0', z, u) → f'(x, u, minus'(z, s'(x)), u)
f'(s'(x), s'(y), z, u) → if'(le'(x, y), f'(s'(x), minus'(y, x), z, u), f'(x, u, z, u))
Sliced the following arguments:
minus'/0
minus'/1
if'/0
le'/0
le'/1
Runtime Complexity TRS:
The TRS R consists of the following rules:
perfectp'(0') → false'
perfectp'(s'(x)) → f'(x, s'(0'), s'(x), s'(x))
f'(0', y, 0', u) → true'
f'(0', y, s'(z), u) → false'
f'(s'(x), 0', z, u) → f'(x, u, minus', u)
f'(s'(x), s'(y), z, u) → if'(f'(s'(x), minus', z, u), f'(x, u, z, u))
Infered types.
Rules:
perfectp'(0') → false'
perfectp'(s'(x)) → f'(x, s'(0'), s'(x), s'(x))
f'(0', y, 0', u) → true'
f'(0', y, s'(z), u) → false'
f'(s'(x), 0', z, u) → f'(x, u, minus', u)
f'(s'(x), s'(y), z, u) → if'(f'(s'(x), minus', z, u), f'(x, u, z, u))
Types:
perfectp' :: 0':s':minus' → false':true':if'
0' :: 0':s':minus'
false' :: false':true':if'
s' :: 0':s':minus' → 0':s':minus'
f' :: 0':s':minus' → 0':s':minus' → 0':s':minus' → 0':s':minus' → false':true':if'
true' :: false':true':if'
minus' :: 0':s':minus'
if' :: false':true':if' → false':true':if' → false':true':if'
_hole_false':true':if'1 :: false':true':if'
_hole_0':s':minus'2 :: 0':s':minus'
_gen_false':true':if'3 :: Nat → false':true':if'
_gen_0':s':minus'4 :: Nat → 0':s':minus'
Heuristically decided to analyse the following defined symbols:
f'
Rules:
perfectp'(0') → false'
perfectp'(s'(x)) → f'(x, s'(0'), s'(x), s'(x))
f'(0', y, 0', u) → true'
f'(0', y, s'(z), u) → false'
f'(s'(x), 0', z, u) → f'(x, u, minus', u)
f'(s'(x), s'(y), z, u) → if'(f'(s'(x), minus', z, u), f'(x, u, z, u))
Types:
perfectp' :: 0':s':minus' → false':true':if'
0' :: 0':s':minus'
false' :: false':true':if'
s' :: 0':s':minus' → 0':s':minus'
f' :: 0':s':minus' → 0':s':minus' → 0':s':minus' → 0':s':minus' → false':true':if'
true' :: false':true':if'
minus' :: 0':s':minus'
if' :: false':true':if' → false':true':if' → false':true':if'
_hole_false':true':if'1 :: false':true':if'
_hole_0':s':minus'2 :: 0':s':minus'
_gen_false':true':if'3 :: Nat → false':true':if'
_gen_0':s':minus'4 :: Nat → 0':s':minus'
Generator Equations:
_gen_false':true':if'3(0) ⇔ false'
_gen_false':true':if'3(+(x, 1)) ⇔ if'(false', _gen_false':true':if'3(x))
_gen_0':s':minus'4(0) ⇔ 0'
_gen_0':s':minus'4(+(x, 1)) ⇔ s'(_gen_0':s':minus'4(x))
The following defined symbols remain to be analysed:
f'
Could not prove a rewrite lemma for the defined symbol f'.
The following conjecture could not be proven:
f'(_gen_0':s':minus'4(+(1, _n6)), _gen_0':s':minus'4(0), _gen_0':s':minus'4(c), _gen_0':s':minus'4(0)) →? _*5
Rules:
perfectp'(0') → false'
perfectp'(s'(x)) → f'(x, s'(0'), s'(x), s'(x))
f'(0', y, 0', u) → true'
f'(0', y, s'(z), u) → false'
f'(s'(x), 0', z, u) → f'(x, u, minus', u)
f'(s'(x), s'(y), z, u) → if'(f'(s'(x), minus', z, u), f'(x, u, z, u))
Types:
perfectp' :: 0':s':minus' → false':true':if'
0' :: 0':s':minus'
false' :: false':true':if'
s' :: 0':s':minus' → 0':s':minus'
f' :: 0':s':minus' → 0':s':minus' → 0':s':minus' → 0':s':minus' → false':true':if'
true' :: false':true':if'
minus' :: 0':s':minus'
if' :: false':true':if' → false':true':if' → false':true':if'
_hole_false':true':if'1 :: false':true':if'
_hole_0':s':minus'2 :: 0':s':minus'
_gen_false':true':if'3 :: Nat → false':true':if'
_gen_0':s':minus'4 :: Nat → 0':s':minus'
Generator Equations:
_gen_false':true':if'3(0) ⇔ false'
_gen_false':true':if'3(+(x, 1)) ⇔ if'(false', _gen_false':true':if'3(x))
_gen_0':s':minus'4(0) ⇔ 0'
_gen_0':s':minus'4(+(x, 1)) ⇔ s'(_gen_0':s':minus'4(x))
No more defined symbols left to analyse.