1 % Heinrich Heine Universitaet Duesseldorf
2 % (c) 2025-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(test_sequent_prover,[]).
6
7 :- use_module(probsrc(module_information),[module_info/2]).
8 :- module_info(group,sequent_prover).
9 :- module_info(description,'This module provides tests for the sequent prover.').
10
11 :- use_module(probsrc(self_check)).
12
13 % % %
14
15 % e.g. for simple rewriting of expression, types are ignored
16
17 test_simp_rule(Rule,Hyp,NewHyp) :-
18 ? sequent_prover_trans(simplify_hyp(Rule,_),[Hyp],[NewHyp]).
19
20 test_simp_rule_with_hyps(Rule,Hyps,Hyp,NewHyp) :-
21 ? sequent_prover_trans(simplify_hyp(Rule,_),[Hyp|Hyps],NewHyps),
22 ? member(NewHyp,NewHyps),
23 \+ member(NewHyp,Hyps).
24
25 test_transition_new_hyp(Rule,Hyps,Goal,NewHyp) :-
26 ? sequent_prover_trans(Rule,Hyps,Goal,NewHyps),
27 ? member(NewHyp,NewHyps),
28 \+ member(NewHyp,Hyps).
29
30 test_transition_r(Rule,Hyps,Goal,NewGoal) :-
31 ? sequent_prover_trans(Rule,Hyps,Goal,Hyps,NewGoal).
32
33 % % %
34
35 % when types / info about existing identifiers are important
36
37 test_simp_rule_with_types(Rule,Hyps,Hyp,NewHyp) :-
38 ? sequent_prover_trans_with_types(simplify_hyp(Rule,_),[Hyp|Hyps],NewHyps),
39 ? member(NewHyp,NewHyps),
40 \+ member(NewHyp,Hyps).
41
42 test_transition_with_types_r(Rule,Hyps,Goal,NewGoal) :-
43 ? sequent_prover_trans_with_types(Rule,Hyps,Goal,Hyps,NewGoal).
44
45 test_transition_with_types_l(Rule,Hyps,Hyp,NewHyp) :-
46 ? sequent_prover_trans_with_types(Rule,[Hyp|Hyps],NewHyps),
47 ? member(NewHyp,NewHyps),
48 \+ member(NewHyp,Hyps).
49
50 % % %
51
52 sequent_prover_axiom(Rule,Hyps,Goal) :-
53 ? sequent_prover:sequent_prover_trans_start(Rule,state(sequent(Hyps,Goal,success),[]),state(success,_)).
54
55 ?sequent_prover_trans(Rule,Hyps,NewHyps) :- sequent_prover_trans(Rule,Hyps,truth,NewHyps).
56 ?sequent_prover_trans(Rule,Hyps,Goal,NewHyps) :- sequent_prover_trans(Rule,Hyps,Goal,NewHyps,Goal).
57 sequent_prover_trans(Rule,Hyps,Goal,NewHyps,NewGoal) :-
58 ? sequent_prover:sequent_prover_trans_desc(Rule,state(sequent(Hyps,Goal,success),[]),state(sequent(NewHyps,NewGoal,success),_),_) ;
59 ? sequent_prover:sequent_prover_trans(Rule,state(sequent(Hyps,Goal,success),[]),state(sequent(NewHyps,NewGoal,success),_)).
60
61 ?sequent_prover_trans_with_types(Rule,Hyps,NewHyps) :- sequent_prover_trans_with_types(Rule,Hyps,truth,NewHyps).
62 ?sequent_prover_trans_with_types(Rule,Hyps,Goal,NewHyps) :- sequent_prover_trans_with_types(Rule,Hyps,Goal,NewHyps,Goal).
63 sequent_prover_trans_with_types(Rule,Hyps,Goal,NewHyps,NewGoal) :-
64 ? sequent_prover:sequent_prover_trans_start(Rule,state(sequent(Hyps,Goal,success),[]),state(sequent(NewHyps,NewGoal,success),_)) ;
65 ? sequent_prover:sequent_prover_trans_start_desc(Rule,state(sequent(Hyps,Goal,success),[]),state(sequent(NewHyps,NewGoal,success),_),_).
66
67 % % %
68
69 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_AND_BTRUE',conjunct(truth,'$'(v)),R), R='$'(v) )).
70 :- assert_must_succeed((test_simp_rule('SIMP_SPECIAL_AND_BTRUE',conjunct(truth,conjunct('$'(v),truth)),R),
71 R=conjunct('$'(v),truth) )).
72 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_AND_BFALSE',conjunct(conjunct('$'(v),'$'(v)),falsity),R),
73 R=falsity)).
74 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND',conjunct(conjunct('$'(v),'$'(w)),'$'(w)),R),
75 R=conjunct('$'(v),'$'(w)) )).
76 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND',conjunct('$'(v),'$'(v)),R), R='$'(v) )).
77 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND',conjunct(conjunct(conjunct('$'(v),'$'(u)),'$'(u)),'$'(u)),R),
78 R=conjunct('$'(v),'$'(u)) )).
79 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND_NOT',conjunct(conjunct(negation('$'(v)),'$'(w)),'$'(v)),R), R=falsity )).
80 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_AND_NOT',conjunct(negation(equal('$'(w),'$'(v))),equal('$'(v),'$'(w))),R),
81 R=falsity )).
82 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OR_BTRUE',disjunct(disjunct('$'(w),truth),'$'(v)),R), R=truth )).
83 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OR_BFALSE',disjunct(disjunct(falsity,'$'(v)),falsity),R),
84 R=disjunct('$'(v),falsity) )).
85 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_OR',disjunct('$'(v),'$'(v)),R), R='$'(v))).
86 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_OR_NOT',disjunct('$'(v),negation('$'(v))),R), R=truth)).
87 :- assert_must_succeed(( test_simp_rule('Evaluate tautology',implication(not_equal('$'(w),'$'(v)),truth),R),
88 R=truth )). % SIMP_SPECIAL_IMP_BTRUE_R
89 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_IMP_BTRUE_L',implication(truth,not_equal('$'(w),'$'(v))),R),
90 R=not_equal('$'(w),'$'(v)) )).
91 :- assert_must_succeed(( test_simp_rule('Evaluate tautology',implication(equal('$'(v),'$'(w)),equal('$'(w),'$'(v))),R),
92 R=truth )). % SIMP_MULTI_IMP
93 :- assert_must_succeed(( test_simp_rule('Propagate negation',negation(less_equal('$'(v),'$'(w))),R),
94 R=greater('$'(v),'$'(w)) )). % SIMP_NOT_LE
95 :- assert_must_succeed(( test_simp_rule('DISTRI_NOT_AND',negation(conjunct('$'(v),'$'(w))),R),
96 R==disjunct(negation('$'(v)),negation('$'(w))))).
97 :- assert_must_succeed(( test_simp_rule('DISTRI_NOT_AND',negation(conjunct(conjunct('$'(u),'$'(v)),'$'(w))),R),
98 R==disjunct(disjunct(negation('$'(u)),negation('$'(v))),negation('$'(w))))).
99 :- assert_must_succeed(( test_simp_rule('DERIV_NOT_IMP',negation(implication('$'(u),'$'(v))),R),
100 R==conjunct('$'(u),negation('$'(v))))).
101 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_NOT_EQUAL_FALSE',negation(equal(boolean_false,'$'(e))),R),
102 R=equal('$'(e),boolean_true))). % SIMP_SPECIAL_NOT_EQUAL_FALSE_L
103 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_NOT_EQUAL_TRUE',negation(equal('$'(e),boolean_true)),R),
104 R=equal('$'(e),boolean_false))). % SIMP_SPECIAL_NOT_EQUAL_TRUE_R
105 :- assert_must_succeed(( test_simp_rule('SIMP_FORALL_AND',
106 forall(['$'(x)],member('$'(x),natural1_set),conjunct(greater('$'(x),0),not_equal('$'(x),'$'(y)))),R),
107 R=conjunct(forall(['$'(x)],member('$'(x),natural1_set),greater('$'(x),0)),forall(['$'(x)],member('$'(x),natural1_set),not_equal('$'(x),'$'(y)))))).
108 :- assert_must_succeed(( test_simp_rule('SIMP_FORALL_AND',forall(['$'(x),'$'(y)],'$'(p),conjunct(conjunct('$'(v),'$'(w)),'$'(u))),R),
109 R=conjunct(conjunct(forall(['$'(x),'$'(y)],'$'(p),'$'(v)),forall(['$'(x),'$'(y)],'$'(p),'$'(w))),forall(['$'(x),'$'(y)],'$'(p),'$'(u))) )).
110 :- assert_must_succeed(( test_simp_rule('SIMP_EXISTS_OR',exists(['$'(x)],disjunct('$'(p),'$'(q))),R),
111 R=disjunct(exists(['$'(x)],'$'(p)),exists(['$'(x)],'$'(q))) )).
112 :- assert_must_succeed(( test_simp_rule('SIMP_FORALL',forall(['$'(x),'$'(y)],greater('$'(x),0),'$'(q)),R),
113 R=forall(['$'(x)],greater('$'(x),0),'$'(q)) )).
114 :- assert_must_succeed(( test_simp_rule('SIMP_FORALL',forall(['$'(y),'$'(z),'$'(x)],greater('$'(x),0),'$'(q)),R),
115 R=forall(['$'(x)],greater('$'(x),0),'$'(q)) )).
116 :- assert_must_succeed(( test_simp_rule('SIMP_FORALL',forall(['$'(y),'$'(z),'$'(x)],disjunct(greater('$'(x),0),greater('$'(y),0)),'$'(q)),R),
117 R=forall(['$'(y),'$'(x)],disjunct(greater('$'(x),0),greater('$'(y),0)),'$'(q)) )).
118 :- assert_must_succeed(( test_simp_rule('SIMP_EQUAL_MAPSTO',equal(couple('$'(e),'$'(f)),couple('$'(g),'$'(h))),R),
119 R=conjunct(equal('$'(e),'$'(g)),equal('$'(f),'$'(h))) )).
120 :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_IN',event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),'$'(s))),R),R='$'(s) )).
121 :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_IN',
122 event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),member(couple('$'(x),'$'(y)),'$'(s))),R),R='$'(s) )).
123 :- assert_must_fail( test_simp_rule('SIMP_COMPSET_IN',
124 event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),set_extension(['$'(w),'$'(x),'$'(y)]))),_) ).
125 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_SUBSETEQ',subset('$'(s),bool_set),R),R=truth )).
126 :- assert_must_succeed((test_simp_rule('Evaluate tautology',subset(set_extension(['$'(red),'$'(blu)]),set_extension(['$'(blu),'$'(red)])),R),
127 R=truth )). % SIMP_MULTI_SUBSETEQ
128 :- assert_must_succeed(( test_simp_rule('DERIV_SUBSETEQ_BUNION',subset(union(union('$'(r),'$'(b)),'$'(p)),'$'(c)),R),
129 R=conjunct(conjunct(subset('$'(r),'$'(c)),subset('$'(b),'$'(c))),subset('$'(p),'$'(c))) )).
130 :- assert_must_succeed(( test_simp_rule('DERIV_SUBSETEQ_BINTER',subset('$'(c),intersection('$'(a),'$'(b))),R),
131 R=conjunct(subset('$'(c),'$'(a)),subset('$'(c),'$'(b))) )).
132 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_SETENUM',set_extension(['$'(a),'$'(a),'$'(b),'$'(b)]),R),
133 R=set_extension(['$'(a),'$'(b)]) )).
134 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_BINTER',intersection('$'(a),intersection(empty_set,'$'(w))),R), R=empty_set)).
135 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_BINTER',intersection('$'(a),intersection('INTEGER','$'(b))),R),
136 R=intersection('$'(a),'$'(b)) )).
137 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_BUNION',union('$'(a),union(pow_subset(bool_set),'$'(b))),R),
138 R=pow_subset(bool_set))).
139 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_SETMINUS',set_subtraction('$'(s),cartesian_product(bool_set,bool_set)),R),
140 R=empty_set)).
141 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_SETMINUS_SETMINUS',
142 set_subtraction(bool_set,set_subtraction(bool_set,'$'(s))),R), R='$'(s))).
143 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_CPROD',cartesian_product('$'(s),empty_set),R), R=empty_set )).
144 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_CPROD',cartesian_product(cartesian_product('$'(t),'$'(s)),empty_set),R),
145 R=empty_set)). % SIMP_SPECIAL_CPROD_R, SIMP_SPECIAL_CPROD_L
146 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OVERL',overwrite(empty_set,'$'(t)),R), R='$'(t) )).
147 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OVERL',overwrite(overwrite('$'(t),'$'(s)),empty_set),R),
148 R=overwrite('$'(t),'$'(s)) )).
149 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_OVERL',overwrite(overwrite(empty_set,'$'(t)),'$'(s)),R),
150 R=overwrite('$'(t),'$'(s)) )).
151 :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_BUNION',finite(union('$'(s),'$'(t))),R), R=conjunct(finite('$'(s)),finite('$'(t))) )).
152 :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_CONVERSE',finite(reverse(set_extension([couple(1,2)]))),R),
153 R=finite(set_extension([couple(1,2)])) )).
154 :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_ID_DOMRES',finite(domain_restriction('$'(e),event_b_identity)),R),
155 R=finite('$'(e)) )).
156 :- assert_must_succeed(( test_simp_rule('DEF_OR',disjunct(disjunct(disjunct('$'(q),'$'(s)),'$'(r)),'$'(t)),R),
157 R=implication(negation('$'(q)),disjunct(disjunct('$'(s),'$'(r)),'$'(t))) )).
158 :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_NATURAL',disjunct('$'(p),finite(natural_set)),R),
159 R=disjunct('$'(p),falsity))). % subterm
160 :- assert_must_succeed(( test_simp_rule('DEF_IN_MAPSTO',member(couple('$'(a),'$'(b)),cartesian_product('$'(n),'$'(m))),R),
161 R=conjunct(member('$'(a),'$'(n)),member('$'(b),'$'(m))) )).
162 :- assert_must_succeed(( test_simp_rule('DEF_IN_MAPSTO',
163 member(couple(couple('$'(a),'$'(b)),'$'(c)),cartesian_product(cartesian_product('$'(n),'$'(m)),'$'(o))),R),
164 R=conjunct(member(couple('$'(a),'$'(b)),cartesian_product('$'(n),'$'(m))),member('$'(c),'$'(o))) )).
165 :- assert_must_succeed(( test_simp_rule('DEF_IN_POW',member(set_extension(['$'(a)]),pow_subset(natural1_set)),R),
166 R=subset(set_extension(['$'(a)]),natural1_set) )).
167 :- assert_must_succeed(( test_simp_rule('DEF_IN_POW1',member(set_extension(['$'(a)]),pow1_subset(natural1_set)),R),
168 R=conjunct(member(set_extension(['$'(a)]),pow_subset(natural1_set)),not_equal(natural1_set,empty_set)) )).
169 :- assert_must_succeed(( test_simp_rule('DEF_SUBSETEQ',subset('$'(s),'$'(t)),R),
170 R=forall(['$'(x)],member('$'(x),'$'(s)),member('$'(x),'$'(t))) )).
171 :- assert_must_succeed(( test_simp_rule('DEF_SUBSETEQ',subset(set_extension(['$'(x)]),'$'(y)),R),
172 R=forall(['$'(z)],member('$'(z),set_extension(['$'(x)])),member('$'(z),'$'(y))) )). % new identifier
173 :- assert_must_succeed(( test_simp_rule('DEF_IN_BUNION',member('$'(e),union('$'(x),'$'(y))),R),
174 R=disjunct(member('$'(e),'$'(x)),member('$'(e),'$'(y))) )).
175 :- assert_must_succeed(( test_simp_rule('DEF_IN_BINTER',member('$'(e),intersection('$'(x),intersection('$'(y),'$'(z)))),R),
176 R=conjunct(member('$'(e),'$'(x)),conjunct(member('$'(e),'$'(y)),member('$'(e),'$'(z)))) )).
177 :- assert_must_succeed(( test_simp_rule('DEF_IN_SETMINUS',member('$'(e),set_subtraction(set_extension(['$'(x)]),'$'(y))),R),
178 R=conjunct(member('$'(e),set_extension(['$'(x)])),negation(member('$'(e),'$'(y)))) )).
179 :- assert_must_succeed(( test_simp_rule('DEF_IN_SETENUM',member('$'(e),set_extension([1,2,3])),R),
180 R=disjunct(disjunct(equal('$'(e),1),equal('$'(e),2)),equal('$'(e),3)) )).
181 :- assert_must_succeed(( test_simp_rule('DEF_IN_KUNION',member(22,general_union('$'(s))),R),
182 R=exists(['$'(x)],conjunct(member('$'(x),'$'(s)),member(22,'$'(x)))) )).
183 :- assert_must_succeed(( test_simp_rule('DEF_IN_KUNION',member(23,general_union('$'(x))),R),
184 R=exists(['$'(y)],conjunct(member('$'(y),'$'(x)),member(23,'$'(y)))) )).
185 :- assert_must_succeed(( test_simp_rule('DEF_SPECIAL_NOT_EQUAL',not_equal(empty_set,'$'(s)),R),R=exists([X],member(X,'$'(s))) )).
186 :- assert_must_succeed(( test_simp_rule('DEF_SPECIAL_NOT_EQUAL',negation(equal('$'(s),empty_set)),R),R=exists([X],member(X,'$'(s))) )).
187 :- assert_must_succeed(( test_simp_rule('DEF_SPECIAL_NOT_EQUAL',negation(subset('$'(s),empty_set)),R),R=exists([X],member(X,'$'(s))) )).
188 :- assert_must_succeed(( test_simp_rule('DERIV_SUBSETEQ_SETMINUS_L',subset(set_subtraction('$'(a),'$'(s)),'$'(t)),R),
189 R=subset('$'(a),union('$'(s),'$'(t))) )).
190 :- assert_must_succeed(( test_simp_rule('SIMP_DOM_SETENUM',domain(set_extension([couple(1,2),couple(2,3)])),R),
191 R=set_extension([1,2]) )).
192 :- assert_must_succeed(( test_simp_rule('SIMP_DOM_SETENUM',domain(set_extension([couple(1,2),couple(1,3)])),R),
193 R=set_extension([1]) )).
194 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_OVERL_CPROD',overwrite(overwrite(overwrite('$'(r),'$'(s)),bool_set),'$'(t)),R),
195 R=overwrite(bool_set,'$'(t)) )).
196 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_OVERL_CPROD',overwrite(overwrite(overwrite('$'(t),'$'(s)),'$'(r)),bool_set),R),
197 R=bool_set )).
198 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_OVERL_CPROD',overwrite(overwrite(overwrite(bool_set,'$'(s)),bool_set),'$'(r)),R),
199 R=overwrite(bool_set,'$'(r)) )).
200 :- assert_must_succeed(( test_simp_rule('SIMP_DPROD_CPROD',
201 direct_product(cartesian_product('$'(a),'$'(b)),cartesian_product('$'(c),'$'(d))),R),
202 R=cartesian_product(intersection('$'(a),'$'(c)),cartesian_product('$'(b),'$'(d))) )).
203 :- assert_must_succeed(( test_simp_rule('SIMP_PPROD_CPROD',
204 parallel_product(cartesian_product('$'(s),'$'(t)),cartesian_product('$'(u),'$'(v))),R),
205 R=cartesian_product(cartesian_product('$'(s),'$'(u)),cartesian_product('$'(t),'$'(v))) )).
206 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_RELIMAGE_CPROD_SING',
207 image(cartesian_product(set_extension(['$'(e)]),'$'(s)),set_extension(['$'(e)])),R),R='$'(s) )).
208 :- assert_must_succeed(( test_simp_rule('SIMP_CONVERSE_SETENUM',
209 reverse(set_extension([couple('$'(a),'$'(b)),couple('$'(c),'$'(d))])),R),
210 R=set_extension([couple('$'(b),'$'(a)),couple('$'(d),'$'(c))]) )).
211 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_REL_R',partial_function('$'(s),empty_set),R),R=set_extension([empty_set]) )).
212 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_REL_R',surjection_relation('$'(s),empty_set),R),
213 R=set_extension([empty_set]) )).
214 :- assert_must_fail( test_simp_rule('SIMP_SPECIAL_REL_R',total_relation('$'(s),empty_set),_) ).
215 :- assert_must_succeed(( test_simp_rule('SIMP_DOM_LAMBDA',
216 domain(event_b_comprehension_set(['$'(x),'$'(y)],couple(add('$'(x),'$'(x)),'$'(y)),member(couple('$'(x),'$'(y)),'$'(p)))),R),
217 R=event_b_comprehension_set(['$'(x),'$'(y)],add('$'(x),'$'(x)),member(couple('$'(x),'$'(y)),'$'(p))) )).
218 :- assert_must_fail( test_simp_rule('SIMP_DOM_LAMBDA',
219 domain(event_b_comprehension_set(['$'(x),'$'(y)],add('$'(x),'$'(x)),member(couple('$'(x),'$'(y)),'$'(p)))),_) ).
220 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LL',function(set_extension([couple('$'(a),1)]),'$'(x)),R),
221 R=1)).
222 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LL',
223 function(set_extension([couple(1,1),couple(2,1),couple(3,1)]),1),R),R=1 )).
224 :- assert_must_fail( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LL',
225 function(set_extension([couple(1,1),couple(2,2),couple(3,1)]),1),_) ).
226 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LR',
227 function(set_extension([couple(1,1),couple(2,3),couple(4,5)]),2),R),R=3 )).
228 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_SETENUM_LR',
229 function(set_extension([couple(add('$'(x),1),'$'(y))]),add(1,'$'(x))),R),R='$'(y) )).
230 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_OVERL_SETENUM',
231 function(overwrite(overwrite('$'(r),'$'(s)),set_extension([couple('$'(x),'$'(y))])),'$'(x)),R),R='$'(y) )).
232 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_BUNION_SETENUM',
233 function(union(union('$'(r),'$'(s)),set_extension([couple(1,2),couple(2,'$'(x))])),2),R),R='$'(x) )).
234 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_FUNIMAGE_BUNION_SETENUM',
235 function(union(set_extension([couple(1,2),couple(2,'$'(x))]),union('$'(r),'$'(s))),2),R),R='$'(x) )).
236 :- assert_must_succeed(( test_simp_rule('SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM',
237 function(set_extension([couple(1,2),couple(2,3),couple(2,4)]),function(set_extension([couple(4,2),couple(3,2),couple(2,1)]),'$'(x))),R),
238 R='$'(x) )).
239 :- assert_must_succeed(( test_simp_rule('DEF_EQUAL_FUNIMAGE',equal(function('$'(f),'$'(x)),'$'(y)),R),
240 R=member(couple('$'(x),'$'(y)),'$'(f)) )).
241 :- assert_must_succeed(( test_simp_rule('DEF_EQUAL_FUNIMAGE',equal(function('$'(f),couple('$'(x),'$'(z))),'$'(y)),R),
242 R=member(couple(couple('$'(x),'$'(z)),'$'(y)),'$'(f)) )).
243 :- assert_must_succeed(( test_simp_rule('DEF_BCOMP',ring(ring(ring('$'(a),'$'(b)),'$'(c)),'$'(d)),R),
244 R=composition(composition(composition('$'(d),'$'(c)),'$'(b)),'$'(a)) )).
245 :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_SING',
246 composition(set_extension([couple('$'(e),'$'(f))]),set_extension([couple('$'(f),'$'(g))])),R), R=set_extension([couple('$'(e),'$'(g))]) )).
247 :- assert_must_succeed(( test_simp_rule('DEF_IN_DOM',member('$'(a),domain('$'(r))),R),
248 R=exists(['$'(x)],member(couple('$'(a),'$'(x)),'$'(r))) )).
249 :- assert_must_succeed(( test_simp_rule('DEF_IN_DOM',member('$'(x),domain('$'(r))),R),
250 R=exists(['$'(y)],member(couple('$'(x),'$'(y)),'$'(r))) )).
251 :- assert_must_succeed(( test_simp_rule('DEF_IN_DOM',member('$'(a),domain(set_extension([couple(1,'$'(x))]))),R),
252 R=exists(['$'(y)],member(couple('$'(a),'$'(y)),set_extension([couple(1,'$'(x))]))) )).
253 :- assert_must_succeed(( test_simp_rule('DEF_IN_FCOMP',
254 member(couple('$'(a),'$'(b)),composition(event_b_identity,set_extension([couple(0,1)]))),R),
255 R=exists(['$'(x)],conjunct(member(couple('$'(a),'$'(x)),event_b_identity),member(couple('$'(x),'$'(b)),set_extension([couple(0,1)])))))).
256 :- assert_must_succeed(( test_simp_rule('DEF_IN_FCOMP',member(couple('$'(a),'$'(x)),composition(composition('$'(r),'$'(s)),'$'(t))),R),
257 R=exists(['$'(y1),'$'(y2)],conjunct(conjunct(member(couple('$'(a),'$'(y1)),'$'(r)),
258 member(couple('$'(y1),'$'(y2)),'$'(s))),member(couple('$'(y2),'$'(x)),'$'(t)))) )).
259 :- assert_must_succeed(( test_simp_rule('DERIV_MULTI_IN_BUNION',member('$'(r),union('$'(a),set_extension(['$'(r)]))),R), R=truth )).
260 :- assert_must_succeed(( test_simp_rule('SIMP_SETMINUS_EQUAL_EMPTY',equal(empty_set,set_subtraction('$'(r),'$'(a))),R),
261 R=subset('$'(r),'$'(a)) )).
262 :- assert_must_succeed(( test_simp_rule('SIMP_SETMINUS_EQUAL_EMPTY',equal(set_subtraction('$'(r),'$'(a)),empty_set),R),
263 R=subset('$'(r),'$'(a)) )).
264 :- assert_must_succeed(( test_simp_rule('SIMP_SETMINUS_EQUAL_EMPTY',subset(set_subtraction('$'(r),'$'(a)),empty_set),R),
265 R=subset('$'(r),'$'(a)) )).
266 :- assert_must_succeed(( test_simp_rule('SIMP_FCOMP_EQUAL_EMPTY',equal(empty_set,composition('$'(r),'$'(a))),R),
267 R=equal(intersection(range('$'(r)),domain('$'(a))),empty_set) )).
268 :- assert_must_succeed(( test_simp_rule('SIMP_OVERL_EQUAL_EMPTY',equal(empty_set,overwrite(overwrite('$'(r),'$'(a)),'$'(b))),R),
269 R=conjunct(conjunct(equal('$'(r),empty_set),equal('$'(a),empty_set)),equal('$'(b),empty_set)) )).
270 :- assert_must_succeed(( test_simp_rule('SIMP_MIN_BUNION_SING',min(union('$'(s),set_extension([min('$'(t))]))),R),
271 R=min(union('$'(s),'$'(t))) )).
272 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_MIN',min(set_extension(['$'(a),'$'(t),3,0,1])),R),R=min(set_extension(['$'(a),'$'(t),0])))).
273 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_CARD_UPTO',card(interval(1,2)),R), R=2 )).
274 :- assert_must_fail( test_simp_rule('SIMP_LIT_CARD_UPTO',card(interval(2,'$'(drei))),_) ).
275 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_0',multiplication(multiplication('$'(i),0),'$'(e)),R), R=0 )).
276 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_1',multiplication(multiplication('$'(i),1),'$'(e)),R), R=multiplication('$'(i),'$'(e)) )).
277 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_MINUS_ODD',
278 multiplication(multiplication(unary_minus('$'(i)),1),'$'(e)),R), R=unary_minus(multiplication(multiplication('$'(i),1),'$'(e))) )).
279 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_MINUS_ODD',
280 multiplication(multiplication('$'(i),-1),'$'(e)),R), R=unary_minus(multiplication(multiplication('$'(i),1),'$'(e))) )).
281 :- assert_must_succeed(( test_simp_rule('SIMP_SPECIAL_PROD_MINUS_EVEN',
282 multiplication(multiplication(unary_minus('$'(i)),-1),'$'(e)),R), R=multiplication(multiplication('$'(i),1),'$'(e)) )).
283 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_MINUS',unary_minus(1),R), R= -1 )).
284 :- assert_must_fail( test_simp_rule('SIMP_LIT_MINUS',unary_minus('$'(a)),_) ).
285 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_GT',greater(1,1),R), R=falsity )).
286 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_GT',greater(2,1),R), R=truth )).
287 :- assert_must_succeed(( test_simp_rule('SIMP_DIV_MINUS',div(-12,unary_minus('$'(x))),R), R=div(12,'$'(x)) )).
288 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_LT',less(0,multiplication(1000000,0)),R), R=falsity )).
289 :- assert_must_succeed(( test_simp_rule('Evaluate tautology',less_equal(0,multiplication(1000,0)),R), R=truth )). % SIMP_MULTI_LE
290 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_DIV_PROD',
291 equal(1,div(multiplication(multiplication('$'(y),'$'(e)),'$'(x)),'$'(e))),R), R=equal(1,multiplication('$'(y),'$'(x))) )).
292 :- assert_must_succeed(( test_simp_rule('Evaluate tautology',member(0,'NATURAL'),R), R=truth )). % SIMP_LIT_IN_NATURAL
293 :- assert_must_fail( test_simp_rule('Evaluate tautology',member(-1,'NATURAL'),_) ).
294 :- assert_must_succeed(( test_simp_rule('Evaluate tautology',member(1,'NATURAL1'),R), R=truth )). % SIMP_LIT_IN_NATURAL1
295 :- assert_must_fail( test_simp_rule('Evaluate tautology',member(0,'NATURAL1'),_) ).
296 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_UPTO',interval(1,0),R),R=empty_set )).
297 :- assert_must_fail( test_simp_rule('SIMP_LIT_UPTO',interval(0,0),_) ).
298 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_IN_MINUS_NATURAL',member(unary_minus(1),natural_set),R),R=falsity )).
299 :- assert_must_succeed(( test_simp_rule('SIMP_LIT_IN_MINUS_NATURAL',member(-1,natural_set),R),R=falsity )).
300 :- assert_must_succeed(( test_simp_rule('SIMP_MINUS_MINUS',unary_minus(unary_minus('$'(e))),R),R='$'(e) )).
301 :- assert_must_succeed(( test_simp_rule('SIMP_MINUS_MINUS',unary_minus(-13),R),R=13 )).
302 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),cartesian_product(integer_set,bool_set)),R),
303 R=cartesian_product(domain('$'(r)),bool_set) )).
304 :- assert_must_fail( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),pow_subset(integer_set,bool_set)),_) ).
305 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),cartesian_product(integer_set,bool_set)),R),
306 R=cartesian_product(domain('$'(r)),bool_set) )).
307 :- assert_must_fail( test_simp_rule('SIMP_TYPE_FCOMP_R',composition('$'(r),pow_subset(integer_set,bool_set)),_) ).
308 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_DOM',domain(cartesian_product(integer_set,bool_set)),R),
309 R=integer_set )).
310 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_DOM',domain(cartesian_product(cartesian_product(integer_set,bool_set),bool_set)),R),
311 R=cartesian_product(integer_set,bool_set) )).
312 :- assert_must_succeed(( test_simp_rule('SIMP_TYPE_RAN',range(cartesian_product(integer_set,bool_set)),R),
313 R=bool_set )).
314 :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_EQUAL',
315 event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),conjunct(member('$'(y),natural_set),equal('$'(x),1))),R),
316 R=event_b_comprehension_set(['$'(y)],couple(1,'$'(y)),member('$'(y),natural_set)) )).
317 :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_EQUAL',
318 event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),conjunct(member('$'(x),natural_set),equal('$'(y),1))),R),
319 R=event_b_comprehension_set(['$'(x)],couple('$'(x),1),member('$'(x),natural_set)) )).
320 :- assert_must_succeed(( test_simp_rule('SIMP_COMPSET_EQUAL',
321 event_b_comprehension_set(['$'(x),'$'(y),'$'(z)],couple(couple('$'(x),'$'(z)),'$'(y)),
322 conjunct(member('$'(y),natural_set),equal(couple('$'(x),'$'(z)),'$'(e)))),R),
323 R=event_b_comprehension_set(['$'(y)],couple('$'(e),'$'(y)),member('$'(y),natural_set)) )).
324 :- assert_must_succeed(( test_simp_rule('SIMP_IN_COMPSET',
325 member('$'(f),event_b_comprehension_set(['$'(x),'$'(y)],add('$'(x),'$'(y)),
326 conjunct(member('$'(x),natural_set),member('$'(y),natural_set)))),R),
327 R=exists(['$'(x),'$'(y)],conjunct(conjunct(member('$'(x),natural_set),member('$'(y),natural_set)),equal(add('$'(x),'$'(y)),'$'(f)))) )).
328 :- assert_must_fail( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT',
329 member('$'(a),event_b_comprehension_set(['$'(x)],couple('$'(x),add('$'(x),1)),member('$'(x),set_extension([3,12])))),_) ).
330 :- assert_must_succeed(( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT',
331 member('$'(a),event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),set_extension([3,12])))),R),
332 R=member('$'(a),set_extension([3,12])) )).
333 :- assert_must_succeed(( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT',
334 member(couple('$'(a),'$'(b)),event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),
335 conjunct(member('$'(x),natural_set),member('$'(y),natural_set)))),R),
336 R=conjunct(member('$'(a),natural_set),member('$'(b),natural_set)) )).
337 :- assert_must_fail( test_simp_rule('SIMP_IN_COMPSET_ONEPOINT',member('$'(a),
338 event_b_comprehension_set(['$'(x),'$'(y)],'$'(x),conjunct(member('$'(x),natural_set),member('$'(y),natural_set)))),_) ).
339 :- assert_must_fail( test_simp_rule('SIMP_SUBSETEQ_COMPSET_R',
340 subset('$'(s),event_b_comprehension_set(['$'(x)],'$'(y),greater('$'(x),'$'(y)))),_) ).
341 :- assert_must_succeed(( test_simp_rule('SIMP_SUBSETEQ_COMPSET_R',
342 subset('$'(s),event_b_comprehension_set(['$'(x)],'$'(x),greater('$'(x),'$'(y)))),R),
343 R=forall([NewId],member(NewId,'$'(s)),greater(NewId,'$'(y))), NewId \= '$'(x), NewId \= '$'(y) )).
344 :- assert_must_succeed(( test_simp_rule('SIMP_SUBSETEQ_COMPSET_R',
345 subset('$'(s),event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),
346 conjunct(member('$'(x),natural_set),member('$'(y),natural_set)))),R),
347 R=forall([NewId1,NewId2],member(couple(NewId1,NewId2),'$'(s)),
348 conjunct(member(NewId1,natural_set),member(NewId2,natural_set))), \+ member(NewId1,['$'(x),'$'(y)]), \+ member(NewId2,['$'(x),'$'(y)]) )).
349 :- assert_must_succeed(( test_simp_rule('SIMP_FUNIMAGE_LAMBDA',
350 equal(5,function(event_b_comprehension_set(['$'(x)],couple('$'(x),add('$'(x),1)),member('$'(x),natural_set)),'$'(y))),R),
351 R=equal(5,add('$'(y),1)) )).
352 :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_LAMBDA',
353 finite(event_b_comprehension_set(['$'(x)],couple('$'(x),add('$'(x),1)),member('$'(x),'$'(set)))),R),
354 R=finite(event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),'$'(set)))) )).
355 :- assert_must_fail( test_simp_rule('SIMP_FINITE_LAMBDA',
356 finite(event_b_comprehension_set(['$'(x),'$'(y)],couple('$'(x),'$'(y)),
357 conjunct(member('$'(x),'$'(set)),member('$'(y),'$'(set))))),_) ).
358 :- assert_must_fail( test_simp_rule('SIMP_FINITE_LAMBDA',
359 finite(event_b_comprehension_set(['$'(x)],couple(1,'$'(x)),member('$'(x),'$'(set)))),_) ).
360 :- assert_must_succeed(( test_simp_rule('SIMP_FINITE_LAMBDA',
361 finite(event_b_comprehension_set(['$'(x)],couple('$'(x),1),member('$'(x),'$'(set)))),R),
362 R=finite(event_b_comprehension_set(['$'(x)],'$'(x),member('$'(x),'$'(set)))) )).
363 :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_DOMRES',
364 composition(domain_restriction('$'(s),'$'(p)),'$'(q)),R),R=domain_restriction('$'(s),composition('$'(p),'$'(q))) )).
365 :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_DOMSUB',
366 composition('$'(t),composition(domain_subtraction('$'(s),'$'(p)),'$'(q))),R),
367 R=composition('$'(t),domain_subtraction('$'(s),composition('$'(p),'$'(q)))) )).
368 :- assert_must_fail( test_simp_rule('DERIV_FCOMP_RANRES',composition(range_restriction('$'(s),'$'(p)),'$'(q)),_) ).
369 :- assert_must_succeed(( test_simp_rule('DERIV_FCOMP_RANRES',
370 composition('$'(p),range_restriction('$'(q),'$'(s))),R),
371 R=range_restriction(composition('$'(p),'$'(q)),'$'(s)) )).
372 :- assert_must_succeed(( test_simp_rule('SIMP_BCOMP_ID',
373 ring(ring(ring('$'(r),domain_restriction('$'(s),event_b_identity)),domain_restriction('$'(t),event_b_identity)),'$'(o)),R),
374 R=ring(ring('$'(r),domain_restriction(intersection('$'(s),'$'(t)),event_b_identity)),'$'(o)) )).
375 :- assert_must_succeed(( test_simp_rule('SIMP_BCOMP_ID',
376 ring(ring(domain_restriction('$'(s),event_b_identity),domain_subtraction('$'(t),event_b_identity)),'$'(r)),R),
377 R=ring(domain_restriction(set_subtraction('$'(s),'$'(t)),event_b_identity),'$'(r)) )).
378 :- assert_must_succeed(( test_simp_rule('SIMP_BCOMP_ID',
379 ring(ring(domain_subtraction('$'(s),event_b_identity),domain_subtraction('$'(t),event_b_identity)),'$'(r)),R),
380 R=ring(domain_subtraction(union('$'(s),'$'(t)),event_b_identity),'$'(r)) )).
381 :- assert_must_succeed(( test_simp_rule('SIMP_FCOMP_ID',
382 composition(composition(domain_restriction('$'(s),event_b_identity),
383 domain_restriction('$'(t),event_b_identity)),domain_subtraction('$'(q),event_b_identity)),R),
384 R=domain_restriction(set_subtraction(intersection('$'(s),'$'(t)),'$'(q)),event_b_identity) )).
385 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL_PLUS_PLUS',
386 greater(add(add('$'(a),'$'(e)),'$'(b)),add(add('$'(c),'$'(e)),'$'(d))),R),
387 R=greater(add('$'(a),'$'(b)),add('$'(c),'$'(d))) )).
388 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL_PLUS_R',
389 greater_equal('$'(c),add(add('$'(a),'$'(c)),'$'(b))),R),
390 R=greater_equal(0,add('$'(a),'$'(b))) )).
391 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL_PLUS_L',
392 less_equal(add(add('$'(a),'$'(c)),'$'(b)),'$'(c)),R),
393 R=less_equal(add('$'(a),'$'(b)),0) )).
394 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL_MINUS_MINUS_R',
395 less_equal(minus('$'(a),'$'(c)),minus('$'(b),'$'(c))),R),
396 R=less_equal('$'(a),'$'(b)) )).
397 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL_MINUS_MINUS_L',
398 not_equal(minus('$'(c),'$'(a)),minus('$'(c),'$'(b))),R),
399 R=not_equal('$'(b),'$'(a)) )).
400 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL',less(-1,minus('$'(y),1)),R),
401 R=less(0,'$'(y)) )).
402 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL',less(minus('$'(u),'$'(x)),add('$'(u),'$'(z))),R),
403 R=less(unary_minus('$'(x)),'$'(z)) )).
404 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL',less(add('$'(u),unary_minus('$'(x))),minus('$'(v),'$'(x))),R),
405 R=less('$'(u),'$'(v)) )).
406 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL',less(minus('$'(u),'$'(x)),add(unary_minus('$'(x)),'$'(v))),R),
407 R=less('$'(u),'$'(v)) )).
408 :- assert_must_succeed(( test_simp_rule('SIMP_MULTI_ARITHREL',less(add(1,minus('$'(u),'$'(x))),add('$'(y),'$'(u))),R),
409 R=less(minus(1,'$'(x)),'$'(y)) )).
410
411 :- assert_must_succeed(( test_simp_rule_with_hyps('SIMP_FUNIMAGE_DOMRES',[member('$'(f),total_function('$'(a),'$'(b)))],
412 function(domain_restriction('$'(e),'$'(f)),'$'(g)),R),
413 R=function('$'(f),'$'(g)) )).
414 :- assert_must_succeed(( test_simp_rule_with_hyps('SIMP_CARD_SETMINUS',[finite('$'(s)),subset('$'(t),'$'(s))],
415 not_equal(0,card(set_subtraction('$'(s),'$'(t)))),R), R=not_equal(0,minus(card('$'(s)),card('$'(t)))) )).
416 :- assert_must_succeed(( test_simp_rule_with_hyps('SIMP_CARD_SETMINUS_SETENUM',
417 [member('$'(e),'$'(s)),member('$'(f),'$'(s)),member('$'(g),'$'(s))],
418 not_equal(0,card(set_subtraction('$'(s),set_extension(['$'(e),'$'(f),'$'(g)])))),R),
419 R=not_equal(0,minus(card('$'(s)),card(set_extension(['$'(e),'$'(f),'$'(g)])))) )).
420 :- assert_must_succeed(( test_simp_rule_with_hyps('DERIV_DOM_TOTALREL'(_),[member('$'(r),total_function('$'(a),'$'(b)))],
421 equal('$'(f),domain('$'(r))),R), R=equal('$'(f),'$'(a)) )).
422 :- assert_must_fail( test_simp_rule_with_hyps('DERIV_DOM_TOTALREL'(_),[member('$'(r),relations('$'(a),'$'(b)))],
423 equal('$'(f),domain('$'(r))),_) ).
424
425 % DISTRI rules
426 :- assert_must_succeed(( test_simp_rule('DISTRI_AND_OR',conjunct('$'(p),disjunct('$'(q),'$'(r))),R),
427 R=disjunct(conjunct('$'(p),'$'(q)),conjunct('$'(p),'$'(r))) )).
428 :- assert_must_succeed(( test_simp_rule('DISTRI_AND_OR',conjunct(disjunct(disjunct('$'(q),'$'(s)),'$'(r)),'$'(t)),R),
429 R=disjunct(disjunct(conjunct('$'(q),'$'(t)),conjunct('$'(s),'$'(t))),conjunct('$'(r),'$'(t))) )).
430 :- assert_must_succeed(( test_simp_rule('DISTRI_OR_AND',disjunct('$'(p),conjunct('$'(q),'$'(r))),R),
431 R=conjunct(disjunct('$'(p),'$'(q)),disjunct('$'(p),'$'(r))) )).
432 :- assert_must_succeed(( test_simp_rule('DISTRI_SUBSETEQ_BUNION_SING',subset(union('$'(s),set_extension(['$'(f)])),'$'(t)),R),
433 R=conjunct(subset('$'(s),'$'(t)),member('$'(f),'$'(t))) )).
434 :- assert_must_succeed(( test_simp_rule('DISTRI_SUBSETEQ_BUNION_SING',
435 subset(union(union('$'(s),set_extension(['$'(f)])),'$'(g)),'$'(t)),R),
436 R=conjunct(conjunct(subset('$'(s),'$'(t)),member('$'(f),'$'(t))),subset('$'(g),'$'(t))) )).
437 :- assert_must_succeed(( test_simp_rule('DISTRI_BINTER_SETMINUS',intersection('$'(a),set_subtraction('$'(s),'$'(t))),R),
438 R=set_subtraction(intersection('$'(a),'$'(s)),intersection('$'(a),'$'(t))) )).
439 :- assert_must_succeed(( test_simp_rule('DISTRI_SETMINUS_BUNION',set_subtraction('$'(a),union('$'(s),'$'(t))),R),
440 R=set_subtraction(set_subtraction('$'(a),'$'(s)),'$'(t)) )).
441 :- assert_must_succeed(( test_simp_rule('DISTRI_DPROD_BUNION',direct_product('$'(r),union('$'(s),'$'(t))),R),
442 R=union(direct_product('$'(r),'$'(s)),direct_product('$'(r),'$'(t))) )). % distri_r
443 :- assert_must_fail( test_simp_rule('DISTRI_DPROD_BUNION',direct_product(union('$'(s),'$'(t)),'$'(r)),_) ).
444 :- assert_must_succeed(( test_simp_rule('DISTRI_OVERL_BUNION_L',overwrite(union('$'(p),'$'(q)),'$'(r)),R),
445 R=union(overwrite('$'(p),'$'(r)),overwrite('$'(q),'$'(r))) )). % distri_l
446 :- assert_must_fail( test_simp_rule('DISTRI_OVERL_BUNION_L',overwrite('$'(r),union('$'(p),'$'(q))),_) ).
447 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMSUB_BUNION_L',domain_subtraction(union('$'(p),'$'(q)),'$'(r)),R),
448 R=intersection(domain_subtraction('$'(p),'$'(r)),domain_subtraction('$'(q),'$'(r))) )).
449 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_BUNION',reverse(union(union('$'(r),'$'(b)),'$'(p))),R),
450 R=union(union(reverse('$'(r)),reverse('$'(b))),reverse('$'(p))) )).
451 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_FCOMP',
452 reverse(composition('$'(r),'$'(b))),R), R=composition(reverse('$'(b)),reverse('$'(r))) )).
453 :- assert_must_succeed(( test_simp_rule('DISTRI_RAN_BUNION',range(union(union('$'(r),'$'(b)),'$'(c))),R),
454 R=union(union(range('$'(r)),range('$'(b))),range('$'(c))) )).
455 :- assert_must_succeed(( test_simp_rule('DISTRI_RANSUB_BUNION_R',
456 range_subtraction('$'(r),union('$'(s),'$'(t))),R),
457 R=intersection(range_subtraction('$'(r),'$'(s)),range_subtraction('$'(r),'$'(t))) )).
458 :- assert_must_succeed(( test_simp_rule('DISTRI_RANSUB_BUNION_L',
459 range_subtraction(union('$'(s),'$'(t)),'$'(r)),R),
460 R=union(range_subtraction('$'(s),'$'(r)),range_subtraction('$'(t),'$'(r))) )).
461 :- assert_must_succeed(( test_simp_rule('DISTRI_RANSUB_BINTER_R',
462 range_subtraction('$'(r),intersection(intersection('$'(s),'$'(t)),'$'(u))),R),
463 R=union(union(range_subtraction('$'(r),'$'(s)),range_subtraction('$'(r),'$'(t))),range_subtraction('$'(r),'$'(u))) )).
464 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',minus('$'(a),add(add('$'(b),'$'(c)),'$'(d))),R),
465 R=minus(minus(minus('$'(a),'$'(b)),'$'(c)),'$'(d)) )).
466 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',minus('$'(a),minus(minus('$'(b),'$'(c)),'$'(d))),R),
467 R=add(add(minus('$'(a),'$'(b)),'$'(c)),'$'(d)) )).
468 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',minus('$'(a),add('$'(x),'$'(y))),R),
469 R=minus(minus('$'(a),'$'(x)),'$'(y)) )).
470 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',minus('$'(a),minus('$'(x),'$'(y))),R),
471 R=add(minus('$'(a),'$'(x)),'$'(y)) )).
472 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',minus('$'(a),add(unary_minus('$'(x)),'$'(y))),R),
473 R=minus(add('$'(a),'$'(x)),'$'(y)) )).
474 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',minus('$'(a),minus(unary_minus('$'(x)),'$'(y))),R),
475 R=add(add('$'(a),'$'(x)),'$'(y)) )).
476 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',unary_minus(add('$'(x),'$'(y))),R),
477 R=minus(unary_minus('$'(x)),'$'(y)) )).
478 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',unary_minus(minus('$'(x),'$'(y))),R),
479 R=add(unary_minus('$'(x)),'$'(y)) )).
480 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',unary_minus(add(unary_minus('$'(x)),'$'(y))),R),
481 R=minus('$'(x),'$'(y)) )).
482 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',unary_minus(minus(unary_minus('$'(x)),'$'(y))),R),
483 R=add('$'(x),'$'(y)) )).
484 :- assert_must_succeed(( test_simp_rule('DISTRI_MINUS',unary_minus(minus(add('$'(u),'$'(x)),'$'(y))),R),
485 R=add(minus(unary_minus('$'(u)),'$'(x)),'$'(y)) )).
486 :- assert_must_succeed(( test_simp_rule('DISTRI_PROD_PLUS',multiplication('$'(a),add('$'(b),'$'(c))),R),
487 R=add(multiplication('$'(a),'$'(b)),multiplication('$'(a),'$'(c))) )).
488 :- assert_must_succeed(( test_simp_rule('DISTRI_PROD_MINUS',multiplication('$'(a),minus('$'(b),'$'(c))),R),
489 R=minus(multiplication('$'(a),'$'(b)),multiplication('$'(a),'$'(c))) )).
490 :- assert_must_succeed(( test_simp_rule('DISTRI_IMP_AND',implication('$'(p),conjunct('$'(q),'$'(r))),R),
491 R=conjunct(implication('$'(p),'$'(q)),implication('$'(p),'$'(r))) )).
492 :- assert_must_succeed(( test_simp_rule('DISTRI_IMP_OR',implication(disjunct('$'(p),'$'(q)),'$'(r)),R),
493 R=conjunct(implication('$'(p),'$'(r)),implication('$'(q),'$'(r))) )).
494 :- assert_must_succeed(( test_simp_rule('DISTRI_FCOMP_BUNION_R',composition('$'(r),union('$'(s),'$'(t))),R),
495 R=union(composition('$'(r),'$'(s)),composition('$'(r),'$'(t))) )).
496 :- assert_must_succeed(( test_simp_rule('DISTRI_FCOMP_BUNION_L',composition(union('$'(s),'$'(t)),'$'(r)),R),
497 R=union(composition('$'(s),'$'(r)),composition('$'(t),'$'(r))) )).
498 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_BUNION_L',domain_restriction(union('$'(s),'$'(t)),'$'(r)),R),
499 R=union(domain_restriction('$'(s),'$'(r)),domain_restriction('$'(t),'$'(r))) )).
500 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_BUNION_R',domain_restriction('$'(r),union('$'(s),'$'(t))),R),
501 R=union(domain_restriction('$'(r),'$'(s)),domain_restriction('$'(r),'$'(t))) )).
502 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_BINTER_R',domain_restriction('$'(r),intersection('$'(s),'$'(t))),R),
503 R=intersection(domain_restriction('$'(r),'$'(s)),domain_restriction('$'(r),'$'(t))) )).
504 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_BINTER_L',domain_restriction(intersection('$'(s),'$'(t)),'$'(r)),R),
505 R=intersection(domain_restriction('$'(s),'$'(r)),domain_restriction('$'(t),'$'(r))) )).
506 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_SETMINUS_R',domain_restriction('$'(r),set_subtraction('$'(s),'$'(t))),R),
507 R=set_subtraction(domain_restriction('$'(r),'$'(s)),domain_restriction('$'(r),'$'(t))) )).
508 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_SETMINUS_L',domain_restriction(set_subtraction('$'(s),'$'(t)),'$'(r)),R),
509 R=set_subtraction(domain_restriction('$'(s),'$'(r)),domain_restriction('$'(t),'$'(r))) )).
510 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMSUB_BINTER_L',domain_subtraction(intersection('$'(p),'$'(q)),'$'(r)),R),
511 R=union(domain_subtraction('$'(p),'$'(r)),domain_subtraction('$'(q),'$'(r))) )).
512 :- assert_must_succeed(( test_simp_rule('DISTRI_RANRES_BUNION_R',range_restriction('$'(r),union('$'(s),'$'(t))),R),
513 R=union(range_restriction('$'(r),'$'(s)),range_restriction('$'(r),'$'(t))) )).
514 :- assert_must_succeed(( test_simp_rule('DISTRI_RANRES_BUNION_L',range_restriction(union('$'(s),'$'(t)),'$'(r)),R),
515 R=union(range_restriction('$'(s),'$'(r)),range_restriction('$'(t),'$'(r))) )).
516 :- assert_must_succeed(( test_simp_rule('DISTRI_RANRES_BINTER_L',range_restriction(intersection('$'(s),'$'(t)),'$'(r)),R),
517 R=intersection(range_restriction('$'(s),'$'(r)),range_restriction('$'(t),'$'(r))) )).
518 :- assert_must_succeed(( test_simp_rule('DISTRI_RANRES_BINTER_R',range_restriction('$'(r),intersection('$'(s),'$'(t))),R),
519 R=intersection(range_restriction('$'(r),'$'(s)),range_restriction('$'(r),'$'(t))) )).
520 :- assert_must_succeed(( test_simp_rule('DISTRI_RANRES_SETMINUS_R',range_restriction('$'(r),set_subtraction('$'(s),'$'(t))),R),
521 R=set_subtraction(range_restriction('$'(r),'$'(s)),range_restriction('$'(r),'$'(t))) )).
522 :- assert_must_succeed(( test_simp_rule('DISTRI_RANRES_SETMINUS_L',range_restriction(set_subtraction('$'(s),'$'(t)),'$'(r)),R),
523 R=set_subtraction(range_restriction('$'(s),'$'(r)),range_restriction('$'(t),'$'(r))) )).
524 :- assert_must_succeed(( test_simp_rule('DISTRI_CPROD_BINTER',cartesian_product('$'(a),intersection('$'(b),'$'(c))),R),
525 R=intersection(cartesian_product('$'(a),'$'(b)),cartesian_product('$'(a),'$'(c))) )).
526 :- assert_must_succeed(( test_simp_rule('DISTRI_CPROD_BUNION',cartesian_product('$'(a),union('$'(b),'$'(c))),R),
527 R=union(cartesian_product('$'(a),'$'(b)),cartesian_product('$'(a),'$'(c))) )).
528 :- assert_must_succeed(( test_simp_rule('DISTRI_CPROD_SETMINUS',cartesian_product('$'(a),set_subtraction('$'(b),'$'(c))),R),
529 R=set_subtraction(cartesian_product('$'(a),'$'(b)),cartesian_product('$'(a),'$'(c))) )).
530 :- assert_must_succeed(( test_simp_rule('DISTRI_BCOMP_BUNION',ring('$'(r),union('$'(s),'$'(t))),R),
531 R=union(ring('$'(r),'$'(s)),ring('$'(r),'$'(t))) )).
532 :- assert_must_succeed(( test_simp_rule('DISTRI_DPROD_SETMINUS',direct_product('$'(r),set_subtraction('$'(s),'$'(t))),R),
533 R=set_subtraction(direct_product('$'(r),'$'(s)),direct_product('$'(r),'$'(t))) )).
534 :- assert_must_succeed(( test_simp_rule('DISTRI_DPROD_BINTER',direct_product('$'(r),intersection('$'(s),'$'(t))),R),
535 R=intersection(direct_product('$'(r),'$'(s)),direct_product('$'(r),'$'(t))) )).
536 :- assert_must_succeed(( test_simp_rule('DISTRI_DPROD_OVERL',direct_product('$'(r),overwrite('$'(s),'$'(t))),R),
537 R=overwrite(direct_product('$'(r),'$'(s)),direct_product('$'(r),'$'(t))) )).
538 :- assert_must_succeed(( test_simp_rule('DISTRI_PPROD_BUNION',parallel_product('$'(r),union('$'(s),'$'(t))),R),
539 R=union(parallel_product('$'(r),'$'(s)),parallel_product('$'(r),'$'(t))) )).
540 :- assert_must_succeed(( test_simp_rule('DISTRI_PPROD_BINTER',parallel_product('$'(r),intersection('$'(s),'$'(t))),R),
541 R=intersection(parallel_product('$'(r),'$'(s)),parallel_product('$'(r),'$'(t))) )).
542 :- assert_must_succeed(( test_simp_rule('DISTRI_PPROD_SETMINUS',parallel_product('$'(r),set_subtraction('$'(s),'$'(t))),R),
543 R=set_subtraction(parallel_product('$'(r),'$'(s)),parallel_product('$'(r),'$'(t))) )).
544 :- assert_must_succeed(( test_simp_rule('DISTRI_PPROD_OVERL',parallel_product('$'(r),overwrite('$'(s),'$'(t))),R),
545 R=overwrite(parallel_product('$'(r),'$'(s)),parallel_product('$'(r),'$'(t))) )).
546 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_DPROD',domain_restriction('$'(p),direct_product('$'(r),'$'(s))),R),
547 R=direct_product(domain_restriction('$'(p),'$'(r)),domain_restriction('$'(p),'$'(s))) )).
548 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMRES_OVERL',domain_restriction('$'(p),overwrite('$'(r),'$'(s))),R),
549 R=overwrite(domain_restriction('$'(p),'$'(r)),domain_restriction('$'(p),'$'(s))) )).
550 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMSUB_BUNION_R',domain_subtraction('$'(p),union('$'(r),'$'(s))),R),
551 R=union(domain_subtraction('$'(p),'$'(r)),domain_subtraction('$'(p),'$'(s))) )).
552 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMSUB_BINTER_R',domain_subtraction('$'(p),intersection('$'(r),'$'(s))),R),
553 R=intersection(domain_subtraction('$'(p),'$'(r)),domain_subtraction('$'(p),'$'(s))) )).
554 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMSUB_DPROD',domain_subtraction('$'(p),direct_product('$'(r),'$'(s))),R),
555 R=direct_product(domain_subtraction('$'(p),'$'(r)), domain_subtraction('$'(p),'$'(s))) )).
556 :- assert_must_succeed(( test_simp_rule('DISTRI_DOMSUB_OVERL',domain_subtraction('$'(p),overwrite('$'(r),'$'(s))),R),
557 R=overwrite(domain_subtraction('$'(p),'$'(r)),domain_subtraction('$'(p),'$'(s))) )).
558 :- assert_must_succeed(( test_simp_rule('DISTRI_OVERL_BINTER_L',overwrite(intersection('$'(p),'$'(q)),'$'(r)),R),
559 R=intersection(overwrite('$'(p),'$'(r)),overwrite('$'(q),'$'(r))) )).
560 :- assert_must_succeed(( test_simp_rule('DISTRI_RANSUB_BINTER_L',range_subtraction(intersection('$'(p),'$'(q)),'$'(r)),R),
561 R=intersection(range_subtraction('$'(p),'$'(r)),range_subtraction('$'(q),'$'(r))) )).
562 :- assert_must_succeed(( test_simp_rule('DERIV_TYPE_SETMINUS_BINTER',set_subtraction(integer_set,intersection('$'(s),'$'(t))),R),
563 R=union(set_subtraction(integer_set,'$'(s)),set_subtraction(integer_set,'$'(t))) )).
564 :- assert_must_succeed(( test_simp_rule('DERIV_TYPE_SETMINUS_BUNION',set_subtraction(bool_set,union('$'(s),'$'(t))),R),
565 R=intersection(set_subtraction(bool_set,'$'(s)),set_subtraction(bool_set,'$'(t))) )).
566 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_BINTER',reverse(intersection('$'(r),'$'(s))),R),
567 R=intersection(reverse('$'(r)),reverse('$'(s))) )).
568 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_SETMINUS',reverse(set_subtraction('$'(r),'$'(s))),R),
569 R=set_subtraction(reverse('$'(r)),reverse('$'(s))) )).
570 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_BCOMP',reverse(ring('$'(r),'$'(s))),R),
571 R=ring(reverse('$'(s)),reverse('$'(r))) )).
572 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_PPROD',reverse(parallel_product('$'(s),'$'(r))),R),
573 R=parallel_product(reverse('$'(s)),reverse('$'(r))) )).
574 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_DOMRES',reverse(domain_restriction('$'(s),'$'(r))),R),
575 R=range_restriction(reverse('$'(r)),'$'(s)) )).
576 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_DOMSUB',reverse(domain_subtraction('$'(s),'$'(r))),R),
577 R=range_subtraction(reverse('$'(r)),'$'(s)) )).
578 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_RANRES',reverse(range_restriction('$'(r),'$'(s))),R),
579 R=domain_restriction('$'(s),reverse('$'(r))) )).
580 :- assert_must_succeed(( test_simp_rule('DISTRI_CONVERSE_RANSUB',reverse(range_subtraction('$'(r),'$'(s))),R),
581 R=domain_subtraction('$'(s),reverse('$'(r))) )).
582 :- assert_must_succeed(( test_simp_rule('DISTRI_DOM_BUNION',domain(union('$'(r),'$'(s))),R),
583 R=union(domain('$'(r)),domain('$'(s))) )).
584 :- assert_must_succeed(( test_simp_rule('DISTRI_RELIMAGE_BUNION_R',image('$'(r),union('$'(s),'$'(t))),R),
585 R=union(image('$'(r),'$'(s)),image('$'(r),'$'(t))) )).
586 :- assert_must_succeed(( test_simp_rule('DISTRI_RELIMAGE_BUNION_L',image(union('$'(s),'$'(t)),'$'(r)),R),
587 R=union(image('$'(s),'$'(r)),image('$'(t),'$'(r))) )).
588
589 :- assert_must_succeed(( test_transition_new_hyp(fun_image_goal,
590 [member('$'(f),partial_function(natural_set,bool_set))],equal('$'(t),function('$'(f),'$'(e))),R),
591 R= member(function('$'(f),'$'(e)),bool_set) )).
592
593 :- assert_must_succeed(( test_transition_r(subset_inter,[subset('$'(x),'$'(u))],equal(intersection('$'(x),'$'(u)),empty_set),R),
594 R= equal('$'(x),empty_set) )).
595 :- assert_must_succeed(( test_transition_r(in_inter,[member('$'(e),'$'(t))],
596 equal(intersection('$'(t),set_extension(['$'(e)])),empty_set),R), R= equal(set_extension(['$'(e)]),empty_set) )).
597
598 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[subset('$'(s),natural_set),subset('$'(t),natural_set)],
599 equal('$'(s),'$'(t)),R), R=conjunct(subset('$'(s),'$'(t)),subset('$'(t),'$'(s))) )).
600 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[equal('$'(s),natural_set)],equal('$'(s),set_extension([4])),R),
601 R=conjunct(subset('$'(s),set_extension([4])),subset(set_extension([4]),'$'(s))) )).
602 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[member('$'(s),pow_subset(bool_set))],
603 equal(set_extension([boolean_true]),'$'(s)),R),
604 R=conjunct(subset(set_extension([boolean_true]),'$'(s)),subset('$'(s),set_extension([boolean_true]))) )).
605 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EQUAL',[],equal(set_extension([1]),set_extension([1])),R),
606 R=conjunct(subset(set_extension([1]),set_extension([1])),subset(set_extension([1]),set_extension([1]))) )).
607 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_SUBSETEQ',[subset('$'(s),natural_set),subset('$'(t),natural_set)],
608 subset('$'(s),'$'(t)),R),R=subset(set_subtraction('INTEGER','$'(t)),set_subtraction('INTEGER','$'(s))) )).
609 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_NOT_EQUAL',[],not_equal('$'(e),1),R),
610 R=disjunct(less('$'(e),1),greater('$'(e),1)) )).
611 :- assert_must_fail( test_simp_rule_with_types('DERIV_NOT_EQUAL',[],not_equal('$'(e),'$'(f)),_) ).
612 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_NOT_EQUAL',[member('$'(f),natural_set)],not_equal('$'(e),'$'(f)),R),
613 R=disjunct(less('$'(e),'$'(f)),greater('$'(e),'$'(f))) )).
614 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_NOT_EQUAL',
615 [exists(['$'(x)],conjunct(conjunct(member('$'(x),natural_set),greater('$'(x),'$'(e))),greater('$'(x),'$'(f))))],
616 not_equal('$'(e),'$'(f)),R),
617 R=disjunct(less('$'(e),'$'(f)),greater('$'(e),'$'(f))) )).
618 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_NOT_EQUAL',[],not_equal(add(1,'$'(e)),multiplication('$'(f),2)),R),
619 R=disjunct(less(add(1,'$'(e)),multiplication('$'(f),2)),greater(add(1,'$'(e)),multiplication('$'(f),2))) )).
620 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EXPAND_PRJS',[member('$'(e),cartesian_product('INTEGER','INTEGER'))],member('$'(e),'$'(f)),R),
621 R=member(couple(function(event_b_first_projection_v2,'$'(e)),function(event_b_second_projection_v2,'$'(e))),'$'(f)) )).
622 :- assert_must_succeed(( test_simp_rule_with_types('DERIV_EXPAND_PRJS',[member('$'(e),cartesian_product('INTEGER',cartesian_product('INTEGER','INTEGER')))],
623 member('$'(e),'$'(f)),R),
624 R=member(couple(function(event_b_first_projection_v2,'$'(e)),function(event_b_second_projection_v2,'$'(e))),'$'(f)) )).
625 :- assert_must_fail( test_simp_rule_with_types('DERIV_EXPAND_PRJS',[member('$'(e),'INTEGER')],member('$'(e),'$'(f)),_) ).
626
627 :- assert_must_succeed(( sequent_prover_trans(imp_l1(_),
628 [greater('$'(x),'$'(y)),implication(greater_equal('$'(x),'$'(y)),equal('$'(c),boolean_true))],R),
629 R= [greater('$'(x),'$'(y)),equal('$'(c),boolean_true)] )).
630 :- assert_must_succeed(( sequent_prover_trans(imp_l1(_),
631 [greater('$'(x),'$'(y)),implication(conjunct('$'(p),greater_equal('$'(x),'$'(y))),equal('$'(c),boolean_true))],R),
632 R= [greater('$'(x),'$'(y)),implication('$'(p),equal('$'(c),boolean_true))] )).
633 :- assert_must_succeed(( sequent_prover_trans(imp_l1(_),
634 [greater('$'(x),'$'(y)),implication(conjunct(conjunct('$'(p),greater_equal('$'(x),'$'(y))),'$'(q)),equal('$'(c),boolean_true))],R),
635 R= [greater('$'(x),'$'(y)),implication(conjunct('$'(p),'$'(q)),equal('$'(c),boolean_true))] )).
636 :- assert_must_succeed(( sequent_prover_trans(one_point_l(_),
637 [forall(['$'(x)],conjunct(greater('$'(x),'$'(y)),equal('$'(x),1)),greater(2,'$'(y)))],R),
638 R= [implication(greater(1,'$'(y)),greater(2,'$'(y)))] )).
639 :- assert_must_succeed(( sequent_prover_trans(one_point_l(_),
640 [forall(['$'(x),'$'(y)],conjunct(member('$'(y),set_extension([1,2])),equal('$'(x),5)),greater('$'(x),'$'(y)))],R),
641 R= [forall(['$'(y)],member('$'(y),set_extension([1,2])),greater(5,'$'(y)))] )).
642 :- assert_must_succeed(( sequent_prover_trans(one_point_l(_),
643 [forall(['$'(x)],equal('$'(x),1),greater('$'(x),'$'(y)))],R), R= [implication(truth,greater(1,'$'(y)))] )).
644
645 :- assert_must_succeed(( sequent_prover_trans(one_point_r(_),[],
646 forall(['$'(x)],conjunct(greater('$'(x),'$'(y)),equal('$'(x),1)),greater(2,'$'(y))),[],R),
647 R= implication(greater(1,'$'(y)),greater(2,'$'(y))) )).
648 :- assert_must_succeed(( sequent_prover_trans(one_point_r(_),[],
649 forall(['$'(x),'$'(y)],conjunct(member('$'(y),set_extension([1,2])),equal('$'(x),5)),greater('$'(x),'$'(y))),[],R),
650 R= forall(['$'(y)],member('$'(y),set_extension([1,2])),greater(5,'$'(y))) )).
651 :- assert_must_succeed(( sequent_prover_trans(one_point_r(_),[],
652 forall(['$'(x)],equal('$'(x),1),greater('$'(x),'$'(y))),[],R), R= implication(truth,greater(1,'$'(y))) )).
653
654 :- assert_must_succeed(( test_transition_with_types_r(deriv_equal_card,
655 [equal('$'(s),set_extension([1,2])),equal('$'(t),set_extension([3,4]))],
656 equal(card('$'(s)),card('$'(t))),R),R= equal('$'(s),'$'(t)) )).
657 :- assert_must_fail( test_transition_with_types_r(deriv_equal_card,
658 [equal('$'(s),set_extension([1])),equal('$'(t),set_extension([boolean_false]))],
659 equal(card('$'(s)),card('$'(t))),_) ).
660 :- assert_must_succeed(( test_transition_with_types_r(deriv_le_card,
661 [member('$'(s),pow1_subset(integer_set)),subset('$'(t),natural1_set)],
662 less_equal(card('$'(s)),card('$'(t))),R),R= subset('$'(s),'$'(t)) )).
663 :- assert_must_fail( test_transition_with_types_r(deriv_le_card,[subset('$'(s),bool_set),subset('$'(t),natural1_set)],
664 less_equal(card('$'(s)),card('$'(t))),_) ).
665 :- assert_must_succeed(( test_transition_with_types_r(all_r,[equal('$'(y),0)],
666 forall(['$'(x)],member('$'(x),natural_set),greater_equal('$'(x),'$'(y))),R),
667 R=implication(member('$'(x),natural_set),greater_equal('$'(x),'$'(y))) )).
668 :- assert_must_succeed(( test_transition_with_types_r(all_r,[member('$'(x),bool_set),equal('$'(y),0)],
669 forall(['$'(x)],member('$'(x),natural_set),greater_equal('$'(x),'$'(y))),R),
670 R=implication(member(NewId,natural_set),greater_equal(NewId,'$'(y))), NewId \= '$'(x), NewId \= '$'(y) )).
671
672 :- assert_must_succeed(( test_transition_with_types_l(xst_l,[],exists(['$'(x)],member('$'(x),bool_set)),R),
673 R=member('$'(x),bool_set) )).
674 :- assert_must_succeed(( test_transition_with_types_l(xst_l,[equal('$'(x),1)],exists(['$'(x)],member('$'(x),bool_set)),R),
675 R=member(NewId,bool_set), NewId \= '$'(x) )).
676 :- assert_must_succeed(( test_transition_with_types_l(xst_l,[equal('$'(x),1)],
677 exists(['$'(x),'$'(y)],conjunct(member('$'(x),bool_set),equal('$'(x),'$'(y)))),R),
678 R=conjunct(member(Id1,bool_set),equal(Id1,Id2)), Id1 \= Id2, Id1 \= '$'(x), Id2 \= '$'(y) )).
679
680 :- assert_must_succeed(( sequent_prover_axiom(hyp,[equal('$'(x),1)],equal('$'(x),1)) )).
681 :- assert_must_succeed(( sequent_prover_axiom(hyp,[greater('$'(x),1)],greater_equal('$'(x),1)) )).
682 :- assert_must_succeed(( sequent_prover_axiom(hyp,[greater_equal('$'(x),1)],member('$'(x),natural_set)) )).
683 :- assert_must_succeed(( sequent_prover_axiom(hyp_or,[equal('$'(x),'$'(y))],disjunct(greater('$'(x),'$'(y)),equal('$'(x),'$'(y)))) )).
684 :- assert_must_succeed(( sequent_prover_axiom(false_hyp,[falsity],_) )).
685 :- assert_must_succeed(( sequent_prover_axiom(cntr,[not_equal('$'(x),'$'(y)),equal('$'(x),'$'(y))],_) )).
686 :- assert_must_succeed(( sequent_prover_axiom(cntr,[less('$'(x),'$'(y)),greater_equal('$'(x),'$'(y))],_) )).
687 :- assert_must_succeed(( sequent_prover_axiom(cntr,[less('$'(x),'$'(y)),greater('$'(x),'$'(y))],_) )).
688 :- assert_must_succeed(( sequent_prover_axiom(fin_rel,[member('$'(f),relations('$'(s),'$'(t))),finite('$'(s)),finite('$'(t))],
689 finite('$'(f))) )).
690 :- assert_must_succeed(( sequent_prover_axiom(fun_goal,[member('$'(f),partial_function('$'(s),'$'(t)))],
691 member('$'(f),partial_function(integer_set,bool_set))) )).
692 :- assert_must_fail( sequent_prover_axiom(fun_goal,[member('$'(f),partial_function('$'(s),'$'(t)))],
693 member('$'(f),partial_function('$'(a),bool_set))) ).
694 :- assert_must_fail( sequent_prover_axiom(fun_goal_rec,
695 [member('$'(f),partial_function('$'(s),'$'(t)))],
696 member('$'(f),partial_function(integer_set,bool_set))) ).
697 :- assert_must_succeed(( sequent_prover_axiom(fun_goal_rec,
698 [member('$'(f),relations('$'(r),partial_function('$'(s),'$'(t))))],
699 member(function('$'(f),'$'(e)),partial_function(integer_set,bool_set))) )).
700 :- assert_must_succeed(( sequent_prover_axiom(fun_goal_rec,
701 [member('$'(f),total_relation('$'(l),total_surjection('$'(r),total_function('$'(s),'$'(t)))))],
702 member(function(function('$'(f),'$'(e1)),'$'(e2)),partial_function(bool_set,bool_set))) )).
703 :- assert_must_succeed(( sequent_prover_axiom('DOM_SUBSET', [subset('$'(a),'$'(b))], subset(domain('$'(a)),domain('$'(b)))) )).
704 :- assert_must_succeed(( sequent_prover_axiom('RAN_SUBSET', [subset('$'(a),'$'(b))], subset(range('$'(a)),range('$'(b)))) )).
705 :- assert_must_succeed(( sequent_prover_axiom('IN_DOM_CPROD', [member('$'(x),domain(cartesian_product('$'(a),'$'(b))))],
706 member('$'(x),'$'(a))) )).
707 :- assert_must_succeed(( sequent_prover_axiom('SETENUM_SUBSET', [subset(set_extension([1,2]),'$'(a))], member(1,'$'(a))) )).
708 :- assert_must_succeed(( sequent_prover_axiom('OVR_RIGHT_SUBSET', [subset(overwrite('$'(f),'$'(g)),'$'(a))],
709 subset('$'(g),'$'(a))) )).
710 :- assert_must_succeed(( sequent_prover_axiom('OVR_RIGHT_SUBSET', [subset(overwrite(overwrite('$'(f),'$'(g)),'$'(h)),'$'(a))],
711 subset(overwrite('$'(g),'$'(h)),'$'(a))) )).
712 :- assert_must_fail( sequent_prover_axiom('OVR_RIGHT_SUBSET',[subset(overwrite(overwrite('$'(f),'$'(g)),'$'(h)),'$'(a))],
713 subset(overwrite('$'(f),'$'(g)),'$'(a))) ).
714 :- assert_must_succeed(( sequent_prover_axiom('RELSET_SUBSET_CPROD',[member('$'(f),relations('$'(a),'$'(b)))],subset('$'(f),cartesian_product('$'(a),'$'(b)))) )).
715 :- assert_must_succeed(( sequent_prover_axiom('DERIV_IN_SUBSET', [member('$'(x),'$'(a)), subset('$'(a),'$'(b))],member('$'(x),'$'(b))) )).
716
717 :- assert_must_fail( sequent_prover:wd_strict_term(conjunct(truth,equal(1,1))) ).
718 :- assert_must_succeed(( sequent_prover:wd_strict_term(equivalence(truth,equal(1,1))) )).
719 :- assert_must_succeed(( sequent_prover:rewrite_once('$'(x),'$'(y),equal('$'(x),'$'(x)),R), R=equal('$'(y),'$'(x)) )).
720 :- assert_must_succeed(( sequent_prover:is_subterm(equal(_,_),conjunct(truth,equal('$'(x),'$'(x)))) )).
721 :- assert_must_succeed(( sequent_prover:split_composition(composition('$'(f),'$'(g)),L,R), L='$'(f), R='$'(g) )).
722 :- assert_must_succeed(( sequent_prover:split_composition(composition(composition('$'(f),'$'(g)),'$'(h)),composition('$'(f),'$'(g)),'$'(h)) )).
723 :- assert_must_succeed(( sequent_prover:split_composition(composition(composition('$'(f),'$'(g)),'$'(h)),'$'(f),composition('$'(g),'$'(h))) )).