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
(cl-text prop
(thisMustBeTrue)
(and (x) (b) (not (c)))
(or (d) (e) (not (f)))
)
(cl-text pred
(P y)
(Q h)
(P g h)
)
(cl-text quant
(forall (x y z) (and (P x) (P y) (not (P z))))
(exists (x) (P x))
)
(cl-text compact
(P g)
(Q P)
(forall (P) (P h))
)
(cl-text func
(= (F g) h)
(= g (G h i j))
(forall (H I) (= (H g) (I h i)))
(= ((J ((K g) h) i) j) k)
)
(cl-text comments
(cl-comment 'CommentedText' (and (x)
(cl-comment 'CommentedSentence' (b))
(= (F g) (cl-comment 'CommentedTerm' h))
)
)
)
(cl-text module1
(cl-module M (forall (a b) (and (P a) (Q b))))
)
(cl-text module2
(cl-module N (cl-excludes ex_a ex_b) (forall (a b) (and (P a) (Q b))))
)
(cl-text module3
(cl-module M1 (cl-excludes ex_a ex_b)
(cl-module M2 (cl-excludes ex_a ex_b)
(exists (a b) (= a b))
)
)
)