fmod INT-LIST is protecting INT .
sorts List .
op nil : -> List [ctor] .
op _:_ : Int List -> List [ctor] .
endfm 

fmod FRAME-SORTING-REQUIREMENTS is protecting INT-LIST .
sort Multiset .
subsort Int < Multiset .
op sorted : List -> Bool .
op null : -> Multiset .
op __ : Multiset Multiset -> Multiset [assoc comm id: null] .
op mset : List -> Multiset .
var L : List .
vars N M : Int .
eq sorted(nil) = true .
eq sorted(N : nil) = true .
ceq sorted(N : M : L) = sorted(M : L) if (N <= M) = true .
ceq sorted(N : M : L) = false if N <= M = false .
eq mset(nil) = null .
eq mset(N : L) = N mset(L) .
endfm 

fmod INSERT-SORT is
protecting INT-LIST .
op ins : Int List -> List .
op sort : List -> List .
vars N M : Int .
var L : List .
eq ins(N, nil) = N : nil .
ceq ins(N, M : L) = N : M : L if N <= M = true .
ceq ins(N, M : L) = M : ins(N, L) if N <= M = false .
eq sort(nil) = nil .
eq sort(N : L) = ins(N, sort(L)) .
endfm

fmod INSERT-SORT-VERIFICATION is
protecting INSERT-SORT .
protecting FRAME-SORTING-REQUIREMENTS .
endfm