YES Time: 0.282145 TRS: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))} DP: DP: { le#(s X, s Y) -> le#(X, Y), app#(cons(N, L), Y) -> app#(L, Y), low#(N, cons(M, L)) -> le#(M, N), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(true(), N, cons(M, L)) -> low#(N, L), iflow#(false(), N, cons(M, L)) -> low#(N, L), high#(N, cons(M, L)) -> le#(M, N), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(true(), N, cons(M, L)) -> high#(N, L), ifhigh#(false(), N, cons(M, L)) -> high#(N, L), quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))), quicksort# cons(N, L) -> low#(N, L), quicksort# cons(N, L) -> high#(N, L), quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> quicksort# high(N, L)} TRS: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))} UR: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L))), a(x, y) -> x, a(x, y) -> y} EDG: {(iflow#(true(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L))) (iflow#(true(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> le#(M, N)) (ifhigh#(true(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L))) (ifhigh#(true(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> le#(M, N)) (quicksort# cons(N, L) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L))) (quicksort# cons(N, L) -> low#(N, L), low#(N, cons(M, L)) -> le#(M, N)) (low#(N, cons(M, L)) -> le#(M, N), le#(s X, s Y) -> le#(X, Y)) (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y)) (low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(false(), N, cons(M, L)) -> low#(N, L)) (low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(true(), N, cons(M, L)) -> low#(N, L)) (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> quicksort# high(N, L)) (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> quicksort# low(N, L)) (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> high#(N, L)) (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> low#(N, L)) (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L)))) (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L)))) (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> low#(N, L)) (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> high#(N, L)) (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> quicksort# low(N, L)) (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> quicksort# high(N, L)) (high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(true(), N, cons(M, L)) -> high#(N, L)) (high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(false(), N, cons(M, L)) -> high#(N, L)) (app#(cons(N, L), Y) -> app#(L, Y), app#(cons(N, L), Y) -> app#(L, Y)) (high#(N, cons(M, L)) -> le#(M, N), le#(s X, s Y) -> le#(X, Y)) (quicksort# cons(N, L) -> high#(N, L), high#(N, cons(M, L)) -> le#(M, N)) (quicksort# cons(N, L) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L))) (ifhigh#(false(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> le#(M, N)) (ifhigh#(false(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L))) (iflow#(false(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> le#(M, N)) (iflow#(false(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L))) (quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))), app#(cons(N, L), Y) -> app#(L, Y))} STATUS: arrows: 0.862222 SCCS (5): Scc: {quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> quicksort# high(N, L)} Scc: { high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(true(), N, cons(M, L)) -> high#(N, L), ifhigh#(false(), N, cons(M, L)) -> high#(N, L)} Scc: { low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(true(), N, cons(M, L)) -> low#(N, L), iflow#(false(), N, cons(M, L)) -> low#(N, L)} Scc: {le#(s X, s Y) -> le#(X, Y)} Scc: {app#(cons(N, L), Y) -> app#(L, Y)} SCC (2): Strict: {quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> quicksort# high(N, L)} Weak: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [iflow](x0, x1, x2) = x0, [ifhigh](x0, x1, x2) = x0, [le](x0, x1) = 0, [app](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [low](x0, x1) = x0, [high](x0, x1) = x0, [s](x0) = 0, [quicksort](x0) = 0, [true] = 0, [0] = 0, [false] = 0, [nil] = 1, [quicksort#](x0) = x0 Strict: quicksort# cons(N, L) -> quicksort# high(N, L) 1 + 0N + 1L >= 0 + 0N + 1L quicksort# cons(N, L) -> quicksort# low(N, L) 1 + 0N + 1L >= 0 + 0N + 1L Weak: quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L))) 0 + 0N + 0L >= 1 + 0N + 0L quicksort nil() -> nil() 0 >= 1 ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)) 1 + 0N + 1L + 0M >= 1 + 0N + 1L + 0M ifhigh(true(), N, cons(M, L)) -> high(N, L) 1 + 0N + 1L + 0M >= 0 + 0N + 1L high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)) 1 + 0N + 1L + 0M >= 1 + 0N + 1L + 0M high(N, nil()) -> nil() 1 + 0N >= 1 iflow(false(), N, cons(M, L)) -> low(N, L) 1 + 0N + 1L + 0M >= 0 + 0N + 1L iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)) 1 + 0N + 1L + 0M >= 1 + 0N + 1L + 0M low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)) 1 + 0N + 1L + 0M >= 1 + 0N + 1L + 0M low(N, nil()) -> nil() 1 + 0N >= 1 app(cons(N, L), Y) -> cons(N, app(L, Y)) 2 + 0Y + 0N + 1L >= 2 + 0Y + 0N + 1L app(nil(), Y) -> Y 2 + 0Y >= 1Y le(s X, s Y) -> le(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X le(s X, 0()) -> false() 0 + 0X >= 0 le(0(), Y) -> true() 0 + 0Y >= 0 Qed SCC (3): Strict: { high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(true(), N, cons(M, L)) -> high#(N, L), ifhigh#(false(), N, cons(M, L)) -> high#(N, L)} Weak: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [iflow](x0, x1, x2) = x0 + x1, [ifhigh](x0, x1, x2) = x0 + x1, [le](x0, x1) = x0, [app](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [s](x0) = 0, [quicksort](x0) = 0, [true] = 0, [0] = 0, [false] = 0, [nil] = 1, [ifhigh#](x0, x1, x2) = x0, [high#](x0, x1) = x0 + 1 Strict: ifhigh#(false(), N, cons(M, L)) -> high#(N, L) 1 + 0N + 1L + 0M >= 1 + 0N + 1L ifhigh#(true(), N, cons(M, L)) -> high#(N, L) 1 + 0N + 1L + 0M >= 1 + 0N + 1L high#(N, cons(M, L)) -> ifhigh#(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 1 + 0N + 1L + 0M Weak: quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L))) 0 + 0N + 0L >= 1 + 0N + 0L quicksort nil() -> nil() 0 >= 1 ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)) 0 + 1N + 0L + 0M >= 2 + 0N + 1L + 0M ifhigh(true(), N, cons(M, L)) -> high(N, L) 0 + 1N + 0L + 0M >= 1 + 0N + 1L high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 0 + 2N + 0L + 0M high(N, nil()) -> nil() 2 + 0N >= 1 iflow(false(), N, cons(M, L)) -> low(N, L) 0 + 1N + 0L + 0M >= 1 + 0N + 1L iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)) 0 + 1N + 0L + 0M >= 2 + 0N + 1L + 0M low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 0 + 2N + 0L + 0M low(N, nil()) -> nil() 2 + 0N >= 1 app(cons(N, L), Y) -> cons(N, app(L, Y)) 2 + 0Y + 0N + 1L >= 2 + 0Y + 0N + 1L app(nil(), Y) -> Y 2 + 0Y >= 1Y le(s X, s Y) -> le(X, Y) 0 + 0Y + 0X >= 0 + 1Y + 0X le(s X, 0()) -> false() 0 + 0X >= 0 le(0(), Y) -> true() 0 + 1Y >= 0 SCCS (0): SCC (3): Strict: { low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)), iflow#(true(), N, cons(M, L)) -> low#(N, L), iflow#(false(), N, cons(M, L)) -> low#(N, L)} Weak: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [iflow](x0, x1, x2) = x0 + x1, [ifhigh](x0, x1, x2) = x0 + x1, [le](x0, x1) = x0, [app](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [s](x0) = 0, [quicksort](x0) = 0, [true] = 0, [0] = 0, [false] = 0, [nil] = 1, [iflow#](x0, x1, x2) = x0, [low#](x0, x1) = x0 + 1 Strict: iflow#(false(), N, cons(M, L)) -> low#(N, L) 1 + 0N + 1L + 0M >= 1 + 0N + 1L iflow#(true(), N, cons(M, L)) -> low#(N, L) 1 + 0N + 1L + 0M >= 1 + 0N + 1L low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 1 + 0N + 1L + 0M Weak: quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L))) 0 + 0N + 0L >= 1 + 0N + 0L quicksort nil() -> nil() 0 >= 1 ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)) 0 + 1N + 0L + 0M >= 2 + 0N + 1L + 0M ifhigh(true(), N, cons(M, L)) -> high(N, L) 0 + 1N + 0L + 0M >= 1 + 0N + 1L high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 0 + 2N + 0L + 0M high(N, nil()) -> nil() 2 + 0N >= 1 iflow(false(), N, cons(M, L)) -> low(N, L) 0 + 1N + 0L + 0M >= 1 + 0N + 1L iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)) 0 + 1N + 0L + 0M >= 2 + 0N + 1L + 0M low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 0 + 2N + 0L + 0M low(N, nil()) -> nil() 2 + 0N >= 1 app(cons(N, L), Y) -> cons(N, app(L, Y)) 2 + 0Y + 0N + 1L >= 2 + 0Y + 0N + 1L app(nil(), Y) -> Y 2 + 0Y >= 1Y le(s X, s Y) -> le(X, Y) 0 + 0Y + 0X >= 0 + 1Y + 0X le(s X, 0()) -> false() 0 + 0X >= 0 le(0(), Y) -> true() 0 + 1Y >= 0 SCCS (0): SCC (1): Strict: {le#(s X, s Y) -> le#(X, Y)} Weak: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [iflow](x0, x1, x2) = 0, [ifhigh](x0, x1, x2) = 0, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [quicksort](x0) = 0, [true] = 0, [0] = 1, [false] = 0, [nil] = 1, [le#](x0, x1) = x0 + 1 Strict: le#(s X, s Y) -> le#(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L))) 0 + 0N + 0L >= 1 + 0N + 0L quicksort nil() -> nil() 0 >= 1 ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)) 0 + 0N + 0L + 0M >= 2 + 0N + 1L + 0M ifhigh(true(), N, cons(M, L)) -> high(N, L) 0 + 0N + 0L + 0M >= 1 + 0N + 1L high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 0 + 0N + 0L + 0M high(N, nil()) -> nil() 2 + 0N >= 1 iflow(false(), N, cons(M, L)) -> low(N, L) 0 + 0N + 0L + 0M >= 1 + 0N + 1L iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)) 0 + 0N + 0L + 0M >= 2 + 0N + 1L + 0M low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 0 + 0N + 0L + 0M low(N, nil()) -> nil() 2 + 0N >= 1 app(cons(N, L), Y) -> cons(N, app(L, Y)) 2 + 0Y + 0N + 1L >= 2 + 0Y + 0N + 1L app(nil(), Y) -> Y 2 + 0Y >= 1Y le(s X, s Y) -> le(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X le(s X, 0()) -> false() 2 + 1X >= 0 le(0(), Y) -> true() 2 + 0Y >= 0 Qed SCC (1): Strict: {app#(cons(N, L), Y) -> app#(L, Y)} Weak: { le(0(), Y) -> true(), le(s X, 0()) -> false(), le(s X, s Y) -> le(X, Y), app(nil(), Y) -> Y, app(cons(N, L), Y) -> cons(N, app(L, Y)), low(N, nil()) -> nil(), low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)), iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)), iflow(false(), N, cons(M, L)) -> low(N, L), high(N, nil()) -> nil(), high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)), ifhigh(true(), N, cons(M, L)) -> high(N, L), ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)), quicksort nil() -> nil(), quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [iflow](x0, x1, x2) = 0, [ifhigh](x0, x1, x2) = 0, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = 0, [s](x0) = 1, [quicksort](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [nil] = 1, [app#](x0, x1) = x0 Strict: app#(cons(N, L), Y) -> app#(L, Y) 1 + 0Y + 0N + 1L >= 0 + 0Y + 1L Weak: quicksort cons(N, L) -> app(quicksort low(N, L), cons(N, quicksort high(N, L))) 2 + 0N + 1L >= 3 + 0N + 1L quicksort nil() -> nil() 2 >= 1 ifhigh(false(), N, cons(M, L)) -> cons(M, high(N, L)) 0 + 0N + 0L + 0M >= 1 + 0N + 0L + 0M ifhigh(true(), N, cons(M, L)) -> high(N, L) 0 + 0N + 0L + 0M >= 0 + 0N + 0L high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L)) 0 + 0N + 0L + 0M >= 0 + 0N + 0L + 0M high(N, nil()) -> nil() 0 + 0N >= 1 iflow(false(), N, cons(M, L)) -> low(N, L) 0 + 0N + 0L + 0M >= 1 + 0N + 1L iflow(true(), N, cons(M, L)) -> cons(M, low(N, L)) 0 + 0N + 0L + 0M >= 2 + 0N + 1L + 0M low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L)) 2 + 0N + 1L + 0M >= 0 + 0N + 0L + 0M low(N, nil()) -> nil() 2 + 0N >= 1 app(cons(N, L), Y) -> cons(N, app(L, Y)) 2 + 0Y + 0N + 1L >= 2 + 0Y + 0N + 1L app(nil(), Y) -> Y 2 + 0Y >= 1Y le(s X, s Y) -> le(X, Y) 2 + 0Y + 0X >= 1 + 0Y + 1X le(s X, 0()) -> false() 2 + 0X >= 0 le(0(), Y) -> true() 2 + 0Y >= 0 Qed