double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'
Infered types.
Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'
Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'
Heuristically decided to analyse the following defined symbols:
permute', ack', plus'
They will be analysed ascendingly in the following order:
ack' < permute'
plus' < ack'
Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'
Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'
Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))
The following defined symbols remain to be analysed:
plus', permute', ack'
They will be analysed ascendingly in the following order:
ack' < permute'
plus' < ack'
Proved the following rewrite lemma:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)
Induction Base:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, 0))))
Induction Step:
plus'(_gen_false':true':0':s'3(_a1642), _gen_false':true':0':s'3(+(2, *(2, +(_$n6, 1))))) →RΩ(1)
s'(plus'(s'(_gen_false':true':0':s'3(_a1642)), _gen_false':true':0':s'3(+(2, *(2, _$n6))))) →RΩ(1)
s'(plus'(_gen_false':true':0':s'3(_a1642), s'(_gen_false':true':0':s'3(+(2, *(2, _$n6)))))) →RΩ(1)
s'(s'(plus'(s'(_gen_false':true':0':s'3(_a1642)), _gen_false':true':0':s'3(+(1, *(2, _$n6)))))) →RΩ(1)
s'(s'(plus'(_gen_false':true':0':s'3(_a1642), s'(_gen_false':true':0':s'3(+(1, *(2, _$n6))))))) →IH
s'(s'(_*4))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'
Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'
Lemmas:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)
Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))
The following defined symbols remain to be analysed:
ack', permute'
They will be analysed ascendingly in the following order:
ack' < permute'
Proved the following rewrite lemma:
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, _n4750))) → _*4, rt ∈ Ω(n4750)
Induction Base:
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, 0)))
Induction Step:
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, +(_$n4751, 1)))) →RΩ(1)
ack'(_gen_false':true':0':s'3(0), ack'(s'(_gen_false':true':0':s'3(0)), _gen_false':true':0':s'3(+(1, _$n4751)))) →IH
ack'(_gen_false':true':0':s'3(0), _*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'
Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'
Lemmas:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, _n4750))) → _*4, rt ∈ Ω(n4750)
Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))
The following defined symbols remain to be analysed:
permute'
Could not prove a rewrite lemma for the defined symbol permute'.
Rules:
double'(x) → permute'(x, x, a')
permute'(x, y, a') → permute'(isZero'(x), x, b')
permute'(false', x, b') → permute'(ack'(x, x), p'(x), c')
permute'(true', x, b') → 0'
permute'(y, x, c') → s'(s'(permute'(x, y, a')))
p'(0') → 0'
p'(s'(x)) → x
ack'(0', x) → plus'(x, s'(0'))
ack'(s'(x), 0') → ack'(x, s'(0'))
ack'(s'(x), s'(y)) → ack'(x, ack'(s'(x), y))
plus'(0', y) → y
plus'(s'(x), y) → plus'(x, s'(y))
plus'(x, s'(s'(y))) → s'(plus'(s'(x), y))
plus'(x, s'(0')) → s'(x)
plus'(x, 0') → x
isZero'(0') → true'
isZero'(s'(x)) → false'
Types:
double' :: false':true':0':s' → false':true':0':s'
permute' :: false':true':0':s' → false':true':0':s' → a':b':c' → false':true':0':s'
a' :: a':b':c'
isZero' :: false':true':0':s' → false':true':0':s'
b' :: a':b':c'
false' :: false':true':0':s'
ack' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
p' :: false':true':0':s' → false':true':0':s'
c' :: a':b':c'
true' :: false':true':0':s'
0' :: false':true':0':s'
s' :: false':true':0':s' → false':true':0':s'
plus' :: false':true':0':s' → false':true':0':s' → false':true':0':s'
_hole_false':true':0':s'1 :: false':true':0':s'
_hole_a':b':c'2 :: a':b':c'
_gen_false':true':0':s'3 :: Nat → false':true':0':s'
Lemmas:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)
ack'(_gen_false':true':0':s'3(1), _gen_false':true':0':s'3(+(1, _n4750))) → _*4, rt ∈ Ω(n4750)
Generator Equations:
_gen_false':true':0':s'3(0) ⇔ true'
_gen_false':true':0':s'3(+(x, 1)) ⇔ s'(_gen_false':true':0':s'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
plus'(_gen_false':true':0':s'3(a), _gen_false':true':0':s'3(+(2, *(2, _n5)))) → _*4, rt ∈ Ω(n5)