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
|
==========================================
reduce in META-MODULE : subsort 'Foo < 'Bar . .
rewrites: 0
result SubsortDecl: subsort 'Foo < 'Bar .
==========================================
reduce in META-MODULE : op 'f : 'Foo -> 'Bar [none] . .
rewrites: 0
result OpDecl: op 'f : 'Foo -> 'Bar [none] .
==========================================
reduce in META-MODULE : ceq 'f['X:Foo] = 'a.Bar if 'g['a.Foo, 'Y:Foo] := 'X:Foo
[none] . .
rewrites: 0
result Equation: ceq 'f['X:Foo] = 'a.Bar if 'g['a.Foo, 'Y:Foo] := 'X:Foo [none]
.
==========================================
reduce in META-MODULE : 'g['a.Foo, 'Y:Foo] := 'X:Foo .
rewrites: 0
result EqCondition: 'g['a.Foo, 'Y:Foo] := 'X:Foo
==========================================
reduce in META-MODULE : fmod 'FOO is
including 'MACHINE-INT .
sorts 'Bar ; 'Foo .
subsort 'Foo < 'Bar .
op 'f : 'Foo -> 'Bar [none] .
op 'g : '`[Bar`] -> '`[Bar`] [none] .
cmb 'X:Bar : 'Foo if 'f['Y:Bar] := 'f['X:Bar] /\ 'g['Y:Bar, 'a.Foo] = 'a.Foo
[none] .
eq 'f['X:Foo] = 'g['a.Foo, 'X:Foo] [none] .
ceq 'f['X:Foo] = 'a.Bar if 'g['a.Foo, 'Y:Foo] := 'X:Foo [none] .
endfm .
rewrites: 0
result FModule: fmod 'FOO is
including 'MACHINE-INT .
sorts 'Bar ; 'Foo .
subsort 'Foo < 'Bar .
op 'f : 'Foo -> 'Bar [none] .
op 'g : '`[Bar`] -> '`[Bar`] [none] .
cmb 'X:Bar : 'Foo if 'f['Y:Bar] := 'f['X:Bar] /\ 'g['Y:Bar, 'a.Foo] = 'a.Foo
[none] .
eq 'f['X:Foo] = 'g['a.Foo, 'X:Foo] [none] .
ceq 'f['X:Foo] = 'a.Bar if 'g['a.Foo, 'Y:Foo] := 'X:Foo [none] .
endfm
==========================================
reduce in META-MODULE : fmod 'FOO is
including 'MACHINE-INT .
sorts 'Bar ; 'Foo .
subsort 'Foo < 'Bar .
op 'f : 'Foo -> 'Bar [none] .
op 'g : '`[Bar`] -> '`[Bar`] [none] .
none
eq 'f['X:Foo] = 'g['a.Foo, 'X:Foo] [none] .
endfm .
rewrites: 0
result FModule: fmod 'FOO is
including 'MACHINE-INT .
sorts 'Bar ; 'Foo .
subsort 'Foo < 'Bar .
op 'f : 'Foo -> 'Bar [none] .
op 'g : '`[Bar`] -> '`[Bar`] [none] .
none
eq 'f['X:Foo] = 'g['a.Foo, 'X:Foo] [none] .
endfm
Bye.
|
