i(x, x) → i(a, b)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
i'(x, x) → i'(a', b')
g'(x, x) → g'(a', b')
h'(s'(f'(x))) → h'(f'(x))
f'(s'(x)) → s'(s'(f'(h'(s'(x)))))
f'(g'(s'(x), y)) → f'(g'(x, s'(y)))
h'(g'(x, s'(y))) → h'(g'(s'(x), y))
h'(i'(x, y)) → i'(i'(c', h'(h'(y))), x)
g'(a', g'(x, g'(b', g'(a', g'(x, y))))) → g'(a', g'(a', g'(a', g'(x, g'(b', g'(b', y))))))
Infered types.
Rules:
i'(x, x) → i'(a', b')
g'(x, x) → g'(a', b')
h'(s'(f'(x))) → h'(f'(x))
f'(s'(x)) → s'(s'(f'(h'(s'(x)))))
f'(g'(s'(x), y)) → f'(g'(x, s'(y)))
h'(g'(x, s'(y))) → h'(g'(s'(x), y))
h'(i'(x, y)) → i'(i'(c', h'(h'(y))), x)
g'(a', g'(x, g'(b', g'(a', g'(x, y))))) → g'(a', g'(a', g'(a', g'(x, g'(b', g'(b', y))))))
Types:
i' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
a' :: a':b':s':c'
b' :: a':b':s':c'
g' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
h' :: a':b':s':c' → a':b':s':c'
s' :: a':b':s':c' → a':b':s':c'
f' :: a':b':s':c' → a':b':s':c'
c' :: a':b':s':c'
_hole_a':b':s':c'1 :: a':b':s':c'
_gen_a':b':s':c'2 :: Nat → a':b':s':c'
Heuristically decided to analyse the following defined symbols:
i', g', h', f'
They will be analysed ascendingly in the following order:
i' < h'
g' < h'
g' < f'
h' = f'
Rules:
i'(x, x) → i'(a', b')
g'(x, x) → g'(a', b')
h'(s'(f'(x))) → h'(f'(x))
f'(s'(x)) → s'(s'(f'(h'(s'(x)))))
f'(g'(s'(x), y)) → f'(g'(x, s'(y)))
h'(g'(x, s'(y))) → h'(g'(s'(x), y))
h'(i'(x, y)) → i'(i'(c', h'(h'(y))), x)
g'(a', g'(x, g'(b', g'(a', g'(x, y))))) → g'(a', g'(a', g'(a', g'(x, g'(b', g'(b', y))))))
Types:
i' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
a' :: a':b':s':c'
b' :: a':b':s':c'
g' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
h' :: a':b':s':c' → a':b':s':c'
s' :: a':b':s':c' → a':b':s':c'
f' :: a':b':s':c' → a':b':s':c'
c' :: a':b':s':c'
_hole_a':b':s':c'1 :: a':b':s':c'
_gen_a':b':s':c'2 :: Nat → a':b':s':c'
Generator Equations:
_gen_a':b':s':c'2(0) ⇔ b'
_gen_a':b':s':c'2(+(x, 1)) ⇔ s'(_gen_a':b':s':c'2(x))
The following defined symbols remain to be analysed:
i', g', h', f'
They will be analysed ascendingly in the following order:
i' < h'
g' < h'
g' < f'
h' = f'
Could not prove a rewrite lemma for the defined symbol i'.
Rules:
i'(x, x) → i'(a', b')
g'(x, x) → g'(a', b')
h'(s'(f'(x))) → h'(f'(x))
f'(s'(x)) → s'(s'(f'(h'(s'(x)))))
f'(g'(s'(x), y)) → f'(g'(x, s'(y)))
h'(g'(x, s'(y))) → h'(g'(s'(x), y))
h'(i'(x, y)) → i'(i'(c', h'(h'(y))), x)
g'(a', g'(x, g'(b', g'(a', g'(x, y))))) → g'(a', g'(a', g'(a', g'(x, g'(b', g'(b', y))))))
Types:
i' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
a' :: a':b':s':c'
b' :: a':b':s':c'
g' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
h' :: a':b':s':c' → a':b':s':c'
s' :: a':b':s':c' → a':b':s':c'
f' :: a':b':s':c' → a':b':s':c'
c' :: a':b':s':c'
_hole_a':b':s':c'1 :: a':b':s':c'
_gen_a':b':s':c'2 :: Nat → a':b':s':c'
Generator Equations:
_gen_a':b':s':c'2(0) ⇔ b'
_gen_a':b':s':c'2(+(x, 1)) ⇔ s'(_gen_a':b':s':c'2(x))
The following defined symbols remain to be analysed:
g', h', f'
They will be analysed ascendingly in the following order:
g' < h'
g' < f'
h' = f'
Could not prove a rewrite lemma for the defined symbol g'.
Rules:
i'(x, x) → i'(a', b')
g'(x, x) → g'(a', b')
h'(s'(f'(x))) → h'(f'(x))
f'(s'(x)) → s'(s'(f'(h'(s'(x)))))
f'(g'(s'(x), y)) → f'(g'(x, s'(y)))
h'(g'(x, s'(y))) → h'(g'(s'(x), y))
h'(i'(x, y)) → i'(i'(c', h'(h'(y))), x)
g'(a', g'(x, g'(b', g'(a', g'(x, y))))) → g'(a', g'(a', g'(a', g'(x, g'(b', g'(b', y))))))
Types:
i' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
a' :: a':b':s':c'
b' :: a':b':s':c'
g' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
h' :: a':b':s':c' → a':b':s':c'
s' :: a':b':s':c' → a':b':s':c'
f' :: a':b':s':c' → a':b':s':c'
c' :: a':b':s':c'
_hole_a':b':s':c'1 :: a':b':s':c'
_gen_a':b':s':c'2 :: Nat → a':b':s':c'
Generator Equations:
_gen_a':b':s':c'2(0) ⇔ b'
_gen_a':b':s':c'2(+(x, 1)) ⇔ s'(_gen_a':b':s':c'2(x))
The following defined symbols remain to be analysed:
f', h'
They will be analysed ascendingly in the following order:
h' = f'
Could not prove a rewrite lemma for the defined symbol f'.
Rules:
i'(x, x) → i'(a', b')
g'(x, x) → g'(a', b')
h'(s'(f'(x))) → h'(f'(x))
f'(s'(x)) → s'(s'(f'(h'(s'(x)))))
f'(g'(s'(x), y)) → f'(g'(x, s'(y)))
h'(g'(x, s'(y))) → h'(g'(s'(x), y))
h'(i'(x, y)) → i'(i'(c', h'(h'(y))), x)
g'(a', g'(x, g'(b', g'(a', g'(x, y))))) → g'(a', g'(a', g'(a', g'(x, g'(b', g'(b', y))))))
Types:
i' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
a' :: a':b':s':c'
b' :: a':b':s':c'
g' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
h' :: a':b':s':c' → a':b':s':c'
s' :: a':b':s':c' → a':b':s':c'
f' :: a':b':s':c' → a':b':s':c'
c' :: a':b':s':c'
_hole_a':b':s':c'1 :: a':b':s':c'
_gen_a':b':s':c'2 :: Nat → a':b':s':c'
Generator Equations:
_gen_a':b':s':c'2(0) ⇔ b'
_gen_a':b':s':c'2(+(x, 1)) ⇔ s'(_gen_a':b':s':c'2(x))
The following defined symbols remain to be analysed:
h'
They will be analysed ascendingly in the following order:
h' = f'
Could not prove a rewrite lemma for the defined symbol h'.
Rules:
i'(x, x) → i'(a', b')
g'(x, x) → g'(a', b')
h'(s'(f'(x))) → h'(f'(x))
f'(s'(x)) → s'(s'(f'(h'(s'(x)))))
f'(g'(s'(x), y)) → f'(g'(x, s'(y)))
h'(g'(x, s'(y))) → h'(g'(s'(x), y))
h'(i'(x, y)) → i'(i'(c', h'(h'(y))), x)
g'(a', g'(x, g'(b', g'(a', g'(x, y))))) → g'(a', g'(a', g'(a', g'(x, g'(b', g'(b', y))))))
Types:
i' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
a' :: a':b':s':c'
b' :: a':b':s':c'
g' :: a':b':s':c' → a':b':s':c' → a':b':s':c'
h' :: a':b':s':c' → a':b':s':c'
s' :: a':b':s':c' → a':b':s':c'
f' :: a':b':s':c' → a':b':s':c'
c' :: a':b':s':c'
_hole_a':b':s':c'1 :: a':b':s':c'
_gen_a':b':s':c'2 :: Nat → a':b':s':c'
Generator Equations:
_gen_a':b':s':c'2(0) ⇔ b'
_gen_a':b':s':c'2(+(x, 1)) ⇔ s'(_gen_a':b':s':c'2(x))
No more defined symbols left to analyse.