del(.(x, .(y, z))) → f(=(x, y), x, y, z)
f(true, x, y, z) → del(.(y, z))
f(false, x, y, z) → .(x, del(.(y, z)))
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))
Infered types.
Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))
Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'
Heuristically decided to analyse the following defined symbols:
del', ='
They will be analysed ascendingly in the following order:
=' < del'
Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))
Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'
Generator Equations:
_gen_.':nil':u':v'3(0) ⇔ nil'
_gen_.':nil':u':v'3(+(x, 1)) ⇔ .'(nil', _gen_.':nil':u':v'3(x))
_gen_true':false':and'4(0) ⇔ false'
_gen_true':false':and'4(+(x, 1)) ⇔ and'(false', _gen_true':false':and'4(x))
The following defined symbols remain to be analysed:
=', del'
They will be analysed ascendingly in the following order:
=' < del'
Could not prove a rewrite lemma for the defined symbol ='.
Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))
Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'
Generator Equations:
_gen_.':nil':u':v'3(0) ⇔ nil'
_gen_.':nil':u':v'3(+(x, 1)) ⇔ .'(nil', _gen_.':nil':u':v'3(x))
_gen_true':false':and'4(0) ⇔ false'
_gen_true':false':and'4(+(x, 1)) ⇔ and'(false', _gen_true':false':and'4(x))
The following defined symbols remain to be analysed:
del'
Proved the following rewrite lemma:
del'(_gen_.':nil':u':v'3(+(2, _n116))) → _*5, rt ∈ Ω(n116)
Induction Base:
del'(_gen_.':nil':u':v'3(+(2, 0)))
Induction Step:
del'(_gen_.':nil':u':v'3(+(2, +(_$n117, 1)))) →RΩ(1)
f'(='(nil', nil'), nil', nil', _gen_.':nil':u':v'3(+(1, _$n117))) →RΩ(1)
f'(true', nil', nil', _gen_.':nil':u':v'3(+(1, _$n117))) →RΩ(1)
del'(.'(nil', _gen_.':nil':u':v'3(+(1, _$n117)))) →IH
_*5
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))
Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'
Lemmas:
del'(_gen_.':nil':u':v'3(+(2, _n116))) → _*5, rt ∈ Ω(n116)
Generator Equations:
_gen_.':nil':u':v'3(0) ⇔ nil'
_gen_.':nil':u':v'3(+(x, 1)) ⇔ .'(nil', _gen_.':nil':u':v'3(x))
_gen_true':false':and'4(0) ⇔ false'
_gen_true':false':and'4(+(x, 1)) ⇔ and'(false', _gen_true':false':and'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
del'(_gen_.':nil':u':v'3(+(2, _n116))) → _*5, rt ∈ Ω(n116)