1 | K### Ambiguous input "mkGotoFrom nm cpeq cpneq cpand cpsum cpcon == |
---|
2 | ### (let |
---|
3 | ### ceq = (duplicateComponent |
---|
4 | ### (case (cpeq) of None => (mkRelationalOperator ''eq'' ''=='') |
---|
5 | ### | Some p => p) 4); |
---|
6 | ### cneq = (case (cpneq) of None => (mkRelationalOperator ''neq'' ''~='') |
---|
7 | ### | Some p => p); |
---|
8 | ### cand = (duplicateComponent |
---|
9 | ### (case (cpand) of None => (mkLogicalOperator ''and'' ''AND'' 2) |
---|
10 | ### | Some p => p) 5); |
---|
11 | ### csum = (duplicateComponent |
---|
12 | ### (case (cpsum) of None => (mkAdd ''sum'' ''++'') |
---|
13 | ### | Some p => p) 2); |
---|
14 | ### ccon = (case (cpcon) of None => (mkConstant ''const'' ''-1'') |
---|
15 | ### | Some p => p) |
---|
16 | ### in |
---|
17 | ### (mkSubsystem nm 1 1 |
---|
18 | ### ([i:[1..5] -> (nm,''In1'') >> (''GotoFrom''@(toString i),''In1'')]@ |
---|
19 | ### [(''GotoFrom1'',''Out1'') >> (cID (nth ceq 1),''In1''), |
---|
20 | ### (''GotoFrom4'',''Out1'') >> (cID (nth ceq 1),''In2''), |
---|
21 | ### (''GotoFrom1'',''Out1'') >> (cID (nth ceq 2),''In1''), |
---|
22 | ### (''GotoFrom5'',''Out1'') >> (cID (nth ceq 2),''In2''), |
---|
23 | ### (''GotoFrom2'',''Out1'') >> (cID (nth ceq 3),''In1''), |
---|
24 | ### (''GotoFrom3'',''Out1'') >> (cID (nth ceq 3),''In2''), |
---|
25 | ### (''GotoFrom2'',''Out1'') >> (cID (nth ceq 4),''In1''), |
---|
26 | ### (''GotoFrom6'',''Out1'') >> (cID (nth ceq 4),''In2''), |
---|
27 | ### (''GotoFrom5'',''Out1'') >> (cID cneq,''In1''), |
---|
28 | ### (''GotoFrom6'',''Out1'') >> (cID cneq,''In2''), |
---|
29 | ### (cID (nth ceq 1),''Out1'') >> (cID (nth cand 1),''In1''), |
---|
30 | ### (cID (nth ceq 2),''Out1'') >> (cID (nth cand 1),''In2''), |
---|
31 | ### (cID (nth ceq 3),''Out1'') >> (cID (nth cand 2),''In1''), |
---|
32 | ### (cID (nth ceq 4),''Out1'') >> (cID (nth cand 2),''In2''), |
---|
33 | ### (cID cneq, ''Out1'') >> (cID (nth cand 3),''In1''), |
---|
34 | ### (cID (nth ceq 1),''Out1'') >> (cID (nth cand 3),''In2''), |
---|
35 | ### (cID (nth cand 1),''Out1'') >> (cID (nth cand 4),''In1''), |
---|
36 | ### (cID (nth cand 2),''Out1'') >> (cID (nth cand 4),''In2''), |
---|
37 | ### (cID (nth cand 3),''Out1'') >> (cID (nth cand 5),''In1''), |
---|
38 | ### (cID (nth cand 4),''Out1'') >> (cID (nth cand 5),''In2''), |
---|
39 | ### (cID (nth cand 5),''Out1'') >> (cID (nth csum 1),''In1''), |
---|
40 | ### (cID ccon, ''Out1'') >> (cID (nth csum 1),''In2''), |
---|
41 | ### (cID (nth csum 1),''Out1'') >> (cID (nth csum 2),''In1''), |
---|
42 | ### (''GotoFrom2'',''Out1'') >> (cID (nth csum 2),''In2'')]) |
---|
43 | ### |
---|
44 | ### ([(mkGotoFrom1 ''GotoFrom1''), |
---|
45 | ### (mkGotoFrom2 ''GotoFrom2''), |
---|
46 | ### (mkGotoFrom3 ''GotoFrom3''), |
---|
47 | ### (mkGotoFrom4 ''GotoFrom4''), |
---|
48 | ### (mkGotoFrom5 ''GotoFrom5''), |
---|
49 | ### (mkGotoFrom6 ''GotoFrom6''), |
---|
50 | ### cneq, ccon]@ceq@cand@csum)))" |
---|
51 | ### produces 2 parse trees.L |
---|
52 | K### ("==" |
---|
53 | ### ("_applC" mkGotoFrom |
---|
54 | ### ("_cargs" nm |
---|
55 | ### ("_cargs" cpeq |
---|
56 | ### ("_cargs" cpneq ("_cargs" cpand ("_cargs" cpsum cpcon)))))) |
---|
57 | ### ("_Let" |
---|
58 | ### ("_binds" |
---|
59 | ### ("_bind" ceq |
---|
60 | ### ("_applC" duplicateComponent |
---|
61 | ### ("_cargs" |
---|
62 | ### ("_case_syntax" cpeq |
---|
63 | ### ("_case2" |
---|
64 | ### ("_case1" None |
---|
65 | ### ("_applC" mkRelationalOperator |
---|
66 | ### ("_cargs" ("_String" ''eq'') ("_String" ''=='')))) |
---|
67 | ### ("_case1" ("_applC" Some p) p))) |
---|
68 | ### ("_Numeral" ("_constify" 4))))) |
---|
69 | ### ("_binds" |
---|
70 | ### ("_bind" cneq |
---|
71 | ### ("_case_syntax" cpneq |
---|
72 | ### ("_case2" |
---|
73 | ### ("_case1" None |
---|
74 | ### ("_applC" mkRelationalOperator |
---|
75 | ### ("_cargs" ("_String" ''neq'') ("_String" ''~='')))) |
---|
76 | ### ("_case1" ("_applC" Some p) p)))) |
---|
77 | ### ("_binds" |
---|
78 | ### ("_bind" cand |
---|
79 | ### ("_applC" duplicateComponent |
---|
80 | ### ("_cargs" |
---|
81 | ### ("_case_syntax" cpand |
---|
82 | ### ("_case2" |
---|
83 | ### ("_case1" None |
---|
84 | ### ("_applC" mkLogicalOperator |
---|
85 | ### ("_cargs" ("_String" ''and'') |
---|
86 | ### ("_cargs" ("_String" ''AND'') |
---|
87 | ### ("_Numeral" ("_constify" 2)))))) |
---|
88 | ### ("_case1" ("_applC" Some p) p))) |
---|
89 | ### ("_Numeral" ("_constify" 5))))) |
---|
90 | ### ("_binds" |
---|
91 | ### ("_bind" csum |
---|
92 | ### ("_applC" duplicateComponent |
---|
93 | ### ("_cargs" |
---|
94 | ### ("_case_syntax" cpsum |
---|
95 | ### ("_case2" |
---|
96 | ### ("_case1" None |
---|
97 | ### ("_applC" mkAdd |
---|
98 | ### ("_cargs" ("_String" ''sum'') |
---|
99 | ### ("_String" ''++'')))) |
---|
100 | ### ("_case1" ("_applC" Some p) p))) |
---|
101 | ### ("_Numeral" ("_constify" 2))))) |
---|
102 | ### ("_bind" ccon |
---|
103 | ### ("_case_syntax" cpcon |
---|
104 | ### ("_case2" |
---|
105 | ### ("_case1" None |
---|
106 | ### ("_applC" mkConstant |
---|
107 | ### ("_cargs" ("_String" ''const'') ("_String" ''-1'')))) |
---|
108 | ### ("_case1" ("_applC" Some p) p)))))))) |
---|
109 | ### ("_applC" mkSubsystem |
---|
110 | ### ("_cargs" nm |
---|
111 | ### ("_cargs" "\<^const>HOL.one_class.one" |
---|
112 | ### ("_cargs" "\<^const>HOL.one_class.one" |
---|
113 | ### ("_cargs" |
---|
114 | ### ("\<^const>List.append" |
---|
115 | ### ("@map1" i |
---|
116 | ### ("upto" "\<^const>HOL.one_class.one" |
---|
117 | ### ("_Numeral" ("_constify" 5))) |
---|
118 | ### ("mkChannel" |
---|
119 | ### ("_tuple" nm ("_tuple_arg" ("_String" ''In1''))) |
---|
120 | ### ("_tuple" |
---|
121 | ### ("\<^const>List.append" ("_String" ''GotoFrom'') |
---|
122 | ### ("_applC" toString i)) |
---|
123 | ### ("_tuple_arg" ("_String" ''In1''))))) |
---|
124 | ### ("@list" |
---|
125 | ### ("_args" |
---|
126 | ### ("mkChannel" |
---|
127 | ### ("_tuple" ("_String" ''GotoFrom1'') |
---|
128 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
129 | ### ("_tuple" |
---|
130 | ### ("_applC" cID |
---|
131 | ### ("_applC" nth |
---|
132 | ### ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
133 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
134 | ### ("_args" |
---|
135 | ### ("mkChannel" |
---|
136 | ### ("_tuple" ("_String" ''GotoFrom4'') |
---|
137 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
138 | ### ("_tuple" |
---|
139 | ### ("_applC" cID |
---|
140 | ### ("_applC" nth |
---|
141 | ### ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
142 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
143 | ### ("_args" |
---|
144 | ### ("mkChannel" |
---|
145 | ### ("_tuple" ("_String" ''GotoFrom1'') |
---|
146 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
147 | ### ("_tuple" |
---|
148 | ### ("_applC" cID |
---|
149 | ### ("_applC" nth |
---|
150 | ### ("_cargs" ceq |
---|
151 | ### ("_Numeral" ("_constify" 2))))) |
---|
152 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
153 | ### ("_args" |
---|
154 | ### ("mkChannel" |
---|
155 | ### ("_tuple" ("_String" ''GotoFrom5'') |
---|
156 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
157 | ### ("_tuple" |
---|
158 | ### ("_applC" cID |
---|
159 | ### ("_applC" nth |
---|
160 | ### ("_cargs" ceq |
---|
161 | ### ("_Numeral" ("_constify" 2))))) |
---|
162 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
163 | ### ("_args" |
---|
164 | ### ("mkChannel" |
---|
165 | ### ("_tuple" ("_String" ''GotoFrom2'') |
---|
166 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
167 | ### ("_tuple" |
---|
168 | ### ("_applC" cID |
---|
169 | ### ("_applC" nth |
---|
170 | ### ("_cargs" ceq |
---|
171 | ### ("_Numeral" ("_constify" 3))))) |
---|
172 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
173 | ### ("_args" |
---|
174 | ### ("mkChannel" |
---|
175 | ### ("_tuple" ("_String" ''GotoFrom3'') |
---|
176 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
177 | ### ("_tuple" |
---|
178 | ### ("_applC" cID |
---|
179 | ### ("_applC" nth |
---|
180 | ### ("_cargs" ceq ("_Numeral" ("_constify" 3))))) |
---|
181 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
182 | ### ("_args" |
---|
183 | ### ("mkChannel" |
---|
184 | ### ("_tuple" ("_String" ''GotoFrom2'') |
---|
185 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
186 | ### ("_tuple" |
---|
187 | ### ("_applC" cID |
---|
188 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 4))))) |
---|
189 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
190 | ### ("_args" |
---|
191 | ### ("mkChannel" |
---|
192 | ### ("_tuple" ("_String" ''GotoFrom6'') |
---|
193 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
194 | ### ("_tuple" |
---|
195 | ### ("_applC" cID ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 4))))) |
---|
196 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
197 | ### ("_args" |
---|
198 | ### ("mkChannel" |
---|
199 | ### ("_tuple" ("_String" ''GotoFrom5'') ("_tuple_arg" ("_String" ''Out1''))) |
---|
200 | ### ("_tuple" ("_applC" cID cneq) ("_tuple_arg" ("_String" ''In1'')))) |
---|
201 | ### ("_args" |
---|
202 | ### ("mkChannel" |
---|
203 | ### ("_tuple" ("_String" ''GotoFrom6'') ("_tuple_arg" ("_String" ''Out1''))) |
---|
204 | ### ("_tuple" ("_applC" cID cneq) ("_tuple_arg" ("_String" ''In2'')))) |
---|
205 | ### ("_args" |
---|
206 | ### ("mkChannel" |
---|
207 | ### ("_tuple" |
---|
208 | ### ("_applC" cID |
---|
209 | ### ("_applC" nth ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
210 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
211 | ### ("_tuple" |
---|
212 | ### ("_applC" cID |
---|
213 | ### ("_applC" nth ("_cargs" cand "\<^const>HOL.one_class.one"))) |
---|
214 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
215 | ### ("_args" |
---|
216 | ### ("mkChannel" |
---|
217 | ### ("_tuple" |
---|
218 | ### ("_applC" cID |
---|
219 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 2))))) |
---|
220 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
221 | ### ("_tuple" |
---|
222 | ### ("_applC" cID |
---|
223 | ### ("_applC" nth ("_cargs" cand "\<^const>HOL.one_class.one"))) |
---|
224 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
225 | ### ("_args" |
---|
226 | ### ("mkChannel" |
---|
227 | ### ("_tuple" |
---|
228 | ### ("_applC" cID |
---|
229 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 3))))) |
---|
230 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
231 | ### ("_tuple" |
---|
232 | ### ("_applC" cID |
---|
233 | ### ("_applC" nth ("_cargs" cand ("_Numeral" ("_constify" 2))))) |
---|
234 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
235 | ### ("_args" |
---|
236 | ### ("mkChannel" |
---|
237 | ### ("_tuple" |
---|
238 | ### ("_applC" cID |
---|
239 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 4))))) |
---|
240 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
241 | ### ("_tuple" |
---|
242 | ### ("_applC" cID |
---|
243 | ### ("_applC" nth ("_cargs" cand ("_Numeral" ("_constify" 2))))) |
---|
244 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
245 | ### ("_args" |
---|
246 | ### ("mkChannel" |
---|
247 | ### ("_tuple" ("_applC" cID cneq) |
---|
248 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
249 | ### ("_tuple" |
---|
250 | ### ("_applC" cID |
---|
251 | ### ("_applC" nth ("_cargs" cand ("_Numeral" ("_constify" 3))))) |
---|
252 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
253 | ### ("_args" |
---|
254 | ### ("mkChannel" |
---|
255 | ### ("_tuple" |
---|
256 | ### ("_applC" cID |
---|
257 | ### ("_applC" nth |
---|
258 | ### ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
259 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
260 | ### ("_tuple" |
---|
261 | ### ("_applC" cID |
---|
262 | ### ("_applC" nth |
---|
263 | ### ("_cargs" cand ("_Numeral" ("_constify" 3))))) |
---|
264 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
265 | ### ("_args" |
---|
266 | ### ("mkChannel" |
---|
267 | ### ("_tuple" |
---|
268 | ### ("_applC" cID |
---|
269 | ### ("_applC" nth |
---|
270 | ### ("_cargs" cand "\<^const>HOL.one_class.one"))) |
---|
271 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
272 | ### ("_tuple" |
---|
273 | ### ("_applC" cID |
---|
274 | ### ("_applC" nth |
---|
275 | ### ("_cargs" cand ("_Numeral" ("_constify" 4))))) |
---|
276 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
277 | ### ("_args" |
---|
278 | ### ("mkChannel" |
---|
279 | ### ("_tuple" |
---|
280 | ### ("_applC" cID |
---|
281 | ### ("_applC" nth |
---|
282 | ### ("_cargs" cand ("_Numeral" ("_constify" 2))))) |
---|
283 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
284 | ### ("_tuple" |
---|
285 | ### ("_applC" cID |
---|
286 | ### ("_applC" nth |
---|
287 | ### ("_cargs" cand ("_Numeral" ("_constify" 4))))) |
---|
288 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
289 | ### ("_args" |
---|
290 | ### ("mkChannel" |
---|
291 | ### ("_tuple" |
---|
292 | ### ("_applC" cID |
---|
293 | ### ("_applC" nth |
---|
294 | ### ("_cargs" cand ("_Numeral" ("_constify" 3))))) |
---|
295 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
296 | ### ("_tuple" |
---|
297 | ### ("_applC" cID |
---|
298 | ### ("_applC" nth |
---|
299 | ### ("_cargs" cand ("_Numeral" ("_constify" 5))))) |
---|
300 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
301 | ### ("_args" |
---|
302 | ### ("mkChannel" |
---|
303 | ### ("_tuple" |
---|
304 | ### ("_applC" cID |
---|
305 | ### ("_applC" nth |
---|
306 | ### ("_cargs" cand ("_Numeral" ("_constify" 4))))) |
---|
307 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
308 | ### ("_tuple" |
---|
309 | ### ("_applC" cID |
---|
310 | ### ("_applC" nth |
---|
311 | ### ("_cargs" cand ("_Numeral" ("_constify" 5))))) |
---|
312 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
313 | ### ("_args" |
---|
314 | ### ("mkChannel" |
---|
315 | ### ("_tuple" |
---|
316 | ### ("_applC" cID |
---|
317 | ### ("_applC" nth |
---|
318 | ### ("_cargs" cand ("_Numeral" ("_constify" 5))))) |
---|
319 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
320 | ### ("_tuple" |
---|
321 | ### ("_applC" cID |
---|
322 | ### ("_applC" nth |
---|
323 | ### ("_cargs" csum "\<^const>HOL.one_class.one"))) |
---|
324 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
325 | ### ("_args" |
---|
326 | ### ("mkChannel" |
---|
327 | ### ("_tuple" ("_applC" cID ccon) |
---|
328 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
329 | ### ("_tuple" |
---|
330 | ### ("_applC" cID |
---|
331 | ### ("_applC" nth |
---|
332 | ### ("_cargs" csum |
---|
333 | ### "\<^const>HOL.one_class.one"))) |
---|
334 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
335 | ### ("_args" |
---|
336 | ### ("mkChannel" |
---|
337 | ### ("_tuple" |
---|
338 | ### ("_applC" cID |
---|
339 | ### ("_applC" nth |
---|
340 | ### ("_cargs" csum |
---|
341 | ### "\<^const>HOL.one_class.one"))) |
---|
342 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
343 | ### ("_tuple" |
---|
344 | ### ("_applC" cID |
---|
345 | ### ("_applC" nth |
---|
346 | ### ("_cargs" csum |
---|
347 | ### ("_Numeral" ("_constify" 2))))) |
---|
348 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
349 | ### ("mkChannel" |
---|
350 | ### ("_tuple" ("_String" ''GotoFrom2'') |
---|
351 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
352 | ### ("_tuple" |
---|
353 | ### ("_applC" cID |
---|
354 | ### ("_applC" nth |
---|
355 | ### ("_cargs" csum |
---|
356 | ### ("_Numeral" ("_constify" 2))))) |
---|
357 | ### ("_tuple_arg" |
---|
358 | ### ("_String" |
---|
359 | ### ''In2''))))))))))))))))))))))))))))) |
---|
360 | ### ("\<^const>List.append" |
---|
361 | ### ("@list" |
---|
362 | ### ("_args" ("_applC" mkGotoFrom1 ("_String" ''GotoFrom1'')) |
---|
363 | ### ("_args" |
---|
364 | ### ("_applC" mkGotoFrom2 ("_String" ''GotoFrom2'')) |
---|
365 | ### ("_args" |
---|
366 | ### ("_applC" mkGotoFrom3 ("_String" ''GotoFrom3'')) |
---|
367 | ### ("_args" |
---|
368 | ### ("_applC" mkGotoFrom4 ("_String" ''GotoFrom4'')) |
---|
369 | ### ("_args" |
---|
370 | ### ("_applC" mkGotoFrom5 ("_String" ''GotoFrom5'')) |
---|
371 | ### ("_args" |
---|
372 | ### ("_applC" mkGotoFrom6 |
---|
373 | ### ("_String" ''GotoFrom6'')) |
---|
374 | ### ("_args" cneq ccon)))))))) |
---|
375 | ### ("\<^const>List.append" ceq |
---|
376 | ### ("\<^const>List.append" cand csum))))))))))L |
---|
377 | K### ("==" |
---|
378 | ### ("_applC" mkGotoFrom |
---|
379 | ### ("_cargs" nm |
---|
380 | ### ("_cargs" cpeq |
---|
381 | ### ("_cargs" cpneq ("_cargs" cpand ("_cargs" cpsum cpcon)))))) |
---|
382 | ### ("_Let" |
---|
383 | ### ("_binds" |
---|
384 | ### ("_bind" ceq |
---|
385 | ### ("_applC" duplicateComponent |
---|
386 | ### ("_cargs" |
---|
387 | ### ("_case_syntax" cpeq |
---|
388 | ### ("_case2" |
---|
389 | ### ("_case1" None |
---|
390 | ### ("_applC" mkRelationalOperator |
---|
391 | ### ("_cargs" ("_String" ''eq'') ("_String" ''=='')))) |
---|
392 | ### ("_case1" ("_applC" Some p) p))) |
---|
393 | ### ("_Numeral" ("_constify" 4))))) |
---|
394 | ### ("_binds" |
---|
395 | ### ("_bind" cneq |
---|
396 | ### ("_case_syntax" cpneq |
---|
397 | ### ("_case2" |
---|
398 | ### ("_case1" None |
---|
399 | ### ("_applC" mkRelationalOperator |
---|
400 | ### ("_cargs" ("_String" ''neq'') ("_String" ''~='')))) |
---|
401 | ### ("_case1" ("_applC" Some p) p)))) |
---|
402 | ### ("_binds" |
---|
403 | ### ("_bind" cand |
---|
404 | ### ("_applC" duplicateComponent |
---|
405 | ### ("_cargs" |
---|
406 | ### ("_case_syntax" cpand |
---|
407 | ### ("_case2" |
---|
408 | ### ("_case1" None |
---|
409 | ### ("_applC" mkLogicalOperator |
---|
410 | ### ("_cargs" ("_String" ''and'') |
---|
411 | ### ("_cargs" ("_String" ''AND'') |
---|
412 | ### ("_Numeral" ("_constify" 2)))))) |
---|
413 | ### ("_case1" ("_applC" Some p) p))) |
---|
414 | ### ("_Numeral" ("_constify" 5))))) |
---|
415 | ### ("_binds" |
---|
416 | ### ("_bind" csum |
---|
417 | ### ("_applC" duplicateComponent |
---|
418 | ### ("_cargs" |
---|
419 | ### ("_case_syntax" cpsum |
---|
420 | ### ("_case2" |
---|
421 | ### ("_case1" None |
---|
422 | ### ("_applC" mkAdd |
---|
423 | ### ("_cargs" ("_String" ''sum'') |
---|
424 | ### ("_String" ''++'')))) |
---|
425 | ### ("_case1" ("_applC" Some p) p))) |
---|
426 | ### ("_Numeral" ("_constify" 2))))) |
---|
427 | ### ("_bind" ccon |
---|
428 | ### ("_case_syntax" cpcon |
---|
429 | ### ("_case2" |
---|
430 | ### ("_case1" None |
---|
431 | ### ("_applC" mkConstant |
---|
432 | ### ("_cargs" ("_String" ''const'') ("_String" ''-1'')))) |
---|
433 | ### ("_case1" ("_applC" Some p) p)))))))) |
---|
434 | ### ("_applC" mkSubsystem |
---|
435 | ### ("_cargs" nm |
---|
436 | ### ("_cargs" "\<^const>HOL.one_class.one" |
---|
437 | ### ("_cargs" "\<^const>HOL.one_class.one" |
---|
438 | ### ("_cargs" |
---|
439 | ### ("\<^const>List.append" |
---|
440 | ### ("@map1" i |
---|
441 | ### ("\<^const>List.finite_intvl_succ_class.upto" |
---|
442 | ### "\<^const>HOL.one_class.one" |
---|
443 | ### ("_Numeral" ("_constify" 5))) |
---|
444 | ### ("mkChannel" |
---|
445 | ### ("_tuple" nm ("_tuple_arg" ("_String" ''In1''))) |
---|
446 | ### ("_tuple" |
---|
447 | ### ("\<^const>List.append" ("_String" ''GotoFrom'') |
---|
448 | ### ("_applC" toString i)) |
---|
449 | ### ("_tuple_arg" ("_String" ''In1''))))) |
---|
450 | ### ("@list" |
---|
451 | ### ("_args" |
---|
452 | ### ("mkChannel" |
---|
453 | ### ("_tuple" ("_String" ''GotoFrom1'') |
---|
454 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
455 | ### ("_tuple" |
---|
456 | ### ("_applC" cID |
---|
457 | ### ("_applC" nth |
---|
458 | ### ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
459 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
460 | ### ("_args" |
---|
461 | ### ("mkChannel" |
---|
462 | ### ("_tuple" ("_String" ''GotoFrom4'') |
---|
463 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
464 | ### ("_tuple" |
---|
465 | ### ("_applC" cID |
---|
466 | ### ("_applC" nth |
---|
467 | ### ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
468 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
469 | ### ("_args" |
---|
470 | ### ("mkChannel" |
---|
471 | ### ("_tuple" ("_String" ''GotoFrom1'') |
---|
472 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
473 | ### ("_tuple" |
---|
474 | ### ("_applC" cID |
---|
475 | ### ("_applC" nth |
---|
476 | ### ("_cargs" ceq |
---|
477 | ### ("_Numeral" ("_constify" 2))))) |
---|
478 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
479 | ### ("_args" |
---|
480 | ### ("mkChannel" |
---|
481 | ### ("_tuple" ("_String" ''GotoFrom5'') |
---|
482 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
483 | ### ("_tuple" |
---|
484 | ### ("_applC" cID |
---|
485 | ### ("_applC" nth |
---|
486 | ### ("_cargs" ceq |
---|
487 | ### ("_Numeral" ("_constify" 2))))) |
---|
488 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
489 | ### ("_args" |
---|
490 | ### ("mkChannel" |
---|
491 | ### ("_tuple" ("_String" ''GotoFrom2'') |
---|
492 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
493 | ### ("_tuple" |
---|
494 | ### ("_applC" cID |
---|
495 | ### ("_applC" nth |
---|
496 | ### ("_cargs" ceq |
---|
497 | ### ("_Numeral" ("_constify" 3))))) |
---|
498 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
499 | ### ("_args" |
---|
500 | ### ("mkChannel" |
---|
501 | ### ("_tuple" ("_String" ''GotoFrom3'') |
---|
502 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
503 | ### ("_tuple" |
---|
504 | ### ("_applC" cID |
---|
505 | ### ("_applC" nth |
---|
506 | ### ("_cargs" ceq ("_Numeral" ("_constify" 3))))) |
---|
507 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
508 | ### ("_args" |
---|
509 | ### ("mkChannel" |
---|
510 | ### ("_tuple" ("_String" ''GotoFrom2'') |
---|
511 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
512 | ### ("_tuple" |
---|
513 | ### ("_applC" cID |
---|
514 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 4))))) |
---|
515 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
516 | ### ("_args" |
---|
517 | ### ("mkChannel" |
---|
518 | ### ("_tuple" ("_String" ''GotoFrom6'') |
---|
519 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
520 | ### ("_tuple" |
---|
521 | ### ("_applC" cID ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 4))))) |
---|
522 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
523 | ### ("_args" |
---|
524 | ### ("mkChannel" |
---|
525 | ### ("_tuple" ("_String" ''GotoFrom5'') ("_tuple_arg" ("_String" ''Out1''))) |
---|
526 | ### ("_tuple" ("_applC" cID cneq) ("_tuple_arg" ("_String" ''In1'')))) |
---|
527 | ### ("_args" |
---|
528 | ### ("mkChannel" |
---|
529 | ### ("_tuple" ("_String" ''GotoFrom6'') ("_tuple_arg" ("_String" ''Out1''))) |
---|
530 | ### ("_tuple" ("_applC" cID cneq) ("_tuple_arg" ("_String" ''In2'')))) |
---|
531 | ### ("_args" |
---|
532 | ### ("mkChannel" |
---|
533 | ### ("_tuple" |
---|
534 | ### ("_applC" cID |
---|
535 | ### ("_applC" nth ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
536 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
537 | ### ("_tuple" |
---|
538 | ### ("_applC" cID |
---|
539 | ### ("_applC" nth ("_cargs" cand "\<^const>HOL.one_class.one"))) |
---|
540 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
541 | ### ("_args" |
---|
542 | ### ("mkChannel" |
---|
543 | ### ("_tuple" |
---|
544 | ### ("_applC" cID |
---|
545 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 2))))) |
---|
546 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
547 | ### ("_tuple" |
---|
548 | ### ("_applC" cID |
---|
549 | ### ("_applC" nth ("_cargs" cand "\<^const>HOL.one_class.one"))) |
---|
550 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
551 | ### ("_args" |
---|
552 | ### ("mkChannel" |
---|
553 | ### ("_tuple" |
---|
554 | ### ("_applC" cID |
---|
555 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 3))))) |
---|
556 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
557 | ### ("_tuple" |
---|
558 | ### ("_applC" cID |
---|
559 | ### ("_applC" nth ("_cargs" cand ("_Numeral" ("_constify" 2))))) |
---|
560 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
561 | ### ("_args" |
---|
562 | ### ("mkChannel" |
---|
563 | ### ("_tuple" |
---|
564 | ### ("_applC" cID |
---|
565 | ### ("_applC" nth ("_cargs" ceq ("_Numeral" ("_constify" 4))))) |
---|
566 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
567 | ### ("_tuple" |
---|
568 | ### ("_applC" cID |
---|
569 | ### ("_applC" nth ("_cargs" cand ("_Numeral" ("_constify" 2))))) |
---|
570 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
571 | ### ("_args" |
---|
572 | ### ("mkChannel" |
---|
573 | ### ("_tuple" ("_applC" cID cneq) |
---|
574 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
575 | ### ("_tuple" |
---|
576 | ### ("_applC" cID |
---|
577 | ### ("_applC" nth ("_cargs" cand ("_Numeral" ("_constify" 3))))) |
---|
578 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
579 | ### ("_args" |
---|
580 | ### ("mkChannel" |
---|
581 | ### ("_tuple" |
---|
582 | ### ("_applC" cID |
---|
583 | ### ("_applC" nth |
---|
584 | ### ("_cargs" ceq "\<^const>HOL.one_class.one"))) |
---|
585 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
586 | ### ("_tuple" |
---|
587 | ### ("_applC" cID |
---|
588 | ### ("_applC" nth |
---|
589 | ### ("_cargs" cand ("_Numeral" ("_constify" 3))))) |
---|
590 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
591 | ### ("_args" |
---|
592 | ### ("mkChannel" |
---|
593 | ### ("_tuple" |
---|
594 | ### ("_applC" cID |
---|
595 | ### ("_applC" nth |
---|
596 | ### ("_cargs" cand "\<^const>HOL.one_class.one"))) |
---|
597 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
598 | ### ("_tuple" |
---|
599 | ### ("_applC" cID |
---|
600 | ### ("_applC" nth |
---|
601 | ### ("_cargs" cand ("_Numeral" ("_constify" 4))))) |
---|
602 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
603 | ### ("_args" |
---|
604 | ### ("mkChannel" |
---|
605 | ### ("_tuple" |
---|
606 | ### ("_applC" cID |
---|
607 | ### ("_applC" nth |
---|
608 | ### ("_cargs" cand ("_Numeral" ("_constify" 2))))) |
---|
609 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
610 | ### ("_tuple" |
---|
611 | ### ("_applC" cID |
---|
612 | ### ("_applC" nth |
---|
613 | ### ("_cargs" cand ("_Numeral" ("_constify" 4))))) |
---|
614 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
615 | ### ("_args" |
---|
616 | ### ("mkChannel" |
---|
617 | ### ("_tuple" |
---|
618 | ### ("_applC" cID |
---|
619 | ### ("_applC" nth |
---|
620 | ### ("_cargs" cand ("_Numeral" ("_constify" 3))))) |
---|
621 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
622 | ### ("_tuple" |
---|
623 | ### ("_applC" cID |
---|
624 | ### ("_applC" nth |
---|
625 | ### ("_cargs" cand ("_Numeral" ("_constify" 5))))) |
---|
626 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
627 | ### ("_args" |
---|
628 | ### ("mkChannel" |
---|
629 | ### ("_tuple" |
---|
630 | ### ("_applC" cID |
---|
631 | ### ("_applC" nth |
---|
632 | ### ("_cargs" cand ("_Numeral" ("_constify" 4))))) |
---|
633 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
634 | ### ("_tuple" |
---|
635 | ### ("_applC" cID |
---|
636 | ### ("_applC" nth |
---|
637 | ### ("_cargs" cand ("_Numeral" ("_constify" 5))))) |
---|
638 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
639 | ### ("_args" |
---|
640 | ### ("mkChannel" |
---|
641 | ### ("_tuple" |
---|
642 | ### ("_applC" cID |
---|
643 | ### ("_applC" nth |
---|
644 | ### ("_cargs" cand ("_Numeral" ("_constify" 5))))) |
---|
645 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
646 | ### ("_tuple" |
---|
647 | ### ("_applC" cID |
---|
648 | ### ("_applC" nth |
---|
649 | ### ("_cargs" csum "\<^const>HOL.one_class.one"))) |
---|
650 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
651 | ### ("_args" |
---|
652 | ### ("mkChannel" |
---|
653 | ### ("_tuple" ("_applC" cID ccon) |
---|
654 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
655 | ### ("_tuple" |
---|
656 | ### ("_applC" cID |
---|
657 | ### ("_applC" nth |
---|
658 | ### ("_cargs" csum |
---|
659 | ### "\<^const>HOL.one_class.one"))) |
---|
660 | ### ("_tuple_arg" ("_String" ''In2'')))) |
---|
661 | ### ("_args" |
---|
662 | ### ("mkChannel" |
---|
663 | ### ("_tuple" |
---|
664 | ### ("_applC" cID |
---|
665 | ### ("_applC" nth |
---|
666 | ### ("_cargs" csum |
---|
667 | ### "\<^const>HOL.one_class.one"))) |
---|
668 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
669 | ### ("_tuple" |
---|
670 | ### ("_applC" cID |
---|
671 | ### ("_applC" nth |
---|
672 | ### ("_cargs" csum |
---|
673 | ### ("_Numeral" ("_constify" 2))))) |
---|
674 | ### ("_tuple_arg" ("_String" ''In1'')))) |
---|
675 | ### ("mkChannel" |
---|
676 | ### ("_tuple" ("_String" ''GotoFrom2'') |
---|
677 | ### ("_tuple_arg" ("_String" ''Out1''))) |
---|
678 | ### ("_tuple" |
---|
679 | ### ("_applC" cID |
---|
680 | ### ("_applC" nth |
---|
681 | ### ("_cargs" csum |
---|
682 | ### ("_Numeral" ("_constify" 2))))) |
---|
683 | ### ("_tuple_arg" |
---|
684 | ### ("_String" |
---|
685 | ### ''In2''))))))))))))))))))))))))))))) |
---|
686 | ### ("\<^const>List.append" |
---|
687 | ### ("@list" |
---|
688 | ### ("_args" ("_applC" mkGotoFrom1 ("_String" ''GotoFrom1'')) |
---|
689 | ### ("_args" |
---|
690 | ### ("_applC" mkGotoFrom2 ("_String" ''GotoFrom2'')) |
---|
691 | ### ("_args" |
---|
692 | ### ("_applC" mkGotoFrom3 ("_String" ''GotoFrom3'')) |
---|
693 | ### ("_args" |
---|
694 | ### ("_applC" mkGotoFrom4 ("_String" ''GotoFrom4'')) |
---|
695 | ### ("_args" |
---|
696 | ### ("_applC" mkGotoFrom5 ("_String" ''GotoFrom5'')) |
---|
697 | ### ("_args" |
---|
698 | ### ("_applC" mkGotoFrom6 |
---|
699 | ### ("_String" ''GotoFrom6'')) |
---|
700 | ### ("_args" cneq ccon)))))))) |
---|
701 | ### ("\<^const>List.append" ceq |
---|
702 | ### ("\<^const>List.append" cand csum))))))))))L |
---|
703 | M*** More than one term is type correct: |
---|
704 | *** ((EmkGotoFromA EnmA EcpeqA EcpneqA EcpandA EcpsumA EcpconA) == |
---|
705 | *** (let (FceqA = |
---|
706 | *** (duplicateComponent |
---|
707 | *** (case EcpeqA of (None => (mkRelationalOperator ''eq'' ''=='')) |
---|
708 | *** | ((Some FpA) => FpA)) |
---|
709 | *** 4)); |
---|
710 | *** (FcneqA = |
---|
711 | *** (case EcpneqA of (None => (mkRelationalOperator ''neq'' ''~='')) |
---|
712 | *** | ((Some FpA) => FpA))); |
---|
713 | *** (FcandA = |
---|
714 | *** (duplicateComponent |
---|
715 | *** (case EcpandA of (None => (mkLogicalOperator ''and'' ''AND'' 2)) |
---|
716 | *** | ((Some FpA) => FpA)) |
---|
717 | *** 5)); |
---|
718 | *** (FcsumA = |
---|
719 | *** (duplicateComponent |
---|
720 | *** (case EcpsumA of (None => (mkAdd ''sum'' ''++'')) |
---|
721 | *** | ((Some FpA) => FpA)) |
---|
722 | *** 2)); |
---|
723 | *** (FcconA = |
---|
724 | *** (case EcpconA of (None => (mkConstant ''const'' ''-1'')) |
---|
725 | *** | ((Some FpA) => FpA))) |
---|
726 | *** in (mkSubsystem EnmA 1 1 |
---|
727 | *** ([FiA:(UptInt.upto 1 5)-> |
---|
728 | *** ((EnmA, ''In1'') >> ((''GotoFrom'' @ (toString FiA)), ''In1''))] @ |
---|
729 | *** [((''GotoFrom1'', ''Out1'') >> ((cID (FceqA ! 1)), ''In1'')), |
---|
730 | *** ((''GotoFrom4'', ''Out1'') >> ((cID (FceqA ! 1)), ''In2'')), |
---|
731 | *** ((''GotoFrom1'', ''Out1'') >> ((cID (FceqA ! 2)), ''In1'')), |
---|
732 | *** ((''GotoFrom5'', ''Out1'') >> ((cID (FceqA ! 2)), ''In2'')), |
---|
733 | *** ((''GotoFrom2'', ''Out1'') >> ((cID (FceqA ! 3)), ''In1'')), |
---|
734 | *** ((''GotoFrom3'', ''Out1'') >> ((cID (FceqA ! 3)), ''In2'')), |
---|
735 | *** ((''GotoFrom2'', ''Out1'') >> ((cID (FceqA ! 4)), ''In1'')), |
---|
736 | *** ((''GotoFrom6'', ''Out1'') >> ((cID (FceqA ! 4)), ''In2'')), |
---|
737 | *** ((''GotoFrom5'', ''Out1'') >> ((cID FcneqA), ''In1'')), |
---|
738 | *** ((''GotoFrom6'', ''Out1'') >> ((cID FcneqA), ''In2'')), |
---|
739 | *** (((cID (FceqA ! 1)), ''Out1'') >> ((cID (FcandA ! 1)), ''In1'')), |
---|
740 | *** (((cID (FceqA ! 2)), ''Out1'') >> ((cID (FcandA ! 1)), ''In2'')), |
---|
741 | *** (((cID (FceqA ! 3)), ''Out1'') >> ((cID (FcandA ! 2)), ''In1'')), |
---|
742 | *** (((cID (FceqA ! 4)), ''Out1'') >> ((cID (FcandA ! 2)), ''In2'')), |
---|
743 | *** (((cID FcneqA), ''Out1'') >> ((cID (FcandA ! 3)), ''In1'')), |
---|
744 | *** (((cID (FceqA ! 1)), ''Out1'') >> ((cID (FcandA ! 3)), ''In2'')), |
---|
745 | *** (((cID (FcandA ! 1)), ''Out1'') >> ((cID (FcandA ! 4)), ''In1'')), |
---|
746 | *** (((cID (FcandA ! 2)), ''Out1'') >> ((cID (FcandA ! 4)), ''In2'')), |
---|
747 | *** (((cID (FcandA ! 3)), ''Out1'') >> ((cID (FcandA ! 5)), ''In1'')), |
---|
748 | *** (((cID (FcandA ! 4)), ''Out1'') >> ((cID (FcandA ! 5)), ''In2'')), |
---|
749 | *** (((cID (FcandA ! 5)), ''Out1'') >> ((cID (FcsumA ! 1)), ''In1'')), |
---|
750 | *** (((cID FcconA), ''Out1'') >> ((cID (FcsumA ! 1)), ''In2'')), |
---|
751 | *** (((cID (FcsumA ! 1)), ''Out1'') >> ((cID (FcsumA ! 2)), ''In1'')), |
---|
752 | *** ((''GotoFrom2'', ''Out1'') >> ((cID (FcsumA ! 2)), ''In2''))]) |
---|
753 | *** ([(mkGotoFrom1 ''GotoFrom1''), (mkGotoFrom2 ''GotoFrom2''), |
---|
754 | *** (mkGotoFrom3 ''GotoFrom3''), (mkGotoFrom4 ''GotoFrom4''), |
---|
755 | *** (mkGotoFrom5 ''GotoFrom5''), (mkGotoFrom6 ''GotoFrom6''), FcneqA, |
---|
756 | *** FcconA] @ |
---|
757 | *** (FceqA @ (FcandA @ FcsumA)))))) |
---|
758 | *** ((EmkGotoFromA EnmA EcpeqA EcpneqA EcpandA EcpsumA EcpconA) == |
---|
759 | *** (let (FceqA = |
---|
760 | *** (duplicateComponent |
---|
761 | *** (case EcpeqA of (None => (mkRelationalOperator ''eq'' ''=='')) |
---|
762 | *** | ((Some FpA) => FpA)) |
---|
763 | *** 4)); |
---|
764 | *** (FcneqA = |
---|
765 | *** (case EcpneqA of (None => (mkRelationalOperator ''neq'' ''~='')) |
---|
766 | *** | ((Some FpA) => FpA))); |
---|
767 | *** (FcandA = |
---|
768 | *** (duplicateComponent |
---|
769 | *** (case EcpandA of (None => (mkLogicalOperator ''and'' ''AND'' 2)) |
---|
770 | *** | ((Some FpA) => FpA)) |
---|
771 | *** 5)); |
---|
772 | *** (FcsumA = |
---|
773 | *** (duplicateComponent |
---|
774 | *** (case EcpsumA of (None => (mkAdd ''sum'' ''++'')) |
---|
775 | *** | ((Some FpA) => FpA)) |
---|
776 | *** 2)); |
---|
777 | *** (FcconA = |
---|
778 | *** (case EcpconA of (None => (mkConstant ''const'' ''-1'')) |
---|
779 | *** | ((Some FpA) => FpA))) |
---|
780 | *** in (mkSubsystem EnmA 1 1 |
---|
781 | *** ([FiA:[1..5]-> |
---|
782 | *** ((EnmA, ''In1'') >> ((''GotoFrom'' @ (toString FiA)), ''In1''))] @ |
---|
783 | *** [((''GotoFrom1'', ''Out1'') >> ((cID (FceqA ! 1)), ''In1'')), |
---|
784 | *** ((''GotoFrom4'', ''Out1'') >> ((cID (FceqA ! 1)), ''In2'')), |
---|
785 | *** ((''GotoFrom1'', ''Out1'') >> ((cID (FceqA ! 2)), ''In1'')), |
---|
786 | *** ((''GotoFrom5'', ''Out1'') >> ((cID (FceqA ! 2)), ''In2'')), |
---|
787 | *** ((''GotoFrom2'', ''Out1'') >> ((cID (FceqA ! 3)), ''In1'')), |
---|
788 | *** ((''GotoFrom3'', ''Out1'') >> ((cID (FceqA ! 3)), ''In2'')), |
---|
789 | *** ((''GotoFrom2'', ''Out1'') >> ((cID (FceqA ! 4)), ''In1'')), |
---|
790 | *** ((''GotoFrom6'', ''Out1'') >> ((cID (FceqA ! 4)), ''In2'')), |
---|
791 | *** ((''GotoFrom5'', ''Out1'') >> ((cID FcneqA), ''In1'')), |
---|
792 | *** ((''GotoFrom6'', ''Out1'') >> ((cID FcneqA), ''In2'')), |
---|
793 | *** (((cID (FceqA ! 1)), ''Out1'') >> ((cID (FcandA ! 1)), ''In1'')), |
---|
794 | *** (((cID (FceqA ! 2)), ''Out1'') >> ((cID (FcandA ! 1)), ''In2'')), |
---|
795 | *** (((cID (FceqA ! 3)), ''Out1'') >> ((cID (FcandA ! 2)), ''In1'')), |
---|
796 | *** (((cID (FceqA ! 4)), ''Out1'') >> ((cID (FcandA ! 2)), ''In2'')), |
---|
797 | *** (((cID FcneqA), ''Out1'') >> ((cID (FcandA ! 3)), ''In1'')), |
---|
798 | *** (((cID (FceqA ! 1)), ''Out1'') >> ((cID (FcandA ! 3)), ''In2'')), |
---|
799 | *** (((cID (FcandA ! 1)), ''Out1'') >> ((cID (FcandA ! 4)), ''In1'')), |
---|
800 | *** (((cID (FcandA ! 2)), ''Out1'') >> ((cID (FcandA ! 4)), ''In2'')), |
---|
801 | *** (((cID (FcandA ! 3)), ''Out1'') >> ((cID (FcandA ! 5)), ''In1'')), |
---|
802 | *** (((cID (FcandA ! 4)), ''Out1'') >> ((cID (FcandA ! 5)), ''In2'')), |
---|
803 | *** (((cID (FcandA ! 5)), ''Out1'') >> ((cID (FcsumA ! 1)), ''In1'')), |
---|
804 | *** (((cID FcconA), ''Out1'') >> ((cID (FcsumA ! 1)), ''In2'')), |
---|
805 | *** (((cID (FcsumA ! 1)), ''Out1'') >> ((cID (FcsumA ! 2)), ''In1'')), |
---|
806 | *** ((''GotoFrom2'', ''Out1'') >> ((cID (FcsumA ! 2)), ''In2''))]) |
---|
807 | *** ([(mkGotoFrom1 ''GotoFrom1''), (mkGotoFrom2 ''GotoFrom2''), |
---|
808 | *** (mkGotoFrom3 ''GotoFrom3''), (mkGotoFrom4 ''GotoFrom4''), |
---|
809 | *** (mkGotoFrom5 ''GotoFrom5''), (mkGotoFrom6 ''GotoFrom6''), FcneqA, |
---|
810 | *** FcconA] @ |
---|
811 | *** (FceqA @ (FcandA @ FcsumA)))))) |
---|
812 | *** At command "constdefs".N |
---|