Pasted

fmod LIST-OBLIG1 is
 	protecting BOOLEAN .
	protecting NATURALS-SIGN .
 	sorts List .
 	op nil : -> List [ctor] .
	op __ : List Nat -> List [ctor] .
 	op length : List -> Nat .
	op concat : List List -> List .
	op insertFront : Nat List -> List .
	ops first last : List -> Nat .
	op rest : List -> List .
	op empty? : List -> Boolean .
	op reverse : List -> List .
 	vars N N' : Nat .
	vars L L' : List .
	---vars true false : Boolean .
 	eq length(nil) = 0 .
	eq length(L N) = s(length(L)) .
	eq concat(L, nil) = L .
	eq concat(L, L' N) = concat(L, L') N .
	eq first(nil) = 0 .                 *** Default/error value
	eq first(nil N) = N .
	eq first(L N N') = first(L N) .
 	--- oppgave 20 (empty?, rest, last, reverse) ---
 	eq last(nil) = 0 .
	eq last(nil N) = N .
	eq last(L N' N) = last(L N) .
 	eq rest(nil) = nil .
	eq rest(nil N) = nil .
	eq rest(L N) = rest(L) N .
 	eq reverse(nil) = nil .
	eq reverse(L)  = reverse(rest(L)) first(L) .
 	eq empty?(nil) = true .
	eq empty?(L) = false .
 endfm