-
Notifications
You must be signed in to change notification settings - Fork 35
/
dtv20111209.clif
465 lines (362 loc) · 27 KB
/
dtv20111209.clif
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
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
(cl-text dtv20111209
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 overlaps time interval2" t1 t2)
(not ("time interval1 is before time interval2" t1 t2))))
(forall ((t1 "time interval") (t2 "time interval"))
(if (not ("time interval1 overlaps time interval2" t1 t2))
(or ("time interval1 is before time interval2" t1 t2)
("time interval1 is before time interval2" t2 t1))))
(forall ((t1 "time interval"))
(not ("time interval1 is before time interval2" t1 t1)))
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 is before time interval2" t1 t2)
(not ("time interval1 is before time interval2" t2 t1))))
(forall ((t1 "time interval") (t2 "time interval"))
(or (and ("time interval1 overlaps time interval2" t1 t2)
(not ("time interval1 is before time interval2" t1 t2))
(not ("time interval1 is before time interval2" t2 t1)))
(and ("time interval1 is before time interval2" t1 t2)
(not ("time interval1 overlaps time interval2" t1 t2))
(not ("time interval1 is before time interval2" t2 t1)))
(and ("time interval1 is before time interval2" t2 t1)
(not ("time interval1 overlaps time interval2" t1 t2))
(not ("time interval1 is before time interval2" t1 t2)))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(if (and ("time interval1 is before time interval2" t1 t2)
("time interval1 is before time interval2" t2 t3))
("time interval1 is before time interval2" t1 t3)))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 is properly before time interval2" t1 t2)
(and ("time interval1 is before time interval2" t1 t2)
(exists ((t3 "time interval"))
(and ("time interval1 is before time interval2" t1 t3)
("time interval1 is before time interval2" t3 t2))))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 equals time interval2" t1 t2)
(and ("time interval1 is part of time interval2" t1 t2)
("time interval1 is part of time interval2" t2 t1))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 meets time interval2" t1 t2)
(and ("time interval1 is before time interval2" t1 t2)
(not (exists ((t3 "time interval"))
(and ("time interval1 is before time interval2" t1 t3)
("time interval1 is before time interval2" t3 t2)))))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 properly overlaps time interval2" t1 t2)
(and ("time interval1 overlaps time interval2" t1 t2)
(exists ((t3 "time interval"))
(and ("time interval1 is proper part of time interval2" t3 t1)
("time interval1 is before time interval2" t3 t2))))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 is properly during time interval2" t1 t2)
(and ("time interval1 is proper part of time interval2" t1 t2)
(exists ((t3 "time interval") (t4 "time interval"))
(and ("time interval1 is proper part of time interval2" t3 t2)
("time interval1 is proper part of time interval2" t4 t2)
("time interval1 is before time interval2" t3 t1)
("time interval1 is before time interval2" t1 t4))))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 starts time interval2" t1 t2)
(and ("time interval1 is proper part of time interval2" t1 t2)
(not (exists ((t3 "time interval"))
(and ("time interval1 is proper part of time interval2" t3 t2)
("time interval1 is before time interval2" t3 t1)))))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 finishes time interval2" t1 t2)
(and ("time interval1 is proper part of time interval2" t1 t2)
(not (exists ((t3 "time interval"))
(and ("time interval1 is proper part of time interval2" t3 t2)
("time interval1 is before time interval2" t1 t3)))))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 precedes time interval2" t1 t2)
(or ("time interval1 is properly before time interval2" t1 t2)
("time interval1 meets time interval2" t1 t2))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 begins time interval2" t1 t2)
(or ("time interval1 equals time interval2" t1 t2)
("time interval1 meets time interval2" t1 t2)
("time interval1 properly overlaps time interval2" t1 t2)
("time interval1 starts time interval2" t1 t2))))
(forall ((t1 "time interval") (t2 "time interval"))
(iff ("time interval1 ends time interval2" t1 t2)
(or ("time interval1 equals time interval2" t1 t2)
("time interval1 meets time interval2" t2 t1)
("time interval1 properly overlaps time interval2" t1 t2)
("time interval1 finishes time interval2" t1 t2))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(iff ("time interval1 plus time interval2 is time interval3" t1 t2 t3)
(or (if (or ("time interval1 is before time interval2" t1 t2)
("time interval1 properly overlaps time interval2" t1 t2))
(and ("time interval1 starts time interval2" t1 t3)
("time interval1 finishes time interval2" t2 t3)))
(if (or ("time interval1 is before time interval2" t2 t1)
("time interval1 properly overlaps time interval2" t2 t1))
(and ("time interval1 starts time interval2" t2 t3)
("time interval1 finishes time interval2" t1 t3)))
(if ("time interval1 is part of time interval2" t1 t2)
(= t2 t3))
(if ("time interval1 is part of time interval2" t2 t1)
(= t1 t3)))))
(forall ((t1 "time interval") (t2 "time interval"))
(exists ((t3 "time interval"))
(and ("time interval1 plus time interval2 is time interval3" t1 t2 t3)
("time interval1 is part of time interval2" t1 t3)
("time interval1 is part of time interval2" t2 t3))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(if (and ("time interval1 is part of time interval2" t1 t3)
("time interval1 is part of time interval2" t2 t3))
("time interval1 is part of time interval2" ("time interval1 plus time interval2 is time interval3" t1 t2) t3)))
(forall ((t1 "time interval") (t2 "time interval"))
(exists ((t3 "time interval"))
(and ("time interval1 plus time interval2 is time interval3" t1 t2 t3)
(forall ((t4 "time interval"))
(if ("time interval1 plus time interval2 is time interval3" t1 t2 t4)
(= t4 t3))))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(iff ("time interval1 to time interval2 specifies time interval3" t1 t2 t3)
(or (and ("time interval1 is properly before time interval2" t1 t2)
(exists ((t4 "time interval"))
(and ("time interval1 meets time interval2" t4 t2)
("time interval1 meets time interval2" t1 t4)
("time interval1 plus time interval2 is time interval3" t1 t4 t3)))
(and ("time interval1 meets time interval2" t1 t2)
(= t1 t3))))))
(forall ((t1 "time interval") (t2 "time interval"))
(exists (t3 "time interval")
(iff ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
(if ("time interval1 starts time interval2" t1 t2)
(and ("time interval1 finishes time interval2" t3 t2)
("time interval1 meets time interval2" t1 t3))))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
(forall ((t4 "time interval"))
(if (and ("time interval1 is part of time interval2" t4 t2)
(not ("time interval1 overlaps time interval2" t4 t1)))
("time interval1 is part of time interval2" t4 t3)))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(if ("time interval1 starts time interval2" t1 t2)
(exists ((i integer))
(and (count ("time interval1 starts time interval2 complementing time interval3" t1 t2) i)
(= i 1)))))
(forall ((t1 "time interval") (t2 "time interval"))
(exists (t3 "time interval")
(iff ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
(if ("time interval1 finishes time interval2" t1 t2)
(and ("time interval1 starts time interval2" t3 t2)
("time interval1 meets time interval2" t3 t1))))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
(exists ((t4 "time interval"))
(if (and ("time interval1 is part of time interval2" t4 t2)
(not ("time interval1 overlaps time interval2" t4 t1)))
("time interval1 is part of time interval2" t4 t3)))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(if ("time interval1 finishes time interval2" t1 t2 t3)
(= 1 (count ("time interval1 finishes time interval2 complementing" t1 t2)))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval"))
(iff ("time interval1 intersects time interval2 with time interval3" t1 t2 t3)
(if ("time interval1 overlaps time interval2" t1 t2)
(and ("time interval1 finishes time interval2" t3 t1)
("time interval1 starts time interval2" t3 t2)))))
(forall ((t1 "time interval") (t2 "time interval") (t3 "time interval")(t4 "time interval"))
(if (and ("time interval1 intersects time interval2 with time interval3" t1 t2 t3)
("time interval1 is part of time interval2" t4 t1)
("time interval1 is part of time interval2" t4 t2))
("time interval1 is part of time interval2" t4 t3)))
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 overlaps time interval2" t1 t2)
(= 1 (count ("time interval1 intersects time interval2" t1 t2)))))
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 is properly before time interval2" t1 t2)
(exists ((t3 "time interval") (t4 "time interval") (t5 "time interval") (t6 "time interval"))
(and ("time interval1 meets time interval2" t1 t3)
("time interval1 meets time interval2" t3 t2)
("time interval1 plus time interval2 is time interval3" t1 t2 t4)
("time interval1 starts time interval2 complementing time interval3" t1 t4 t5)
("time interval1 finishes time interval2 complementing time interval3" t2 t4 t6)
("time interval1 intersects time interval2 with time interval3" t5 t6 t3)))))
(forall ((d1 duration))
(leq d1 d1))
(forall ((d1 duration) (d2 duration))
(or (leq d1 d2)
(leq d2 d1)))
(forall ((d1 duration) (d2 duration))
(if (and (leq d1 d2)
(leq d2 d1))
(= d1 d2)))
(forall ((d1 duration) (d2 duration) (d3 duration))
(if (and (leq d1 d2)
(leq d2 d3))
(leq d1 d3)))
(forall ((d1 duration) (d2 duration))
(iff (lt d1 d2)
(and (leq d1 d2)
(not (= d2 d1)))))
(forall ((d1 duration) (d2 duration) (d3 duration) (d4 duration))
(= (+ (+ d1 d2) d3) (+ d1 (+ d2 d3))))
(forall ((d1 duration) (d2 duration))
(= (+ d1 d2) (+ d2 d1)))
(forall ((d1 duration))
(exists ((d2 duration))
(= D0 (+ d1 d2))))
(forall ((n1 number) (d1 duration))
(exists ((d2 duration))
(mult n1 d1 d2)))
(forall ((d1 duration) (d2 duration) (n1 number))
(exists ((d3 duration))
(if (= d3 (mult n1 (+ d1 d2)))
(= d3 (+ (mult n1 d1) (mult n1 d2))))))
(forall ((d1 duration) (n1 number) (n2 number))
(= (mult (+ n1 n2) d1) (+ (mult n1 d1) (mult n2 d1))))
(forall ((d1 duration))
(mult 0 d1 D0))
(forall ((n1 number) (d1 duration))
(exists ((d2 duration))
(iff (= D0 (* n1 d1))
(or (= n1 0)
(= d1 D0)))))
(forall ((d1 duration))
(if (not (= d1 D0))
(exists ((d2 duration) (n1 number))
(= (mult d1 n1) d2))))
(forall ((t "time interval") (d1 duration) (d2 duration))
(if (and ("time interval has duration" t d1)
("time interval has duration" t d2))
(= d1 d2)))
(forall ((t "time interval"))
(gt ("duration of" t) D0))
(forall ((t "time interval"))
(not (= ("duration of" t) D0)))
(forall ((t "time interval"))
(not (= D0 (- (D0 t)))))
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 is part of time interval2" t1 t2)
(leq ("duration of time interval" t1) ("duration of time interval" t2))))
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 meets time interval2" t1 t2)
(exists ((t3 "time interval") (d3 duration))
(and ("time interval3 equals time interval1 plus time interval2" t3 t1 t2)
("duration3 equals duration1 plus duration2" d3 ("duration of" t1) ("duration of" t2))
(= d3 ("duration of" t3))))))
(forall ((t1 "time interval") (t2 "time interval"))
(exists ((t3 "time interval"))
(if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
(= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))))))
(forall ((t1 "time interval") (t2 "time interval"))
(exists ((t3 "time interval"))
(if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
(= ("duration of" t3) (- ("duration of" t2) ("duration of" t1))))))
(forall ((o occurrence) (t "time interval"))
(iff ("occurrence occurs within time interval" o t)
(exists ((t2 "time interval"))
(and ("time interval1 is part of time interval2" t2 t)
("occurrence occurs throughout time interval" o t2)))))
(forall ((o occurrence) (t "time interval"))
(iff ("occurrence occurs for time interval" o t)
(and ("occurrence occurs throughout time interval" o t)
(exists ((t2 "time interval"))
(and ("time interval1 meets time interval2" t2 t)
(not ("occurrence occurs within time interval" o t2))))
(exists ((t3 "time interval"))
(and ("time interval1 meets time interval2" t t3)
(not ("occurrence occurs within time interval" o t3)))))))
(forall ((o occurrence) (d duration))
(iff ("occurrence lasts for duration" o d)
(exists ((t "time interval"))
(and ("occurrence occurs for time interval" o t)
("time interval has duration" t d)))))
(forall ((o1 occurrence) (o2 occurrence))
(iff ("occurrence1 precedes occurrence2" o1 o2)
(forall ((t1 "time interval") (t2 "time interval"))
(if (and ("situation model occurs for time interval" o1 t1)
("situation model occurs for time interval" o2 t2))
("time interval1 precedes time interval2" t1 t2)))))
(forall ((o1 occurrence) (o2 occurrence) (o3 occurrence))
(if (and ("occurrence1 precedes occurrence2" o1 o2)
("occurrence1 precedes occurrence2" o2 o3))
("occurrence1 precedes occurrence2" o1 o3)))
(forall ((o1 occurrence) (o2 occurrence))
(iff ("occurrence1 starts before occurrence2" o1 o2)
(forall ((t1 "time interval") (t2 "time interval"))
(if (and ("situation model occurs for time interval" o1 t1)
("situation model occurs for time interval" o2 t2))
("time interval1 starts before time interval2" t1 t2)))))
(forall ((o1 occurrence) (o2 occurrence))
(iff ("occurrence1 ends before occurrence2" o1 o2)
(forall ((t1 "time interval") (t2 "time interval"))
(if (and ("situation model occurs for time interval" o1 t1)
("situation model occurs for time interval" o2 t2))
("time interval1 ends before time interval2" t1 t2)))))
(forall ((s1 "situation model") (s2 "situation model"))
(iff ("situation model1 precedes situation model2" s1 s2)
(forall ((o1 occurrence) (o2 occurrence))
(if (and ("situation model has occurrence" s1 o1)
("situation model has occurrence" s2 o2))
("occurrence1 precedes occurrence2" o1 o2)))))
(forall ((s1 "situation model") (s2 "situation model"))
(iff ("situation model1 starts before situation model2" s1 s2)
(forall ((o1 occurrence) (o2 occurrence))
(if (and ("situation model has occurrence" s1 o1)
("situation model has occurrence" s2 o2))
("occurrence1 starts before occurrence2" o1 o2)))))
(forall ((s1 "situation model") (s2 "situation model"))
(iff ("situation model1 ends before situation model2" s1 s2)
(forall ((o1 occurrence) (o2 occurrence))
(if (and ("situation model has occurrence" s1 o1)
("situation model has occurrence" s2 o2))
("occurrence1 ends before occurrence2" o1 o2)))))
(forall (s schedule) (and (exists ((g "general situation model") (tt "time table")) (and ("schedule is for general situation model" s g) ("schedule has time table" s tt) (set s) (forall ((i thing)) (if ("set has element" s i) (and ("individual situation model" i) ("refinement refines situation model" i g) (exists ((te "table entry")) (and ("time table has table entry" tt te) ("situation model occurs for time interval" i te))) )))))))
(forall ((s "schedule") (tt "time table")) (iff ("schedule has time table" s tt) (forall (ti "time interval") (and ("time table has table entry" tt ti) (exists ((i "individual occurrence")) (and ("set has member" s i) ("individual situation model occurs over time interval" i ti)))))))
(forall ((s "schedule") (span "time interval")) (iff ("schedule has time span" s span) (and (forall ((tt "time table") (ti "time interval")) (if (and ("schedule has time table" s tt) ("time table has time table period" tt ti)) (= span ti))))))
(exists ((s sequence)) (exists ((i1 index) (sp1 "sequence position") (i2 index) (sp2 "sequence position")) (if (and ("sequence has sequence position" s sp1) ("sequence has sequence position" s sp2) ("sequence position has index" sp1 i1) ("sequence position has index" sp2 i2) (= i1 i2)) (= sp1 sp2))))
(forall ((s "sequence position") (nsp "sequence position") (sp "sequence position")) (iff ("next sequence position succeeds sequence position" nsp sp) (exists ((sp2 "sequence position") (ni index) (i2 index)) (and ("sequence position1 precedes sequence position2" sp nsp) ("sequence position1 precedes sequence position2" sp sp2) ("sequence position has index" nsp ni) ("sequence position has index" sp3 i2) (<= ni i2)))))
(forall ((s sequence) (member thing)) (iff ("sequence has member" s member) (exists ((sp "sequence position")) (and ("sequence has sequence position" s sp) ("sequence position has member" sp m)))))
(forall ((s sequence) (index integer) (member thing)) (iff ("member has index in sequence" member index s) (exists ((sp "sequence position")) (and ("sequence has sequence position" s sp) ("sequence position has index" sp index) ("sequence position has member" sp member)))))
(forall ((s sequence) (index integer) (member thing)) (iff ("index of member in sequence" index member s) (exists ((sp "sequence position")) (if (and ("sequence has sequence position" s sp) ("sequence position has member" sp member)) ("sequence position has index" sp index) ))))
(forall ((s sequence) (index integer) (member thing)) (iff ("member with index in sequence " member index s) (exists ((sp "sequence position")) (if (and ("sequence has sequence position" s sp) ("sequence position has index" sp index)) ("sequence position has member" sp member)))))
(forall ((member thing) (s sequence)) (exists ((c concept)) (iff ("sequence is of concept" s c) (if ("member participates in sequence" member s) ("concept corresponds to instance" c member)))))
(forall ((s sequence) (p "index order position")) (iff ("sequence has index order position" s p) (exists ((i1 index) (i2 index)) (and ("sequence position has index" p i1) ("sequence has index origin value" s i2) (= i1 i2)))))
(forall ((s sequence)) (iff ("consecutive sequence" s) (forall ((sp1 "sequence position")) (if (and ("sequence has sequence position" s sp1) (not (exists ((first "sequence position")) (and ("sequence has first position" s first) (= sp1 first)))) ) (exists ((sp2 "sequence position") (i1 index) (i2 index)) (and ("sequence is next after sequence position" sp1 sp2) ("sequence position has index" sp1 i1) ("sequence position has index" sp2 i2) (= (+ 1 i1) i2)))))))
(forall ((s sequence)) (iff ("unique sequence" s) (forall ((member thing) (sp1 "sequence position") (sp2 "sequence position")) (if (and ("sequence has sequence position" s sp1) ("sequence has sequence position" s sp2) ("sequence position has element" sp1 member) ("sequence position has element" sp2 member)) (= sp1 sp2)))))
(forall (s sequence) (iff ("regular sequence" s) (and ("consecutive sequence" s) ("unique sequence" s))))
(forall ((s sequence)(m1 thing)(m2 thing)) (iff ("member1 precedes member2 in unique sequence" m1 m2 s) (and ("member participates in sequence" m1 s) ("member participates in sequence" m2 s) (forall ((sp1 "sequence position") (sp2 "sequence position")) (if (and ("sequence position of member" sp1 m1) ("sequence position of member" sp2 m2)) ("sequence position1 precedes sequence position2" sp1 sp2))))))
(forall ((s "finite sequence") (m thing)) (iff ("sequence has first member" s m) (exists (first "sequence position") (and ("sequence has first position" s first) ("sequence position has member" first m)))))
(forall ((s sequence) (m thing)) (iff ("sequence has last member" s m) (exists (last "sequence position") (and ("sequence has last position" s last) ("sequence position has member" last m)))))
(forall ((s "sequence") (nm thing) (m thing)) (iff ("next member is next after thing in unique sequence" nm m s) (exists (sp "sequence position") (and ("sequence has sequence position" s sp) ("sequence position has member" sp m) (forall (sp2 "sequence position") (if (and ("sequence has sequence position" s sp2) ("sequence position has member" sp2 m)) (= sp2 sp))) (exists (np "sequence position") (and ("sequence has sequence position" s np) ("next sequence position succeeds sequence position" np sp) ("sequence position has element" np nm))) ))))
(forall ((s sequence) (last thing)) (if ("sequence has last member" s last) (not (exists (m thing) ("member is next after thing in sequence" m last s)))))
(forall ((s "unique sequence") (m thing)) (if (and ("element participates in sequence" m s) (not (exists (nm thing) ("next member is next after thing in sequence" nm m s)))) ("sequence has last member" s m)))
(forall ((s sequence) (pm thing) (m thing)) (iff ("previous member is just before thing in unique sequence" pm m s) (exists (sp "sequence position") (and ("sequence has sequence position" s sp) ("sequence position has member" sp m) (forall (sp2 "sequence position") (if (and ("sequence has sequence position" s sp2) ("sequence position has member" sp2 m)) (= sp2 sp))) (exists (pp "sequence position") (and ("sequence has sequence position" s pp) ("next sequence position succeeds sequence position" sp pp) ("sequence position has element" pp pm))) ))))
(forall ((s sequence) (first thing)) (if ("sequence has first member" s first) (not (exists (m thing) ("member is just before thing in sequence" m first s)))))
(forall ((s "unique sequence") (m thing)) (if (and ("element participates in sequence" m s) (not (exists (pm thing) ("previous member is just before thing in sequence" pm m s)))) ("sequence has first member" s m)))
(forall ((quantity quantity)) (= (count ("quantity has quantity kind" quantity)) 1))
(forall (("system of units" "system of units")) (= (count ("system of units is for system of quantities" "system of units")) 1))
(forall ((thing thing)) (iff ("quantity value"(thing)) (or ("atomic quantity value"(thing)) ("compound quantity value"(thing)))))
(forall (("atomic quantity value 1" "atomic quantity value") ("atomic quantity value 2" "atomic quantity value") ("measurement unit" "measurement unit")) (iff (converted "atomic quantity value 1" "atomic quantity value 2" "measurement unit") (exists ((quantity quantity) ("measurement unit 2" "measurement unit")) (and ("quantity value has measurement unit" "atomic quantity value 2" "measurement unit 2") (= "measurement unit" "measurement unit 2") (= "atomic value 1" quantity) (= "atomic value 2" quantity)))))
(forall (("atomic quantity value 2" "atomic quantity value") ("measurement unit" "measurement unit")) (= (count ("atomic quantity value1 is atomic quantity value2 converted to measurement unit" "atomic quantity value 2" "measurement unit")) 1))
(forall (("compound quantity value" "compound quantity value")) (>= (count ("compound quantity value has atomic quantity value" "compound quantity value")) 2))
(forall (("compound quantity value" "compound quantity value") ("atomic quantity value" "atomic quantity value")) (iff ("is equivalent to" "compound quantity value" "atomic quantity value") (forall ("atomic quantity value 1" "atomic quantity value") (exists (("quantity 1" quantity) ("quantity 2" quantity) ("quantity kind 1" "quantity kind") ("quantity kind 2" "quantity kind")) (and ("compound quantity value has atomic quantity value" "compound quantity value" "atomic quantity value 1") ("quantity value quantifies quantity" "atomic quantity value 1" "quantity 1") ("quantity has quantity kind" "quantity 1" "quantity kind 1") ("quantity value quantifies quantity" "atomic quantity value" "quantity 2") ("quantity has quantity kind" "quantity 2" "quantity kind 2") (= "quantity kind 1" "quantity kind 2"))))))
(forall ((part thing))
("part of" part part))
(forall ((part thing) (whole thing))
(if (and ("part of" part whole)
("part of" whole part))
(= part whole)))
(forall ((part thing) (whole thing) (part3 thing))
(if (and ("part of" part whole)
("part of" whole part3))
("part of" part part3)))
(forall ((part1 thing) (part2 thing))
(iff (overlaps part1 part2)
(exists ((part3 thing))
(and ("part of" part3 part1)
("part of" part3 part2)))))
(forall ((whole thing) (part thing))
(iff ("proper part" part whole)
(and ("part of" part whole)
(not ("part of" whole part)))))
(forall ((part1 thing) (whole thing))
(if ("proper part" part1 whole)
(exists ((part2 thing))
(and ("proper part" part2 whole)
(not (overlaps part2 part1))))))
)