f(j(x, y), y) → g(f(x, k(y)))
f(x, h1(y, z)) → h2(0, x, h1(y, z))
g(h2(x, y, h1(z, u))) → h2(s(x), y, h1(z, u))
h2(x, j(y, h1(z, u)), h1(z, u)) → h2(s(x), y, h1(s(z), u))
i(f(x, h(y))) → y
i(h2(s(x), y, h1(x, z))) → z
k(h(x)) → h1(0, x)
k(h1(x, y)) → h1(s(x), y)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(j'(x, y), y) → g'(f'(x, k'(y)))
f'(x, h1'(y, z)) → h2'(0', x, h1'(y, z))
g'(h2'(x, y, h1'(z, u))) → h2'(s'(x), y, h1'(z, u))
h2'(x, j'(y, h1'(z, u)), h1'(z, u)) → h2'(s'(x), y, h1'(s'(z), u))
i'(f'(x, h'(y))) → y
i'(h2'(s'(x), y, h1'(x, z))) → z
k'(h'(x)) → h1'(0', x)
k'(h1'(x, y)) → h1'(s'(x), y)
Infered types.
Rules:
f'(j'(x, y), y) → g'(f'(x, k'(y)))
f'(x, h1'(y, z)) → h2'(0', x, h1'(y, z))
g'(h2'(x, y, h1'(z, u))) → h2'(s'(x), y, h1'(z, u))
h2'(x, j'(y, h1'(z, u)), h1'(z, u)) → h2'(s'(x), y, h1'(s'(z), u))
i'(f'(x, h'(y))) → y
i'(h2'(s'(x), y, h1'(x, z))) → z
k'(h'(x)) → h1'(0', x)
k'(h1'(x, y)) → h1'(s'(x), y)
Types:
f' :: j' → h1':h' → f':g':h2'
j' :: j' → h1':h' → j'
g' :: f':g':h2' → f':g':h2'
k' :: h1':h' → h1':h'
h1' :: 0':s' → i' → h1':h'
h2' :: 0':s' → j' → h1':h' → f':g':h2'
0' :: 0':s'
s' :: 0':s' → 0':s'
i' :: f':g':h2' → i'
h' :: i' → h1':h'
_hole_f':g':h2'1 :: f':g':h2'
_hole_j'2 :: j'
_hole_h1':h'3 :: h1':h'
_hole_0':s'4 :: 0':s'
_hole_i'5 :: i'
_gen_j'6 :: Nat → j'
_gen_0':s'7 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
f', h2'
They will be analysed ascendingly in the following order:
h2' < f'
Rules:
f'(j'(x, y), y) → g'(f'(x, k'(y)))
f'(x, h1'(y, z)) → h2'(0', x, h1'(y, z))
g'(h2'(x, y, h1'(z, u))) → h2'(s'(x), y, h1'(z, u))
h2'(x, j'(y, h1'(z, u)), h1'(z, u)) → h2'(s'(x), y, h1'(s'(z), u))
i'(f'(x, h'(y))) → y
i'(h2'(s'(x), y, h1'(x, z))) → z
k'(h'(x)) → h1'(0', x)
k'(h1'(x, y)) → h1'(s'(x), y)
Types:
f' :: j' → h1':h' → f':g':h2'
j' :: j' → h1':h' → j'
g' :: f':g':h2' → f':g':h2'
k' :: h1':h' → h1':h'
h1' :: 0':s' → i' → h1':h'
h2' :: 0':s' → j' → h1':h' → f':g':h2'
0' :: 0':s'
s' :: 0':s' → 0':s'
i' :: f':g':h2' → i'
h' :: i' → h1':h'
_hole_f':g':h2'1 :: f':g':h2'
_hole_j'2 :: j'
_hole_h1':h'3 :: h1':h'
_hole_0':s'4 :: 0':s'
_hole_i'5 :: i'
_gen_j'6 :: Nat → j'
_gen_0':s'7 :: Nat → 0':s'
Generator Equations:
_gen_j'6(0) ⇔ _hole_j'2
_gen_j'6(+(x, 1)) ⇔ j'(_gen_j'6(x), h1'(0', _hole_i'5))
_gen_0':s'7(0) ⇔ 0'
_gen_0':s'7(+(x, 1)) ⇔ s'(_gen_0':s'7(x))
The following defined symbols remain to be analysed:
h2', f'
They will be analysed ascendingly in the following order:
h2' < f'
Could not prove a rewrite lemma for the defined symbol h2'.
Rules:
f'(j'(x, y), y) → g'(f'(x, k'(y)))
f'(x, h1'(y, z)) → h2'(0', x, h1'(y, z))
g'(h2'(x, y, h1'(z, u))) → h2'(s'(x), y, h1'(z, u))
h2'(x, j'(y, h1'(z, u)), h1'(z, u)) → h2'(s'(x), y, h1'(s'(z), u))
i'(f'(x, h'(y))) → y
i'(h2'(s'(x), y, h1'(x, z))) → z
k'(h'(x)) → h1'(0', x)
k'(h1'(x, y)) → h1'(s'(x), y)
Types:
f' :: j' → h1':h' → f':g':h2'
j' :: j' → h1':h' → j'
g' :: f':g':h2' → f':g':h2'
k' :: h1':h' → h1':h'
h1' :: 0':s' → i' → h1':h'
h2' :: 0':s' → j' → h1':h' → f':g':h2'
0' :: 0':s'
s' :: 0':s' → 0':s'
i' :: f':g':h2' → i'
h' :: i' → h1':h'
_hole_f':g':h2'1 :: f':g':h2'
_hole_j'2 :: j'
_hole_h1':h'3 :: h1':h'
_hole_0':s'4 :: 0':s'
_hole_i'5 :: i'
_gen_j'6 :: Nat → j'
_gen_0':s'7 :: Nat → 0':s'
Generator Equations:
_gen_j'6(0) ⇔ _hole_j'2
_gen_j'6(+(x, 1)) ⇔ j'(_gen_j'6(x), h1'(0', _hole_i'5))
_gen_0':s'7(0) ⇔ 0'
_gen_0':s'7(+(x, 1)) ⇔ s'(_gen_0':s'7(x))
The following defined symbols remain to be analysed:
f'
Could not prove a rewrite lemma for the defined symbol f'.
Rules:
f'(j'(x, y), y) → g'(f'(x, k'(y)))
f'(x, h1'(y, z)) → h2'(0', x, h1'(y, z))
g'(h2'(x, y, h1'(z, u))) → h2'(s'(x), y, h1'(z, u))
h2'(x, j'(y, h1'(z, u)), h1'(z, u)) → h2'(s'(x), y, h1'(s'(z), u))
i'(f'(x, h'(y))) → y
i'(h2'(s'(x), y, h1'(x, z))) → z
k'(h'(x)) → h1'(0', x)
k'(h1'(x, y)) → h1'(s'(x), y)
Types:
f' :: j' → h1':h' → f':g':h2'
j' :: j' → h1':h' → j'
g' :: f':g':h2' → f':g':h2'
k' :: h1':h' → h1':h'
h1' :: 0':s' → i' → h1':h'
h2' :: 0':s' → j' → h1':h' → f':g':h2'
0' :: 0':s'
s' :: 0':s' → 0':s'
i' :: f':g':h2' → i'
h' :: i' → h1':h'
_hole_f':g':h2'1 :: f':g':h2'
_hole_j'2 :: j'
_hole_h1':h'3 :: h1':h'
_hole_0':s'4 :: 0':s'
_hole_i'5 :: i'
_gen_j'6 :: Nat → j'
_gen_0':s'7 :: Nat → 0':s'
Generator Equations:
_gen_j'6(0) ⇔ _hole_j'2
_gen_j'6(+(x, 1)) ⇔ j'(_gen_j'6(x), h1'(0', _hole_i'5))
_gen_0':s'7(0) ⇔ 0'
_gen_0':s'7(+(x, 1)) ⇔ s'(_gen_0':s'7(x))
No more defined symbols left to analyse.