(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
The (relative) TRS S consists of the following rules:
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
insert(::(@x17874_3, @xs17875_3), ::(nil, @ys17560_3)) →+ ::(nil, insert(::(@x17874_3, @xs17875_3), @ys17560_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@ys17560_3 / ::(nil, @ys17560_3)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
The (relative) TRS S consists of the following rules:
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#less(@x, @y) → #cklt(#compare(@x, @y))
and(@x, @y) → #and(@x, @y)
insert(@x, @l) → insert#1(@l, @x)
insert#1(::(@y, @ys), @x) → insert#2(leq(@x, @y), @x, @y, @ys)
insert#1(nil, @x) → ::(@x, nil)
insert#2(#false, @x, @y, @ys) → ::(@y, insert(@x, @ys))
insert#2(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
isortlist(@l) → isortlist#1(@l)
isortlist#1(::(@x, @xs)) → insert(@x, isortlist(@xs))
isortlist#1(nil) → nil
leq(@l1, @l2) → leq#1(@l1, @l2)
leq#1(::(@x, @xs), @l2) → leq#2(@l2, @x, @xs)
leq#1(nil, @l2) → #true
leq#2(::(@y, @ys), @x, @xs) → or(#less(@x, @y), and(#equal(@x, @y), leq(@xs, @ys)))
leq#2(nil, @x, @xs) → #false
or(@x, @y) → #or(@x, @y)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#or(#false, #false) → #false
#or(#false, #true) → #true
#or(#true, #false) → #true
#or(#true, #true) → #true
Types:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
#eq,
#compare,
insert,
insert#1,
leq,
isortlist,
isortlist#1,
leq#1They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1
(8) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
#eq, #compare, insert, insert#1, leq, isortlist, isortlist#1, leq#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
#eq(
gen_:::nil:#0:#neg:#pos:#s4_3(
+(
1,
n6_3)),
gen_:::nil:#0:#neg:#pos:#s4_3(
n6_3)) →
#false, rt ∈ Ω(0)
Induction Base:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s4_3(0)) →RΩ(0)
#false
Induction Step:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, +(n6_3, 1))), gen_:::nil:#0:#neg:#pos:#s4_3(+(n6_3, 1))) →RΩ(0)
#and(#eq(nil, nil), #eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3))) →RΩ(0)
#and(#true, #eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3))) →IH
#and(#true, #false) →RΩ(0)
#false
We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).
(10) Complex Obligation (BEST)
(11) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
#compare, insert, insert#1, leq, isortlist, isortlist#1, leq#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1
(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol #compare.
(13) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
leq#1, insert, insert#1, leq, isortlist, isortlist#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1
(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
leq#1(
gen_:::nil:#0:#neg:#pos:#s4_3(
+(
1,
n6609912_3)),
gen_:::nil:#0:#neg:#pos:#s4_3(
n6609912_3)) →
*5_3, rt ∈ Ω(n6609912
3)
Induction Base:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s4_3(0))
Induction Step:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, +(n6609912_3, 1))), gen_:::nil:#0:#neg:#pos:#s4_3(+(n6609912_3, 1))) →RΩ(1)
leq#2(gen_:::nil:#0:#neg:#pos:#s4_3(+(n6609912_3, 1)), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3))) →RΩ(1)
or(#less(nil, nil), and(#equal(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#equal(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#eq(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)))) →RΩ(0)
or(#cklt(#compare(nil, nil)), and(#true, leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#true, leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)))) →IH
or(#cklt(#compare(nil, nil)), and(#true, *5_3))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(15) Complex Obligation (BEST)
(16) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)) → *5_3, rt ∈ Ω(n66099123)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
leq, insert, insert#1, isortlist, isortlist#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1
(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
leq(
gen_:::nil:#0:#neg:#pos:#s4_3(
n31189360_3),
gen_:::nil:#0:#neg:#pos:#s4_3(
n31189360_3)) →
*5_3, rt ∈ Ω(n31189360
3)
Induction Base:
leq(gen_:::nil:#0:#neg:#pos:#s4_3(0), gen_:::nil:#0:#neg:#pos:#s4_3(0))
Induction Step:
leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(n31189360_3, 1)), gen_:::nil:#0:#neg:#pos:#s4_3(+(n31189360_3, 1))) →RΩ(1)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(n31189360_3, 1)), gen_:::nil:#0:#neg:#pos:#s4_3(+(n31189360_3, 1))) →RΩ(1)
leq#2(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n31189360_3)), nil, gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) →RΩ(1)
or(#less(nil, nil), and(#equal(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#equal(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#eq(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)))) →RΩ(0)
or(#cklt(#compare(nil, nil)), and(#true, leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)))) →IH
or(#cklt(#compare(nil, nil)), and(#true, *5_3))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(18) Complex Obligation (BEST)
(19) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)) → *5_3, rt ∈ Ω(n66099123)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
leq#1, insert, insert#1, isortlist, isortlist#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
leq < insert#1
leq = leq#1
isortlist = isortlist#1
(20) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
leq#1(
gen_:::nil:#0:#neg:#pos:#s4_3(
+(
1,
n54570090_3)),
gen_:::nil:#0:#neg:#pos:#s4_3(
n54570090_3)) →
*5_3, rt ∈ Ω(n54570090
3)
Induction Base:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s4_3(0))
Induction Step:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, +(n54570090_3, 1))), gen_:::nil:#0:#neg:#pos:#s4_3(+(n54570090_3, 1))) →RΩ(1)
leq#2(gen_:::nil:#0:#neg:#pos:#s4_3(+(n54570090_3, 1)), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3))) →RΩ(1)
or(#less(nil, nil), and(#equal(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#equal(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#eq(nil, nil), leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)))) →RΩ(0)
or(#cklt(#compare(nil, nil)), and(#true, leq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)))) →RΩ(1)
or(#cklt(#compare(nil, nil)), and(#true, leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)))) →IH
or(#cklt(#compare(nil, nil)), and(#true, *5_3))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(21) Complex Obligation (BEST)
(22) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
insert#1, insert, isortlist, isortlist#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
isortlist = isortlist#1
(23) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
insert#1(
gen_:::nil:#0:#neg:#pos:#s4_3(
+(
1,
n79157408_3)),
gen_:::nil:#0:#neg:#pos:#s4_3(
1)) →
*5_3, rt ∈ Ω(n79157408
3)
Induction Base:
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s4_3(1))
Induction Step:
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, +(n79157408_3, 1))), gen_:::nil:#0:#neg:#pos:#s4_3(1)) →RΩ(1)
insert#2(leq(gen_:::nil:#0:#neg:#pos:#s4_3(1), nil), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3))) →RΩ(1)
insert#2(leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(1), nil), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3))) →RΩ(1)
insert#2(leq#2(nil, nil, gen_:::nil:#0:#neg:#pos:#s4_3(0)), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3))) →RΩ(1)
insert#2(#false, gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3))) →RΩ(1)
::(nil, insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3)))) →RΩ(1)
::(nil, insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1))) →IH
::(nil, *5_3)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(24) Complex Obligation (BEST)
(25) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n791574083)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
insert, isortlist, isortlist#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
isortlist = isortlist#1
(26) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
insert(
gen_:::nil:#0:#neg:#pos:#s4_3(
1),
gen_:::nil:#0:#neg:#pos:#s4_3(
n79186636_3)) →
*5_3, rt ∈ Ω(n79186636
3)
Induction Base:
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(0))
Induction Step:
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(+(n79186636_3, 1))) →RΩ(1)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(n79186636_3, 1)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) →RΩ(1)
insert#2(leq(gen_:::nil:#0:#neg:#pos:#s4_3(1), nil), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) →RΩ(1)
insert#2(leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(1), nil), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) →RΩ(1)
insert#2(leq#2(nil, nil, gen_:::nil:#0:#neg:#pos:#s4_3(0)), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) →RΩ(1)
insert#2(#false, gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) →RΩ(1)
::(nil, insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3))) →IH
::(nil, *5_3)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(27) Complex Obligation (BEST)
(28) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n791574083)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
insert#1, isortlist, isortlist#1
They will be analysed ascendingly in the following order:
insert = insert#1
insert < isortlist#1
isortlist = isortlist#1
(29) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
insert#1(
gen_:::nil:#0:#neg:#pos:#s4_3(
+(
1,
n79212620_3)),
gen_:::nil:#0:#neg:#pos:#s4_3(
1)) →
*5_3, rt ∈ Ω(n79212620
3)
Induction Base:
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, 0)), gen_:::nil:#0:#neg:#pos:#s4_3(1))
Induction Step:
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, +(n79212620_3, 1))), gen_:::nil:#0:#neg:#pos:#s4_3(1)) →RΩ(1)
insert#2(leq(gen_:::nil:#0:#neg:#pos:#s4_3(1), nil), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3))) →RΩ(1)
insert#2(leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(1), nil), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3))) →RΩ(1)
insert#2(leq#2(nil, nil, gen_:::nil:#0:#neg:#pos:#s4_3(0)), gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3))) →RΩ(1)
insert#2(#false, gen_:::nil:#0:#neg:#pos:#s4_3(1), nil, gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3))) →RΩ(1)
::(nil, insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)))) →RΩ(1)
::(nil, insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1))) →IH
::(nil, *5_3)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(30) Complex Obligation (BEST)
(31) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
isortlist#1, isortlist
They will be analysed ascendingly in the following order:
isortlist = isortlist#1
(32) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
isortlist#1(
gen_:::nil:#0:#neg:#pos:#s4_3(
n79243034_3)) →
*5_3, rt ∈ Ω(n79243034
3)
Induction Base:
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(0))
Induction Step:
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(n79243034_3, 1))) →RΩ(1)
insert(nil, isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(n79243034_3))) →RΩ(1)
insert(nil, isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79243034_3))) →IH
insert(nil, *5_3)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(33) Complex Obligation (BEST)
(34) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79243034_3)) → *5_3, rt ∈ Ω(n792430343)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
isortlist
They will be analysed ascendingly in the following order:
isortlist = isortlist#1
(35) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
isortlist(
gen_:::nil:#0:#neg:#pos:#s4_3(
n79269613_3)) →
*5_3, rt ∈ Ω(n79269613
3)
Induction Base:
isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(0))
Induction Step:
isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(+(n79269613_3, 1))) →RΩ(1)
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(n79269613_3, 1))) →RΩ(1)
insert(nil, isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(n79269613_3))) →IH
insert(nil, *5_3)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(36) Complex Obligation (BEST)
(37) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79243034_3)) → *5_3, rt ∈ Ω(n792430343)
isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(n79269613_3)) → *5_3, rt ∈ Ω(n792696133)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
The following defined symbols remain to be analysed:
isortlist#1
They will be analysed ascendingly in the following order:
isortlist = isortlist#1
(38) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
isortlist#1(
gen_:::nil:#0:#neg:#pos:#s4_3(
n79300691_3)) →
*5_3, rt ∈ Ω(n79300691
3)
Induction Base:
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(0))
Induction Step:
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(n79300691_3, 1))) →RΩ(1)
insert(nil, isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(n79300691_3))) →RΩ(1)
insert(nil, isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79300691_3))) →IH
insert(nil, *5_3)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(39) Complex Obligation (BEST)
(40) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79300691_3)) → *5_3, rt ∈ Ω(n793006913)
isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(n79269613_3)) → *5_3, rt ∈ Ω(n792696133)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(41) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(42) BOUNDS(n^1, INF)
(43) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79300691_3)) → *5_3, rt ∈ Ω(n793006913)
isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(n79269613_3)) → *5_3, rt ∈ Ω(n792696133)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(44) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(45) BOUNDS(n^1, INF)
(46) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79243034_3)) → *5_3, rt ∈ Ω(n792430343)
isortlist(gen_:::nil:#0:#neg:#pos:#s4_3(n79269613_3)) → *5_3, rt ∈ Ω(n792696133)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(47) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(48) BOUNDS(n^1, INF)
(49) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
isortlist#1(gen_:::nil:#0:#neg:#pos:#s4_3(n79243034_3)) → *5_3, rt ∈ Ω(n792430343)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(50) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(51) BOUNDS(n^1, INF)
(52) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79212620_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n792126203)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(53) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(54) BOUNDS(n^1, INF)
(55) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n791574083)
insert(gen_:::nil:#0:#neg:#pos:#s4_3(1), gen_:::nil:#0:#neg:#pos:#s4_3(n79186636_3)) → *5_3, rt ∈ Ω(n791866363)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(56) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(57) BOUNDS(n^1, INF)
(58) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
insert#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n79157408_3)), gen_:::nil:#0:#neg:#pos:#s4_3(1)) → *5_3, rt ∈ Ω(n791574083)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(59) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(60) BOUNDS(n^1, INF)
(61) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(62) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n54570090_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n54570090_3)) → *5_3, rt ∈ Ω(n545700903)
(63) BOUNDS(n^1, INF)
(64) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)) → *5_3, rt ∈ Ω(n66099123)
leq(gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3), gen_:::nil:#0:#neg:#pos:#s4_3(n31189360_3)) → *5_3, rt ∈ Ω(n311893603)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(65) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)) → *5_3, rt ∈ Ω(n66099123)
(66) BOUNDS(n^1, INF)
(67) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)) → *5_3, rt ∈ Ω(n66099123)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(68) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
leq#1(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6609912_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6609912_3)) → *5_3, rt ∈ Ω(n66099123)
(69) BOUNDS(n^1, INF)
(70) Obligation:
Innermost TRS:
Rules:
#equal(
@x,
@y) →
#eq(
@x,
@y)
#less(
@x,
@y) →
#cklt(
#compare(
@x,
@y))
and(
@x,
@y) →
#and(
@x,
@y)
insert(
@x,
@l) →
insert#1(
@l,
@x)
insert#1(
::(
@y,
@ys),
@x) →
insert#2(
leq(
@x,
@y),
@x,
@y,
@ys)
insert#1(
nil,
@x) →
::(
@x,
nil)
insert#2(
#false,
@x,
@y,
@ys) →
::(
@y,
insert(
@x,
@ys))
insert#2(
#true,
@x,
@y,
@ys) →
::(
@x,
::(
@y,
@ys))
isortlist(
@l) →
isortlist#1(
@l)
isortlist#1(
::(
@x,
@xs)) →
insert(
@x,
isortlist(
@xs))
isortlist#1(
nil) →
nilleq(
@l1,
@l2) →
leq#1(
@l1,
@l2)
leq#1(
::(
@x,
@xs),
@l2) →
leq#2(
@l2,
@x,
@xs)
leq#1(
nil,
@l2) →
#trueleq#2(
::(
@y,
@ys),
@x,
@xs) →
or(
#less(
@x,
@y),
and(
#equal(
@x,
@y),
leq(
@xs,
@ys)))
leq#2(
nil,
@x,
@xs) →
#falseor(
@x,
@y) →
#or(
@x,
@y)
#and(
#false,
#false) →
#false#and(
#false,
#true) →
#false#and(
#true,
#false) →
#false#and(
#true,
#true) →
#true#cklt(
#EQ) →
#false#cklt(
#GT) →
#false#cklt(
#LT) →
#true#compare(
#0,
#0) →
#EQ#compare(
#0,
#neg(
@y)) →
#GT#compare(
#0,
#pos(
@y)) →
#LT#compare(
#0,
#s(
@y)) →
#LT#compare(
#neg(
@x),
#0) →
#LT#compare(
#neg(
@x),
#neg(
@y)) →
#compare(
@y,
@x)
#compare(
#neg(
@x),
#pos(
@y)) →
#LT#compare(
#pos(
@x),
#0) →
#GT#compare(
#pos(
@x),
#neg(
@y)) →
#GT#compare(
#pos(
@x),
#pos(
@y)) →
#compare(
@x,
@y)
#compare(
#s(
@x),
#0) →
#GT#compare(
#s(
@x),
#s(
@y)) →
#compare(
@x,
@y)
#eq(
#0,
#0) →
#true#eq(
#0,
#neg(
@y)) →
#false#eq(
#0,
#pos(
@y)) →
#false#eq(
#0,
#s(
@y)) →
#false#eq(
#neg(
@x),
#0) →
#false#eq(
#neg(
@x),
#neg(
@y)) →
#eq(
@x,
@y)
#eq(
#neg(
@x),
#pos(
@y)) →
#false#eq(
#pos(
@x),
#0) →
#false#eq(
#pos(
@x),
#neg(
@y)) →
#false#eq(
#pos(
@x),
#pos(
@y)) →
#eq(
@x,
@y)
#eq(
#s(
@x),
#0) →
#false#eq(
#s(
@x),
#s(
@y)) →
#eq(
@x,
@y)
#eq(
::(
@x_1,
@x_2),
::(
@y_1,
@y_2)) →
#and(
#eq(
@x_1,
@y_1),
#eq(
@x_2,
@y_2))
#eq(
::(
@x_1,
@x_2),
nil) →
#false#eq(
nil,
::(
@y_1,
@y_2)) →
#false#eq(
nil,
nil) →
#true#or(
#false,
#false) →
#false#or(
#false,
#true) →
#true#or(
#true,
#false) →
#true#or(
#true,
#true) →
#trueTypes:
#equal :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#less :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #EQ:#GT:#LT
and :: #false:#true → #false:#true → #false:#true
#and :: #false:#true → #false:#true → #false:#true
insert :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
:: :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
insert#2 :: #false:#true → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
nil :: :::nil:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
isortlist :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
isortlist#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
leq#1 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
leq#2 :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s → #false:#true
or :: #false:#true → #false:#true → #false:#true
#or :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:#0:#neg:#pos:#s
#neg :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#pos :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
#s :: :::nil:#0:#neg:#pos:#s → :::nil:#0:#neg:#pos:#s
hole_#false:#true1_3 :: #false:#true
hole_:::nil:#0:#neg:#pos:#s2_3 :: :::nil:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_3 :: #EQ:#GT:#LT
gen_:::nil:#0:#neg:#pos:#s4_3 :: Nat → :::nil:#0:#neg:#pos:#s
Lemmas:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
Generator Equations:
gen_:::nil:#0:#neg:#pos:#s4_3(0) ⇔ nil
gen_:::nil:#0:#neg:#pos:#s4_3(+(x, 1)) ⇔ ::(nil, gen_:::nil:#0:#neg:#pos:#s4_3(x))
No more defined symbols left to analyse.
(71) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(1) was proven with the following lemma:
#eq(gen_:::nil:#0:#neg:#pos:#s4_3(+(1, n6_3)), gen_:::nil:#0:#neg:#pos:#s4_3(n6_3)) → #false, rt ∈ Ω(0)
(72) BOUNDS(1, INF)