addlist(Cons(x, xs'), Cons(S(0), xs)) → Cons(S(x), addlist(xs', xs))
addlist(Cons(S(0), xs'), Cons(x, xs)) → Cons(S(x), addlist(xs', xs))
addlist(Nil, ys) → Nil
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(xs, ys) → addlist(xs, ys)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
addlist'(Cons'(x, xs'), Cons'(S'(0'), xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Cons'(S'(0'), xs'), Cons'(x, xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Nil', ys) → Nil'
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
goal'(xs, ys) → addlist'(xs, ys)
Infered types.
Rules:
addlist'(Cons'(x, xs'), Cons'(S'(0'), xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Cons'(S'(0'), xs'), Cons'(x, xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Nil', ys) → Nil'
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
goal'(xs, ys) → addlist'(xs, ys)
Types:
addlist' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_0':S'2 :: 0':S'
_hole_True':False'3 :: True':False'
_gen_Cons':Nil'4 :: Nat → Cons':Nil'
_gen_0':S'5 :: Nat → 0':S'
Heuristically decided to analyse the following defined symbols:
addlist'
Rules:
addlist'(Cons'(x, xs'), Cons'(S'(0'), xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Cons'(S'(0'), xs'), Cons'(x, xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Nil', ys) → Nil'
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
goal'(xs, ys) → addlist'(xs, ys)
Types:
addlist' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_0':S'2 :: 0':S'
_hole_True':False'3 :: True':False'
_gen_Cons':Nil'4 :: Nat → Cons':Nil'
_gen_0':S'5 :: Nat → 0':S'
Generator Equations:
_gen_Cons':Nil'4(0) ⇔ Nil'
_gen_Cons':Nil'4(+(x, 1)) ⇔ Cons'(0', _gen_Cons':Nil'4(x))
_gen_0':S'5(0) ⇔ 0'
_gen_0':S'5(+(x, 1)) ⇔ S'(_gen_0':S'5(x))
The following defined symbols remain to be analysed:
addlist'
Could not prove a rewrite lemma for the defined symbol addlist'.
Rules:
addlist'(Cons'(x, xs'), Cons'(S'(0'), xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Cons'(S'(0'), xs'), Cons'(x, xs)) → Cons'(S'(x), addlist'(xs', xs))
addlist'(Nil', ys) → Nil'
notEmpty'(Cons'(x, xs)) → True'
notEmpty'(Nil') → False'
goal'(xs, ys) → addlist'(xs, ys)
Types:
addlist' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: 0':S' → Cons':Nil' → Cons':Nil'
S' :: 0':S' → 0':S'
0' :: 0':S'
Nil' :: Cons':Nil'
notEmpty' :: Cons':Nil' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_hole_0':S'2 :: 0':S'
_hole_True':False'3 :: True':False'
_gen_Cons':Nil'4 :: Nat → Cons':Nil'
_gen_0':S'5 :: Nat → 0':S'
Generator Equations:
_gen_Cons':Nil'4(0) ⇔ Nil'
_gen_Cons':Nil'4(+(x, 1)) ⇔ Cons'(0', _gen_Cons':Nil'4(x))
_gen_0':S'5(0) ⇔ 0'
_gen_0':S'5(+(x, 1)) ⇔ S'(_gen_0':S'5(x))
No more defined symbols left to analyse.