blob: e212f835dfc421ef5a19f08d0b331aae85a93cb4 (
plain)
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
|
(declare forall (! s sort
(! t (term s)
(! f formula
formula))))
(program eqterm ((n1 term) (n2 term)) bool
(do (markvar n1)
(let s (ifmarked n2 tt ff)
(do (markvar n1) s))))
(program is_inst_t ((ti term) (t term) (k term)) bool
(match t
((apply s1 s2 t1 t2)
(match ti
((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
(default ff)))
(default (eqterm ti (ifmarked t k t)))))
(program is_inst_f ((fi formula) (f formula) (k term)) bool
(match f
((and f1 f2) (match fi
((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((or f1 f2) (match fi
((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((impl f1 f2) (match fi
((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((not f1) (match fi
((not fi1) (is_inst_f fi1 f1 k))
(default ff)))
((iff f1 f2) (match fi
((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((xor f1 f2) (match fi
((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((ifte f1 f2 f3) (match fi
((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k)
(tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff)))
(ff ff)))
(default ff)))
((= s t1 t2) (match fi
((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
(default ff)))
((forall s t1 f1) (match fi
((forall s ti1 fi1) (is_inst_f fi1 f1 k))
(default ff)))
(default ff)))
(program is_inst ((fi formula) (f formula) (t term) (k term)) bool
(do (markvar t)
(let f1 (is_inst_f fi f k)
(do (markvar t) f1))))
(declare skolem
(! s sort
(! t (term s)
(! f formula
(! p (th_holds (not (forall s t f)))
(! u (! k (term s)
(! fi formula
(! p1 (th_holds (not fi))
(! r (^ (is_inst fi f t k) tt)
(holds cln)))))
(holds cln)))))))
(declare inst
(! s sort
(! t (term s)
(! f formula
(! k (term s)
(! fi formula
(! p (th_holds (forall s t f))
(! r (^ (is_inst fi f t k) tt)
(! u (! p1 (th_holds fi)
(holds cln))
(holds cln))))))))))
|
