REC-SPEC QuickSort SORTS Bool Nat NatList NatListPair OPS true : -> Bool false : -> Bool not : Bool -> Bool 0 : -> Nat 10 : -> Nat s : Nat -> Nat st : Nat Nat -> Bool get : Nat Nat -> Bool nil : -> NatList cons : Nat NatList -> NatList plus : Nat Nat -> Nat times : Nat Nat -> Nat rev : Nat -> NatList pair : NatList NatList -> NatListPair split : Nat NatList -> NatListPair qsort : NatList -> NatList append : NatList NatList -> NatList p1 : ListPair -> NatList p2 : ListPair -> NatList VARS N M : Nat L L1 L2 LT GT : NatList RULES 10 -> s(s(s(s(s(s(s(s(s(s(0)))))))))) not(true) -> false not(false) -> true st(0, s(N)) -> true st(s(N), 0) -> false st(N, N) -> false st(s(N), s(M)) -> st(N, M) get(N, M) -> not(st(N, M)) plus(0, N) -> N plus(s(N), M) -> s(plus(N, M)) times(0, N) -> 0 times(s(N), M) -> plus(M, times(N, M)) rev(s(N)) -> cons(s(N), rev(N)) rev(0) -> cons(0, nil) split(N, cons(M, L)) -> pair(p1(split(N, L)), cons(M, p2(split(N, L)))) if st(N, M) -><- true split(N, cons(M, L)) -> pair(cons(M, p1(split(N, L))), p2(split(N, L))) if get(N, M) -><- true split(N, nil) -> pair(nil, nil) append(cons(N, L), LT) -> cons(N, append(L, LT)) append(nil, L) -> L qsort(nil) -> nil qsort(cons(N, L)) -> append(qsort(p1(split(N, L))), cons(N, qsort(p2(split(N, L))))) p1(pair(L1, L2)) -> L1 p2(pair(L1, L2)) -> L2 END-SPEC get normal form for: qsort(rev(10)) % resut: % cons(0,cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),cons(s(s(s(s(s(0))))),cons(s(s(s(s(s(s(0)))))),cons(s(s( % s(s(s(s(s(0))))))),cons(s(s(s(s(s(s(s(s(0)))))))),cons(s(s(s(s(s(s(s(s(s(0))))))))),cons(s(s(s(s(s(s(s(s(s(s( % 0)))))))))),nil))))))))))) get normal form for: qsort(rev(times(10, 10))) get normal form for: qsort(rev(times(10, times(10, 10))))