blob: d4aad002d5506d85dea326a0950e0dba37f5ebe7 (
plain) (
blame)
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
|
%%% NAME/LOGIN-ID _____________________/______________________
%%% ACKNOWLEDGMENTS:
%%%
%%% ===============
%%% Predicate Logic - Propositional formulas involving quantifiers
%%% ===============
%%%
%%% Prove these using only (SPLIT), (FLATTEN), (INST) and (SKOLEM) commands
%%% ~~~~
th_B: THEORY
BEGIN
U: TYPE+ % Arbitrary nonempty type
a,b,c: U % Constants of type U
x,y,z: VAR U % Variables of type U
P,Q,R: [U -> bool] % Predicate names
B_0: LEMMA (FORALL x: P(x)) => P(a)
B_1: LEMMA ((FORALL x: P(x) => Q(x)) AND P(a)) => Q(a)
B_2: LEMMA (FORALL x: P(x)) => (EXISTS y: P(y))
B_3: LEMMA (FORALL x: P(x)) OR (EXISTS y: NOT P(y))
B_4: LEMMA NOT (FORALL x: P(x)) IFF (EXISTS x: NOT P(x))
B_5: LEMMA NOT (EXISTS x: P(x)) IFF (FORALL x: NOT P(x))
B_6: LEMMA (FORALL x: P(x)) AND (FORALL x: Q(x))
IFF (FORALL x: P(x) AND Q(x))
B_7: LEMMA (EXISTS x: P(x)) OR (EXISTS x: Q(x))
IFF (EXISTS x: P(x) OR Q(x))
END th_B
|
