{- \section{Introduction}

In this document, we prove the correctness of insertion sort.

\subsection{Preliminaries}

In the sections below, we rely on various definitions stated in the

following separate documents:

-}

--#include "Sorting/predikatlogik.alfa"

--#include "Sorting/satslogik.alfa"

--#include "Sorting/decide.alfa"

--#include "Sorting/nat.alfa"

{- \section{Miscellaneuos definitions and lemmas}

Here we define what a list is, what it means for a list to be sorted (ordered)

and how to insert a new element at the right position in a sorted list.

-}

List (A::Set) :: Set

= data Nil | Cons (x::A) (xs::List A)

singleton (A::Set)(x::A) :: List A

= Cons@_ x Nil@_

IsLeAll (x::Nat)(xs::List Nat) :: Prop

= case xs of -- use layout!

(Nil) -> Triviality

(Cons x' xs') -> And (LeNat x x') (IsLeAll x xs')

IsSorted (xs::List Nat) :: Prop

= case xs of {

(Nil) -> Triviality;

(Cons x xs') -> And (IsLeAll x xs') (IsSorted xs');}

{-

Regarding the above definition of what it means for a list to be sorted, it is

worth noting that, for empty lists, there is nothing to prove, and for

non-empty lists, there are two things to prove.

-}

insert (x::Nat)(xs::List Nat) :: List Nat

= case xs of {

(Nil) -> singleton Nat x;

(Cons x' xs') -> ifLt (List Nat) x x' (Cons@_ x xs) (Cons@_ x' (insert x xs'));}

IsLeFirst (a::Nat)

(x::Nat)

(xs::List Nat)

(ax::LeNat a x)

(p::IsSorted (Cons@_ x xs))

:: IsLeAll a (Cons@_ x xs)

= case xs of {

(Nil) ->

let ndgoal :: IsLeAll a (Cons@_ x Nil@_)

= AndIntro (LeNat a x) (IsLeAll a Nil@_)

(let ndgoal :: LeNat a x

= ax

in ndgoal)

(let ndgoal :: IsLeAll a Nil@_

= trivial

in ndgoal)

in ndgoal;

(Cons x' xs') ->

let ndgoal :: IsLeAll a (Cons@_ x (Cons@_ x' xs'))

= AndIntro (LeNat a x) (IsLeAll a (Cons@_ x' xs'))

(let ndgoal :: LeNat a x

= ax

in ndgoal)

(let ndgoal :: IsLeAll a (Cons@_ x' xs')

= AndElim (IsLeAll x (Cons@_ x' xs')) (IsSorted (Cons@_ x' xs'))

(IsLeAll a (Cons@_ x' xs'))

(let ndgoal :: IsSorted (Cons@_ x xs)

= p

in ndgoal)

(\(h::IsLeAll x (Cons@_ x' xs')) ->

\(h'::IsSorted (Cons@_ x' xs')) ->

let ndgoal :: IsLeAll a (Cons@_ x' xs')

= AndElim (LeNat x x') (IsLeAll x xs')

(IsLeAll a (Cons@_ x' xs'))

(let ndgoal :: And (LeNat x x') (IsLeAll x xs')

= h

in ndgoal)

(\(h0::LeNat x x') ->

\(h1::IsLeAll x xs') ->

let ndgoal :: IsLeAll a (Cons@_ x' xs')

= IsLeFirst a x' xs'

(let ndgoal :: LeNat a x'

= letrans a x x'

(let ndgoal :: LeNat a x

= ax

in ndgoal)

(let ndgoal :: LeNat x x'

= h0

in ndgoal)

in ndgoal)

(let ndgoal :: IsSorted (Cons@_ x' xs')

= h'

in ndgoal)

in ndgoal)

in ndgoal)

in ndgoal)

in ndgoal;}

ThInsertInSorted (x::Nat)(xs::List Nat)(p::IsSorted xs)

:: IsSorted (insert x xs)

= case xs of {

(Nil) ->

let ndgoal :: IsSorted (insert x Nil@_)

= AndIntro (IsLeAll x Nil@_) (IsSorted Nil@_)

(let ndgoal :: IsLeAll x Nil@_

= trivial

in ndgoal)

(let ndgoal :: IsSorted Nil@_

= trivial

in ndgoal)

in ndgoal;

(Cons x' xs') ->

ifLtCase (List Nat) (\(h::List Nat) -> IsSorted h) x x'

(Cons@_ x (Cons@_ x' xs'))

(Cons@_ x' (insert x xs'))

(\(h::LeNat x x') ->

let ndgoal :: IsSorted (Cons@_ x (Cons@_ x' xs'))

= AndIntro (IsLeAll x (Cons@_ x' xs')) (IsSorted (Cons@_ x' xs'))

(let ndgoal :: IsLeAll x (Cons@_ x' xs')

= IsLeFirst x x' xs'

(let ndgoal :: LeNat x x'

= h

in ndgoal)

(let ndgoal :: IsSorted (Cons@_ x' xs')

= p

in ndgoal)

in ndgoal)

(let ndgoal :: IsSorted (Cons@_ x' xs')

= p

in ndgoal)

in ndgoal)

(\(h::Not (LeNat x x')) ->

let indhyp :: IsSorted (insert x xs')

= let ndgoal :: IsSorted (insert x xs')

= ThInsertInSorted x xs'

(let ndgoal :: IsSorted xs'

= And2Elim (IsLeAll x' xs') (IsSorted xs')

(let ndgoal :: And (IsLeAll x' xs') (IsSorted xs')

= p

in ndgoal)

in ndgoal)

in ndgoal

lemma1 :: LeNat x' x

= leSym x x' h

lemma2 (x'::Nat)(x::Nat)(xs'::List Nat)(px::LeNat x' x)(pxs::IsLeAll x' xs')

:: IsLeAll x' (insert x xs')

= case xs' of {

(Nil) ->

let ndgoal :: IsLeAll x' (insert x Nil@_)

= AndIntro (LeNat x' x) (IsLeAll x' Nil@_) px trivial

in ndgoal;

(Cons x0 xs0) ->

ifLtCase (List Nat) (\(h'::List Nat) -> IsLeAll x' h') x x0

(Cons@_ x (Cons@_ x0 xs0))

(Cons@_ x0 (insert x xs0))

(\(h'::LeNat x x0) ->

let ndgoal :: IsLeAll x' (Cons@_ x (Cons@_ x0 xs0))

= AndIntro (LeNat x' x) (IsLeAll x' (Cons@_ x0 xs0))

(let ndgoal :: LeNat x' x

= px

in ndgoal)

(let ndgoal :: IsLeAll x' (Cons@_ x0 xs0)

= pxs

in ndgoal)

in ndgoal)

(\(h'::Not (LeNat x x0)) ->

let ndgoal :: IsLeAll x' (Cons@_ x0 (insert x xs0))

= AndElim (LeNat x' x0) (IsLeAll x' xs0)

(IsLeAll x' (Cons@_ x0 (insert x xs0)))

(let ndgoal :: And (LeNat x' x0) (IsLeAll x' xs0)

= pxs

in ndgoal)

(\(h0::LeNat x' x0) ->

\(h1::IsLeAll x' xs0) ->

let ndgoal :: IsLeAll x' (Cons@_ x0 (insert x xs0))

= AndIntro (LeNat x' x0) (IsLeAll x' (insert x xs0))

(let ndgoal :: LeNat x' x0

= h0

in ndgoal)

(let ndgoal :: IsLeAll x' (insert x xs0)

= lemma2 x' x xs0

(let ndgoal :: LeNat x' x

= px

in ndgoal)

(let ndgoal :: IsLeAll x' xs0

= h1

in ndgoal)

in ndgoal)

in ndgoal)

in ndgoal);}

in let ndgoal :: IsSorted (Cons@_ x' (insert x xs'))

= AndIntro (IsLeAll x' (insert x xs')) (IsSorted (insert x xs'))

(let ndgoal :: IsLeAll x' (insert x xs')

= lemma2 x' x xs'

(let ndgoal :: LeNat x' x

= lemma1

in ndgoal)

(let ndgoal :: IsLeAll x' xs'

= And1Elim (IsLeAll x' xs') (IsSorted xs')

(let ndgoal :: And (IsLeAll x' xs') (IsSorted xs')

= p

in ndgoal)

in ndgoal)

in ndgoal)

(let ndgoal :: IsSorted (insert x xs')

= indhyp

in ndgoal)

in ndgoal);}

{- \section{Definitions and lemmas relating to permutations}

-}

count (x::Nat)(xs::List Nat) :: Nat

= case xs of {

(Nil) -> Zero@_;

(Cons x' xs') -> ifEq Nat x x' (Succ@_ (count x xs')) (count x xs');}

Permutation (xs::List Nat)(ys::List Nat) :: Prop

= ForAll Nat (\(n::Nat) -> EqNat (count n xs) (count n ys))

ThPermNil :: Permutation Nil@_ Nil@_

= let ndgoal :: Permutation Nil@_ Nil@_

= ForAllIntro Nat (\(n::Nat) -> EqNat (count n Nil@_) (count n Nil@_))

(\(any::Nat) ->

let ndgoal :: EqNat (count any Nil@_) (count any Nil@_)

= trivial

in ndgoal)

in ndgoal

ThPermCons (x::Nat)(ys::List Nat)(zs::List Nat)(p::Permutation ys zs)

:: Permutation (Cons@_ x ys) (Cons@_ x zs)

= {-#H#-}ForAllIntro Nat

(\(n::Nat) -> EqNat (count n (Cons@_ x ys)) (count n (Cons@_ x zs)))

(\(n::Nat) ->

ifEqCase Nat (\(h::Nat) -> EqNat h (count n (Cons@_ x zs))) n x

(Succ@_ (count n ys))

(count n ys)

(\(h::EqNat n x) ->

ifEqCase Nat (\(h'::Nat) -> EqNat (Succ@_ (count n ys)) h') n x

(Succ@_ (count n zs))

(count n zs)

(\(h'::EqNat n x) ->

ForAllElim Nat (\(h0::Nat) -> EqNat (count h0 ys) (count h0 zs)) n p)

(\(h'::Not (EqNat n x)) ->

AbsurdityElim (EqNat (Succ@_ (count n ys)) (count n zs))

(ImpliesElim (EqNat n x) Absurdity h' h)))

(\(h::Not (EqNat n x)) ->

ifEqCase Nat (\(h'::Nat) -> EqNat (count n ys) h') n x (Succ@_ (count n zs))

(count n zs)

(\(h'::EqNat n x) ->

AbsurdityElim (EqNat (count n ys) (Succ@_ (count n zs)))

(ImpliesElim (EqNat n x) Absurdity h h'))

(\(h'::Not (EqNat n x)) ->

ForAllElim Nat (\(h0::Nat) -> EqNat (count h0 ys) (count h0 zs)) n p)))

ThPermTrans (xs::List Nat)

(ys::List Nat)

(zs::List Nat)

(xy::Permutation xs ys)

(yz::Permutation ys zs)

:: Permutation xs zs

= ForAllIntro Nat (\(n::Nat) -> EqNat (count n xs) (count n zs))

(\(any::Nat) ->

trans (count any xs) (count any ys) (count any zs)

(ForAllElim Nat (\(h::Nat) -> EqNat (count h xs) (count h ys)) any xy)

(ForAllElim Nat (\(h::Nat) -> EqNat (count h ys) (count h zs)) any yz))

ThPermSwap (x1::Nat)(x2::Nat)(xs::List Nat)

:: Permutation (Cons@_ x1 (Cons@_ x2 xs)) (Cons@_ x2 (Cons@_ x1 xs))

= {-#H#-}ForAllIntro Nat

(\(n::Nat) ->

EqNat (count n (Cons@_ x1 (Cons@_ x2 xs))) (count n (Cons@_ x2 (Cons@_ x1 xs))))

(\(any::Nat) ->

ifEqCase Nat (\(h'::Nat) -> EqNat h' (count any (Cons@_ x2 (Cons@_ x1 xs)))) any

x1

(Succ@_ (count any (Cons@_ x2 xs)))

(count any (Cons@_ x2 xs))

(\(h'::EqNat any x1) ->

ifEqCase Nat (\(h::Nat) -> EqNat (Succ@_ (count any (Cons@_ x2 xs))) h) any x2

(Succ@_ (count any (Cons@_ x1 xs)))

(count any (Cons@_ x1 xs))

(\(h::EqNat any x2) ->

ifEqCase Nat (\(h0::Nat) -> EqNat h0 (count any (Cons@_ x1 xs))) any x2

(Succ@_ (count any xs))

(count any xs)

(\(h0::EqNat any x2) ->

ifEqCase Nat (\(h1::Nat) -> EqNat (Succ@_ (count any xs)) h1) any x1

(Succ@_ (count any xs))

(count any xs)

(\(h1::EqNat any x1) -> refl (count any xs))

(\(h1::Not (EqNat any x1)) ->

AbsurdityElim (EqNat (Succ@_ (count any xs)) (count any xs))

(ImpliesElim (EqNat any x1) Absurdity h1 h')))

(\(h0::Not (EqNat any x2)) ->

AbsurdityElim (EqNat (count any xs) (count any (Cons@_ x1 xs)))

(ImpliesElim (EqNat any x2) Absurdity h0 h)))

(\(h::Not (EqNat any x2)) ->

ifEqCase Nat (\(h0::Nat) -> EqNat (Succ@_ (count any (Cons@_ x2 xs))) h0) any x1

(Succ@_ (count any xs))

(count any xs)

(\(h0::EqNat any x1) ->

ifEqCase Nat (\(h1::Nat) -> EqNat h1 (count any xs)) any x2

(Succ@_ (count any xs))

(count any xs)

(\(h1::EqNat any x2) ->

AbsurdityElim (EqNat (Succ@_ (count any xs)) (count any xs))

(ImpliesElim (EqNat any x2) Absurdity h h1))

(\(h1::Not (EqNat any x2)) -> refl (count any xs)))

(\(h0::Not (EqNat any x1)) ->

AbsurdityElim (EqNat (Succ@_ (count any (Cons@_ x2 xs))) (count any xs))

(ImpliesElim (EqNat any x1) Absurdity h0 h'))))

(\(h'::Not (EqNat any x1)) ->

ifEqCase Nat (\(h0::Nat) -> EqNat (count any (Cons@_ x2 xs)) h0) any x2

(Succ@_ (count any (Cons@_ x1 xs)))

(count any (Cons@_ x1 xs))

(\(h0::EqNat any x2) ->

ifEqCase Nat (\(h::Nat) -> EqNat h (Succ@_ (count any (Cons@_ x1 xs)))) any x2

(Succ@_ (count any xs))

(count any xs)

(\(h::EqNat any x2) ->

ifEqCase Nat (\(h1::Nat) -> EqNat (count any xs) h1) any x1

(Succ@_ (count any xs))

(count any xs)

(\(h1::EqNat any x1) ->

AbsurdityElim (EqNat (count any xs) (Succ@_ (count any xs)))

(ImpliesElim (EqNat any x1) Absurdity h' h1))

(\(h1::Not (EqNat any x1)) -> refl (count any xs)))

(\(h::Not (EqNat any x2)) ->

AbsurdityElim (EqNat (count any xs) (Succ@_ (count any (Cons@_ x1 xs))))

(ImpliesElim (EqNat any x2) Absurdity h h0)))

(\(h::Not (EqNat any x2)) ->

ifEqCase Nat (\(h0::Nat) -> EqNat h0 (count any (Cons@_ x1 xs))) any x2

(Succ@_ (count any xs))

(count any xs)

(\(h0::EqNat any x2) ->

AbsurdityElim (EqNat (Succ@_ (count any xs)) (count any (Cons@_ x1 xs)))

(ImpliesElim (EqNat any x2) Absurdity h h0))

(\(h0::Not (EqNat any x2)) ->

ifEqCase Nat (\(h1::Nat) -> EqNat (count any xs) h1) any x1

(Succ@_ (count any xs))

(count any xs)

(\(h1::EqNat any x1) ->

AbsurdityElim (EqNat (count any xs) (Succ@_ (count any xs)))

(ImpliesElim (EqNat any x1) Absurdity h' h1))

(\(h1::Not (EqNat any x1)) -> refl (count any xs))))))

ThPermInsert (x::Nat)(xs::List Nat) :: Permutation (Cons@_ x xs) (insert x xs)

= case xs of {

(Nil) ->

ForAllIntro Nat

(\(n::Nat) -> EqNat (count n (Cons@_ x Nil@_)) (count n (insert x Nil@_)))

(\(any::Nat) -> refl (count any (Cons@_ x Nil@_)));

(Cons x' xs') ->

ifLtCase (List Nat) (\(h::List Nat) -> Permutation (Cons@_ x (Cons@_ x' xs')) h)

x

x'

(Cons@_ x (Cons@_ x' xs'))

(Cons@_ x' (insert x xs'))

(\(h::LeNat x x') ->

ForAllIntro Nat

(\(n::Nat) ->

EqNat (count n (Cons@_ x (Cons@_ x' xs'))) (count n (Cons@_ x (Cons@_ x' xs'))))

(\(any::Nat) -> refl (count any (Cons@_ x (Cons@_ x' xs')))))

(\(h::Not (LeNat x x')) ->

let indhyp :: Permutation (Cons@_ x xs') (insert x xs')

= ThPermInsert x xs'

in let it :: Permutation (Cons@_ x (Cons@_ x' xs')) (Cons@_ x' (insert x xs'))

= ThPermTrans (Cons@_ x (Cons@_ x' xs')) (Cons@_ x' (Cons@_ x xs'))

(Cons@_ x' (insert x xs'))

(ThPermSwap x x' xs')

(ThPermCons x' (Cons@_ x xs') (insert x xs') indhyp)

in it);}

{-

\section{The sorting algorithm, the correctness criterion and

the correctness proof}

-}

sort (xs::List Nat) :: List Nat

= case xs of {

(Nil) -> Nil@_;

(Cons x xs') -> insert x (sort xs');}

SortSpec (xs::List Nat)(ys::List Nat) :: Prop

= And (Permutation xs ys) (IsSorted ys)

-- %% Although SortLemma is only used in ThSortIsCorrect, I made it global to be able to specify linearization properties for it.

SortLemma (x::Nat)(xs'::List Nat)(h::Permutation xs' (sort xs'))

:: Permutation (Cons@_ x xs') (sort (Cons@_ x xs'))

= let ndgoal :: Permutation (Cons@_ x xs') (sort (Cons@_ x xs'))

= ThPermTrans (Cons@_ x xs') (Cons@_ x (sort xs')) (sort (Cons@_ x xs'))

(let ndgoal :: Permutation (Cons@_ x xs') (Cons@_ x (sort xs'))

= ThPermCons x xs' (sort xs')

(let ndgoal :: Permutation xs' (sort xs')

= h

in ndgoal)

in ndgoal)

(let ndgoal :: Permutation (Cons@_ x (sort xs')) (sort (Cons@_ x xs'))

= ThPermInsert x (sort xs')

in ndgoal)

in ndgoal

ThSortIsCorrect (xs::List Nat) :: SortSpec xs (sort xs)

= case xs of {

(Nil) ->

let ndgoal :: SortSpec Nil@_ (sort Nil@_)

= AndIntro (Permutation Nil@_ (sort Nil@_)) (IsSorted (sort Nil@_))

(let ndgoal :: Permutation Nil@_ (sort Nil@_)

= ThPermNil

in ndgoal)

(let ndgoal :: IsSorted (sort Nil@_)

= trivial

in ndgoal)

in ndgoal;

(Cons x xs') ->

let indhyp :: SortSpec xs' (sort xs')

= ThSortIsCorrect xs'

in let ndgoal :: SortSpec (Cons@_ x xs') (sort (Cons@_ x xs'))

= AndElim (Permutation xs' (sort xs')) (IsSorted (sort xs'))

(SortSpec (Cons@_ x xs') (sort (Cons@_ x xs')))

(let ndgoal :: SortSpec xs' (sort xs')

= indhyp

in ndgoal)

(\(h::Permutation xs' (sort xs')) ->

\(h'::IsSorted (sort xs')) ->

let ndgoal :: SortSpec (Cons@_ x xs') (sort (Cons@_ x xs'))

= AndIntro (Permutation (Cons@_ x xs') (sort (Cons@_ x xs')))

(IsSorted (sort (Cons@_ x xs')))

(let ndgoal :: Permutation (Cons@_ x xs') (sort (Cons@_ x xs'))

= SortLemma x xs'

(let ndgoal :: Permutation xs' (sort xs')

= h

in ndgoal)

in ndgoal)

(let ndgoal :: IsSorted (sort (Cons@_ x xs'))

= ThInsertInSorted x (sort xs')

(let ndgoal :: IsSorted (sort xs')

= h'

in ndgoal)

in ndgoal)

in ndgoal)

in ndgoal;}

-- \section{A simple corollary}

ThSorting

:: ForAll (List Nat)

(\(xs::List Nat) -> Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys))

= let ndgoal

:: ForAll (List Nat)

(\(xs::List Nat) -> Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys))

= ForAllIntro (List Nat)

(\(xs::List Nat) -> Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys))

(\(xs::List Nat) ->

let ndgoal :: Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys)

= ExistsIntro (List Nat) (\(ys::List Nat) -> SortSpec xs ys) (sort xs)

(let ndgoal :: SortSpec xs (sort xs)

= ThSortIsCorrect xs

in ndgoal)

in ndgoal)

in ndgoal

sortfun :: List Nat -> List Nat

= \(xs::List Nat) -> sort xs

ThSorting2 =

ExistsIntro (List Nat -> List Nat)

(\(f::List Nat -> List Nat) ->

ForAll (List Nat) (\(xs::List Nat) -> SortSpec xs (f xs)))

sortfun

(ForAllIntro (List Nat) (\(xs::List Nat) -> SortSpec xs (sort xs))

(\(any::List Nat) -> ThSortIsCorrect any))

{-# Alfa hiding on

var "if" hide 2

con "Nil" as "[]"

con "Cons" infix rightassoc 5 as ":"

var "ThPermTrans" hide 3

var "ThPermCons" hide 3

var "ThPermInsert" hide 2

var "ThInsertInSorted" hide 2

var "Permutation" infix 4 as "~" with symbolfont

var "List" mixfix 0 as "[_]"

var "IsLeFirst" hide 3

var "singleton" hide 1 mixfix 0 as "[_]"

var "listInd" hide 2

var "SortLemma" hide 2

#-}

{-# GF Eng insert x xs = mkPN (["the list with"]++x.s!pnv++["inserted into"]++xs.s!pnv) #-}

{-# GF Eng IsLeAll x xs = mkSent (x.s!pnv++["is less than or equal to all the elements of"]++xs.s!pnv) #-}

{-# GF Eng IsLeFirst a x xs ax p =

mkText (ax.s!text++"."++p.s!text++

[". This means that "]++

a.s!pnv++["is less than or equal to all the elements of the list with"]++

x.s!pnv++["prepended to"]++xs.s!pnv) #-}

{-# GF Eng SortLemma x xs' h =

mkText (h.s!text++[". Use SortLemma"]) #-}

{-# GF Eng ThInsertInSorted x xs p =

mkText (p.s!text++[". Use the correctness of insertion"]) #-}

{-# GF Eng ThPermNil = mkThm ["the permutation of empty list theorem"] #-}

{-# GF Eng ThPermCons x ys zs p =

mkText (p.s!text++

[". We can now use the theorem about prepending an element to permutations"]) #-}

{-# GF Eng ThPermTrans xs ys zs xy yz =

mkText (indent("·"++xy.s!text++"."++newParagraph++"·"++yz.s!text)++

[". By the transitivity of the permutation relation,"]++

zs.s!pnv++"is a permutation of"++xs.s!pnv) #-}

{-# GF Eng ThPermInsert x xs = mkThm ["the theorem that inserting yields a permutation of prepending"] #-}

{-# GF Sve IsLeAll x xs = mkSent (x.s!pn++["är mindre än alla element i"]++xs.s!pn) #-}

{-# GF Sve CCCons x xs = mkPN (["listan med"]++x.s!pn++["insatt först i"]++xs.s!pn) en #-}

{-# GF Sve singleton A x = mkPN (["enelementslistan med"]++x.s!pn) en #-}

{-# GF Sve CCNil = mkPN ["den tomma listan"] en #-}

{-# GF Sve List A = {s = tbl {n => ("list"+nomReg1!n)++"av" ++ A.s ! (cn pl)} ; form = CN en} #-}

{-# GF Eng ThSortIsCorrect xs = mkThm(["the correctness of insertion sort applied to"]++xs.s!pnv) #-}

{-# GF Eng ThSorting = mkThm ["a sorting theorem"] #-}

{-# GF Eng SortSpec xs ys = mkSent(ys.s!pnv++["is a sorted version of"]++xs.s!pnv) #-}

{-# GF Eng sort xs = mkPN(["insertion sort applied to"]++xs.s!pnv) #-}

{-# GF Eng sortfun xs = mkPN(["insertion sort"]) #-}

{-# GF Eng List A = mkCN(tbl {n=>("list"+nomReg!n)++"of"++A.s!(cn pl)}) #-}

{-# GF Eng Permutation xs ys = mkSent(ys.s!pnv++["is a permutation of"]++xs.s!pnv) #-}

{-# GF Eng count x xs = mkPN(["the number of occurences of"]++x.s!pnv++"in"++xs.s!pnv) #-}

{-# GF Eng singleton A x = mkPN(["the singleton list containing"]++x.s!pnv) #-}

{-# GF Eng IsSorted xs = mkSent (xs.s!pnv ++ ["is sorted"]) #-}

{-# GF Eng CCCons x xs = mkPN (["the list with"]++x.s!pnv++["prepended to"]++xs.s!pnv) #-}

{-# GF Eng CCNil = mkPN ["the empty list"] #-}