1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
|
Maude> ==========================================
reduce in META-LEVEL : upEqs('ATTR-TEST, true) .
rewrites: 1
result EquationSet: eq '_and_['A:Bool,'A:Bool] = 'A:Bool [none] .
eq '_and_['A:Bool,'_xor_['B:Bool,'C:Bool]] = '_xor_['_and_['A:Bool,'B:Bool],
'_and_['A:Bool,'C:Bool]] [none] .
eq '_and_['false.Bool,'A:Bool] = 'false.Bool [none] .
eq '_and_['true.Bool,'A:Bool] = 'A:Bool [none] .
eq '_implies_['A:Bool,'B:Bool] = 'not_['_xor_['A:Bool,'_and_['A:Bool,'B:Bool]]]
[none] .
eq '_or_['A:Bool,'B:Bool] = '_xor_['_and_['A:Bool,'B:Bool],'_xor_['A:Bool,
'B:Bool]] [none] .
eq '_xor_['A:Bool,'A:Bool] = 'false.Bool [none] .
eq '_xor_['false.Bool,'A:Bool] = 'A:Bool [none] .
eq 'f['X:Foo,'a.Foo] = 'X:Foo [label('first) metadata(
"this is the first equation")] .
eq 'f['b.Foo,'Y:Foo] = 'b.Foo [metadata("this is the second equation")] .
eq 'not_['A:Bool] = '_xor_['true.Bool,'A:Bool] [none] .
==========================================
reduce in META-LEVEL : upRls('ATTR-TEST, true) .
rewrites: 1
result Rule: rl 'a.Foo => 'b.Foo [label('r1)] .
==========================================
reduce in META-LEVEL : upMbs('ATTR-TEST, true) .
rewrites: 1
result MembAx: mb 'a.Foo : 'Foo [label('baz) metadata("this is an mb")] .
==========================================
reduce in META-LEVEL : upEqs('ATTR-TEST, false) .
rewrites: 1
result EquationSet: eq 'f['X:Foo,'a.Foo] = 'X:Foo [label('first) metadata(
"this is the first equation")] .
eq 'f['b.Foo,'Y:Foo] = 'b.Foo [metadata("this is the second equation")] .
==========================================
reduce in META-LEVEL : upRls('ATTR-TEST, false) .
rewrites: 1
result Rule: rl 'a.Foo => 'b.Foo [label('r1)] .
==========================================
reduce in META-LEVEL : upMbs('ATTR-TEST, false) .
rewrites: 1
result MembAx: mb 'a.Foo : 'Foo [label('baz) metadata("this is an mb")] .
==========================================
reduce in META-LEVEL : upRls('BOOL, true) .
rewrites: 1
result RuleSet: (none).RuleSet
==========================================
reduce in META-LEVEL : upRls('KNIGHT, true) .
rewrites: 1
result RuleSet: rl 'knight['0.Zero] => '`[_`,_`]['s_['0.Zero],'s_['0.Zero]] [
none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_['0.Zero]],
'_+_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_['0.Zero]],
'_-_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_^2['0.Zero]],
'_+_['Y:Int,'s_['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_+_['X:Int,'s_^2['0.Zero]],
'_-_['Y:Int,'s_['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_['0.Zero]],
'_+_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_['0.Zero]],
'_-_['Y:Int,'s_^2['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_^2['0.Zero]],
'_+_['Y:Int,'s_['0.Zero]]] [none] .
rl 'move_['`[_`,_`]['X:Int,'Y:Int]] => '`[_`,_`]['_-_['X:Int,'s_^2['0.Zero]],
'_-_['Y:Int,'s_['0.Zero]]] [none] .
crl 'knight['N:Int] => '__['L:List,'__['P:Pair,'Q:Pair]] if '_>_['N:Int,
'0.Zero] = 'true.Bool /\ 'knight['_-_['N:Int,'s_['0.Zero]]] => '__['L:List,
'P:Pair] /\ 'move_['P:Pair] => 'Q:Pair /\ 'legal['Q:Pair] = 'true.Bool /\
'not_['contains['__['L:List,'P:Pair],'Q:Pair]] = 'true.Bool [none] .
==========================================
rewrite in INTROSPECTION : rules .
rewrites: 2
result Rule: rl 'rules.RuleSet => 'upRls[''INTROSPECTION.Sort,'false.Bool] [
none] .
==========================================
rewrite in SELF-REFLECTION : myRules .
rewrites: 2
result RuleSet: rl 'allRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,
'true.Bool] [none] .
rl 'myRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,'false.Bool] [none] .
==========================================
rewrite in SELF-REFLECTION : allRules .
rewrites: 2
result RuleSet: rl 'allRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,
'true.Bool] [none] .
rl 'myRules.RuleSet => 'upRls[''SELF-REFLECTION.Sort,'false.Bool] [none] .
rl 'rules.RuleSet => 'upRls[''INTROSPECTION.Sort,'false.Bool] [none] .
==========================================
reduce in META-LEVEL : upEqs('META-LEVEL, true) .
rewrites: 1
result EquationSet: eq '$card['none.EmptyTypeSet,'C:Nat] = 'C:Nat [none] .
eq '$card['_;_['E:Qid,'S:QidSet],'C:Nat] = '$card['S:QidSet,'_+_['C:Nat,'s_[
'0.Zero]]] [owise] .
eq '$card['_;_['N:NeQidSet,'N:NeQidSet,'S:QidSet],'C:Nat] = '$card['_;_[
'N:NeQidSet,'S:QidSet],'C:Nat] [none] .
eq '$diff['none.EmptyTypeSet,'S':QidSet,'A:QidSet] = 'A:QidSet [none] .
eq '$diff['_;_['E:Qid,'S:QidSet],'S':QidSet,'A:QidSet] = '$diff['S:QidSet,
'S':QidSet,'if_then_else_fi['_in_['E:Qid,'S':QidSet],'A:QidSet,'_;_['E:Qid,
'A:QidSet]]] [none] .
eq '$intersect['none.EmptyTypeSet,'S':QidSet,'A:QidSet] = 'A:QidSet [none] .
eq '$intersect['_;_['E:Qid,'S:QidSet],'S':QidSet,'A:QidSet] = '$intersect[
'S:QidSet,'S':QidSet,'if_then_else_fi['_in_['E:Qid,'S':QidSet],'_;_['E:Qid,
'A:QidSet],'A:QidSet]] [none] .
eq '$reverse['nil.NatList,'A:NatList] = 'A:NatList [none] .
eq '$reverse['nil.TypeList,'A:QidList] = 'A:QidList [none] .
eq '$reverse['__['E:Nat,'L:NatList],'A:NatList] = '$reverse['L:NatList,'__[
'E:Nat,'A:NatList]] [none] .
eq '$reverse['__['E:Qid,'L:QidList],'A:QidList] = '$reverse['L:QidList,'__[
'E:Qid,'A:QidList]] [none] .
eq '$size['nil.NatList,'C:Nat] = 'C:Nat [none] .
eq '$size['nil.TypeList,'C:Nat] = 'C:Nat [none] .
eq '$size['__['E:Nat,'L:NatList],'C:Nat] = '$size['L:NatList,'_+_['C:Nat,'s_[
'0.Zero]]] [none] .
eq '$size['__['E:Qid,'L:QidList],'C:Nat] = '$size['L:QidList,'_+_['C:Nat,'s_[
'0.Zero]]] [none] .
eq '_;_['A:Assignment,'A:Assignment] = 'A:Assignment [none] .
eq '_;_['N:NeQidSet,'N:NeQidSet] = 'N:NeQidSet [none] .
eq '_;_['T:TypeList,'T:TypeList] = 'T:TypeList [none] .
eq '_\_['S:QidSet,'N:NeQidSet] = '$diff['S:QidSet,'N:NeQidSet,
'none.EmptyTypeSet] [none] .
eq '_\_['S:QidSet,'none.EmptyTypeSet] = 'S:QidSet [none] .
eq '__['A:Attr,'A:Attr] = 'A:Attr [none] .
eq '__['E:Equation,'E:Equation] = 'E:Equation [none] .
eq '__['M:MembAx,'M:MembAx] = 'M:MembAx [none] .
eq '__['O:OpDecl,'O:OpDecl] = 'O:OpDecl [none] .
eq '__['O:OpMapping,'O:OpMapping] = 'O:OpMapping [none] .
eq '__['R:Rule,'R:Rule] = 'R:Rule [none] .
eq '__['S:SortMapping,'S:SortMapping] = 'S:SortMapping [none] .
eq '__['S:SubsortDecl,'S:SubsortDecl] = 'S:SubsortDecl [none] .
eq '_and-then_['false.Bool,'B:`[Bool`]] = 'false.Bool [none] .
eq '_and-then_['true.Bool,'B:`[Bool`]] = 'B:`[Bool`] [none] .
eq '_and_['A:Bool,'A:Bool] = 'A:Bool [none] .
eq '_and_['A:Bool,'_xor_['B:Bool,'C:Bool]] = '_xor_['_and_['A:Bool,'B:Bool],
'_and_['A:Bool,'C:Bool]] [none] .
eq '_and_['false.Bool,'A:Bool] = 'false.Bool [none] .
eq '_and_['true.Bool,'A:Bool] = 'A:Bool [none] .
eq '_implies_['A:Bool,'B:Bool] = 'not_['_xor_['A:Bool,'_and_['A:Bool,'B:Bool]]]
[none] .
eq '_in_['E:Qid,'S:QidSet] = 'false.Bool [owise] .
eq '_in_['E:Qid,'_;_['E:Qid,'S:QidSet]] = 'true.Bool [none] .
eq '_or-else_['false.Bool,'B:`[Bool`]] = 'B:`[Bool`] [none] .
eq '_or-else_['true.Bool,'B:`[Bool`]] = 'true.Bool [none] .
eq '_or_['A:Bool,'B:Bool] = '_xor_['_and_['A:Bool,'B:Bool],'_xor_['A:Bool,
'B:Bool]] [none] .
eq '_psubset_['S:QidSet,'S':QidSet] = '_and-then_['_=/=_['S:QidSet,'S':QidSet],
'_subset_['S:QidSet,'S':QidSet]] [none] .
eq '_subset_['none.EmptyTypeSet,'S':QidSet] = 'true.Bool [none] .
eq '_subset_['_;_['E:Qid,'S:QidSet],'S':QidSet] = '_and-then_['_in_['E:Qid,
'S':QidSet],'_subset_['S:QidSet,'S':QidSet]] [none] .
eq '_xor_['A:Bool,'A:Bool] = 'false.Bool [none] .
eq '_xor_['false.Bool,'A:Bool] = 'A:Bool [none] .
eq '`[_`]['Q:Qid] = 'th_is_sorts_._____endth['Q:Qid,'including_.['Q:Qid],
'none.EmptyTypeSet,'none.SubsortDeclSet,'none.OpDeclSet,'none.MembAxSet,
'none.EquationSet,'none.RuleSet] [none] .
eq 'append['A:NatList,'L:NatList] = '__['A:NatList,'L:NatList] [none] .
eq 'append['A:QidList,'L:QidList] = '__['A:QidList,'L:QidList] [none] .
eq 'delete['E:Qid,'S:QidSet] = 'S:QidSet [owise] .
eq 'delete['E:Qid,'_;_['E:Qid,'S:QidSet]] = 'delete['E:Qid,'S:QidSet] [none] .
eq 'front['__['L:NatList,'E:Nat]] = 'L:NatList [none] .
eq 'front['__['L:QidList,'E:Qid]] = 'L:QidList [none] .
eq 'getContext['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,'C:Context]] =
'C:Context [none] .
eq 'getContext['`{_`,_`}['S:Substitution,'C:Context]] = 'C:Context [none] .
eq 'getEqs['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'EQS:EquationSet [none] .
eq 'getEqs['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'EQS:EquationSet [none] .
eq 'getEqs['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'EQS:EquationSet [none] .
eq 'getEqs['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'EQS:EquationSet [none] .
eq 'getFrom['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
'ME:ModuleExpression [none] .
eq 'getImports['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'IL:ImportList [none] .
eq 'getImports['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'IL:ImportList [none] .
eq 'getImports['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'IL:ImportList [none] .
eq 'getImports['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'IL:ImportList [none] .
eq 'getMbs['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'MAS:MembAxSet [none] .
eq 'getMbs['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'MAS:MembAxSet [none] .
eq 'getMbs['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'MAS:MembAxSet [none] .
eq 'getMbs['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'MAS:MembAxSet [none] .
eq 'getName['C:Constant] = 'qid['substr['string['C:Constant],'0.Zero,'rfind[
'string['C:Constant],'".".Char,'length['string['C:Constant]]]]] [none] .
eq 'getName['V:Variable] = 'qid['substr['string['V:Variable],'0.Zero,'rfind[
'string['V:Variable],'":".Char,'length['string['V:Variable]]]]] [none] .
eq 'getName['fmod_is_sorts_.____endfm['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'Q:Qid [none] .
eq 'getName['fmod_is_sorts_.____endfm['_`{_`}['Q:Qid,'PDL:ParameterDeclList],
'IL:ImportList,'SS:SortSet,'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,
'MAS:MembAxSet,'EQS:EquationSet]] = 'Q:Qid [none] .
eq 'getName['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'Q:Qid [none] .
eq 'getName['mod_is_sorts_._____endm['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'Q:Qid [none] .
eq 'getName['mod_is_sorts_._____endm['_`{_`}['Q:Qid,'PDL:ParameterDeclList],
'IL:ImportList,'SS:SortSet,'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,
'MAS:MembAxSet,'EQS:EquationSet,'RLS:RuleSet]] = 'Q:Qid [none] .
eq 'getName['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'Q:Qid [none] .
eq 'getName['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] = 'Q:Qid [
none] .
eq 'getOpMappings['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
'OMS:OpMappingSet [none] .
eq 'getOps['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'OPDS:OpDeclSet [none] .
eq 'getOps['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'OPDS:OpDeclSet [none] .
eq 'getOps['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'OPDS:OpDeclSet [none] .
eq 'getOps['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'OPDS:OpDeclSet [none] .
eq 'getRls['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'none.RuleSet [none] .
eq 'getRls['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'none.RuleSet [none] .
eq 'getRls['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'RLS:RuleSet [none] .
eq 'getRls['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'RLS:RuleSet [none] .
eq 'getSortMappings['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
'SMS:SortMappingSet [none] .
eq 'getSorts['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'SS:SortSet [none] .
eq 'getSorts['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'SS:SortSet [none] .
eq 'getSorts['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'SS:SortSet [none] .
eq 'getSorts['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'SS:SortSet [none] .
eq 'getSubsorts['fmod_is_sorts_.____endfm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'SSDS:SubsortDeclSet [none] .
eq 'getSubsorts['fth_is_sorts_.____endfth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet]] =
'SSDS:SubsortDeclSet [none] .
eq 'getSubsorts['mod_is_sorts_._____endm['H:Header,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'SSDS:SubsortDeclSet [none] .
eq 'getSubsorts['th_is_sorts_._____endth['Q:Qid,'IL:ImportList,'SS:SortSet,
'SSDS:SubsortDeclSet,'OPDS:OpDeclSet,'MAS:MembAxSet,'EQS:EquationSet,
'RLS:RuleSet]] = 'SSDS:SubsortDeclSet [none] .
eq 'getSubstitution['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,
'C:Context]] = 'S:Substitution [none] .
eq 'getSubstitution['`{_`,_`,_`}['T:Term,'T:Type,'S:Substitution]] =
'S:Substitution [none] .
eq 'getSubstitution['`{_`,_`}['S:Substitution,'C:Context]] = 'S:Substitution [
none] .
eq 'getTerm['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,'C:Context]] =
'T:Term [none] .
eq 'getTerm['`{_`,_`,_`}['T:Term,'T:Type,'S:Substitution]] = 'T:Term [none] .
eq 'getTerm['`{_`,_`}['T:Term,'T:Type]] = 'T:Term [none] .
eq 'getTo['view_from_to_is__endv['Q:Qid,'ME:ModuleExpression,
'ME':ModuleExpression,'SMS:SortMappingSet,'OMS:OpMappingSet]] =
'ME':ModuleExpression [none] .
eq 'getType['C:Constant] = 'qid['substr['string['C:Constant],'_+_['s_['0.Zero],
'rfind['string['C:Constant],'".".Char,'length['string['C:Constant]]]],
'length['string['C:Constant]]]] [none] .
eq 'getType['V:Variable] = 'qid['substr['string['V:Variable],'_+_['s_['0.Zero],
'rfind['string['V:Variable],'":".Char,'length['string['V:Variable]]]],
'length['string['V:Variable]]]] [none] .
eq 'getType['`{_`,_`,_`,_`}['T:Term,'T:Type,'S:Substitution,'C:Context]] =
'T:Type [none] .
eq 'getType['`{_`,_`,_`}['T:Term,'T:Type,'S:Substitution]] = 'T:Type [none] .
eq 'getType['`{_`,_`}['T:Term,'T:Type]] = 'T:Type [none] .
eq 'head['__['E:Nat,'L:NatList]] = 'E:Nat [none] .
eq 'head['__['E:Qid,'L:QidList]] = 'E:Qid [none] .
eq 'insert['E:Qid,'S:QidSet] = '_;_['E:Qid,'S:QidSet] [none] .
eq 'intersection['S:QidSet,'N:NeQidSet] = '$intersect['S:QidSet,'N:NeQidSet,
'none.EmptyTypeSet] [none] .
eq 'intersection['S:QidSet,'none.EmptyTypeSet] = 'none.EmptyTypeSet [none] .
eq 'last['__['L:NatList,'E:Nat]] = 'E:Nat [none] .
eq 'last['__['L:QidList,'E:Qid]] = 'E:Qid [none] .
eq 'metaPrettyPrint['M:Module,'T:Term] = 'metaPrettyPrint['M:Module,'T:Term,
'__['mixfix.PrintOption,'__['flat.PrintOption,'__['format.PrintOption,'__[
'number.PrintOption,'rat.PrintOption]]]]] [none] .
eq 'not_['A:Bool] = '_xor_['true.Bool,'A:Bool] [none] .
eq 'occurs['E:Nat,'nil.NatList] = 'false.Bool [none] .
eq 'occurs['E:Nat,'__['E':Nat,'L:NatList]] = 'if_then_else_fi['_==_['E:Nat,
'E':Nat],'true.Bool,'occurs['E:Nat,'L:NatList]] [none] .
eq 'occurs['E:Qid,'nil.TypeList] = 'false.Bool [none] .
eq 'occurs['E:Qid,'__['E':Qid,'L:QidList]] = 'if_then_else_fi['_==_['E:Qid,
'E':Qid],'true.Bool,'occurs['E:Qid,'L:QidList]] [none] .
eq 'reverse['L:NatList] = '$reverse['L:NatList,'nil.NatList] [none] .
eq 'reverse['L:QidList] = '$reverse['L:QidList,'nil.TypeList] [none] .
eq 'size['L:NatList] = '$size['L:NatList,'0.Zero] [none] .
eq 'size['L:QidList] = '$size['L:QidList,'0.Zero] [none] .
eq 'tail['__['E:Nat,'L:NatList]] = 'L:NatList [none] .
eq 'tail['__['E:Qid,'L:QidList]] = 'L:QidList [none] .
eq 'union['S:QidSet,'S':QidSet] = '_;_['S:QidSet,'S':QidSet] [none] .
eq '|_|['S:QidSet] = '$card['S:QidSet,'0.Zero] [none] .
Maude> Bye.
|
