fmod MY_LIST is

pr NAT .

sorts List .

subsort Nat < List .

op nil : -> List [ctor] .

op __ : List List -> List [ctor assoc id: nil] .

var L : List .

var E : Nat .

op reverse : List -> List .

eq reverse(nil) = nil .

eq reverse(E L) = reverse(L) E .

endfm

fth MY_LISTVIEW is

pr NAT .

sorts List .

subsort Nat < List .

op nil : -> List .

op __ : List List -> List [assoc id: nil] .

var L : List .

var E : Nat .

op reverse : List -> List .

eq reverse(reverse(L)) = L .

endfth

view V from MY_LISTVIEW to MY_LIST is

sort List to List .

op nil to nil .

op __ to __ .

op reverse to reverse .

endv