1Maude> fmod BAR is
2  inc FOO * (sort Foo to Baz, sort Bar to Quux) .
3endfm
4fmod BAR is
5  sorts Bool Baz Quux .
6  subsort Baz < Quux .
7  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
8    0 gather (& & &) special (
9    id-hook BranchSymbol
10    term-hook 1 (true)
11    term-hook 2 (false))] .
12  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
13    special (
14    id-hook EqualitySymbol
15    term-hook equalTerm (true)
16    term-hook notEqualTerm (false))] .
17  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
18    special (
19    id-hook EqualitySymbol
20    term-hook equalTerm (false)
21    term-hook notEqualTerm (true))] .
22  op true : -> Bool [ctor special (
23    id-hook SystemTrue)] .
24  op false : -> Bool [ctor special (
25    id-hook SystemFalse)] .
26  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
27  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
28  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
29  op not_ : Bool -> Bool [prec 53 gather (E)] .
30  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
31  eq true and A:Bool = A:Bool .
32  eq false and A:Bool = false .
33  eq A:Bool and A:Bool = A:Bool .
34  eq false xor A:Bool = A:Bool .
35  eq A:Bool xor A:Bool = false .
36  eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
37  eq not A:Bool = true xor A:Bool .
38  eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
39  eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
40endfm
41fmod THREE is
42  inc TWO * (sort Foo to Foo', sort Baz to Baz', sort Quux to Quux') .
43  sorts Jaz .
44  subsorts Jaz < Baz' .
45endfm
46fmod THREE is
47  sorts Bool Baz' Bar Quux' Jaz .
48  subsorts Quux' Jaz < Baz' .
49  subsort Baz' < Bar .
50  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
51    0 gather (& & &) special (
52    id-hook BranchSymbol
53    term-hook 1 (true)
54    term-hook 2 (false))] .
55  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
56    special (
57    id-hook EqualitySymbol
58    term-hook equalTerm (true)
59    term-hook notEqualTerm (false))] .
60  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
61    special (
62    id-hook EqualitySymbol
63    term-hook equalTerm (false)
64    term-hook notEqualTerm (true))] .
65  op true : -> Bool [ctor special (
66    id-hook SystemTrue)] .
67  op false : -> Bool [ctor special (
68    id-hook SystemFalse)] .
69  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
70  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
71  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
72  op not_ : Bool -> Bool [prec 53 gather (E)] .
73  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
74  eq true and A:Bool = A:Bool .
75  eq false and A:Bool = false .
76  eq A:Bool and A:Bool = A:Bool .
77  eq false xor A:Bool = A:Bool .
78  eq A:Bool xor A:Bool = false .
79  eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
80  eq not A:Bool = true xor A:Bool .
81  eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
82  eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
83endfm
84fmod BAR is
85  inc FOO * (sort Foo to Baz, op a to b) .
86endfm
87fmod BAR is
88  sorts Bool Baz Bar .
89  subsort Baz < Bar .
90  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
91    0 gather (& & &) special (
92    id-hook BranchSymbol
93    term-hook 1 (true)
94    term-hook 2 (false))] .
95  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
96    special (
97    id-hook EqualitySymbol
98    term-hook equalTerm (true)
99    term-hook notEqualTerm (false))] .
100  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
101    special (
102    id-hook EqualitySymbol
103    term-hook equalTerm (false)
104    term-hook notEqualTerm (true))] .
105  op true : -> Bool [ctor special (
106    id-hook SystemTrue)] .
107  op false : -> Bool [ctor special (
108    id-hook SystemFalse)] .
109  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
110  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
111  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
112  op not_ : Bool -> Bool [prec 53 gather (E)] .
113  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
114  op b : -> Baz .
115  eq true and A:Bool = A:Bool .
116  eq false and A:Bool = false .
117  eq A:Bool and A:Bool = A:Bool .
118  eq false xor A:Bool = A:Bool .
119  eq A:Bool xor A:Bool = false .
120  eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
121  eq not A:Bool = true xor A:Bool .
122  eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
123  eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
124endfm
125fmod BAR' is
126  inc FOO' * (sort Foo to Quux, op _+_ : [Foo] [Foo] -> [Foo] to _*_ [prec 29
127    gather (E e)], op _+_ : [Baz] [Baz] -> [Foo] to _._ [prec 27 gather (E e)])
128    .
129endfm
130fmod BAR' is
131  sorts Bool Quux Bar Baz .
132  subsort Quux < Bar .
133  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
134    0 gather (& & &) special (
135    id-hook BranchSymbol
136    term-hook 1 (true)
137    term-hook 2 (false))] .
138  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
139    special (
140    id-hook EqualitySymbol
141    term-hook equalTerm (true)
142    term-hook notEqualTerm (false))] .
143  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
144    special (
145    id-hook EqualitySymbol
146    term-hook equalTerm (false)
147    term-hook notEqualTerm (true))] .
148  op true : -> Bool [ctor special (
149    id-hook SystemTrue)] .
150  op false : -> Bool [ctor special (
151    id-hook SystemFalse)] .
152  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
153  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
154  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
155  op not_ : Bool -> Bool [prec 53 gather (E)] .
156  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
157  op a : -> Baz .
158  op _*_ : Quux Quux -> Quux [assoc comm prec 29 gather (E e)] .
159  op _._ : Baz Baz -> Quux [prec 27 gather (E e)] .
160  eq true and A:Bool = A:Bool .
161  eq false and A:Bool = false .
162  eq A:Bool and A:Bool = A:Bool .
163  eq false xor A:Bool = A:Bool .
164  eq A:Bool xor A:Bool = false .
165  eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
166  eq not A:Bool = true xor A:Bool .
167  eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
168  eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
169endfm
170==========================================
171reduce in BAR' : a . a * a . a .
172rewrites: 0
173result Quux: a . a * a . a
174fmod BAR'' is
175  inc FOO' * (sort Foo to Quux, op _+_ to _*_ [prec 29 gather (E E)]) .
176endfm
177fmod BAR'' is
178  sorts Bool Quux Bar Baz .
179  subsort Quux < Bar .
180  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
181    0 gather (& & &) special (
182    id-hook BranchSymbol
183    term-hook 1 (true)
184    term-hook 2 (false))] .
185  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
186    special (
187    id-hook EqualitySymbol
188    term-hook equalTerm (true)
189    term-hook notEqualTerm (false))] .
190  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
191    special (
192    id-hook EqualitySymbol
193    term-hook equalTerm (false)
194    term-hook notEqualTerm (true))] .
195  op true : -> Bool [ctor special (
196    id-hook SystemTrue)] .
197  op false : -> Bool [ctor special (
198    id-hook SystemFalse)] .
199  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
200  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
201  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
202  op not_ : Bool -> Bool [prec 53 gather (E)] .
203  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
204  op a : -> Baz .
205  op _*_ : Quux Quux -> Quux [assoc comm prec 29 gather (E E)] .
206  op _*_ : Baz Baz -> Quux [prec 29 gather (E E)] .
207  eq true and A:Bool = A:Bool .
208  eq false and A:Bool = false .
209  eq A:Bool and A:Bool = A:Bool .
210  eq false xor A:Bool = A:Bool .
211  eq A:Bool xor A:Bool = false .
212  eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
213  eq not A:Bool = true xor A:Bool .
214  eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
215  eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
216endfm
217==========================================
218reduce in BAR'' : a * a * a * a .
219rewrites: 0
220result Quux: a * a * a * a
221==========================================
222reduce in BAR'' : a * a * a * a .
223rewrites: 0
224result Quux: a * a * a * a
225fmod TEST is
226  inc BASH * (op f : [Foo] -> [Foo] to g) .
227endfm
228fmod TEST is
229  sorts Bool Foo Bar .
230  subsort Foo < Bar .
231  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
232    0 gather (& & &) special (
233    id-hook BranchSymbol
234    term-hook 1 (true)
235    term-hook 2 (false))] .
236  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
237    special (
238    id-hook EqualitySymbol
239    term-hook equalTerm (true)
240    term-hook notEqualTerm (false))] .
241  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
242    special (
243    id-hook EqualitySymbol
244    term-hook equalTerm (false)
245    term-hook notEqualTerm (true))] .
246  op true : -> Bool [ctor special (
247    id-hook SystemTrue)] .
248  op false : -> Bool [ctor special (
249    id-hook SystemFalse)] .
250  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
251  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
252  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
253  op not_ : Bool -> Bool [prec 53 gather (E)] .
254  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
255  op g : Foo -> Foo .
256  op g : Bar -> Bar .
257  eq true and A:Bool = A:Bool .
258  eq false and A:Bool = false .
259  eq A:Bool and A:Bool = A:Bool .
260  eq false xor A:Bool = A:Bool .
261  eq A:Bool xor A:Bool = false .
262  eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
263  eq not A:Bool = true xor A:Bool .
264  eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
265  eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
266endfm
267fmod BOOL
268fmod TRUTH-VALUE
269fmod BOOL-OPS
270fmod TRUTH
271fmod EXT-BOOL
272fmod NAT
273fmod INT
274fmod RAT
275fmod FLOAT
276fmod STRING
277fmod CONVERSION
278fmod RANDOM
279fmod QID
280fth TRIV
281fth STRICT-WEAK-ORDER
282fth STRICT-TOTAL-ORDER
283fth TOTAL-PREORDER
284fth TOTAL-ORDER
285fth DEFAULT
286fmod LIST
287fmod WEAKLY-SORTABLE-LIST
288fmod SORTABLE-LIST
289fmod WEAKLY-SORTABLE-LIST'
290fmod SORTABLE-LIST'
291fmod SET
292fmod LIST-AND-SET
293fmod SORTABLE-LIST-AND-SET
294fmod SORTABLE-LIST-AND-SET'
295fmod LIST*
296fmod SET*
297fmod MAP
298fmod ARRAY
299fmod NAT-LIST
300fmod QID-LIST
301fmod QID-SET
302fmod META-TERM
303fmod META-MODULE
304fmod META-VIEW
305fmod META-LEVEL
306mod COUNTER
307mod LOOP-MODE
308mod CONFIGURATION
309fmod FOO
310fmod BAR
311fmod ONE
312fmod TWO
313fmod THREE
314fmod FOO'
315fmod BAR'
316fmod BAR''
317fmod DIFF
318fmod BASH
319fmod TEST
320fth X :: TRIV
321fth X :: STRICT-WEAK-ORDER
322fmod LIST{STRICT-WEAK-ORDER}
323fmod LIST{STRICT-WEAK-ORDER}{[X]}
324fmod LIST{STRICT-WEAK-ORDER}{[X]} * (sort NeList{STRICT-WEAK-ORDER}{X} to
325    NeList{X}, sort List{STRICT-WEAK-ORDER}{X} to List{X})
326fth X :: STRICT-TOTAL-ORDER
327fmod WEAKLY-SORTABLE-LIST{STRICT-TOTAL-ORDER}
328fmod LIST{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}
329fmod LIST{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]}
330fmod LIST{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]} * (sort NeList{
331    STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeList{STRICT-TOTAL-ORDER}{X},
332    sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to List{
333    STRICT-TOTAL-ORDER}{X})
334fmod WEAKLY-SORTABLE-LIST{STRICT-TOTAL-ORDER}{[X]}
335fmod WEAKLY-SORTABLE-LIST{STRICT-TOTAL-ORDER}{[X]} * (sort NeList{
336    STRICT-TOTAL-ORDER}{X} to NeList{X}, sort List{STRICT-TOTAL-ORDER}{X} to
337    List{X})
338fmod LIST{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]} * (sort NeList{
339    STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeList{STRICT-TOTAL-ORDER}{X},
340    sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to List{
341    STRICT-TOTAL-ORDER}{X}) * (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X},
342    sort List{STRICT-TOTAL-ORDER}{X} to List{X})
343fth X :: TOTAL-PREORDER
344fmod LIST{TOTAL-PREORDER}
345fmod LIST{TOTAL-PREORDER}{[X]}
346fmod LIST{TOTAL-PREORDER}{[X]} * (sort NeList{TOTAL-PREORDER}{X} to NeList{X},
347    sort List{TOTAL-PREORDER}{X} to List{X})
348fth X :: TOTAL-ORDER
349fmod WEAKLY-SORTABLE-LIST'{TOTAL-ORDER}
350fmod LIST{TOTAL-PREORDER}{TOTAL-ORDER}
351fmod LIST{TOTAL-PREORDER}{TOTAL-ORDER}{[X]}
352fmod LIST{TOTAL-PREORDER}{TOTAL-ORDER}{[X]} * (sort NeList{TOTAL-PREORDER}{
353    TOTAL-ORDER}{X} to NeList{TOTAL-ORDER}{X}, sort List{TOTAL-PREORDER}{
354    TOTAL-ORDER}{X} to List{TOTAL-ORDER}{X})
355fmod WEAKLY-SORTABLE-LIST'{TOTAL-ORDER}{[X]}
356fmod WEAKLY-SORTABLE-LIST'{TOTAL-ORDER}{[X]} * (sort NeList{TOTAL-ORDER}{X} to
357    NeList{X}, sort List{TOTAL-ORDER}{X} to List{X})
358fmod LIST{TOTAL-PREORDER}{TOTAL-ORDER}{[X]} * (sort NeList{TOTAL-PREORDER}{
359    TOTAL-ORDER}{X} to NeList{TOTAL-ORDER}{X}, sort List{TOTAL-PREORDER}{
360    TOTAL-ORDER}{X} to List{TOTAL-ORDER}{X}) * (sort NeList{TOTAL-ORDER}{X} to
361    NeList{X}, sort List{TOTAL-ORDER}{X} to List{X})
362fmod LIST{[X]}
363fmod SET{[X]}
364fmod SORTABLE-LIST{[X]}
365fmod LIST-AND-SET{STRICT-WEAK-ORDER}
366fmod SET{STRICT-WEAK-ORDER}
367fmod SET{STRICT-WEAK-ORDER}{[X]}
368fmod LIST-AND-SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}
369fmod SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}
370fmod SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]}
371fmod LIST-AND-SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]}
372fmod LIST-AND-SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]} * (sort NeList{
373    STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeList{STRICT-TOTAL-ORDER}{X},
374    sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to List{
375    STRICT-TOTAL-ORDER}{X})
376fmod LIST-AND-SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]} * (sort NeList{
377    STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeList{STRICT-TOTAL-ORDER}{X},
378    sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to List{
379    STRICT-TOTAL-ORDER}{X}) * (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X},
380    sort List{STRICT-TOTAL-ORDER}{X} to List{X}, sort NeSet{STRICT-WEAK-ORDER}{
381    STRICT-TOTAL-ORDER}{X} to NeSet{X}, sort Set{STRICT-WEAK-ORDER}{
382    STRICT-TOTAL-ORDER}{X} to Set{X})
383fmod SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{[X]} * (sort NeSet{
384    STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeSet{X}, sort Set{
385    STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to Set{X})
386fmod SORTABLE-LIST'{[X]}
387fmod LIST-AND-SET{TOTAL-PREORDER}
388fmod SET{TOTAL-PREORDER}
389fmod SET{TOTAL-PREORDER}{[X]}
390fmod LIST-AND-SET{TOTAL-PREORDER}{TOTAL-ORDER}
391fmod SET{TOTAL-PREORDER}{TOTAL-ORDER}
392fmod SET{TOTAL-PREORDER}{TOTAL-ORDER}{[X]}
393fmod LIST-AND-SET{TOTAL-PREORDER}{TOTAL-ORDER}{[X]}
394fmod LIST-AND-SET{TOTAL-PREORDER}{TOTAL-ORDER}{[X]} * (sort NeList{
395    TOTAL-PREORDER}{TOTAL-ORDER}{X} to NeList{TOTAL-ORDER}{X}, sort List{
396    TOTAL-PREORDER}{TOTAL-ORDER}{X} to List{TOTAL-ORDER}{X})
397fmod LIST-AND-SET{TOTAL-PREORDER}{TOTAL-ORDER}{[X]} * (sort NeList{
398    TOTAL-PREORDER}{TOTAL-ORDER}{X} to NeList{TOTAL-ORDER}{X}, sort List{
399    TOTAL-PREORDER}{TOTAL-ORDER}{X} to List{TOTAL-ORDER}{X}) * (sort NeList{
400    TOTAL-ORDER}{X} to NeList{X}, sort List{TOTAL-ORDER}{X} to List{X}, sort
401    NeSet{TOTAL-PREORDER}{TOTAL-ORDER}{X} to NeSet{X}, sort Set{
402    TOTAL-PREORDER}{TOTAL-ORDER}{X} to Set{X})
403fmod SET{TOTAL-PREORDER}{TOTAL-ORDER}{[X]} * (sort NeSet{TOTAL-PREORDER}{
404    TOTAL-ORDER}{X} to NeSet{X}, sort Set{TOTAL-PREORDER}{TOTAL-ORDER}{X} to
405    Set{X})
406fth Y :: TRIV
407fth Y :: DEFAULT
408fmod LIST{Nat}
409fmod LIST{Nat} * (sort NeList{Nat} to NeNatList, sort List{Nat} to NatList)
410fmod LIST{Qid}
411fmod LIST{Qid} * (sort NeList{Qid} to NeQidList, sort List{Qid} to QidList)
412fmod SET{Qid}
413fmod SET{Qid} * (sort NeSet{Qid} to NeQidSet, sort Set{Qid} to QidSet)
414fmod QID-SET * (op _`,_ to _;_ [prec 43], op empty to none)
415fmod SET{Qid} * (sort NeSet{Qid} to NeQidSet, sort Set{Qid} to QidSet) * (op
416    _`,_ to _;_ [prec 43], op empty to none)
417fmod ONE * (sort Foo to Baz)
418fmod TWO * (sort Baz to Baz', sort Quux to Quux')
419fmod ONE * (sort Foo to Baz) * (sort Baz to Baz')
420fmod FOO * (sort Foo to Baz, op a to b)
421fmod FOO' * (sort Foo to Quux, op _+_ : [Baz] [Baz] -> [Foo,Bar] to _._ [prec
422    27 gather (E e)], op _+_ : [Foo,Bar] [Foo,Bar] -> [Foo,Bar] to _*_ [prec 29
423    gather (E e)])
424fmod FOO' * (sort Foo to Quux, op _+_ to _*_ [prec 29 gather (E E)])
425fmod BASH * (op f : [Foo,Bar] -> [Foo,Bar] to g)
426fmod DIFF * (op f : [Bar] -> [Bar] to g, op f : [Foo] -> [Foo] to g)
427Maude> Bye.
428