Skip to content
Permalink
master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Go to file
 
 
Cannot retrieve contributors at this time
{- \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"] #-}