inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x, y) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x, z)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y, z))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Sliced the following arguments:
plus'/1
Runtime Complexity TRS:
The TRS R consists of the following rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Infered types.
Rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Types:
inc' :: s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
plus' :: s':0' → s':0'
ifPlus' :: false':true' → s':0' → s':0' → s':0' → s':0'
eq' :: s':0' → s':0' → false':true'
minus' :: s':0' → s':0' → s':0'
false' :: false':true'
true' :: false':true'
times' :: s':0' → s':0' → s':0'
timesIter' :: s':0' → s':0' → s':0' → s':0'
ifTimes' :: false':true' → s':0' → s':0' → s':0' → s':0' → s':0'
f' :: g':h'
g' :: g':h'
h' :: g':h'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_hole_g':h'3 :: g':h'
_gen_s':0'4 :: Nat → s':0'
Heuristically decided to analyse the following defined symbols:
inc', plus', eq', minus', timesIter'
They will be analysed ascendingly in the following order:
inc' < plus'
eq' < plus'
minus' < plus'
plus' < timesIter'
eq' < timesIter'
minus' < timesIter'
Rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Types:
inc' :: s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
plus' :: s':0' → s':0'
ifPlus' :: false':true' → s':0' → s':0' → s':0' → s':0'
eq' :: s':0' → s':0' → false':true'
minus' :: s':0' → s':0' → s':0'
false' :: false':true'
true' :: false':true'
times' :: s':0' → s':0' → s':0'
timesIter' :: s':0' → s':0' → s':0' → s':0'
ifTimes' :: false':true' → s':0' → s':0' → s':0' → s':0' → s':0'
f' :: g':h'
g' :: g':h'
h' :: g':h'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_hole_g':h'3 :: g':h'
_gen_s':0'4 :: Nat → s':0'
Generator Equations:
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))
The following defined symbols remain to be analysed:
inc', plus', eq', minus', timesIter'
They will be analysed ascendingly in the following order:
inc' < plus'
eq' < plus'
minus' < plus'
plus' < timesIter'
eq' < timesIter'
minus' < timesIter'
Proved the following rewrite lemma:
inc'(_gen_s':0'4(_n6)) → _gen_s':0'4(+(1, _n6)), rt ∈ Ω(1 + n6)
Induction Base:
inc'(_gen_s':0'4(0)) →RΩ(1)
s'(0')
Induction Step:
inc'(_gen_s':0'4(+(_$n7, 1))) →RΩ(1)
s'(inc'(_gen_s':0'4(_$n7))) →IH
s'(_gen_s':0'4(+(1, _$n7)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Types:
inc' :: s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
plus' :: s':0' → s':0'
ifPlus' :: false':true' → s':0' → s':0' → s':0' → s':0'
eq' :: s':0' → s':0' → false':true'
minus' :: s':0' → s':0' → s':0'
false' :: false':true'
true' :: false':true'
times' :: s':0' → s':0' → s':0'
timesIter' :: s':0' → s':0' → s':0' → s':0'
ifTimes' :: false':true' → s':0' → s':0' → s':0' → s':0' → s':0'
f' :: g':h'
g' :: g':h'
h' :: g':h'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_hole_g':h'3 :: g':h'
_gen_s':0'4 :: Nat → s':0'
Lemmas:
inc'(_gen_s':0'4(_n6)) → _gen_s':0'4(+(1, _n6)), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))
The following defined symbols remain to be analysed:
eq', plus', minus', timesIter'
They will be analysed ascendingly in the following order:
eq' < plus'
minus' < plus'
plus' < timesIter'
eq' < timesIter'
minus' < timesIter'
Proved the following rewrite lemma:
eq'(_gen_s':0'4(_n784), _gen_s':0'4(+(1, _n784))) → false', rt ∈ Ω(1 + n784)
Induction Base:
eq'(_gen_s':0'4(0), _gen_s':0'4(+(1, 0))) →RΩ(1)
false'
Induction Step:
eq'(_gen_s':0'4(+(_$n785, 1)), _gen_s':0'4(+(1, +(_$n785, 1)))) →RΩ(1)
eq'(_gen_s':0'4(_$n785), _gen_s':0'4(+(1, _$n785))) →IH
false'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Types:
inc' :: s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
plus' :: s':0' → s':0'
ifPlus' :: false':true' → s':0' → s':0' → s':0' → s':0'
eq' :: s':0' → s':0' → false':true'
minus' :: s':0' → s':0' → s':0'
false' :: false':true'
true' :: false':true'
times' :: s':0' → s':0' → s':0'
timesIter' :: s':0' → s':0' → s':0' → s':0'
ifTimes' :: false':true' → s':0' → s':0' → s':0' → s':0' → s':0'
f' :: g':h'
g' :: g':h'
h' :: g':h'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_hole_g':h'3 :: g':h'
_gen_s':0'4 :: Nat → s':0'
Lemmas:
inc'(_gen_s':0'4(_n6)) → _gen_s':0'4(+(1, _n6)), rt ∈ Ω(1 + n6)
eq'(_gen_s':0'4(_n784), _gen_s':0'4(+(1, _n784))) → false', rt ∈ Ω(1 + n784)
Generator Equations:
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))
The following defined symbols remain to be analysed:
minus', plus', timesIter'
They will be analysed ascendingly in the following order:
minus' < plus'
plus' < timesIter'
minus' < timesIter'
Proved the following rewrite lemma:
minus'(_gen_s':0'4(_n2103), _gen_s':0'4(_n2103)) → _gen_s':0'4(0), rt ∈ Ω(1 + n2103)
Induction Base:
minus'(_gen_s':0'4(0), _gen_s':0'4(0)) →RΩ(1)
0'
Induction Step:
minus'(_gen_s':0'4(+(_$n2104, 1)), _gen_s':0'4(+(_$n2104, 1))) →RΩ(1)
minus'(_gen_s':0'4(_$n2104), _gen_s':0'4(_$n2104)) →IH
_gen_s':0'4(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Types:
inc' :: s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
plus' :: s':0' → s':0'
ifPlus' :: false':true' → s':0' → s':0' → s':0' → s':0'
eq' :: s':0' → s':0' → false':true'
minus' :: s':0' → s':0' → s':0'
false' :: false':true'
true' :: false':true'
times' :: s':0' → s':0' → s':0'
timesIter' :: s':0' → s':0' → s':0' → s':0'
ifTimes' :: false':true' → s':0' → s':0' → s':0' → s':0' → s':0'
f' :: g':h'
g' :: g':h'
h' :: g':h'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_hole_g':h'3 :: g':h'
_gen_s':0'4 :: Nat → s':0'
Lemmas:
inc'(_gen_s':0'4(_n6)) → _gen_s':0'4(+(1, _n6)), rt ∈ Ω(1 + n6)
eq'(_gen_s':0'4(_n784), _gen_s':0'4(+(1, _n784))) → false', rt ∈ Ω(1 + n784)
minus'(_gen_s':0'4(_n2103), _gen_s':0'4(_n2103)) → _gen_s':0'4(0), rt ∈ Ω(1 + n2103)
Generator Equations:
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))
The following defined symbols remain to be analysed:
plus', timesIter'
They will be analysed ascendingly in the following order:
plus' < timesIter'
Could not prove a rewrite lemma for the defined symbol plus'.
Rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Types:
inc' :: s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
plus' :: s':0' → s':0'
ifPlus' :: false':true' → s':0' → s':0' → s':0' → s':0'
eq' :: s':0' → s':0' → false':true'
minus' :: s':0' → s':0' → s':0'
false' :: false':true'
true' :: false':true'
times' :: s':0' → s':0' → s':0'
timesIter' :: s':0' → s':0' → s':0' → s':0'
ifTimes' :: false':true' → s':0' → s':0' → s':0' → s':0' → s':0'
f' :: g':h'
g' :: g':h'
h' :: g':h'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_hole_g':h'3 :: g':h'
_gen_s':0'4 :: Nat → s':0'
Lemmas:
inc'(_gen_s':0'4(_n6)) → _gen_s':0'4(+(1, _n6)), rt ∈ Ω(1 + n6)
eq'(_gen_s':0'4(_n784), _gen_s':0'4(+(1, _n784))) → false', rt ∈ Ω(1 + n784)
minus'(_gen_s':0'4(_n2103), _gen_s':0'4(_n2103)) → _gen_s':0'4(0), rt ∈ Ω(1 + n2103)
Generator Equations:
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))
The following defined symbols remain to be analysed:
timesIter'
Could not prove a rewrite lemma for the defined symbol timesIter'.
Rules:
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
plus'(x) → ifPlus'(eq'(x, 0'), minus'(x, s'(0')), x, inc'(x))
ifPlus'(false', x, y, z) → plus'(x)
ifPlus'(true', x, y, z) → y
minus'(s'(x), s'(y)) → minus'(x, y)
minus'(0', x) → 0'
minus'(x, 0') → x
minus'(x, x) → 0'
eq'(s'(x), s'(y)) → eq'(x, y)
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(0', 0') → true'
eq'(x, x) → true'
times'(x, y) → timesIter'(x, y, 0')
timesIter'(x, y, z) → ifTimes'(eq'(x, 0'), minus'(x, s'(0')), y, z, plus'(y))
ifTimes'(true', x, y, z, u) → z
ifTimes'(false', x, y, z, u) → timesIter'(x, y, u)
f' → g'
f' → h'
Types:
inc' :: s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
plus' :: s':0' → s':0'
ifPlus' :: false':true' → s':0' → s':0' → s':0' → s':0'
eq' :: s':0' → s':0' → false':true'
minus' :: s':0' → s':0' → s':0'
false' :: false':true'
true' :: false':true'
times' :: s':0' → s':0' → s':0'
timesIter' :: s':0' → s':0' → s':0' → s':0'
ifTimes' :: false':true' → s':0' → s':0' → s':0' → s':0' → s':0'
f' :: g':h'
g' :: g':h'
h' :: g':h'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_hole_g':h'3 :: g':h'
_gen_s':0'4 :: Nat → s':0'
Lemmas:
inc'(_gen_s':0'4(_n6)) → _gen_s':0'4(+(1, _n6)), rt ∈ Ω(1 + n6)
eq'(_gen_s':0'4(_n784), _gen_s':0'4(+(1, _n784))) → false', rt ∈ Ω(1 + n784)
minus'(_gen_s':0'4(_n2103), _gen_s':0'4(_n2103)) → _gen_s':0'4(0), rt ∈ Ω(1 + n2103)
Generator Equations:
_gen_s':0'4(0) ⇔ 0'
_gen_s':0'4(+(x, 1)) ⇔ s'(_gen_s':0'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
inc'(_gen_s':0'4(_n6)) → _gen_s':0'4(+(1, _n6)), rt ∈ Ω(1 + n6)