Pairs.het revision d6087be434086ef1a79922001fec798bc397c56a
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
library Pairs
logic HasCASL
spec S =
type t;
var a;
op p1 : a * a -> Unit
op p2 : a * a ->? Unit
op p3 : ?a * a ->? Unit
op p4 : a * ?a ->? Unit
op p5 : ?a * ?a ->? Unit
op p6 : ?a * a -> Unit
op p7 : a * ?a -> Unit
op p8 : ?a * ?a -> Unit
op f1 : a * a -> a
op f2 : a * a ->? a
op f3 : ?a * a ->? a
op f4 : a * ?a ->? a
op f5 : ?a * ?a ->? a
op f6 : ?a * a -> a
op f7 : a * ?a -> a
op f8 : ?a * ?a -> a
op c : Unit
op b : ? Unit
op o : t
op p : ?t
. p1 (c, b)
. p1 (b, c)
. p1 (c, c)
. p1 (b, b)
. p1 (o, p)
. p1 (p, o)
. p1 (o, o)
. p1 (p, p)
. p2 (c, b)
. p2 (b, c)
. p2 (c, c)
. p2 (b, b)
. p2 (o, p)
. p2 (p, o)
. p2 (o, o)
. p2 (p, p)
. p3 (c, b)
. p3 (b, c)
. p3 (c, c)
. p3 (b, b)
. p3 (o, p)
. p3 (p, o)
. p3 (o, o)
. p3 (p, p)
. p4 (c, b)
. p4 (b, c)
. p4 (c, c)
. p4 (b, b)
. p4 (o, p)
. p4 (p, o)
. p4 (o, o)
. p4 (p, p)
. p5 (c, b)
. p5 (b, c)
. p5 (c, c)
. p5 (b, b)
. p5 (o, p)
. p5 (p, o)
. p5 (o, o)
. p5 (p, p)
. p6 (c, b)
. p6 (b, c)
. p6 (c, c)
. p6 (b, b)
. p6 (o, p)
. p6 (p, o)
. p6 (o, o)
. p6 (p, p)
. p7 (c, b)
. p7 (b, c)
. p7 (c, c)
. p7 (b, b)
. p7 (o, p)
. p7 (p, o)
. p7 (o, o)
. p7 (p, p)
. p8 (c, b)
. p8 (b, c)
. p8 (c, c)
. p8 (b, b)
. p8 (o, p)
. p8 (p, o)
. p8 (o, o)
. p8 (p, p)
. def f1 (c, b)
. def f1 (b, c)
. def f1 (c, c)
. def f1 (b, b)
. def f1 (o, p)
. def f1 (p, o)
. def f1 (o, o)
. def f1 (p, p)
. def f2 (c, b)
. def f2 (b, c)
. def f2 (c, c)
. def f2 (b, b)
. def f2 (o, p)
. def f2 (p, o)
. def f2 (o, o)
. def f2 (p, p)
. def f3 (c, b)
. def f3 (b, c)
. def f3 (c, c)
. def f3 (b, b)
. def f3 (o, p)
. def f3 (p, o)
. def f3 (o, o)
. def f3 (p, p)
. def f4 (c, b)
. def f4 (b, c)
. def f4 (c, c)
. def f4 (b, b)
. def f4 (o, p)
. def f4 (p, o)
. def f4 (o, o)
. def f4 (p, p)
. def f5 (c, b)
. def f5 (b, c)
. def f5 (c, c)
. def f5 (b, b)
. def f5 (o, p)
. def f5 (p, o)
. def f5 (o, o)
. def f5 (p, p)
. def f6 (c, b)
. def f6 (b, c)
. def f6 (c, c)
. def f6 (b, b)
. def f6 (o, p)
. def f6 (p, o)
. def f6 (o, o)
. def f6 (p, p)
. def f7 (c, b)
. def f7 (b, c)
. def f7 (c, c)
. def f7 (b, b)
. def f7 (o, p)
. def f7 (p, o)
. def f7 (o, o)
. def f7 (p, p)
. def f8 (c, b)
. def f8 (b, c)
. def f8 (c, c)
. def f8 (b, b)
. def f8 (o, p)
. def f8 (p, o)
. def f8 (o, o)
. def f8 (p, p)