fth ALPHA-ASSOC is

sort Foo .

op f : Foo Foo -> Foo [ctor assoc] .

endfth

fmod OTHER-ALPHA-ASSOC is

sort Elt .

op g : Elt Elt -> Elt [ctor] .

var E : Elt .

eq g(E, g(E, E)) = g(g(E, E), E) [nonexec] .

endfm

view VALPHA from ALPHA-ASSOC to OTHER-ALPHA-ASSOC is

sort Foo to Elt .

op f to g .

endv

fmod MY-LIST is

sorts List Elt .

subsort Elt < List .

op nil : -> List [ctor] .

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

var L : List .

var E : Elt .

op reverse : List -> List .

eq reverse(nil) = nil .

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

endfm

fth ASSOC-OP is

sort Elt .

op __ : Elt Elt -> Elt [assoc] .

endfth

fth ANOTHER-ASSOC-OP is

sort Foo .

op _._ : Foo Foo -> Foo .

vars F1 F2 F3 : Foo .

eq F1 . (F2 . F3) = (F1 . F2) . F3 .

endfth

view ASSOC from ASSOC-OP to ANOTHER-ASSOC-OP is

sort Elt to Foo .

op __ to _._ .

endv

fmod TEST is

sorts A B C .

subsort A < B .

sorts D E F .

subsort D < F .

subsort D < E .

op a : -> A .

op b : -> B .

op c : -> B .

op f : A -> B .

op g : A A -> B .

op h : A A -> A [assoc comm id: a] .

vars X Y : A .

eq f(a) = b .

eq f(X) = c [owise] .

eq g(a,X) = b .

eq g(X, Y) = c [owise] .

ceq h(a, a) = a

if true /\ not false .

endfm

fmod TEST2 is

sorts C D .

subsort C < D .

op c : -> C .

op d : -> D .

op {_} : C -> C .

op g : C -> D .

eq g(c) = d .

endfm

fmod TEST3 is

pr TEST + (TEST2 * (sort C to CC, sort D to DD, op g to gg)) .

op x : -> CC .

endfm

fth TEST4 is

sort Foo .

ops a b : -> Foo .

op f : Foo -> Foo .

endfth

fmod TEST5{X :: TEST4 * (sort Foo to Faa)} is

sort Test5 .

op c : -> Test5 .

endfm

view VNat from TRIV * (sort Elt to Elt2) to NAT * (sort Nat to Naaaaat) is

sort Elt2 to Naaaaat .

endv

view V1 from TRIV to BOOL is

sort Elt to Bool .

endv

fmod TEST6{X :: TRIV} is

sort Foo6 .

endfm

fmod TEST7 is

ex TEST .

pr (TEST6 * (sort Foo6 to Fooooo6)){V1} .

endfm

fth TEST8 is

sorts Foo Faa .

op update : Foo -> Faa .

endfth

view V2 from TEST8 to BOOL is

sort Foo to Bool .

sort Faa to Bool .

op update(X:Foo) to term _or_(true, X:Bool) .

endv

fmod TEST9 is

sorts A B .

subsort A < B .

op a_ : A -> A [prec 10] .

op _a_ : A A -> A [prec 11] .

endfm

fmod TEST10 is

pr TEST9 * (op a_ : B -> B to b_ [prec 12],

sort A to C) .

endfm

fmod TEST11 is

pr LIST{Nat} .

endfm

fmod TEST12 is

pr LIST{TRIV}{TRIV}{Nat} .

endfm

fmod TEST13{X :: TRIV, Y :: TRIV} is

sort L{X,Y} .

endfm

fmod TEST14 is

pr TEST13{Nat, Nat} .

endfm

fth TEST15 is

sort Elta .

endfth

view V3 from TRIV to TEST15 is

sort Elt to Elta .

endv

fmod TEST16{Y :: TRIV} is

pr LIST{Y} .

endfm