Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/isort-fold)

The rewrite relation of the following TRS is considered.

fold#3(insert_ord(x2),Nil) → Nil (1)
fold#3(insert_ord(x6),Cons(x4,x2)) → insert_ord#2(x6,x4,fold#3(insert_ord(x6),x2)) (2)
cond_insert_ord_x_ys_1(True,x3,x2,x1) → Cons(x3,Cons(x2,x1)) (3)
cond_insert_ord_x_ys_1(False,x0,x5,x2) → Cons(x5,insert_ord#2(leq,x0,x2)) (4)
insert_ord#2(leq,x2,Nil) → Cons(x2,Nil) (5)
insert_ord#2(leq,x6,Cons(x4,x2)) → cond_insert_ord_x_ys_1(leq#2(x6,x4),x6,x4,x2) (6)
leq#2(0,x8) → True (7)
leq#2(S(x12),0) → False (8)
leq#2(S(x4),S(x2)) → leq#2(x4,x2) (9)
main(x3) → fold#3(insert_ord(leq),x3) (10)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n2).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
fold#3#(insert_ord(z0),Nil) → c (12)
originates from
fold#3(insert_ord(z0),Nil) → Nil (11)
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
originates from
fold#3(insert_ord(z0),Cons(z1,z2)) → insert_ord#2(z0,z1,fold#3(insert_ord(z0),z2)) (13)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
originates from
cond_insert_ord_x_ys_1(True,z0,z1,z2) → Cons(z0,Cons(z1,z2)) (15)
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
originates from
cond_insert_ord_x_ys_1(False,z0,z1,z2) → Cons(z1,insert_ord#2(leq,z0,z2)) (17)
insert_ord#2#(leq,z0,Nil) → c4 (20)
originates from
insert_ord#2(leq,z0,Nil) → Cons(z0,Nil) (19)
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
originates from
insert_ord#2(leq,z0,Cons(z1,z2)) → cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) (21)
leq#2#(0,z0) → c6 (24)
originates from
leq#2(0,z0) → True (23)
leq#2#(S(z0),0) → c7 (26)
originates from
leq#2(S(z0),0) → False (25)
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
originates from
leq#2(S(z0),S(z1)) → leq#2(z0,z1) (27)
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)
originates from
main(z0) → fold#3(insert_ord(leq),z0) (29)
Moreover, we add the following terms to the innermost strategy.
fold#3#(insert_ord(z0),Nil)
fold#3#(insert_ord(z0),Cons(z1,z2))
cond_insert_ord_x_ys_1#(True,z0,z1,z2)
cond_insert_ord_x_ys_1#(False,z0,z1,z2)
insert_ord#2#(leq,z0,Nil)
insert_ord#2#(leq,z0,Cons(z1,z2))
leq#2#(0,z0)
leq#2#(S(z0),0)
leq#2#(S(z0),S(z1))
main#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.
main(z0) → fold#3(insert_ord(leq),z0) (29)

1.1.1 Rule Shifting

The rules
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[fold#3(x1, x2)] = 1 + 1 · x1 + 2 · x2
[insert_ord#2(x1, x2, x3)] = 2 + 1 · x3
[cond_insert_ord_x_ys_1(x1,...,x4)] = 1 + 3 · x1 + 1 · x4
[leq#2(x1, x2)] = 1
[fold#3#(x1, x2)] = 0
[cond_insert_ord_x_ys_1#(x1,...,x4)] = 0
[insert_ord#2#(x1, x2, x3)] = 0
[leq#2#(x1, x2)] = 0
[main#(x1)] = 1
[0] = 0
[True] = 3
[S(x1)] = 1 · x1 + 0
[False] = 3
[insert_ord(x1)] = 1
[Nil] = 0
[Cons(x1, x2)] = 2 + 1 · x2
[leq] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
fold#3#(insert_ord(z0),Nil) → c (12)
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
insert_ord#2#(leq,z0,Nil) → c4 (20)
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
leq#2#(0,z0) → c6 (24)
leq#2#(S(z0),0) → c7 (26)
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)

1.1.1.1 Rule Shifting

The rules
fold#3#(insert_ord(z0),Nil) → c (12)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
insert_ord#2#(leq,z0,Nil) → c4 (20)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[fold#3(x1, x2)] = 1 + 1 · x1 + 1 · x2
[insert_ord#2(x1, x2, x3)] = 1 + 1 · x2
[cond_insert_ord_x_ys_1(x1,...,x4)] = 1 + 1 · x2 + 1 · x3 + 1 · x4
[leq#2(x1, x2)] = 1 + 1 · x1 + 1 · x2
[fold#3#(x1, x2)] = 1 · x1 + 0 + 1 · x2
[cond_insert_ord_x_ys_1#(x1,...,x4)] = 1 + 1 · x2
[insert_ord#2#(x1, x2, x3)] = 1 + 1 · x2
[leq#2#(x1, x2)] = 0
[main#(x1)] = 1 + 1 · x1
[0] = 1
[True] = 1
[S(x1)] = 1 + 1 · x1
[False] = 1
[insert_ord(x1)] = 1
[Nil] = 1
[Cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[leq] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
fold#3#(insert_ord(z0),Nil) → c (12)
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
insert_ord#2#(leq,z0,Nil) → c4 (20)
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
leq#2#(0,z0) → c6 (24)
leq#2#(S(z0),0) → c7 (26)
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)

1.1.1.1.1 Rule Shifting

The rules
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[fold#3(x1, x2)] = 1 + 1 · x1 + 1 · x2
[insert_ord#2(x1, x2, x3)] = 1 + 1 · x2
[cond_insert_ord_x_ys_1(x1,...,x4)] = 1 + 1 · x2 + 1 · x3 + 1 · x4
[leq#2(x1, x2)] = 1 + 1 · x1 + 1 · x2
[fold#3#(x1, x2)] = 1 · x1 + 0 + 1 · x2
[cond_insert_ord_x_ys_1#(x1,...,x4)] = 1 · x2 + 0
[insert_ord#2#(x1, x2, x3)] = 1 · x2 + 0
[leq#2#(x1, x2)] = 0
[main#(x1)] = 1 + 1 · x1
[0] = 1
[True] = 1
[S(x1)] = 1 + 1 · x1
[False] = 1
[insert_ord(x1)] = 1
[Nil] = 1
[Cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[leq] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
fold#3#(insert_ord(z0),Nil) → c (12)
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
insert_ord#2#(leq,z0,Nil) → c4 (20)
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
leq#2#(0,z0) → c6 (24)
leq#2#(S(z0),0) → c7 (26)
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)

1.1.1.1.1.1 Rule Shifting

The rules
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[fold#3(x1, x2)] = 1 · x2 + 0
[insert_ord#2(x1, x2, x3)] = 1 · x2 + 0 + 1 · x3
[cond_insert_ord_x_ys_1(x1,...,x4)] = 1 · x2 + 0 + 1 · x3 + 1 · x4
[leq#2(x1, x2)] = 0
[fold#3#(x1, x2)] = 1 · x2 · x2 + 0
[cond_insert_ord_x_ys_1#(x1,...,x4)] = 2 · x2 · x4 + 0
[insert_ord#2#(x1, x2, x3)] = 2 · x2 · x3 + 0
[leq#2#(x1, x2)] = 2 · x1 · x2 + 0
[main#(x1)] = 2 + 2 · x1 + 1 · x1 · x1
[0] = 0
[True] = 0
[S(x1)] = 2 + 1 · x1
[False] = 0
[insert_ord(x1)] = 0
[Nil] = 0
[Cons(x1, x2)] = 1 · x1 + 0 + 1 · x2
[leq] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
fold#3#(insert_ord(z0),Nil) → c (12)
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
insert_ord#2#(leq,z0,Nil) → c4 (20)
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
leq#2#(0,z0) → c6 (24)
leq#2#(S(z0),0) → c7 (26)
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)
cond_insert_ord_x_ys_1(False,z0,z1,z2) → Cons(z1,insert_ord#2(leq,z0,z2)) (17)
cond_insert_ord_x_ys_1(True,z0,z1,z2) → Cons(z0,Cons(z1,z2)) (15)
insert_ord#2(leq,z0,Nil) → Cons(z0,Nil) (19)
insert_ord#2(leq,z0,Cons(z1,z2)) → cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) (21)
fold#3(insert_ord(z0),Cons(z1,z2)) → insert_ord#2(z0,z1,fold#3(insert_ord(z0),z2)) (13)
fold#3(insert_ord(z0),Nil) → Nil (11)

1.1.1.1.1.1.1 Rule Shifting

The rules
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
leq#2#(0,z0) → c6 (24)
leq#2#(S(z0),0) → c7 (26)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[fold#3(x1, x2)] = 2 · x2 + 0
[insert_ord#2(x1, x2, x3)] = 1 + 1 · x3
[cond_insert_ord_x_ys_1(x1,...,x4)] = 2 + 1 · x4
[leq#2(x1, x2)] = 0
[fold#3#(x1, x2)] = 2 · x2 · x2 + 0
[cond_insert_ord_x_ys_1#(x1,...,x4)] = 1 + 2 · x4
[insert_ord#2#(x1, x2, x3)] = 1 + 2 · x3
[leq#2#(x1, x2)] = 1
[main#(x1)] = 2 + 2 · x1 + 2 · x1 · x1
[0] = 0
[True] = 0
[S(x1)] = 0
[False] = 0
[insert_ord(x1)] = 0
[Nil] = 0
[Cons(x1, x2)] = 1 + 1 · x2
[leq] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
fold#3#(insert_ord(z0),Nil) → c (12)
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
insert_ord#2#(leq,z0,Nil) → c4 (20)
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
leq#2#(0,z0) → c6 (24)
leq#2#(S(z0),0) → c7 (26)
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)
cond_insert_ord_x_ys_1(False,z0,z1,z2) → Cons(z1,insert_ord#2(leq,z0,z2)) (17)
cond_insert_ord_x_ys_1(True,z0,z1,z2) → Cons(z0,Cons(z1,z2)) (15)
insert_ord#2(leq,z0,Nil) → Cons(z0,Nil) (19)
insert_ord#2(leq,z0,Cons(z1,z2)) → cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) (21)
fold#3(insert_ord(z0),Cons(z1,z2)) → insert_ord#2(z0,z1,fold#3(insert_ord(z0),z2)) (13)
fold#3(insert_ord(z0),Nil) → Nil (11)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7] = 0
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[fold#3(x1, x2)] = 2 · x2 + 0
[insert_ord#2(x1, x2, x3)] = 1 + 1 · x3
[cond_insert_ord_x_ys_1(x1,...,x4)] = 2 + 1 · x4
[leq#2(x1, x2)] = 0
[fold#3#(x1, x2)] = 2 · x2 + 0 + 2 · x2 · x2
[cond_insert_ord_x_ys_1#(x1,...,x4)] = 2 + 2 · x4
[insert_ord#2#(x1, x2, x3)] = 2 · x3 + 0
[leq#2#(x1, x2)] = 0
[main#(x1)] = 2 + 2 · x1 + 2 · x1 · x1
[0] = 0
[True] = 0
[S(x1)] = 0
[False] = 0
[insert_ord(x1)] = 0
[Nil] = 0
[Cons(x1, x2)] = 1 + 1 · x2
[leq] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
fold#3#(insert_ord(z0),Nil) → c (12)
fold#3#(insert_ord(z0),Cons(z1,z2)) → c1(insert_ord#2#(z0,z1,fold#3(insert_ord(z0),z2)),fold#3#(insert_ord(z0),z2)) (14)
cond_insert_ord_x_ys_1#(True,z0,z1,z2) → c2 (16)
cond_insert_ord_x_ys_1#(False,z0,z1,z2) → c3(insert_ord#2#(leq,z0,z2)) (18)
insert_ord#2#(leq,z0,Nil) → c4 (20)
insert_ord#2#(leq,z0,Cons(z1,z2)) → c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) (22)
leq#2#(0,z0) → c6 (24)
leq#2#(S(z0),0) → c7 (26)
leq#2#(S(z0),S(z1)) → c8(leq#2#(z0,z1)) (28)
main#(z0) → c9(fold#3#(insert_ord(leq),z0)) (30)
cond_insert_ord_x_ys_1(False,z0,z1,z2) → Cons(z1,insert_ord#2(leq,z0,z2)) (17)
cond_insert_ord_x_ys_1(True,z0,z1,z2) → Cons(z0,Cons(z1,z2)) (15)
insert_ord#2(leq,z0,Nil) → Cons(z0,Nil) (19)
insert_ord#2(leq,z0,Cons(z1,z2)) → cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) (21)
fold#3(insert_ord(z0),Cons(z1,z2)) → insert_ord#2(z0,z1,fold#3(insert_ord(z0),z2)) (13)
fold#3(insert_ord(z0),Nil) → Nil (11)

1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).