a__p(0) → 0
a__p(s(X)) → mark(X)
a__leq(0, Y) → true
a__leq(s(X), 0) → false
a__leq(s(X), s(Y)) → a__leq(mark(X), mark(Y))
a__if(true, X, Y) → mark(X)
a__if(false, X, Y) → mark(Y)
a__diff(X, Y) → a__if(a__leq(mark(X), mark(Y)), 0, s(diff(p(X), Y)))
mark(p(X)) → a__p(mark(X))
mark(leq(X1, X2)) → a__leq(mark(X1), mark(X2))
mark(if(X1, X2, X3)) → a__if(mark(X1), X2, X3)
mark(diff(X1, X2)) → a__diff(mark(X1), mark(X2))
mark(0) → 0
mark(s(X)) → s(mark(X))
mark(true) → true
mark(false) → false
a__p(X) → p(X)
a__leq(X1, X2) → leq(X1, X2)
a__if(X1, X2, X3) → if(X1, X2, X3)
a__diff(X1, X2) → diff(X1, X2)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Infered types.
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Heuristically decided to analyse the following defined symbols:
a__p', mark', a__leq', a__if'
They will be analysed ascendingly in the following order:
a__p' = mark'
a__p' = a__leq'
a__p' = a__if'
mark' = a__leq'
mark' = a__if'
a__leq' = a__if'
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Generator Equations:
_gen_0':s':true':false':p':diff':leq':if'2(0) ⇔ 0'
_gen_0':s':true':false':p':diff':leq':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':false':p':diff':leq':if'2(x))
The following defined symbols remain to be analysed:
mark', a__p', a__leq', a__if'
They will be analysed ascendingly in the following order:
a__p' = mark'
a__p' = a__leq'
a__p' = a__if'
mark' = a__leq'
mark' = a__if'
a__leq' = a__if'
Proved the following rewrite lemma:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n4)) → _gen_0':s':true':false':p':diff':leq':if'2(_n4), rt ∈ Ω(1 + n4)
Induction Base:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(0)) →RΩ(1)
0'
Induction Step:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(+(_$n5, 1))) →RΩ(1)
s'(mark'(_gen_0':s':true':false':p':diff':leq':if'2(_$n5))) →IH
s'(_gen_0':s':true':false':p':diff':leq':if'2(_$n5))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Lemmas:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n4)) → _gen_0':s':true':false':p':diff':leq':if'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_0':s':true':false':p':diff':leq':if'2(0) ⇔ 0'
_gen_0':s':true':false':p':diff':leq':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':false':p':diff':leq':if'2(x))
The following defined symbols remain to be analysed:
a__p', a__leq', a__if'
They will be analysed ascendingly in the following order:
a__p' = mark'
a__p' = a__leq'
a__p' = a__if'
mark' = a__leq'
mark' = a__if'
a__leq' = a__if'
Could not prove a rewrite lemma for the defined symbol a__p'.
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Lemmas:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n4)) → _gen_0':s':true':false':p':diff':leq':if'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_0':s':true':false':p':diff':leq':if'2(0) ⇔ 0'
_gen_0':s':true':false':p':diff':leq':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':false':p':diff':leq':if'2(x))
The following defined symbols remain to be analysed:
a__leq', a__if'
They will be analysed ascendingly in the following order:
a__p' = mark'
a__p' = a__leq'
a__p' = a__if'
mark' = a__leq'
mark' = a__if'
a__leq' = a__if'
Proved the following rewrite lemma:
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_n1237), _gen_0':s':true':false':p':diff':leq':if'2(_n1237)) → true', rt ∈ Ω(1 + n1237 + n12372)
Induction Base:
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(0), _gen_0':s':true':false':p':diff':leq':if'2(0)) →RΩ(1)
true'
Induction Step:
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(+(_$n1238, 1)), _gen_0':s':true':false':p':diff':leq':if'2(+(_$n1238, 1))) →RΩ(1)
a__leq'(mark'(_gen_0':s':true':false':p':diff':leq':if'2(_$n1238)), mark'(_gen_0':s':true':false':p':diff':leq':if'2(_$n1238))) →LΩ(1 + $n1238)
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_$n1238), mark'(_gen_0':s':true':false':p':diff':leq':if'2(_$n1238))) →LΩ(1 + $n1238)
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_$n1238), _gen_0':s':true':false':p':diff':leq':if'2(_$n1238)) →IH
true'
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Lemmas:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n4)) → _gen_0':s':true':false':p':diff':leq':if'2(_n4), rt ∈ Ω(1 + n4)
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_n1237), _gen_0':s':true':false':p':diff':leq':if'2(_n1237)) → true', rt ∈ Ω(1 + n1237 + n12372)
Generator Equations:
_gen_0':s':true':false':p':diff':leq':if'2(0) ⇔ 0'
_gen_0':s':true':false':p':diff':leq':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':false':p':diff':leq':if'2(x))
The following defined symbols remain to be analysed:
a__if', a__p', mark'
They will be analysed ascendingly in the following order:
a__p' = mark'
a__p' = a__leq'
a__p' = a__if'
mark' = a__leq'
mark' = a__if'
a__leq' = a__if'
Could not prove a rewrite lemma for the defined symbol a__if'.
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Lemmas:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n4)) → _gen_0':s':true':false':p':diff':leq':if'2(_n4), rt ∈ Ω(1 + n4)
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_n1237), _gen_0':s':true':false':p':diff':leq':if'2(_n1237)) → true', rt ∈ Ω(1 + n1237 + n12372)
Generator Equations:
_gen_0':s':true':false':p':diff':leq':if'2(0) ⇔ 0'
_gen_0':s':true':false':p':diff':leq':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':false':p':diff':leq':if'2(x))
The following defined symbols remain to be analysed:
mark', a__p'
They will be analysed ascendingly in the following order:
a__p' = mark'
a__p' = a__leq'
a__p' = a__if'
mark' = a__leq'
mark' = a__if'
a__leq' = a__if'
Proved the following rewrite lemma:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n3490)) → _gen_0':s':true':false':p':diff':leq':if'2(_n3490), rt ∈ Ω(1 + n3490)
Induction Base:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(0)) →RΩ(1)
0'
Induction Step:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(+(_$n3491, 1))) →RΩ(1)
s'(mark'(_gen_0':s':true':false':p':diff':leq':if'2(_$n3491))) →IH
s'(_gen_0':s':true':false':p':diff':leq':if'2(_$n3491))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Lemmas:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n3490)) → _gen_0':s':true':false':p':diff':leq':if'2(_n3490), rt ∈ Ω(1 + n3490)
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_n1237), _gen_0':s':true':false':p':diff':leq':if'2(_n1237)) → true', rt ∈ Ω(1 + n1237 + n12372)
Generator Equations:
_gen_0':s':true':false':p':diff':leq':if'2(0) ⇔ 0'
_gen_0':s':true':false':p':diff':leq':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':false':p':diff':leq':if'2(x))
The following defined symbols remain to be analysed:
a__p'
They will be analysed ascendingly in the following order:
a__p' = mark'
a__p' = a__leq'
a__p' = a__if'
mark' = a__leq'
mark' = a__if'
a__leq' = a__if'
Could not prove a rewrite lemma for the defined symbol a__p'.
Rules:
a__p'(0') → 0'
a__p'(s'(X)) → mark'(X)
a__leq'(0', Y) → true'
a__leq'(s'(X), 0') → false'
a__leq'(s'(X), s'(Y)) → a__leq'(mark'(X), mark'(Y))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__diff'(X, Y) → a__if'(a__leq'(mark'(X), mark'(Y)), 0', s'(diff'(p'(X), Y)))
mark'(p'(X)) → a__p'(mark'(X))
mark'(leq'(X1, X2)) → a__leq'(mark'(X1), mark'(X2))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(diff'(X1, X2)) → a__diff'(mark'(X1), mark'(X2))
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(true') → true'
mark'(false') → false'
a__p'(X) → p'(X)
a__leq'(X1, X2) → leq'(X1, X2)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__diff'(X1, X2) → diff'(X1, X2)
Types:
a__p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
0' :: 0':s':true':false':p':diff':leq':if'
s' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
mark' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
true' :: 0':s':true':false':p':diff':leq':if'
false' :: 0':s':true':false':p':diff':leq':if'
a__if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
a__diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
diff' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
p' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
leq' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
if' :: 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if' → 0':s':true':false':p':diff':leq':if'
_hole_0':s':true':false':p':diff':leq':if'1 :: 0':s':true':false':p':diff':leq':if'
_gen_0':s':true':false':p':diff':leq':if'2 :: Nat → 0':s':true':false':p':diff':leq':if'
Lemmas:
mark'(_gen_0':s':true':false':p':diff':leq':if'2(_n3490)) → _gen_0':s':true':false':p':diff':leq':if'2(_n3490), rt ∈ Ω(1 + n3490)
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_n1237), _gen_0':s':true':false':p':diff':leq':if'2(_n1237)) → true', rt ∈ Ω(1 + n1237 + n12372)
Generator Equations:
_gen_0':s':true':false':p':diff':leq':if'2(0) ⇔ 0'
_gen_0':s':true':false':p':diff':leq':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':false':p':diff':leq':if'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
a__leq'(_gen_0':s':true':false':p':diff':leq':if'2(_n1237), _gen_0':s':true':false':p':diff':leq':if'2(_n1237)) → true', rt ∈ Ω(1 + n1237 + n12372)