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
class Type
var t:Type
class TYPE < Type
type Pred __ : -Type -> Type; Unit:TYPE
class a, b, c
class a, b, c <d; a<b
type s:c
pred tt : s
var x : s
program tt = \x: s . ()
program __res__ (x: s, y: t) : s = x ;
fst (x: s, y: t) : s = x ;
snd (x: s, y: t) : t = y
pred eq : s * s
type s < ?s
program all (p: (?s)) : (?Unit) = eq(p, tt)
program And (x, y: (?Unit)) :(?Unit) = t1() res t2()
program __impl__ (x, y: (?Unit)) = eq(x, x And y)
program __or__ (x, y: (?Unit)) :(?Unit) = all(\r: (?Unit).
((x impl r) res (y impl r)) impl r)
; ex (p: (?s)) :(?Unit) = all(\r: (?Unit).
all(\x:s. p(x) impl r) impl r)
; ff () :(?Unit) = all(\r: (?Unit). r())
;
forall x: t; y : t
%(..)%
. x = y
%[% [ ] % %[
]%
%[ ]%
]%
%[ ]%
sort s
op a: (?s); %[ Should be: op a:?s ]%
type Data1 ::= a | b | c;
type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1
type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?
Data1)
type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:?Data1)?
axioms true ;forall x:s.e;
forall x:s.e