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
|
fmod TEST is
sorts Bool Zero NzNat Nat .
subsorts Zero NzNat < Nat .
op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
0 gather (& & &) special (
id-hook BranchSymbol
term-hook 1 (true)
term-hook 2 (false))] .
op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
special (
id-hook EqualitySymbol
term-hook equalTerm (true)
term-hook notEqualTerm (false))] .
op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
special (
id-hook EqualitySymbol
term-hook equalTerm (false)
term-hook notEqualTerm (true))] .
op true : -> Bool [ctor special (
id-hook SystemTrue)] .
op false : -> Bool [ctor special (
id-hook SystemFalse)] .
op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
op not_ : Bool -> Bool [prec 53 gather (E)] .
op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
op 0 : -> Zero [ctor] .
op s_ : Nat -> NzNat [ctor iter prec 15 gather (E) special (
id-hook SuccSymbol
term-hook zeroTerm (0))] .
op _+_ : NzNat Nat -> NzNat [assoc comm prec 33 gather (e E) special (
id-hook ACU_NumberOpSymbol (+)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _+_ : Nat Nat -> Nat [assoc comm prec 33 gather (e E) special (
id-hook ACU_NumberOpSymbol (+)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op sd : Nat Nat -> Nat [comm special (
id-hook CUI_NumberOpSymbol (sd)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _*_ : NzNat NzNat -> NzNat [assoc comm prec 31 gather (e E) special (
id-hook ACU_NumberOpSymbol (*)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _*_ : Nat Nat -> Nat [assoc comm prec 31 gather (e E) special (
id-hook ACU_NumberOpSymbol (*)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _quo_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
id-hook NumberOpSymbol (quo)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _rem_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
id-hook NumberOpSymbol (rem)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _^_ : Nat Nat -> Nat [prec 29 gather (E e) special (
id-hook NumberOpSymbol (^)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _^_ : NzNat Nat -> NzNat [prec 29 gather (E e) special (
id-hook NumberOpSymbol (^)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op modExp : [Nat] [Nat] [Nat] -> [Nat] [special (
id-hook NumberOpSymbol (modExp)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op gcd : NzNat Nat -> NzNat [assoc comm special (
id-hook ACU_NumberOpSymbol (gcd)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op gcd : Nat Nat -> Nat [assoc comm special (
id-hook ACU_NumberOpSymbol (gcd)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op lcm : NzNat NzNat -> NzNat [assoc comm special (
id-hook ACU_NumberOpSymbol (lcm)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op lcm : Nat Nat -> Nat [assoc comm special (
id-hook ACU_NumberOpSymbol (lcm)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op min : NzNat NzNat -> NzNat [assoc comm special (
id-hook ACU_NumberOpSymbol (min)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op min : Nat Nat -> Nat [assoc comm special (
id-hook ACU_NumberOpSymbol (min)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op max : NzNat Nat -> NzNat [assoc comm special (
id-hook ACU_NumberOpSymbol (max)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op max : Nat Nat -> Nat [assoc comm special (
id-hook ACU_NumberOpSymbol (max)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _xor_ : Nat Nat -> Nat [assoc comm prec 55 gather (e E) special (
id-hook ACU_NumberOpSymbol (xor)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _&_ : Nat Nat -> Nat [assoc comm prec 53 gather (e E) special (
id-hook ACU_NumberOpSymbol (&)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _|_ : NzNat Nat -> NzNat [assoc comm prec 57 gather (e E) special (
id-hook ACU_NumberOpSymbol (|)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _|_ : Nat Nat -> Nat [assoc comm prec 57 gather (e E) special (
id-hook ACU_NumberOpSymbol (|)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _>>_ : Nat Nat -> Nat [prec 35 gather (E e) special (
id-hook NumberOpSymbol (>>)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _<<_ : Nat Nat -> Nat [prec 35 gather (E e) special (
id-hook NumberOpSymbol (<<)
op-hook succSymbol (s_ : Nat ~> NzNat))] .
op _<_ : Nat Nat -> Bool [prec 37 gather (E E) special (
id-hook NumberOpSymbol (<)
op-hook succSymbol (s_ : Nat ~> NzNat)
term-hook trueTerm (true)
term-hook falseTerm (false))] .
op _<=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
id-hook NumberOpSymbol (<=)
op-hook succSymbol (s_ : Nat ~> NzNat)
term-hook trueTerm (true)
term-hook falseTerm (false))] .
op _>_ : Nat Nat -> Bool [prec 37 gather (E E) special (
id-hook NumberOpSymbol (>)
op-hook succSymbol (s_ : Nat ~> NzNat)
term-hook trueTerm (true)
term-hook falseTerm (false))] .
op _>=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
id-hook NumberOpSymbol (>=)
op-hook succSymbol (s_ : Nat ~> NzNat)
term-hook trueTerm (true)
term-hook falseTerm (false))] .
op _divides_ : NzNat Nat -> Bool [prec 51 gather (E E) special (
id-hook NumberOpSymbol (divides)
op-hook succSymbol (s_ : Nat ~> NzNat)
term-hook trueTerm (true)
term-hook falseTerm (false))] .
op r : -> Nat .
eq true and A:Bool = A:Bool .
eq false and A:Bool = false .
eq A:Bool and A:Bool = A:Bool .
eq false xor A:Bool = A:Bool .
eq A:Bool xor A:Bool = false .
eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
eq not A:Bool = true xor A:Bool .
eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
eq r = 5 .
endfm
fmod TEST{Y :: TWO} is
sort Y$Bar .
op Y$d : -> Y$Bar [pconst] .
eq X:Y$Bar = Y$d .
eq Y$d = Y$d .
endfm
fmod TEST{Y :: TWO} is
sort Y$Bar .
op Y$d : -> Y$Bar [pconst] .
op g : Y$Bar Y$Bar -> Y$Bar .
eq g(Y$d, Y$d) = g(Y$d, Y$d) .
endfm
Bye.
|
