and(true, y) → y
and(false, y) → false
eq(nil, nil) → true
eq(cons(t, l), nil) → false
eq(nil, cons(t, l)) → false
eq(cons(t, l), cons(t', l')) → and(eq(t, t'), eq(l, l'))
eq(var(l), var(l')) → eq(l, l')
eq(var(l), apply(t, s)) → false
eq(var(l), lambda(x, t)) → false
eq(apply(t, s), var(l)) → false
eq(apply(t, s), apply(t', s')) → and(eq(t, t'), eq(s, s'))
eq(apply(t, s), lambda(x, t)) → false
eq(lambda(x, t), var(l)) → false
eq(lambda(x, t), apply(t, s)) → false
eq(lambda(x, t), lambda(x', t')) → and(eq(x, x'), eq(t, t'))
if(true, var(k), var(l')) → var(k)
if(false, var(k), var(l')) → var(l')
ren(var(l), var(k), var(l')) → if(eq(l, l'), var(k), var(l'))
ren(x, y, apply(t, s)) → apply(ren(x, y, t), ren(x, y, s))
ren(x, y, lambda(z, t)) → lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
and'(true', y) → y
and'(false', y) → false'
eq'(nil', nil') → true'
eq'(cons'(t, l), nil') → false'
eq'(nil', cons'(t, l)) → false'
eq'(cons'(t, l), cons'(t', l')) → and'(eq'(t, t'), eq'(l, l'))
eq'(var'(l), var'(l')) → eq'(l, l')
eq'(var'(l), apply'(t, s)) → false'
eq'(var'(l), lambda'(x, t)) → false'
eq'(apply'(t, s), var'(l)) → false'
eq'(apply'(t, s), apply'(t', s')) → and'(eq'(t, t'), eq'(s, s'))
eq'(apply'(t, s), lambda'(x, t)) → false'
eq'(lambda'(x, t), var'(l)) → false'
eq'(lambda'(x, t), apply'(t, s)) → false'
eq'(lambda'(x, t), lambda'(x', t')) → and'(eq'(x, x'), eq'(t, t'))
if'(true', var'(k), var'(l')) → var'(k)
if'(false', var'(k), var'(l')) → var'(l')
ren'(var'(l), var'(k), var'(l')) → if'(eq'(l, l'), var'(k), var'(l'))
ren'(x, y, apply'(t, s)) → apply'(ren'(x, y, t), ren'(x, y, s))
ren'(x, y, lambda'(z, t)) → lambda'(var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), ren'(x, y, ren'(z, var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), t)))
Infered types.
Rules:
and'(true', y) → y
and'(false', y) → false'
eq'(nil', nil') → true'
eq'(cons'(t, l), nil') → false'
eq'(nil', cons'(t, l)) → false'
eq'(cons'(t, l), cons'(t', l')) → and'(eq'(t, t'), eq'(l, l'))
eq'(var'(l), var'(l')) → eq'(l, l')
eq'(var'(l), apply'(t, s)) → false'
eq'(var'(l), lambda'(x, t)) → false'
eq'(apply'(t, s), var'(l)) → false'
eq'(apply'(t, s), apply'(t', s')) → and'(eq'(t, t'), eq'(s, s'))
eq'(apply'(t, s), lambda'(x, t)) → false'
eq'(lambda'(x, t), var'(l)) → false'
eq'(lambda'(x, t), apply'(t, s)) → false'
eq'(lambda'(x, t), lambda'(x', t')) → and'(eq'(x, x'), eq'(t, t'))
if'(true', var'(k), var'(l')) → var'(k)
if'(false', var'(k), var'(l')) → var'(l')
ren'(var'(l), var'(k), var'(l')) → if'(eq'(l, l'), var'(k), var'(l'))
ren'(x, y, apply'(t, s)) → apply'(ren'(x, y, t), ren'(x, y, s))
ren'(x, y, lambda'(z, t)) → lambda'(var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), ren'(x, y, ren'(z, var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), t)))
Types:
and' :: true':false' → true':false' → true':false'
true' :: true':false'
false' :: true':false'
eq' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → true':false'
nil' :: nil':cons':var':apply':lambda'
cons' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
var' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
apply' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
lambda' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
if' :: true':false' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
ren' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
_hole_true':false'1 :: true':false'
_hole_nil':cons':var':apply':lambda'2 :: nil':cons':var':apply':lambda'
_gen_nil':cons':var':apply':lambda'3 :: Nat → nil':cons':var':apply':lambda'
Heuristically decided to analyse the following defined symbols:
eq', ren'
They will be analysed ascendingly in the following order:
eq' < ren'
Rules:
and'(true', y) → y
and'(false', y) → false'
eq'(nil', nil') → true'
eq'(cons'(t, l), nil') → false'
eq'(nil', cons'(t, l)) → false'
eq'(cons'(t, l), cons'(t', l')) → and'(eq'(t, t'), eq'(l, l'))
eq'(var'(l), var'(l')) → eq'(l, l')
eq'(var'(l), apply'(t, s)) → false'
eq'(var'(l), lambda'(x, t)) → false'
eq'(apply'(t, s), var'(l)) → false'
eq'(apply'(t, s), apply'(t', s')) → and'(eq'(t, t'), eq'(s, s'))
eq'(apply'(t, s), lambda'(x, t)) → false'
eq'(lambda'(x, t), var'(l)) → false'
eq'(lambda'(x, t), apply'(t, s)) → false'
eq'(lambda'(x, t), lambda'(x', t')) → and'(eq'(x, x'), eq'(t, t'))
if'(true', var'(k), var'(l')) → var'(k)
if'(false', var'(k), var'(l')) → var'(l')
ren'(var'(l), var'(k), var'(l')) → if'(eq'(l, l'), var'(k), var'(l'))
ren'(x, y, apply'(t, s)) → apply'(ren'(x, y, t), ren'(x, y, s))
ren'(x, y, lambda'(z, t)) → lambda'(var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), ren'(x, y, ren'(z, var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), t)))
Types:
and' :: true':false' → true':false' → true':false'
true' :: true':false'
false' :: true':false'
eq' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → true':false'
nil' :: nil':cons':var':apply':lambda'
cons' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
var' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
apply' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
lambda' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
if' :: true':false' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
ren' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
_hole_true':false'1 :: true':false'
_hole_nil':cons':var':apply':lambda'2 :: nil':cons':var':apply':lambda'
_gen_nil':cons':var':apply':lambda'3 :: Nat → nil':cons':var':apply':lambda'
Generator Equations:
_gen_nil':cons':var':apply':lambda'3(0) ⇔ nil'
_gen_nil':cons':var':apply':lambda'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons':var':apply':lambda'3(x))
The following defined symbols remain to be analysed:
eq', ren'
They will be analysed ascendingly in the following order:
eq' < ren'
Proved the following rewrite lemma:
eq'(_gen_nil':cons':var':apply':lambda'3(_n5), _gen_nil':cons':var':apply':lambda'3(_n5)) → true', rt ∈ Ω(1 + n5)
Induction Base:
eq'(_gen_nil':cons':var':apply':lambda'3(0), _gen_nil':cons':var':apply':lambda'3(0)) →RΩ(1)
true'
Induction Step:
eq'(_gen_nil':cons':var':apply':lambda'3(+(_$n6, 1)), _gen_nil':cons':var':apply':lambda'3(+(_$n6, 1))) →RΩ(1)
and'(eq'(nil', nil'), eq'(_gen_nil':cons':var':apply':lambda'3(_$n6), _gen_nil':cons':var':apply':lambda'3(_$n6))) →RΩ(1)
and'(true', eq'(_gen_nil':cons':var':apply':lambda'3(_$n6), _gen_nil':cons':var':apply':lambda'3(_$n6))) →IH
and'(true', true') →RΩ(1)
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
and'(true', y) → y
and'(false', y) → false'
eq'(nil', nil') → true'
eq'(cons'(t, l), nil') → false'
eq'(nil', cons'(t, l)) → false'
eq'(cons'(t, l), cons'(t', l')) → and'(eq'(t, t'), eq'(l, l'))
eq'(var'(l), var'(l')) → eq'(l, l')
eq'(var'(l), apply'(t, s)) → false'
eq'(var'(l), lambda'(x, t)) → false'
eq'(apply'(t, s), var'(l)) → false'
eq'(apply'(t, s), apply'(t', s')) → and'(eq'(t, t'), eq'(s, s'))
eq'(apply'(t, s), lambda'(x, t)) → false'
eq'(lambda'(x, t), var'(l)) → false'
eq'(lambda'(x, t), apply'(t, s)) → false'
eq'(lambda'(x, t), lambda'(x', t')) → and'(eq'(x, x'), eq'(t, t'))
if'(true', var'(k), var'(l')) → var'(k)
if'(false', var'(k), var'(l')) → var'(l')
ren'(var'(l), var'(k), var'(l')) → if'(eq'(l, l'), var'(k), var'(l'))
ren'(x, y, apply'(t, s)) → apply'(ren'(x, y, t), ren'(x, y, s))
ren'(x, y, lambda'(z, t)) → lambda'(var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), ren'(x, y, ren'(z, var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), t)))
Types:
and' :: true':false' → true':false' → true':false'
true' :: true':false'
false' :: true':false'
eq' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → true':false'
nil' :: nil':cons':var':apply':lambda'
cons' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
var' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
apply' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
lambda' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
if' :: true':false' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
ren' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
_hole_true':false'1 :: true':false'
_hole_nil':cons':var':apply':lambda'2 :: nil':cons':var':apply':lambda'
_gen_nil':cons':var':apply':lambda'3 :: Nat → nil':cons':var':apply':lambda'
Lemmas:
eq'(_gen_nil':cons':var':apply':lambda'3(_n5), _gen_nil':cons':var':apply':lambda'3(_n5)) → true', rt ∈ Ω(1 + n5)
Generator Equations:
_gen_nil':cons':var':apply':lambda'3(0) ⇔ nil'
_gen_nil':cons':var':apply':lambda'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons':var':apply':lambda'3(x))
The following defined symbols remain to be analysed:
ren'
Could not prove a rewrite lemma for the defined symbol ren'.
Rules:
and'(true', y) → y
and'(false', y) → false'
eq'(nil', nil') → true'
eq'(cons'(t, l), nil') → false'
eq'(nil', cons'(t, l)) → false'
eq'(cons'(t, l), cons'(t', l')) → and'(eq'(t, t'), eq'(l, l'))
eq'(var'(l), var'(l')) → eq'(l, l')
eq'(var'(l), apply'(t, s)) → false'
eq'(var'(l), lambda'(x, t)) → false'
eq'(apply'(t, s), var'(l)) → false'
eq'(apply'(t, s), apply'(t', s')) → and'(eq'(t, t'), eq'(s, s'))
eq'(apply'(t, s), lambda'(x, t)) → false'
eq'(lambda'(x, t), var'(l)) → false'
eq'(lambda'(x, t), apply'(t, s)) → false'
eq'(lambda'(x, t), lambda'(x', t')) → and'(eq'(x, x'), eq'(t, t'))
if'(true', var'(k), var'(l')) → var'(k)
if'(false', var'(k), var'(l')) → var'(l')
ren'(var'(l), var'(k), var'(l')) → if'(eq'(l, l'), var'(k), var'(l'))
ren'(x, y, apply'(t, s)) → apply'(ren'(x, y, t), ren'(x, y, s))
ren'(x, y, lambda'(z, t)) → lambda'(var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), ren'(x, y, ren'(z, var'(cons'(x, cons'(y, cons'(lambda'(z, t), nil')))), t)))
Types:
and' :: true':false' → true':false' → true':false'
true' :: true':false'
false' :: true':false'
eq' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → true':false'
nil' :: nil':cons':var':apply':lambda'
cons' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
var' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
apply' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
lambda' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
if' :: true':false' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
ren' :: nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda' → nil':cons':var':apply':lambda'
_hole_true':false'1 :: true':false'
_hole_nil':cons':var':apply':lambda'2 :: nil':cons':var':apply':lambda'
_gen_nil':cons':var':apply':lambda'3 :: Nat → nil':cons':var':apply':lambda'
Lemmas:
eq'(_gen_nil':cons':var':apply':lambda'3(_n5), _gen_nil':cons':var':apply':lambda'3(_n5)) → true', rt ∈ Ω(1 + n5)
Generator Equations:
_gen_nil':cons':var':apply':lambda'3(0) ⇔ nil'
_gen_nil':cons':var':apply':lambda'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons':var':apply':lambda'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
eq'(_gen_nil':cons':var':apply':lambda'3(_n5), _gen_nil':cons':var':apply':lambda'3(_n5)) → true', rt ∈ Ω(1 + n5)