is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → cons(x, l)
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → cons'(x, l)
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Infered types.
Rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → cons'(x, l)
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Types:
is_empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: hd' → nil':cons' → nil':cons'
false' :: true':false'
hd' :: nil':cons' → hd'
tl' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
ifappend' :: nil':cons' → nil':cons' → true':false' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_hd'3 :: hd'
_gen_nil':cons'4 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
append'
Rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → cons'(x, l)
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Types:
is_empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: hd' → nil':cons' → nil':cons'
false' :: true':false'
hd' :: nil':cons' → hd'
tl' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
ifappend' :: nil':cons' → nil':cons' → true':false' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_hd'3 :: hd'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(_hole_hd'3, _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
append'
Could not prove a rewrite lemma for the defined symbol append'.
Rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → cons'(x, l)
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Types:
is_empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: hd' → nil':cons' → nil':cons'
false' :: true':false'
hd' :: nil':cons' → hd'
tl' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
ifappend' :: nil':cons' → nil':cons' → true':false' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_hd'3 :: hd'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(_hole_hd'3, _gen_nil':cons'4(x))
No more defined symbols left to analyse.