1		% Heinrich Heine Universitaet Duesseldorf
2		% (c) 2025-2025 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		% Implementation of a Sequent Prover
6		% where we can use the ProB animator to perform proof steps
7		% proof rules taken/adapted from https://wiki.event-b.org/index.php/Inference_Rules
8		% rewrite rules taken/adapted from https://wiki.event-b.org/index.php/All_Rewrite_Rules
9		% the term representation is the one from ProB's well_definedness prover
10
11		:- module(sequent_prover,[initialise_for_po_file/1,
12
13		cont_length/2,
14		get_continuations/2,
15		translate_term/2
16		]).
17
18		:- use_module(probsrc(module_information),[module_info/2]).
19		:- module_info(group,sequent_prover).
20		:- module_info(description,'This module provides rewrite and inference rules for the sequent_prover').
21
22		:- use_module(library(lists)).
23		:- use_module(library(samsort)).
24		:- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2]).
25		:- use_module(probsrc(tools),[ajoin/2, flatten/2, list_intersection/3, list_difference/3]).
26		:- use_module(probsrc(translate),[transform_raw/2, with_translation_mode/2]).
27		:- use_module(wdsrc(well_def_hyps),[convert_norm_expr_to_raw/2,
28		normalize_expression/2, normalize_predicate/2,
29		translate_norm_expr_with_limit/3]).
30
31		% ------------------------
32
33		initialise_for_po_file(File) :-
34		bb_put(po_counter,1),
35	?	load_from_po_file(File,Hyps,Goal,PO,Info),
36		sort(Hyps,SHyps),
37		% for ProB XTL Mode: specifying the start states:
38		bb_get(po_counter,PONR),
39		assertz(xtl_interface:start(state(sequent(SHyps,Goal,success(PONR)),Info),[description(PO)])),
40		P1 is PONR+1, bb_put(po_counter,P1),
41		fail.
42		initialise_for_po_file(_) :-
43		% assert other xtl_interface predicates:
44		assertz((xtl_interface:trans(A,B,C) :- sequent_prover:sequent_prover_trans_start(A,B,C))),
45		assertz((xtl_interface:trans(A,B,C,D) :- sequent_prover:sequent_prover_trans_start_desc(A,B,C,D))),
46		assertz((xtl_interface:trans_prop(A,B) :- sequent_prover:trans_prop(A,B))),
47		assertz((xtl_interface:prop(A,B) :- sequent_prover:prop(A,B))),
48		assertz((xtl_interface:symb_trans(A,B,C) :- sequent_prover:symb_trans(A,B,C))),
49		assertz((xtl_interface:symb_trans_enabled(A,B) :- sequent_prover:symb_trans_enabled(A,B))),
50		assertz((xtl_interface:animation_function_result(A,B) :- sequent_prover:animation_function_result(A,B))),
51		assertz((xtl_interface:animation_image_right_click_transition(A,B,C) :- sequent_prover:animation_image_right_click_transition(A,B,C))),
52		assertz((xtl_interface:animation_image_right_click_transition(A,B,C,D) :- sequent_prover:animation_image_right_click_transition(A,B,C,D))),
53		assertz(xtl_interface:nr_state_properties(30)). % TODO: a dynamic solution would be nice.
54
55		% declare these public as we will assert calls to them in the code above for initialise_for_po_file:
56		:- public prop/2, sequent_prover_trans/3, sequent_prover_trans_desc/4, symb_trans/3, symb_trans_enabled/2.
57		:- public animation_function_result/2, animation_image_right_click_transition/3, animation_image_right_click_transition/4.
58		:- public sequent_prover_trans_start/3, sequent_prover_trans_start_desc/4.
59
60		% ------------------------
61
62		get_normalised_bexpr(Expr,NormExpr) :-
63		transform_raw(Expr,TExpr),
64		normalize_predicate(TExpr,NormExpr).
65
66		:- use_module(probsrc(xtl_interface),[get_disprover_po/6]).
67		load_from_po_file(_File,Hyps,Goal,FullPOLabel,[rawsets(RawSets),des_hyps(OtherHyps)]) :-
68		% we use the disprover_po facts already loaded in xtl_interface, load_po_file(File) not necessary
69	?	get_disprover_po(POLabel,Context,RawGoal,RawAllHyps,RawSelHyps,RodinStatus),
70		ajoin([POLabel,' (',RodinStatus,')'],FullPOLabel),
71		get_normalised_bexpr(RawGoal,Goal),
72		list_difference(RawAllHyps,RawSelHyps,RawNotSelHyps),
73		maplist(get_normalised_bexpr,RawSelHyps,Hyps),
74		maplist(get_normalised_bexpr,RawNotSelHyps,OtherHyps),
75		bmachine_eventb:extract_ctx_sections(Context,_Name,_Extends,RawSets,_Constants,_AbstractConstants,_Axioms,_Theorems).
76
77
78		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs) :-
79		get_scope(Hyps,Info,Scope),
80		get_identifier_types(Scope,IdsTypes),
81		new_aux_identifier(IdsTypes,Y), !,
82		get_wd_pos2(equal('$'(Y),NormExpr),Scope,POs).
83
84		get_wd_pos(NormExpr,Hyps,Info,POs) :-
85		get_scope(Hyps,Info,Scope),
86		get_wd_pos2(NormExpr,Scope,POs).
87
88		get_wd_pos2(NormExpr,Scope,POs) :-
89		convert_norm_expr_to_raw(NormExpr,ParsedRaw),
90		bmachine:b_type_check_raw_expr(ParsedRaw,Scope,TypedPred,open(_)),
91		well_def_hyps:empty_hyps(H),
92		well_def_analyser:compute_all_wd_pos(TypedPred,H,[],TPOs),
93		maplist(rewrite_type_set,TPOs,TPOsT),
94		maplist(normalize_predicate,TPOsT,POs).
95
96		get_scope(Hyps,Info,[identifier([])]) :-
97		get_meta_info(des_hyps,Info,DHyps),
98		append(Hyps,DHyps,AllHyps),
99		filter_hyps(AllHyps,[]), !.
100		get_scope(Hyps,Info,[identifier(Res)]) :-
101		get_meta_info(des_hyps,Info,DHyps),
102		append(Hyps,DHyps,AllHyps),
103		filter_hyps(AllHyps,HypsRel),
104	?	list_to_op(HypsRel,HypsConj,conjunct),
105		used_identifiers(HypsConj,Ids),
106		get_set_types(Ids,Info,SetIds),
107		get_typed_identifiers(HypsConj,[identifier(SetIds)],List),
108		append(SetIds,List,AllIds),
109		select_types(AllIds,Res).
110
111		filter_hyps([],[]).
112		filter_hyps([Expr|Hyps],Res) :- with_ids(Expr,_), !, filter_hyps(Hyps,Res).
113		filter_hyps([Expr|Hyps],[Expr|Res]) :- filter_hyps(Hyps,Res).
114
115		get_set_types([],_,[]).
116		get_set_types(['$'(SetId)|T],Info,[b(identifier(SetId),set(global(SetId)),[])|R]) :-
117		is_deferred_set('$'(SetId),Info),!,
118		get_set_types(T,Info,R).
119		get_set_types([_|T],Info,R) :- get_set_types(T,Info,R).
120
121		rewrite_type_set(X,X) :- \+ compound(X).
122		rewrite_type_set(b(typeset,set(global(SET)),I),b(identifier(SET),set(global(SET)),I)) :- !.
123		rewrite_type_set(C,NewC) :- C=..[Op|Args],
124		maplist(rewrite_type_set,Args,NewArgs),
125		NewC =.. [Op|NewArgs].
126
127		in_scope(Id,[identifier(List)]) :- memberchk(b(identifier(Id),_,[]),List).
128
129		get_typed_identifiers(NormExpr,List) :- get_typed_identifiers(NormExpr,[],List).
130
131		get_typed_identifiers(NormExpr,Scope,List) :-
132		convert_norm_expr_to_raw(NormExpr,ParsedRaw),
133		Quantifier = forall,
134		bmachine:b_type_open_predicate(Quantifier,ParsedRaw,Scope,TypedPred,[]),
135		TypedPred = b(forall(List,_,_),_,_), !.
136		get_typed_identifiers(NormExpr,_,List) :-
137		used_identifiers(NormExpr,Ids),
138		maplist(any_type,Ids,List).
139
140		any_type('$'(X),b(identifier(X),any,[])).
141
142		select_types(Types,Selected) :- sort(Types,Sorted), select_types_aux(Sorted,Selected).
143
144		select_types_aux([],[]).
145		select_types_aux([b(identifier(X),any,_)|R],Res) :- member(b(identifier(X),T,_),R), T \= any, !, select_types_aux(R,Res).
146		select_types_aux([Id|R],[Id|Res]) :- select_types_aux(R,Res).
147
148		get_typed_ast(NormExpr,TExpr) :-
149		convert_norm_expr_to_raw(NormExpr,RawExpr),
150		transform_raw(RawExpr,TExpr).
151
152		get_identifier_types([identifier(IdsTypes)],IdsTypes).
153
154		prove_predicate(Hyps,Goal) :-
155		get_typed_ast(Goal,TGoal),
156		maplist(get_typed_ast,Hyps,THyps),
157		atelierb_provers_interface:prove_predicate(THyps,TGoal,proved).
158
159		get_meta_info(Key,Info,Content) :- El=..[Key,Content], memberchk(El,Info), !.
160		get_meta_info(_,_,[]).
161
162		update_meta_infos(Key,Info,Values,Info1) :-
163		get_meta_info(Key,Info,Content),
164		Content \= [], !,
165		Old=..[Key,Content],
166		New=..[Key,Values],
167	?	select(Old,Info,New,Info1).
168		update_meta_infos(Key,Info,Values,[El|Info]) :- El=..[Key,Values].
169
170		add_meta_info(Key,Info,Value,Info1) :- add_meta_infos(Key,Info,[Value],Info1).
171
172		add_meta_infos(Key,Info,Values,Info1) :-
173		get_meta_info(Key,Info,Content),
174		Content \= [], !,
175		Old=..[Key,Content],
176		append(Values,Content,NewContent),
177		New=..[Key,NewContent],
178		select(Old,Info,New,Info1).
179		add_meta_infos(Key,Info,Values,[El|Info]) :- El=..[Key,Values].
180
181		remove_meta_info(Key,Info,Value,Info1) :-
182		get_meta_info(Key,Info,Content),
183		Old=..[Key,Content],
184	?	select(Value,Content,Content0),
185		New=..[Key,Content0],
186	?	select(Old,Info,New,Info1).
187
188		% ------------------------
189
190		get_po_description(PONR,PO) :-
191		xtl_interface:start(state(sequent(_SHyps,_Goal,success(PONR)),_Info),[description(PO)]).
192
193		% specifying properties that appear in the State Properties view:
194		prop(success(_Nr),goal).
195		prop(success(Nr),'='('DISCHARGED',PO)) :- get_po_description(Nr,PO).
196		prop(sequent(_,X,_), '='('GOAL',XS)) :- translate_term(X,XS).
197		prop(sequent(Hyps,_,_),'='(HypNr,XS)) :- nth1(Nr,Hyps,X),
198		translate_term(X,XS), ajoin(['HYP',Nr],HypNr).
199		prop(sequent(_,_,Cont),'='('CONTINUATION',P)) :- cont_length(Cont,P).
200
201		prop(state(S,_),Val) :- prop(S,Val).
202
203		translate_term(Term,Str) :-
204		catch(with_translation_mode(unicode,translate_norm_expr_with_limit(Term,300,Str)),_Exc,Str=Term).
205
206		cont_length(sequent(_,_,C),R) :- !, cont_length(C,R1), R is R1+1.
207		cont_length(success(_),R) :- !, R=0.
208		cont_length(C,R) :- add_internal_error('Illegal continuation:',cont_length(C,R)),R=0.
209
210		% ------------------------
211
212		:- discontiguous trans_prop/2, symb_trans/4, symb_trans_enabled/2.
213
214		sequent_prover_trans_start(Rule,state(Sequent,Info),NewState) :-
215	?	update_info(Sequent,Info,Info1),
216	?	sequent_prover_trans(Rule,state(Sequent,Info1),NewState).
217		sequent_prover_trans_start_desc(Rule,state(Sequent,Info),NewState,Descr) :-
218	?	update_info(Sequent,Info,Info1),
219	?	sequent_prover_trans_desc(Rule,state(Sequent,Info1),NewState,Descr).
220
221		update_info(Sequent,Info,Info1) :-
222		Sequent = sequent(Hyps,_,_),
223		get_scope(Hyps,Info,[identifier(IdsTypes)]),
224	?	update_meta_infos(ids_types,Info,IdsTypes,Info1).
225
226		sequent_prover_trans(Rule,state(Sequent,Info),state(NewSequent,Info)) :-
227	?	trans_with_info(Rule,Sequent,NewSequent,Info).
228
229		sequent_prover_trans_desc(Rule,state(Sequent,Info),state(NewSequent,Info),Descr) :-
230	?	trans_desc_with_info(Rule,Sequent,NewSequent,Info,Descr).
231		sequent_prover_trans_desc(RuleArg,state(Sequent,Info),state(NewSequent,Info1),[description(Descr)]) :-
232		(trans_with_args(RuleArg,Sequent,NewSequent), Info1 = Info
233	?	; trans_with_args(RuleArg,state(Sequent,Info),state(NewSequent,Info1))),
234		RuleArg=..[Rule,Arg], create_descr(Rule,Arg,Descr).
235		sequent_prover_trans_desc(RuleArg,state(sequent(Hyps,Goal,Cont),Info),state(Cont,Info),[description(Descr)]) :-
236		axiom2(RuleArg,Hyps,Goal), RuleArg=..[Rule,Arg], create_descr(Rule,Arg,Descr).
237
238		% specifying the next state relation using proof rules:
239
240		sequent_prover_trans_desc(mon_deselect(Nr),state(sequent(Hyps,Goal,Cont),Info),state(sequent(Hyps0,Goal,Cont),Info1),[description(Descr)]) :-
241		nth1(Nr,Hyps,Hyp,Hyps0),
242		add_meta_info(des_hyps,Info,Hyp,Info1),
243		create_descr(mon_deselect,Hyp,Descr).
244
245		% transition rules requiring Infos and returning descriptions
246		trans_desc_with_info(Rule,Sequent,NewSequent,_Info,Desc) :-
247		trans_desc_wo_info(Rule,Sequent,NewSequent,Desc).
248		trans_desc_with_info(simplify_goal(Rule),sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont),Info,[description(Descr)]) :-
249	?	simp_rule(Goal,NewGoal,Rule,level0,Descr,Info)
250		; simp_rule_with_hyps(Goal,NewGoal,Rule,Hyps), create_descr(Rule,Goal,Descr).
251		trans_desc_with_info(simplify_hyp(Rule,Hyp),sequent(Hyps,Goal,Cont),sequent(SHyps,Goal,Cont),Info,[description(Descr)]) :-
252	?	select(Hyp,Hyps,NewHyp,NewHyps),
253	?	(simp_rule(Hyp,NewHyp,Rule,level0,Descr,Info)
254	?	; simp_rule_with_hyps(Hyp,NewHyp,Rule,Hyps), create_descr(Rule,Hyp,Descr)),
255		without_duplicates(NewHyps,SHyps).
256
257		% transition rules without descriptions but with Info being passed
258	?	trans_with_info(Rule,Sequent,NewSequent,_Info) :- trans_wo_info(Rule,Sequent,NewSequent).
259		trans_with_info(deriv_le_card,sequent(Hyps,Goal,Cont),sequent(Hyps,subset(S,T),Cont),Info) :- % covers DERIV_GE_CARD too
260		is_less_eq(Goal,card(S),card(T)),
261		get_meta_info(ids_types,Info,IdsTypes),
262	?	same_type(S,T,IdsTypes).
263		trans_with_info(deriv_lt_card,sequent(Hyps,Goal,Cont),sequent(Hyps,subset_strict(S,T),Cont),Info) :- % / DERIV_GT_CARD
264		is_less(Goal,card(S),card(T)),
265		get_meta_info(ids_types,Info,IdsTypes),
266		same_type(S,T,IdsTypes).
267		trans_with_info(deriv_equal_card,sequent(Hyps,equal(card(S),card(T)),Cont),sequent(Hyps,equal(S,T),Cont),Info) :-
268		get_meta_info(ids_types,Info,IdsTypes),
269	?	same_type(S,T,IdsTypes).
270		trans_with_info(sim_rel_image_r,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
271		rewrite_once(image(F,set_extension([E])),set_extension([function(F,E)]),Goal,NewGoal),
272		get_wd_pos(NewGoal,Hyps,Info,POs),
273		add_wd_pos(Hyps,POs,sequent(Hyps,NewGoal,Cont),NewSequent).
274		trans_with_info(sim_rel_image_l,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
275		select(Hyp,Hyps,Hyps0),
276		rewrite_once(image(F,set_extension([E])),set_extension([function(F,E)]),Hyp,NewHyp),
277		add_hyp(NewHyp,Hyps0,Hyps1),
278		get_wd_pos(NewHyp,Hyps0,Info,POs),
279		add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,Cont),NewSequent).
280		trans_with_info(sim_fcomp_l,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
281		select(Hyp,Hyps,Hyps0),
282		Sub = function(Comp,X),
283		is_subterm(Sub,Hyp),
284		split_composition(Comp,F,G),
285		NewSub = function(G,function(F,X)),
286		rewrite_once(Sub,NewSub,Hyp,NewHyp),
287		add_hyp(NewHyp,Hyps0,Hyps1),
288		get_wd_pos(NewHyp,Hyps0,Info,POs),
289		add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,Cont),NewSequent).
290		trans_with_info(sim_fcomp_r,sequent(Hyps,Goal,Cont),NewSequent,Info) :-
291		Sub = function(Comp,X),
292		is_subterm(Sub,Goal),
293		split_composition(Comp,F,G),
294		NewSub = function(G,function(F,X)),
295		rewrite_once(Sub,NewSub,Goal,NewGoal),
296		get_wd_pos(NewGoal,Hyps,Info,POs),
297		add_wd_pos(Hyps,POs,sequent(Hyps,NewGoal,Cont),NewSequent).
298		trans_with_info(xst_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont),Info) :-
299		Hyp = exists(Ids,P),
300	?	select(Hyp,Hyps,NewP,Hyps1),
301		get_meta_info(ids_types,Info,IdsTypes),
302		replace_used_ids(Ids,IdsTypes,NewIds),
303		rewrite_pairwise_rev(Ids,NewIds,P,NewP).
304		trans_with_info(all_r,sequent(Hyps,forall(Ids,P,Q),Cont),sequent(Hyps,NewImp,Cont),Info) :-
305		get_meta_info(ids_types,Info,IdsTypes),
306		replace_used_ids(Ids,IdsTypes,NewIds),
307		rewrite_pairwise_rev(Ids,NewIds,implication(P,Q),NewImp).
308
309	?	trans_wo_info(Rule,sequent(Hyps,Goal,Cont),Cont) :- axiom(Rule,Hyps,Goal).
310		trans_wo_info(dbl_hyp,sequent(Hyps,Goal,Cont),sequent(SHyps,Goal,Cont)) :-
311		% not really necessary if we remove duplicates in Hyps everywhere else
312		without_duplicates(Hyps,SHyps), SHyps \= Hyps.
313		trans_wo_info(or_r,sequent(Hyps,disjunct(GA,GB),Cont),sequent(Hyps1,GA,Cont)) :-
314		negate(GB,NotGB), % we could also negate GA and use GB as goal
315		add_hyp(NotGB,Hyps,Hyps1).
316		trans_wo_info(imp_r,sequent(Hyps,implication(G1,G2),Cont),
317		sequent(Hyps1,G2,Cont)) :-
318		add_hyp(G1,Hyps,Hyps1).
319		trans_wo_info(and_r,sequent(Hyps,conjunct(G1,G2),Cont),
320		sequent(Hyps,G1,sequent(Hyps,G2,Cont))).
321		trans_wo_info(neg_in,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
322		member(member(E,set_extension(L)),Hyps),
323		member(InEq,Hyps),
324		is_no_equality(InEq,E,B),
325		member(C,L),
326		equal_terms(B,C),
327		select(C,L,R),
328		select(member(E,set_extension(L)),Hyps,member(E,set_extension(R)),Hyps1).
329		trans_wo_info(contradict_r,sequent(Hyps,Goal,Cont),sequent(Hyps0,falsity,Cont)) :-
330		add_hyp(negation(Goal),Hyps,Hyps0).
331		trans_wo_info(upper_bound_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(Set),Cont)) :-
332		Goal = exists([B],forall([X],member(X,Set),greater_equal(B,X))). % TODO: Set must not contain any bound variable
333		trans_wo_info(fin_lt_0,sequent(Hyps,finite(S),Cont),sequent(Hyps,Goal1,sequent(Hyps,Goal2,Cont))):-
334		new_identifier(S,X),
335		new_identifier(member(S,X),N),
336		Goal1 = exists([N],forall([X],member(X,S),less_equal(N,X))),
337		Goal2 = subset(S,set_subtraction(integer_set,natural1_set)).
338		trans_wo_info(fin_ge_0,sequent(Hyps,finite(S),Cont),sequent(Hyps,Goal1,sequent(Hyps,Goal2,Cont))):-
339		new_identifier(S,X),
340		new_identifier(member(S,X),N),
341		Goal1 = exists([N],forall([X],member(X,S),less_equal(X,N))),
342		Goal2 = subset(S,natural_set).
343		trans_wo_info(fin_binter_r,sequent(Hyps,finite(I),Cont),sequent(Hyps,Disj,Cont)) :-
344		I = intersection(_,_),
345		finite_intersection(I,Disj).
346		trans_wo_info(fin_kinter_r,sequent(Hyps,finite(general_intersection(S)),Cont),
347		sequent(Hyps,conjunct(exists([X],member(X,S)),finite(X)),Cont)) :- new_identifier(S,X).
348		trans_wo_info(fin_qinter_r,sequent(Hyps,finite(quantified_intersection([X],P,E)),Cont),
349		sequent(Hyps,conjunct(exists([X],member(X,P)),finite(E)),Cont)).
350		trans_wo_info(fin_kunion_r,sequent(Hyps,finite(general_union(S)),Cont),
351		sequent(Hyps,conjunct(finite(S),forall([X],member(X,S),finite(X))),Cont)) :- new_identifier(S,X).
352		trans_wo_info(fin_qunion_r,sequent(Hyps,finite(quantified_union([X],P,E)),Cont),
353		sequent(Hyps,conjunct(finite(event_b_comprehension_set([X],E,P)),forall([X],P,finite(E))),Cont)).
354		trans_wo_info(fin_setminus_r,sequent(Hyps,finite(set_subtraction(S,_)),Cont),sequent(Hyps,finite(S),Cont)).
355		trans_wo_info(fin_rel_img_r,sequent(Hyps,finite(image(F,_)),Cont),sequent(Hyps,finite(F),Cont)).
356		trans_wo_info(fin_rel_ran_r,sequent(Hyps,finite(range(F)),Cont),sequent(Hyps,finite(F),Cont)).
357		trans_wo_info(fin_rel_dom_r,sequent(Hyps,finite(domain(F)),Cont),sequent(Hyps,finite(F),Cont)).
358		trans_wo_info(fin_fun_dom,sequent(Hyps,finite(Fun),Cont),sequent(Hyps,truth,Cont1)) :-
359		member_hyps(member(Fun,FunType),Hyps),
360		is_fun(FunType,_,Dom,_),
361		(member_hyps(finite(Dom),Hyps)
362		-> Cont1 = Cont
363		; Cont1 = sequent(Hyps,finite(Dom),Cont)).
364		trans_wo_info(fin_fun_ran,sequent(Hyps,finite(Fun),Cont),sequent(Hyps,truth,Cont1)) :-
365		member_hyps(member(Fun,FunType),Hyps),
366		is_inj(FunType,_,Ran),
367		(member_hyps(finite(Ran),Hyps)
368		-> Cont1 = Cont
369		; Cont1 = sequent(Hyps,finite(Ran),Cont)).
370		trans_wo_info(sim_ov_rel,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),relations(A,B)),Cont),
371		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
372		member_hyps(member(Fun,FunType),Hyps),
373		is_rel(FunType,_,A,B).
374		trans_wo_info(sim_ov_trel,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),total_relation(A,B)),Cont),
375		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
376		member_hyps(member(Fun,FunType),Hyps),
377		is_rel(FunType,total,A,B).
378		trans_wo_info(sim_ov_pfun,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),partial_function(A,B)),Cont),
379		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
380		member_hyps(member(Fun,FunType),Hyps),
381		is_fun(FunType,_,A,B).
382		trans_wo_info(sim_ov_tfun,sequent(Hyps,member(overwrite(Fun,set_extension([couple(X,Y)])),total_function(A,B)),Cont),
383		sequent(Hyps,member(X,A),sequent(Hyps,member(Y,B),Cont))) :-
384		member_hyps(member(Fun,FunType),Hyps),
385		is_fun(FunType,total,A,B).
386		trans_wo_info(fun_image_goal,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
387		wd_strict_term(Goal),
388	?	is_subterm(Hyp,Goal),
389		Hyp = function(F,E),
390		member(member(F,RType),Hyps),
391		is_rel(RType,_,_,Ran),
392		\+ member(member(function(F,E),Ran),Hyps),
393		add_hyp(member(function(F,E),Ran),Hyps,Hyps1).
394		trans_wo_info(ov_setenum_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
395		select(Hyp,Hyps,Hyps0),
396		wd_strict_term(Hyp),
397		Fun = function(overwrite(F,set_extension([couple(E,V)])),G),
398		rewrite_once(Fun,V,Hyp,Hyp1),
399		add_hyps([equal(G,E),Hyp1],Hyps0,Hyps1),
400		rewrite_once(Fun,function(domain_subtraction(set_extension([E]),F),G),Hyp,Hyp2),
401		add_hyps([negation(equal(G,E)),Hyp2],Hyps0,Hyps2).
402		trans_wo_info(ov_setenum_r,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,sequent(Hyps2,Goal2,Cont))) :-
403		wd_strict_term(Goal),
404		Fun = function(overwrite(F,set_extension([couple(E,V)])),G),
405		rewrite_once(Fun,V,Goal,Goal1),
406		add_hyp(equal(G,E),Hyps,Hyps1),
407		rewrite_once(Fun,function(domain_subtraction(set_extension([E]),F),G),Goal,Goal2),
408		add_hyp(negation(equal(G,E)),Hyps,Hyps2).
409		trans_wo_info(ov_l,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
410		select(Hyp,Hyps,Hyps0),
411		wd_strict_term(Hyp),
412		Fun = function(overwrite(F,S),G),
413		rewrite_once(Fun,function(S,G),Hyp,Hyp1),
414		add_hyps([member(G,domain(S)),Hyp1],Hyps0,Hyps1),
415		rewrite_once(Fun,function(domain_subtraction(domain(S),F),G),Hyp,Hyp2),
416		add_hyps([negation(member(G,domain(S))),Hyp2],Hyps0,Hyps2).
417		trans_wo_info(ov_r,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,sequent(Hyps2,Goal2,Cont))) :-
418		wd_strict_term(Goal),
419		Fun = function(overwrite(F,S),G),
420		rewrite_once(Fun,function(S,G),Goal,Goal1),
421		add_hyp(member(G,domain(S)),Hyps,Hyps1),
422		rewrite_once(Fun,function(domain_subtraction(domain(S),F),G),Goal,Goal2),
423		add_hyp(negation(member(G,domain(S))),Hyps,Hyps2).
424		trans_wo_info(subset_inter,sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont)) :-
425		member_hyps(subset(T,U),Hyps),
426		free_identifiers(Goal,Ids),
427	?	member(T,Ids), % T and U are not bound
428		member(U,Ids),
429	?	is_subterm(Inter,Goal),
430		select_op(U,Inter,Inter0,intersection),
431	?	rewrite_once(Inter,Inter0,Goal,NewGoal),
432	?	member_of(intersection,T,Inter).
433		trans_wo_info(in_inter,sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont)) :-
434		member_hyps(member(E,T),Hyps),
435		free_identifiers(Goal,Ids),
436		member(E,Ids),
437	?	member(T,Ids),
438	?	is_subterm(Inter,Goal),
439		select_op(T,Inter,Inter0,intersection),
440	?	rewrite_once(Inter,Inter0,Goal,NewGoal),
441		member_of(intersection,set_extension([E]),Inter).
442		trans_wo_info(notin_inter,sequent(Hyps,Goal,Cont),sequent(Hyps,NewGoal,Cont)) :-
443		member_hyps(negation(member(E,T)),Hyps),
444		free_identifiers(Goal,Ids),
445		member(E,Ids),
446		member(T,Ids),
447		Inter = intersection(_,_),
448		is_subterm(Inter,Goal),
449		rewrite_once(Inter,empty_set,Goal,NewGoal),
450		member_of(intersection,set_extension([E]),Inter),
451		member_of(intersection,T,Inter).
452		trans_wo_info(card_interv,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,sequent(Hyps2,Goal2,Cont))) :-
453		wd_strict_term(Goal),
454		rewrite_once(card(interval(A,B)),add(minus(B,A),1),Goal,Goal1),
455		rewrite_once(card(interval(A,B)),0,Goal,Goal2),
456		add_hyp(less_equal(A,B),Hyps,Hyps1),
457		add_hyp(less(B,A),Hyps,Hyps2).
458		trans_wo_info(card_empty_interv,sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
459		select(Hyp,Hyps,Hyps0),
460		wd_strict_term(Hyp),
461		rewrite_once(card(interval(A,B)),add(minus(B,A),1),Hyp,Hyp1),
462		rewrite_once(card(interval(A,B)),0,Hyp,Hyp2),
463		add_hyps([less_equal(A,B),Hyp1],Hyps0,Hyps1),
464		add_hyps([less(B,A),Hyp2],Hyps0,Hyps2).
465		trans_wo_info(simp_card_setminus_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps1,Goal,Cont))) :-
466		select(Hyp,Hyps,Hyps0),
467		rewrite_once(card(set_subtraction(S,T)),minus(card(S),card(intersection(S,T))),Hyp,Hyp1),
468		add_hyp(Hyp1,Hyps0,Hyps1).
469		trans_wo_info(simp_card_setminus_r,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps,NewGoal,Cont))) :-
470		rewrite_once(card(set_subtraction(S,T)),minus(card(S),card(intersection(S,T))),Goal,NewGoal).
471		trans_wo_info(simp_card_cprod_l,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps,finite(T),sequent(NewHyps,Goal,Cont)))) :-
472		select(Hyp,Hyps,NewHyp,NewHyps),
473		rewrite_once(card(cartesian_product(S,T)),multiplication(card(S),card(T)),Hyp,NewHyp).
474		trans_wo_info(simp_card_cprod_r,sequent(Hyps,Goal,Cont),sequent(Hyps,finite(S),sequent(Hyps,finite(T),sequent(Hyps,NewGoal,Cont)))) :-
475		rewrite_once(card(cartesian_product(S,T)),multiplication(card(S),card(T)),Goal,NewGoal).
476		trans_wo_info(skip_to_cont,sequent(Hyps,Goal,Cont),NewState) :-
477		Cont \= success(_),
478		append_sequents(Cont,sequent(Hyps,Goal,success(PO_Nr)),NewState,PO_Nr).
479
480		% trans_desc_wo_info/4
481		trans_desc_wo_info(eq(Dir,X,Y),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,Cont),[description(Descr)]) :-
482		select(equal(X,Y),Hyps,Hyps0),
483		(Dir=lr,
484		maplist(rewrite(X,Y),Hyps0,Hyps1),
485		rewrite(X,Y,Goal,Goal1)
486		; Dir=rl,
487		maplist(rewrite(Y,X),Hyps0,Hyps1),
488		rewrite(Y,X,Goal,Goal1)),
489		create_descr(eq,Dir,equal(X,Y),Descr).
490		trans_desc_wo_info(eqv(Dir,X,Y),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal1,Cont),[description(Descr)]) :-
491		select(equivalence(X,Y),Hyps,Hyps0),
492		(Dir=lr,
493		maplist(rewrite(X,Y),Hyps0,Hyps1),
494		rewrite(X,Y,Goal,Goal1)
495		; Dir=rl,
496		maplist(rewrite(Y,X),Hyps0,Hyps1),
497		rewrite(Y,X,Goal,Goal1)),
498		create_descr(eq,Dir,equal(X,Y),Descr).
499
500		trans_with_args(and_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
501		Hyp = conjunct(P,Q),
502		select(Hyp,Hyps,Hyps0),
503		add_hyps(P,Q,Hyps0,Hyps1).
504		trans_with_args(imp_l1(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
505		Imp = implication(P,Q),
506		select(Imp,Hyps,implication(NewP,Q),Hyps1),
507		select_conjunct(PP,P,NewP),
508		member(H,Hyps),
509		equal_terms(H,PP).
510		trans_with_args(reselect_hyp(Hyp),state(sequent(Hyps,Goal,Cont),Info),state(sequent(Hyps1,Goal,Cont),Info1)) :-
511	?	remove_meta_info(des_hyps,Info,Hyp,Info1),
512		add_hyp(Hyp,Hyps,Hyps1).
513		trans_with_args(imp_and_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
514		Hyp = implication(P,conjunct(Q,R)),
515		select(Hyp,Hyps,Hyps0),
516		add_hyps(implication(P,Q),implication(P,R),Hyps0,Hyps1).
517		trans_with_args(imp_or_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,Cont)) :-
518		Hyp = implication(disjunct(P,Q),R),
519		select(Hyp,Hyps,Hyps0),
520		add_hyps(implication(P,R),implication(Q,R),Hyps0,Hyps1).
521		trans_with_args(contradict_l(P),sequent(Hyps,Goal,Cont),sequent(Hyps1,NotP,Cont)):-
522		select(P,Hyps,Hyps0),
523		negate(P,NotP),
524		negate(Goal,NotGoal),
525		add_hyp(NotGoal,Hyps0,Hyps1).
526		trans_with_args(or_l(Hyp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
527		Hyp = disjunct(P,Q),
528		select(Hyp,Hyps,Hyps0),
529		add_hyp(P,Hyps0,Hyps1),
530		add_hyp(Q,Hyps0,Hyps2).
531		trans_with_args(case(D),sequent(Hyps,Goal,Cont),NewState) :-
532		member(D,Hyps),
533		D = disjunct(_,_),
534		select(D,Hyps,Hyps0),
535		extract_disjuncts(D,Hyps0,Goal,Cont,NewState).
536		trans_with_args(imp_case(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont))) :-
537		Imp = implication(P,Q),
538		select(Imp,Hyps,Hyps0),
539		add_hyp(negation(P),Hyps0,Hyps1),
540		add_hyp(Q,Hyps0,Hyps2).
541		trans_with_args(mh(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps0,P,sequent(Hyps1,Goal,Cont))) :-
542		Imp = implication(P,Q),
543		select(Imp,Hyps,Hyps0),
544		add_hyp(Q,Hyps0,Hyps1).
545		trans_with_args(hm(Imp),sequent(Hyps,Goal,Cont),sequent(Hyps0,negation(Q),sequent(Hyps1,Goal,Cont))) :-
546		Imp = implication(P,Q),
547		select(Imp,Hyps,Hyps0),
548		add_hyp(negation(P),Hyps0,Hyps1).
549		trans_with_args(def_expn_step(power_of(E,P)),sequent(Hyps,Goal,Cont),sequent(Hyps,not_equal(P,0),sequent(NewHyps,Goal,Cont))) :-
550		select(Hyp,Hyps,Hyps0),
551		rewrite_once(power_of(E,P),multiplication(E,power_of(E,minus(P,1))),Hyp,NewHyp),
552		add_hyp(NewHyp,Hyps0,NewHyps).
553		trans_with_args(def_expn_step(power_of(E,P)),sequent(Hyps,Goal,Cont),sequent(Hyps,not_equal(P,0),sequent(Hyps,NewGoal,Cont))) :-
554		rewrite_once(power_of(E,P),multiplication(E,power_of(E,minus(P,1))),Goal,NewGoal).
555		trans_with_args(induc_nat(X),state(sequent(Hyps,Goal,Cont),Info),
556		state(sequent(Hyps,member(X,natural_set),sequent(Hyps1,Goal,sequent(Hyps2,GoalN1,Cont))),Info)) :-
557		free_identifiers(Goal,Ids),
558		member(X,Ids),
559		of_integer_type(X,Info),
560		new_identifier(Goal,N),
561		add_hyp(equal(X,0),Hyps,Hyps1),
562		rewrite(X,N,Goal,GoalN),
563		add_hyps([member(N,natural_set),GoalN],Hyps,Hyps2),
564		rewrite(X,add(N,1),Goal,GoalN1).
565		trans_with_args(induc_nat_compl(X),state(sequent(Hyps,Goal,Cont),Info),
566		state(sequent(Hyps,member(X,natural_set),sequent(Hyps,Goal0,sequent(Hyps2,GoalN,Cont))),Info)) :-
567		free_identifiers(Goal,Ids),
568		member(X,Ids),
569		of_integer_type(X,Info),
570		new_identifiers(Goal,2,[K,N]),
571		rewrite(X,0,Goal,Goal0),
572		rewrite(X,N,Goal,GoalN),
573		rewrite(X,K,Goal,GoalK),
574		add_hyps([member(N,natural_set),forall([K],conjunct(less_equal(0,K),less(K,N)),GoalK)],Hyps,Hyps2).
575
576		create_descr(Rule,T,Descr) :- translate_term(T,TS),
577		ajoin([Rule,' (',TS,')'],Descr).
578
579		create_descr(Rule,S,T,Descr) :- translate_term(T,TS),
580		ajoin([Rule,' (',S,',',TS,')'],Descr).
581
582		/*
583		sequent_prover_trans(auto_simplify,state(Sequent,Info),state(NewSequent,Info)) :-
584		apply_simp_rules(Sequent,Info,NewSequent),
585		Sequent \= NewSequent.
586
587		apply_simp_rules(Sequent,Info,Res) :-
588		( sequent_prover_trans_desc(simplify_goal(Rule),state(Sequent,Info),state(NewSequent,Info),_)
589		; sequent_prover_trans_desc(simplify_hyp(Rule,_),state(Sequent,Info),state(NewSequent,Info),_)),
590		trivial_rule(Rule), !,
591		apply_simp_rules(NewSequent,Info,Res).
592		% apply_simp_rules(sequent(Hyps,Goal,Cont),_,Cont) :- axiom(Rule,Hyps,Goal), !.
593		apply_simp_rules(Sequent,_,Sequent).
594
595		trivial_rule(Rule) :- sub_atom(Rule,_,_,_,'MULTI').
596		trivial_rule(Rule) :- sub_atom(Rule,_,_,_,'SPECIAL').
597		trivial_rule(Rule) :- sub_atom(Rule,_,_,_,'TYPE').
598		trivial_rule('Evaluate tautology').
599
600		*/
601
602		symb_trans(Rule,state(Sequent,Info),state(NewSequent,Info)) :- symb_trans(Rule,Sequent,NewSequent,Info).
603		symb_trans_enabled(Rule,state(Sequent,_)) :- symb_trans_enabled(Rule,Sequent).
604
605		symb_trans(add_hyp(Hyp),sequent(Hyps0,Goal,Cont),NewSequent,Info) :- % CUT
606		parse_input(Hyp,add_hyp,TExpr),
607		normalize_predicate(TExpr,NormExpr),
608		get_wd_pos(NormExpr,Hyps0,Info,POs),
609		add_hyps(POs,Hyps0,Hyps1),
610		translate_finite_expr(NormExpr,NewExpr),
611		add_hyps([NewExpr|POs],Hyps0,Hyps2),
612		add_wd_pos(Hyps0,POs,sequent(Hyps1,NewExpr,sequent(Hyps2,Goal,Cont)),NewSequent).
613		trans_prop(add_hyp,param_names(['Hyp'])).
614		symb_trans_enabled(add_hyp,sequent(_,_,_)).
615
616		symb_trans(distinct_case(Pred),sequent(Hyps0,Goal,Cont),NewSequent,Info) :-
617		parse_input(Pred,distinct_case,TExpr),
618		normalize_predicate(TExpr,NormExpr),
619		get_wd_pos(NormExpr,Hyps0,Info,POs),
620		translate_finite_expr(NormExpr,NewExpr),
621		add_hyps([NewExpr|POs],Hyps0,Hyps1),
622		add_hyps([negation(NewExpr)|POs],Hyps0,Hyps2),
623		add_wd_pos(Hyps0,POs,sequent(Hyps1,Goal,sequent(Hyps2,Goal,Cont)),NewSequent).
624		trans_prop(distinct_case,param_names(['Pred'])).
625		symb_trans_enabled(distinct_case,sequent(_,_,_)).
626
627		symb_trans(exists_inst(Inst),sequent(Hyps,exists([X|Ids],Pred),Cont),NewSequent,Info) :-
628		parse_input(Inst,exists_inst,TExpr),
629		normalize_expression(TExpr,NormExpr),
630		rewrite(X,NormExpr,Pred,Goal1),
631		(Ids = [] -> Goal = Goal1 ; Goal = exists(Ids,Goal1)),
632		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
633		add_wd_pos(Hyps,POs,sequent(Hyps,Goal,Cont),NewSequent).
634		trans_prop(exists_inst,param_names(['Inst'])).
635		symb_trans_enabled(exists_inst,sequent(_,exists(_,_),_)).
636
637		symb_trans(forall_inst(Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
638		parse_input(Inst,forall_inst,TExpr),
639		normalize_expression(TExpr,NormExpr),
640		select(Hyp,Hyps,NewHyp,NewHyps),
641		Hyp = forall([X|Ids],P,Q),
642		rewrite(X,NormExpr,P,P1),
643		rewrite(X,NormExpr,Q,Q1),
644		(Ids = [] -> NewHyp = implication(P1,Q1) ; NewHyp = forall(Ids,P1,Q1)),
645		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
646		add_wd_pos(Hyps,POs,sequent(NewHyps,Goal,Cont),NewSequent).
647		trans_prop(forall_inst,param_names(['Inst'])).
648		symb_trans_enabled(forall_inst,sequent(Hyps,_,_)) :- memberchk(forall(_,_,_),Hyps).
649
650		symb_trans(forall_inst_mp(Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
651		parse_input(Inst,forall_inst_mp,TExpr),
652		normalize_expression(TExpr,NormExpr),
653		rewrite(X,NormExpr,P,P1),
654		rewrite(X,NormExpr,Q,Q1),
655		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
656		select(forall([X],P,Q),Hyps,Hyps0),
657		add_hyps(POs,Hyps0,Hyps1),
658		add_hyps([Q1|POs],Hyps0,Hyps2),
659		add_wd_pos(Hyps,POs,sequent(Hyps1,P1,sequent(Hyps2,Goal,Cont)),NewSequent).
660		trans_prop(forall_inst_mp,param_names(['Inst'])).
661		symb_trans_enabled(forall_inst_mp,sequent(Hyps,_,_)) :- memberchk(forall([_],_,_),Hyps).
662
663		symb_trans(forall_inst_mt(Inst),sequent(Hyps,Goal,Cont),NewSequent,Info) :-
664		parse_input(Inst,forall_inst_mt,TExpr),
665		normalize_expression(TExpr,NormExpr),
666		rewrite(X,NormExpr,negation(P),P1),
667		rewrite(X,NormExpr,negation(Q),Q1),
668		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
669		select(forall([X],P,Q),Hyps,Hyps0),
670		add_hyps(POs,Hyps0,Hyps1),
671		add_hyps([P1|POs],Hyps0,Hyps2),
672		add_wd_pos(Hyps,POs,sequent(Hyps1,Q1,sequent(Hyps2,Goal,Cont)),NewSequent).
673		trans_prop(forall_inst_mt,param_names(['Inst'])).
674		symb_trans_enabled(forall_inst_mt,sequent(Hyps,_,_)) :- memberchk(forall([_],_,_),Hyps).
675
676		:- use_module(probsrc(b_ast_cleanup),[clean_up_pred_or_expr/3]).
677		symb_trans(Command,sequent(Hyps,Goal,Cont),Cont,_) :- use_prover(Command,Hyps,Goal).
678
679		use_prover(Command,Hyps,Goal) :-
680		prover_command(Command,ProverList),
681		get_typed_ast(Goal,TGoal),
682		maplist(get_typed_ast,Hyps,THyps),
683		maplist(clean_up_pred_or_expr(_NonGroundExceptions),THyps,CleanTHyps),
684		clean_up_pred_or_expr(_NonGroundExceptions,TGoal,CleanTGoal), % TODO: exceptions
685		(bsyntaxtree:is_truth(CleanTGoal)
686		-> true % if ast_cleanup gives a true goal, we don't have to call a prover
687		; prove_sequent(ProverList,CleanTHyps,CleanTGoal)
688		).
689		prove_sequent(prob_wd_prover,THyps,TGoal) :- !,
690		well_def_analyser:prove_sequent(proving,TGoal,THyps).
691		prove_sequent(ProverList,THyps,TGoal) :-
692		atelierb_provers_interface:prove_predicate_with_provers(ProverList,THyps,TGoal,proved).
693		prover_command(ml_pp,[ml,pp]).
694		prover_command(ml,[ml]).
695		prover_command(pp,[pp]).
696		prover_command(prob_wd_prover,prob_wd_prover).
697		trans_prop(Cmd,param_names([])) :- prover_command(Cmd,_).
698		symb_trans_enabled(Cmd,sequent(_,_,_)) :- prover_command(Cmd,_).
699
700		symb_trans(prob_disprover,sequent(Hyps,Goal,Cont),NewState,Info) :-
701		convert_norm_expr_to_raw(Goal,RawGoal),
702		maplist(convert_norm_expr_to_raw,Hyps,RawHyps),
703		AllHyps = RawHyps, SelectedHyps = RawHyps, Timeout = 1000,
704		% TO DO: pass information about top-level types, new deferred sets, ...
705		disprover:disprove(RawGoal,AllHyps,SelectedHyps,Timeout,OutResult),
706		format(user_output,'ProB Disprover Result = ~w (Info=~w)~n',[OutResult,Info]),
707		dispatch_result(OutResult,Cont,NewState).
708		trans_prop(prob_disprover,param_names([])).
709		symb_trans_enabled(prob_disprover,sequent(_,_,_)).
710
711		dispatch_result(contradiction_found,Cont,Cont).
712		dispatch_result(contradiction_in_hypotheses,Cont,Cont).
713		dispatch_result(solution_on_selected_hypotheses(S),_,counter_example(S)).
714		dispatch_result(solution(S),_,counter_example(S)).
715		% other results are no_solution_found(_) and time_out
716
717		symb_trans(rewrite_hyp(HypNr,NewHyp),sequent(Hyps,Goal,Cont),sequent(NewHyps,Goal,Cont),Info) :-
718		ground(HypNr),
719		get_hyp(Hyps,HypNr,SelHyp),
720		parse_input(NewHyp,rewrite_hyp,TExpr),
721		b_interpreter_check:norm_pred_check(TExpr,RewrittenHyp),
722		select(SelHyp,Hyps,Hyps0),
723		get_wd_pos(RewrittenHyp,Hyps,Info,[]),
724		prove_predicate([SelHyp],RewrittenHyp),
725		translate_finite_expr(RewrittenHyp,NewExpr),
726		add_hyp(NewExpr,Hyps0,NewHyps).
727		trans_prop(rewrite_hyp,param_names(['HypNr','NewHyp'])).
728		symb_trans_enabled(rewrite_hyp,sequent(_,_,_)).
729
730		:- use_module(probsrc(tools),[split_atom/3]).
731		symb_trans(derive_hyp(HypNrs,NewHyp),sequent(Hyps,Goal,Cont),sequent(NewHyps,Goal,Cont),Info) :-
732		ground(HypNrs),
733		split_atom(HypNrs,[','],Indices),
734		maplist(get_hyp(Hyps),Indices,SelHyps),
735		parse_input(NewHyp,derive_hyp,TExpr),
736		b_interpreter_check:norm_pred_check(TExpr,NormExpr),
737		get_wd_pos(NormExpr,Hyps,Info,[]),
738		prove_predicate(SelHyps,NormExpr),
739		translate_finite_expr(NormExpr,NewExpr),
740		add_hyp(NewExpr,Hyps,NewHyps).
741		trans_prop(derive_hyp,param_names(['HypNrs','NewHyp'])).
742		symb_trans_enabled(derive_hyp,sequent(_,_,_)).
743
744		symb_trans(dis_binter_r(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps,NormExpr,sequent(Hyps,NewGoal,Cont)),Info) :-
745		parse_input(PFun,dis_binter_r,TExpr),
746		normalize_predicate(TExpr,NormExpr),
747		NormExpr = member(reverse(F),partial_function(A,B)),
748		type_expression(A,Info),
749		type_expression(B,Info),
750		Sub = image(F,Inter),
751		Inter = intersection(_,_),
752		is_subterm(Sub,Goal),
753		image_intersection(F,Inter,NewSub),
754		rewrite_once(Sub,NewSub,Goal,NewGoal).
755		trans_prop(dis_binter_r,param_names(['PFun'])).
756		symb_trans_enabled(dis_binter_r,sequent(_,Goal,_)) :- is_subterm(image(_,Inter),Goal), Inter = intersection(_,_).
757
758		symb_trans(dis_binter_l(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps0,NormExpr,sequent(Hyps1,Goal,Cont)),Info) :-
759		parse_input(PFun,dis_binter_l,TExpr),
760		normalize_predicate(TExpr,NormExpr),
761		NormExpr = member(reverse(F),partial_function(A,B)),
762		type_expression(A,Info),
763		type_expression(B,Info),
764		select(Hyp,Hyps,Hyps0),
765		Sub = image(F,Inter),
766		Inter = intersection(_,_),
767		is_subterm(Sub,Hyp),
768		Inter = intersection(_,_),
769		image_intersection(F,Inter,NewSub),
770		rewrite(Sub,NewSub,Hyp,NewHyp),
771		add_hyp(NewHyp,Hyps0,Hyps1).
772		trans_prop(dis_binter_l,param_names(['PFun'])).
773		symb_trans_enabled(dis_binter_l,sequent(Hyps,_,_)) :- member(Hyp,Hyps), is_subterm(image(_,Inter),Hyp), Inter = intersection(_,_).
774
775		symb_trans(dis_setminus_r(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps,NormExpr,sequent(Hyps,NewGoal,Cont)),Info) :-
776		parse_input(PFun,dis_setminus_r,TExpr),
777		normalize_predicate(TExpr,NormExpr),
778		NormExpr = member(reverse(F),partial_function(A,B)),
779		type_expression(A,Info),
780		type_expression(B,Info),
781		rewrite(image(F,set_subtraction(S,T)),set_subtraction(image(F,S),image(F,T)),Goal,NewGoal).
782		trans_prop(dis_setminus_r,param_names(['PFun'])).
783		symb_trans_enabled(dis_setminus_r,sequent(_,Goal,_)) :- is_subterm(image(_,set_subtraction(_,_)),Goal).
784
785		symb_trans(dis_setminus_l(PFun),sequent(Hyps,Goal,Cont),sequent(Hyps0,NormExpr,sequent(Hyps1,Goal,Cont)),Info) :-
786		parse_input(PFun,dis_setminus_l,TExpr),
787		normalize_predicate(TExpr,NormExpr), !,
788		NormExpr = member(reverse(F),partial_function(A,B)),
789		type_expression(A,Info),
790		type_expression(B,Info),
791		select(Hyp,Hyps,Hyps0),
792		is_subterm(image(_,set_subtraction(_,_)),Hyp),
793		rewrite(image(F,set_subtraction(S,T)),set_subtraction(image(F,S),image(F,T)),Hyp,NewHyp),
794		add_hyp(NewHyp,Hyps0,Hyps1).
795		trans_prop(dis_setminus_l,param_names(['PFun'])).
796		symb_trans_enabled(dis_setminus_l,sequent(Hyps,_,_)) :- member(Hyp,Hyps), is_subterm(image(_,set_subtraction(_,_)),Hyp).
797
798		symb_trans(fin_subseteq_r(Set),sequent(Hyps,finite(S),Cont),NewSequent,Info) :-
799		parse_input(Set,fin_subseteq_r,TExpr),
800		normalize_expression(TExpr,NormExpr),
801		get_meta_info(ids_types,Info,IdsTypes), % NormExpr has to be a set
802		same_type(S,NormExpr,IdsTypes),
803		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
804		add_wd_pos(Hyps,POs,sequent(Hyps,subset(S,NormExpr),sequent(Hyps,finite(NormExpr),Cont)),NewSequent).
805		trans_prop(fin_subseteq_r,param_names(['Set'])).
806		symb_trans_enabled(fin_subseteq_r,sequent(_,finite(_),_)).
807
808		symb_trans(fin_fun1_r(PFun),sequent(Hyps,finite(F),Cont),NewSequent,Info) :-
809		parse_input(PFun,fin_fun1_r,TExpr),
810		normalize_expression(TExpr,NormExpr),
811		NormExpr = partial_function(S,T),
812		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
813		add_wd_pos(Hyps,POs,sequent(Hyps,member(F,partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
814		trans_prop(fin_fun1_r,param_names(['PFun'])).
815		symb_trans_enabled(fin_fun1_r,sequent(_,finite(_),_)).
816
817		symb_trans(fin_fun2_r(PFun),sequent(Hyps,finite(F),Cont),NewSequent,Info) :-
818		parse_input(PFun,fin_fun2_r,TExpr),
819		normalize_expression(TExpr,NormExpr),
820		NormExpr = partial_function(S,T),
821		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
822		add_wd_pos(Hyps,POs,sequent(Hyps,member(reverse(F),partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
823		trans_prop(fin_fun2_r,param_names(['PFun'])).
824		symb_trans_enabled(fin_fun2_r,sequent(_,finite(_),_)).
825
826		symb_trans(fin_fun_img_r(PFun),sequent(Hyps,finite(image(F,Set)),Cont),NewSequent,Info) :-
827		parse_input(PFun,fin_fun_img_r,TExpr),
828		normalize_expression(TExpr,NormExpr),
829		NormExpr = partial_function(S,T),
830		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
831		add_wd_pos(Hyps,POs,sequent(Hyps,member(F,partial_function(S,T)),sequent(Hyps,finite(Set),Cont)),NewSequent).
832		trans_prop(fin_fun_img_r,param_names(['PFun'])).
833		symb_trans_enabled(fin_fun_img_r,sequent(_,finite(image(_,_)),_)).
834
835		symb_trans(fin_fun_ran_r(PFun),sequent(Hyps,finite(range(F)),Cont),NewSequent,Info) :-
836		parse_input(PFun,fin_fun_ran_r,TExpr),
837		normalize_expression(TExpr,NormExpr),
838		NormExpr = partial_function(S,T),
839		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
840		add_wd_pos(Hyps,POs,sequent(Hyps,member(F,partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
841		trans_prop(fin_fun_ran_r,param_names(['PFun'])).
842		symb_trans_enabled(fin_fun_ran_r,sequent(_,finite(range(_)),_)).
843
844		symb_trans(fin_fun_dom_r(PFun),sequent(Hyps,finite(domain(F)),Cont),NewSequent,Info) :-
845		parse_input(PFun,fin_fun_dom_r,TExpr),
846		normalize_expression(TExpr,NormExpr),
847		NormExpr = partial_function(S,T),
848		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
849		add_wd_pos(Hyps,POs,sequent(Hyps,member(reverse(F),partial_function(S,T)),sequent(Hyps,finite(S),Cont)),NewSequent).
850		trans_prop(fin_fun_dom_r,param_names(['PFun'])).
851		symb_trans_enabled(fin_fun_dom_r,sequent(_,finite(domain(_)),_)).
852
853		symb_trans(fin_rel_r(Rel),sequent(Hyps,finite(R),Cont),NewSequent,Info) :-
854		parse_input(Rel,fin_rel_r,TExpr),
855		normalize_expression(TExpr,NormExpr), !,
856		NormExpr = relations(S,T),
857		get_wd_pos_of_expr(NormExpr,Hyps,Info,POs),
858		add_wd_pos(Hyps,POs,sequent(Hyps,member(R,relations(S,T)),sequent(Hyps,finite(S),sequent(Hyps,finite(T),Cont))),NewSequent).
859		trans_prop(fin_rel_r,param_names(['Rel'])).
860		symb_trans_enabled(fin_rel_r,sequent(_,finite(_),_)).
861
862		parse_input(Param,Res) :- parse_input(Param,'?',Res).
863		parse_input(Param,Context,Res) :-
864		ground(Param),
865		(number(Param) -> number_codes(Param,CParam)
866		; Param = [Nr|_], number(Nr) -> CParam = Param % already codes list
867		; atom(Param) -> atom_codes(Param,CParam)
868		; ajoin(['Illegal input to proof rule ',Context,' (must be Prolog atom or string):'],Msg),
869		add_error(sequent_prover,Msg,Param), fail
870		),
871		bmachine:b_parse_only(formula,CParam,Parsed,_,_Error),
872		transform_raw(Parsed,TExpr),
873		adapt_for_eventb(TExpr,Res).
874
875		adapt_for_eventb(Term,Term) :- atomic(Term).
876		adapt_for_eventb(Term,Result) :-
877		Term=..[F|Args],
878		replace_functor(F,NewFunctor),
879		maplist(adapt_for_eventb,Args,NewArgs),
880		Result=..[NewFunctor|NewArgs].
881
882		replace_functor(concat,power_of).
883		replace_functor(power_of,cartesian_product).
884		replace_functor(minus_or_set_subtract,minus).
885		replace_functor(mult_or_cart,multiplication).
886		replace_functor(F,F).
887
888		translate_finite_expr(X,Y) :- rewrite(member(S,fin_subset(S)),finite(S),X,Y).
889
890		get_hyp(Hyps,Index,Hyp) :-
891		atom_codes(Index,C),
892		number_codes(Nr,C),
893		nth1(Nr,Hyps,Hyp).
894
895		add_hyp(Hyp,Hyps0,NewHyps) :- append(Hyps0,[Hyp],Hyps1), without_duplicates(Hyps1,NewHyps).
896		add_hyps(Hyp1,Hyp2,Hyps0,NewHyps) :- append(Hyps0,[Hyp1,Hyp2],Hyps1), without_duplicates(Hyps1,NewHyps).
897		add_hyps(NewHyps,Hyps,SHyps) :- append(Hyps,NewHyps,All), without_duplicates(All,SHyps).
898
899		% select and remove a conjunct:
900		select_conjunct(X,conjunct(A,B),Rest) :- !,
901		(select_conjunct(X,A,RA), conjoin(RA,B,Rest)
902		;
903		select_conjunct(X,B,RB), conjoin(A,RB,Rest)).
904		select_conjunct(X,X,truth).
905
906		conjoin(truth,X,R) :- !, R=X.
907		conjoin(X,truth,R) :- !, R=X.
908		conjoin(X,Y,conjunct(X,Y)).
909
910		% select and remove (first occurrence of) X:
911		select_op(X,C,Rest,Op) :- C=..[Op,A,B],
912	?	(select_op(X,A,RA,Op), conjoin(RA,B,Rest,Op)
913		;
914	?	select_op(X,B,RB,Op), conjoin(A,RB,Rest,Op)), !.
915		select_op(X,X,E,Op) :- neutral_element(Op,E).
916		select_op(X,Y,E,Op) :- neutral_element(Op,E), equal_terms(X,Y).
917
918		% replace (first occurrence of) X by Z:
919		select_op(X,C,Z,New,Op) :- C=..[Op,A,B],
920		(select_op(X,A,Z,RA,Op), conjoin(RA,B,New,Op) ;
921		select_op(X,B,Z,RB,Op), conjoin(A,RB,New,Op)), !.
922		select_op(X,X,Z,Z,_) :- !.
923		select_op(X,Y,Z,Z,_) :- equal_terms(X,Y).
924
925		conjoin(E,X,R,Op) :- neutral_element(Op,E), !, R=X.
926		conjoin(X,E,R,Op) :- neutral_element(Op,E), !, R=X.
927		conjoin(X,Y,C,Op) :- C=..[Op,X,Y].
928
929		neutral_element(conjunct,true) :- !.
930		neutral_element(disjunct,false) :- !.
931		neutral_element(add,0) :- !.
932		neutral_element(multiplication,1) :- !.
933		neutral_element(_,placeholder).
934
935		negate(truth,Res) :- !, Res=falsity.
936		negate(falsity,Res) :- !, Res=truth.
937		negate(equal(X,Y),R) :- !, R=not_equal(X,Y).
938		negate(not_equal(X,Y),R) :- !, R=equal(X,Y).
939		negate(greater(X,Y),R) :- !, R=less_equal(X,Y).
940		negate(less(X,Y),R) :- !, R=greater_equal(X,Y).
941		negate(greater_equal(X,Y),R) :- !, R=less(X,Y).
942		negate(less_equal(X,Y),R) :- !, R=greater(X,Y).
943		negate(disjunct(X,Y),R) :- !, R=conjunct(NX,NY), negate(X,NX), negate(Y,NY).
944		negate(conjunct(X,Y),R) :- !, R=disjunct(NX,NY), negate(X,NX), negate(Y,NY).
945		negate(implication(X,Y),R) :- !, R=conjunct(X,NY), negate(Y,NY).
946		negate(negation(X),R) :- !, R=X.
947		negate(P,negation(P)).
948
949		is_fun(partial_function(DOM,RAN),partial,DOM,RAN).
950		is_fun(partial_injection(DOM,RAN),partial,DOM,RAN).
951		is_fun(partial_surjection(DOM,RAN),partial,DOM,RAN).
952		is_fun(partial_bijection(DOM,RAN),partial,DOM,RAN).
953		is_fun(total_function(DOM,RAN),total,DOM,RAN).
954		is_fun(total_injection(DOM,RAN),total,DOM,RAN).
955		is_fun(total_surjection(DOM,RAN),total,DOM,RAN).
956		is_fun(total_bijection(DOM,RAN),total,DOM,RAN).
957
958		is_rel(F,Type,DOM,RAN) :- is_fun(F,Type,DOM,RAN).
959		is_rel(relations(DOM,RAN),partial,DOM,RAN).
960		is_rel(total_relation(DOM,RAN),total,DOM,RAN).
961		is_rel(surjection_relation(DOM,RAN),partial,DOM,RAN).
962		is_rel(total_surjection_relation(DOM,RAN),total,DOM,RAN).
963
964		is_surj(total_bijection(DOM,RAN),DOM,RAN).
965		is_surj(total_surjection(DOM,RAN),DOM,RAN).
966		is_surj(partial_surjection(DOM,RAN),DOM,RAN).
967		is_surj(surjection_relation(DOM,RAN),DOM,RAN).
968		is_surj(total_surjection_relation(DOM,RAN),DOM,RAN).
969
970		is_inj(partial_injection(DOM,RAN),DOM,RAN).
971		is_inj(partial_bijection(DOM,RAN),DOM,RAN).
972		is_inj(total_injection(DOM,RAN),DOM,RAN).
973		is_inj(total_bijection(DOM,RAN),DOM,RAN).
974
975		% rewrite X to E
976		rewrite(X,Y,E,NewE) :- equal_terms(X,E),!, NewE=Y.
977		rewrite(_X,_Y,E,NewE) :- atomic(E),!, NewE=E.
978		rewrite(_X,_Y,'$'(E),NewE) :- atomic(E),!, NewE='$'(E).
979		rewrite(X,_,E,NewE) :- with_ids(E,Ids), member(X,Ids),!, NewE=E.
980		rewrite(X,Y,C,NewC) :- C=..[Op|Args],
981		maplist(rewrite(X,Y), Args,NewArgs),
982		NewC =.. [Op|NewArgs].
983
984		with_ids(exists(Ids,_),Ids).
985		with_ids(event_b_comprehension_set(Ids,_),Ids).
986		with_ids(forall(Ids,_,_),Ids).
987		with_ids(quantified_union(Ids,_,_),Ids).
988		with_ids(quantified_intersection(Ids,_,_),Ids).
989
990		% axioms: proof rules without antecedent, discharging goal directly
991		axiom(hyp,Hyps,Goal) :- member_hyps(Goal,Hyps).
992		axiom(hyp,Hyps,member(X,Nat)) :-
993		is_natural_set(Nat),
994		(member_hyps(greater_equal(X,0),Hyps) ; member_hyps(greater_equal(X,1),Hyps)).
995		axiom(hyp_or,Hyps,Goal) :- member_of(disjunct,P,Goal), member_hyps(P,Hyps).
996		axiom(false_hyp,Hyps,_Goal) :- member_hyps(falsity,Hyps).
997		axiom(true_goal,_,truth).
998		axiom(Rule,_Hyps,Goal) :- axiom_wo_hyps(Goal,Rule).
999		axiom(cntr,Hyps,_) :-
1000		member(P,Hyps),
1001		(NotP = negation(P) ; negate(P,NotP)),
1002		select(P,Hyps,Hyps0),
1003		member_hyps(NotP,Hyps0).
1004		axiom(fin_rel,Hyps,finite(Fun)) :-
1005		member_hyps(member(Fun,FunType),Hyps),
1006		is_rel(FunType,_,Dom,Ran),
1007		member_hyps(finite(Dom),Hyps),
1008		member_hyps(finite(Ran),Hyps).
1009		axiom(fin_l_lower_bound,Hyps,exists([N],forall([X],member(X,S),LessEq))) :-
1010		member_hyps(finite(S),Hyps),
1011		is_less_eq(LessEq,N,X).
1012		axiom(fin_l_upper_bound,Hyps,exists([N],forall([X],member(X,S),LessEq))) :-
1013		member_hyps(finite(S),Hyps),
1014		is_less_eq(LessEq,X,N).
1015	?	axiom(derive_goal,Hyps,Goal) :- derive_goal(Hyps,Goal), \+ is_true(Goal), \+ axiom(hyp,Hyps,Goal).
1016
1017		% from chapter 2, "Modeling in Event-B"
1018		axiom(p2,Hyps,member(Add,Nat)) :-
1019		is_natural_set(Nat),
1020		member(member(N,Nat),Hyps),
1021		equal_terms(Add,add(N,1)).
1022		axiom(p2_,Hyps,member(Sub,Nat)) :-
1023		is_natural_set(Nat),
1024		member(L,Hyps),
1025		is_less(L,0,N),
1026		equal_terms(Sub,minus(N,1)).
1027		axiom(inc,Hyps,Goal) :-
1028		member(L,Hyps),
1029		is_less(L,N,M),
1030		equal_terms(Goal,less_equal(add(N,1),M)).
1031		axiom(dec,Hyps,Goal) :-
1032		member(L,Hyps),
1033		is_less_eq(L,N,M),
1034		equal_terms(Goal,less(minus(N,1),M)).
1035
1036		axiom2(fun_goal(member(F,FType)),Hyps,member(F,PFType)) :-
1037		is_fun(PFType,partial,_,_),
1038		member_hyps(member(F,FType),Hyps),
1039		is_fun(FType,_,_,_).
1040
1041		axiom_wo_hyps(true,true_goal).
1042		axiom_wo_hyps(eq(E,E),eql).
1043
1044		member_hyps(Goal,Hyps) :-
1045	?	(member(Goal,Hyps) -> true
1046		; equiv(Goal,G2), member(G2,Hyps) -> true), !.
1047		member_hyps(Goal,Hyps) :-
1048		ground(Goal),
1049	?	member(G2,Hyps),
1050		comparable(Goal,G2),
1051		list_representation(Goal,L1),
1052		list_representation(G2,L2),
1053		equal_length(L1,L2),
1054		stronger_list(L2,L1).
1055
1056		% replace by normalisation
1057		equiv(equal(A,B),equal(B,A)).
1058		equiv(not_equal(A,B),not_equal(B,A)).
1059		equiv(greater(A,B),less(B,A)).
1060		equiv(less(A,B),greater(B,A)).
1061		equiv(greater_equal(A,B),less_equal(B,A)).
1062		equiv(less_equal(A,B),greater_equal(B,A)).
1063
1064		derive_goal(Hyps,Goal) :-
1065		Goal=..[F,_,_],
1066		(comparison(F) ; F = member),
1067		used_identifiers(Goal,GoalIds),
1068	?	find_hyps_with(GoalIds,Hyps,SelectedHyps),
1069		use_prover(prob_wd_prover,SelectedHyps,Goal).
1070
1071		find_hyps_with(_,[],[]).
1072		find_hyps_with(Ids,[Hyp|T],[Hyp|R]) :-
1073		used_identifiers(Hyp,HypIds),
1074		\+ list_intersection(Ids,HypIds,[]), !,
1075		find_hyps_with(Ids,T,R).
1076		find_hyps_with(Ids,[_|T],R) :- find_hyps_with(Ids,T,R).
1077
1078		/* not used:
1079		is_transitive(Hyps,Goal) :-
1080		Goal=..[F,L,R],
1081		comparison(F),
1082		F \= not_equal,
1083		is_transitive_aux(Hyps,F,L,R,[]).
1084
1085		is_transitive_aux(Hyps,F,L,R,_) :-
1086		Ex=..[F,L,R],
1087		(member(Ex,Hyps) ; equiv(Ex,G2), member(G2,Hyps)).
1088		is_transitive_aux(Hyps,F,L,R,Visited) :-
1089		Ex=..[F,L,M],
1090		(member(Ex,Hyps) ; equiv(Ex,G2), member(G2,Hyps)),
1091		\+ member(M,Visited),
1092		is_transitive_aux(Hyps,F,M,R,[L|Visited]).
1093
1094		lower_bound(Hyps,B,X) :- member(L,Hyps), is_less_eq(L,B,X), number(B).
1095		lower_bound(Hyps,B1,X) :- member(L,Hyps), is_less(L,B,X), number(B), B1 is B+1.
1096		lower_bound(Hyps,B,X) :- member(Eq,Hyps), is_equality(Eq,B,X), number(B).
1097
1098		upper_bound(Hyps,X,B) :- member(L,Hyps),is_less_eq(L,X,B), number(B).
1099		upper_bound(Hyps,X,B1) :- member(L,Hyps), is_less(L,X,B), number(B), B1 is B-1.
1100		upper_bound(Hyps,X,B) :- member(Eq,Hyps), is_equality(Eq,X,B), number(B).
1101		*/
1102
1103
1104		% simp_rule/6
1105		simp_rule(X,NewX,Rule,Op,Descr,Info) :-
1106	?	(simp_rule(X,NewX,Rule)
1107	?	; simp_rule(X,NewX,Rule,Op)
1108	?	; simp_rule(X,NewX,Rule,Op,Info)
1109	?	; simp_rule_with_info(X,NewX,Rule,Info)),
1110		create_descr(Rule,X,Descr).
1111		simp_rule(X,NewX,Rule,_,Descr,_) :- simp_rule_with_descr(X,NewX,Rule,Descr).
1112		simp_rule(Expr,Res,Expr,_,Descr,_) :- compute(Expr,Res), create_descr('Compute',Expr,Descr).
1113		% allow simplifications deeper inside the term:
1114		simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,P], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,Q].
1115	?	simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,P,R], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,Q,R].
1116	?	simp_rule(C,NewC,Rule,_,Descr,Info) :- C=..[F,R,P], simp_rule(P,Q,Rule,F,Descr,Info), NewC=..[F,R,Q].
1117
1118
1119		% simp_rule/5
1120		simp_rule(U,Ty,'SIMP_TYPE_BUNION',OuterOp,Info) :- OuterOp \= union,
1121	?	member_of(union,Ty,U), type_expression(Ty,Info).
1122		simp_rule(Over,Res,'SIMP_TYPE_OVERL_CPROD',OuterOp,Info) :-
1123		OuterOp \= overwrite,
1124		Over = overwrite(_,_),
1125		op_to_list(Over,List,overwrite),
1126		overwrite_type(List,[],ResList,Info),
1127		List \= ResList,
1128	?	list_to_op(ResList,Res,overwrite).
1129
1130		% rules that do not require hyps:
1131		simp_rule(not_equal(L,L),falsity,'SIMP_MULTI_NOTEQUAL').
1132		simp_rule(less_equal(I,J),Res,'SIMP_LIT_LE') :- number(I), number(J), (I =< J -> Res=truth ; Res=falsity). % where I and J are literals
1133		simp_rule(less(I,J),Res,'SIMP_LIT_LT') :- number(I), number(J), (I < J -> Res=truth ; Res=falsity).
1134		simp_rule(greater_equal(I,J),Res,'SIMP_LIT_GE') :- number(I), number(J), (I >= J -> Res=truth ; Res=falsity).
1135		simp_rule(greater(I,J),Res,'SIMP_LIT_GT') :- number(I), number(J), (I > J -> Res=truth ; Res=falsity).
1136		simp_rule(equal(I,J),Res,'SIMP_LIT_EQUAL') :- number(I), number(J), (I = J -> Res=truth ; Res=falsity).
1137		simp_rule(not_equal(L,R),negation(equal(L,R)),'SIMP_NOTEQUAL').
1138		simp_rule(domain(event_b_comprehension_set(Ids,couple(E,_),P)),event_b_comprehension_set(Ids,E,P),'SIMP_DOM_LAMBDA').
1139		simp_rule(range(event_b_comprehension_set(Ids,couple(_,F),P)),event_b_comprehension_set(Ids,F,P),'SIMP_RAN_LAMBDA').
1140		simp_rule(negation(equal(Set,empty_set)),exists([X],member(X,Set)),'DEF_SPECIAL_NOT_EQUAL') :- new_identifier(Set,X).
1141		simp_rule(Expr,Res,'SIMP_SETENUM_EQUAL_EMPTY') :-is_empty(Expr,set_extension(L)), length(L,LL),
1142		(LL > 0 -> Res = falsity ; Res = truth).
1143		simp_rule(Expr,greater(I,J),'SIMP_UPTO_EQUAL_EMPTY') :- is_empty(Expr,interval(I,J)).
1144		simp_rule(Eq,falsity,'SIMP_UPTO_EQUAL_INTEGER') :- is_equality(Eq,interval(_,_),Z), is_integer_set(Z).
1145		simp_rule(Eq,falsity,'SIMP_UPTO_EQUAL_NATURAL') :- is_equality(Eq,interval(_,_),Nat), is_natural_set(Nat).
1146		simp_rule(Eq,falsity,'SIMP_UPTO_EQUAL_NATURAL1') :- is_equality(Eq,interval(_,_),Nat), is_natural1_set(Nat).
1147		simp_rule(Expr,falsity,'SIMP_SPECIAL_EQUAL_REL') :- is_empty(Expr,relations(_,_)).
1148		simp_rule(Expr,conjunct(negation(equal(A,empty_set)),equal(B,empty_set)),'SIMP_SPECIAL_EQUAL_RELDOM') :-
1149		is_empty(Expr,R),
1150		(R = total_relation(A,B) ;
1151		R = total_function(A,B)).
1152		simp_rule(Expr,conjunct(equal(A,empty_set),negation(equal(B,empty_set))),'SIMP_SREL_EQUAL_EMPTY') :-
1153		is_empty(Expr,surjection_relation(A,B)).
1154		simp_rule(Expr,equivalence(equal(A,empty_set),negation(equal(B,empty_set))),'SIMP_STREL_EQUAL_EMPTY') :-
1155		is_empty(Expr,total_surjection_relation(A,B)).
1156		simp_rule(Expr,equal(R,empty_set),'SIMP_DOM_EQUAL_EMPTY') :- is_empty(Expr,domain(R)).
1157		simp_rule(Expr,equal(R,empty_set),'SIMP_RAN_EQUAL_EMPTY') :- is_empty(Expr,range(R)).
1158		simp_rule(Expr,equal(intersection(range(P),domain(Q)),empty_set),'SIMP_FCOMP_EQUAL_EMPTY') :- is_empty(Expr,composition(P,Q)).
1159		simp_rule(Expr,equal(intersection(range(Q),domain(P)),empty_set),'SIMP_BCOMP_EQUAL_EMPTY') :- is_empty(Expr,ring(P,Q)).
1160		simp_rule(Expr,equal(intersection(domain(R),S),empty_set),'SIMP_DOMRES_EQUAL_EMPTY') :- is_empty(Expr,domain_restriction(S,R)).
1161		simp_rule(Expr,subset(domain(R),S),'SIMP_DOMSUB_EQUAL_EMPTY') :- is_empty(Expr,domain_subtraction(S,R)).
1162		simp_rule(Expr,equal(intersection(range(R),S),empty_set),'SIMP_RANRES_EQUAL_EMPTY') :- is_empty(Expr,range_restriction(R,S)).
1163		simp_rule(Expr,subset(range(R),S),'SIMP_RANSUB_EQUAL_EMPTY') :- is_empty(Expr,range_subtraction(R,S)).
1164		simp_rule(Expr,equal(R,empty_set),'SIMP_CONVERSE_EQUAL_EMPTY') :- is_empty(Expr,reverse(R)).
1165		simp_rule(Expr,equal(domain_restriction(S,R),empty_set),'SIMP_RELIMAGE_EQUAL_EMPTY') :- is_empty(Expr,image(R,S)).
1166		simp_rule(Expr,Res,'SIMP_OVERL_EQUAL_EMPTY') :- is_empty(Expr,Over), Over = overwrite(_,_), and_empty(Over,Res,overwrite).
1167		simp_rule(Expr,equal(intersection(domain(P),domain(Q)),empty_set),'SIMP_DPROD_EQUAL_EMPTY') :- is_empty(Expr,direct_product(P,Q)).
1168		simp_rule(Expr,disjunct(equal(P,empty_set),equal(Q,empty_set)),'SIMP_PPROD_EQUAL_EMPTY') :- is_empty(Expr,parallel_product(P,Q)).
1169		simp_rule(Expr,falsity,'SIMP_ID_EQUAL_EMPTY') :- is_empty(Expr,event_b_identity).
1170		simp_rule(Expr,falsity,'SIMP_PRJ1_EQUAL_EMPTY') :- is_empty(Expr,event_b_first_projection_v2).
1171		simp_rule(Expr,falsity,'SIMP_PRJ2_EQUAL_EMPTY') :- is_empty(Expr,event_b_second_projection_v2).
1172		simp_rule(Eq,P,'SIMP_LIT_EQUAL_KBOOL_TRUE') :- is_equality(Eq,convert_bool(P),boolean_true).
1173		simp_rule(Eq,negation(P),'SIMP_LIT_EQUAL_KBOOL_FALSE') :- is_equality(Eq,convert_bool(P),boolean_false).
1174		simp_rule(convert_bool(Eq),P,'SIMP_KBOOL_LIT_EQUAL_TRUE') :- is_equality(Eq,P,boolean_true).
1175		simp_rule(implication(truth,P),P,'SIMP_SPECIAL_IMP_BTRUE_L').
1176		simp_rule(implication(P,falsity),negation(P),'SIMP_SPECIAL_IMP_BFALSE_R').
1177		simp_rule(not_member(L,R),negation(member(L,R)),'SIMP_NOTIN').
1178		simp_rule(not_subset_strict(L,R),negation(subset_strict(L,R)),'SIMP_NOTSUBSET').
1179		simp_rule(not_subset(L,R),negation(subset(L,R)),'SIMP_NOTSUBSETEQ').
1180		simp_rule(I,equal(E,boolean_true),'SIMP_SPECIAL_NOT_EQUAL_FALSE') :- is_no_equality(I,E,boolean_false).
1181	?	simp_rule(I,equal(E,boolean_false),'SIMP_SPECIAL_NOT_EQUAL_TRUE') :- is_no_equality(I,E,boolean_true).
1182		simp_rule(forall(X,P1,P2),Res,'SIMP_FORALL_AND') :- P2 = conjunct(_,_), distribute_forall(X,P1,P2,Res).
1183		simp_rule(exists(X,D),Res,'SIMP_EXISTS_OR') :- D = disjunct(_,_), distribute_exists(X,D,Res).
1184		simp_rule(exists(X,implication(P,Q)),implication(forall(X,truth,P),exists(X,Q)),'SIMP_EXISTS_IMP').
1185	?	simp_rule(forall(L,P1,P2),forall(Used,P1,P2),'SIMP_FORALL') :- remove_unused_identifier(L,P1,Used).
1186		simp_rule(exists(L,P),exists(Used,P),'SIMP_EXISTS') :- remove_unused_identifier(L,P,Used).
1187		simp_rule(negation(forall(X,P1,P2)),exists(X,negation(implication(P1,P2))),'DERIV_NOT_FORALL').
1188		simp_rule(negation(exists(X,P)),forall(X,truth,negation(P)),'DERIV_NOT_EXISTS').
1189		simp_rule(event_b_comprehension_set(Ids,E,P),event_b_comprehension_set(Used,E,P),'SIMP_COMPSET') :- % own rule
1190		remove_unused_identifier(Ids,P,Used).
1191		simp_rule(equal(boolean_true,boolean_false),falsity,'SIMP_SPECIAL_EQUAL_TRUE').
1192		simp_rule(equal(couple(E,F),couple(G,H)),conjunct(equal(E,G),equal(F,H)),'SIMP_EQUAL_MAPSTO').
1193		simp_rule(equal(SetE,SetF),equal(E,F),'SIMP_EQUAL_SING') :- singleton_set(SetE,E),singleton_set(SetF,F).
1194		simp_rule(set_subtraction(S,S),empty_set,'SIMP_MULTI_SETMINUS').
1195		simp_rule(set_subtraction(S,empty_set),S,'SIMP_SPECIAL_SETMINUS_R').
1196		simp_rule(set_subtraction(empty_set,_),empty_set,'SIMP_SPECIAL_SETMINUS_L').
1197		simp_rule(member(E,set_subtraction(_,set_extension(L))),falsity,'DERIV_MULTI_IN_SETMINUS') :- member(F,L), equal_terms(E,F).
1198		simp_rule(member(E,U),truth,'DERIV_MULTI_IN_BUNION') :- U = union(_,_),
1199		member_of(union,set_extension(L),U),
1200		member(F,L),
1201		equal_terms(E,F).
1202		simp_rule(convert_bool(truth),boolean_true,'SIMP_SPECIAL_KBOOL_BTRUE').
1203		simp_rule(convert_bool(falsity),boolean_false,'SIMP_SPECIAL_KBOOL_BFALSE').
1204		simp_rule(subset(Union,T),Res,'DISTRI_SUBSETEQ_BUNION_SING') :-
1205	?	member_of(union,SetF,Union),
1206		singleton_set(SetF,_),
1207		union_subset_member(T,Union,Res).
1208		simp_rule(finite(S),exists([N,F],member(F,total_bijection(interval(1,N),S))),'DEF_FINITE') :-
1209		new_identifier(S,N),
1210		new_function(S,F).
1211		simp_rule(finite(U),Conj,'SIMP_FINITE_BUNION') :- U = union(_,_), finite_union(U,Conj).
1212		simp_rule(finite(pow_subset(S)),finite(S),'SIMP_FINITE_POW').
1213		simp_rule(finite(cartesian_product(S,T)),disjunct(disjunct(equal(S,empty_set),equal(T,empty_set)),conjunct(finite(S),finite(T))),'DERIV_FINITE_CPROD').
1214		simp_rule(finite(reverse(R)),finite(R),'SIMP_FINITE_CONVERSE').
1215		simp_rule(finite(domain_restriction(E,event_b_identity)),finite(E),'SIMP_FINITE_ID_DOMRES').
1216		simp_rule(finite(domain_restriction(E,event_b_first_projection_v2)),finite(E),'SIMP_FINITE_PRJ1_DOMRES').
1217		simp_rule(finite(domain_restriction(E,event_b_second_projection_v2)),finite(E),'SIMP_FINITE_PRJ2_DOMRES').
1218		simp_rule(finite(Nat),falsity,'SIMP_FINITE_NATURAL') :- is_natural_set(Nat).
1219		simp_rule(finite(Nat),falsity,'SIMP_FINITE_NATURAL1') :- is_natural1_set(Nat).
1220		simp_rule(finite(Z),falsity,'SIMP_FINITE_INTEGER') :- is_integer_set(Z).
1221		simp_rule(Eq,P,'SIMP_SPECIAL_EQV_BTRUE') :- is_equivalence(Eq,P,truth).
1222		simp_rule(Eq,negation(P),'SIMP_SPECIAL_EQV_BFALSE') :- is_equivalence(Eq,P,falsity).
1223		simp_rule(subset_strict(A,B),conjunct(subset(A,B),negation(equal(A,B))),'DEF_SUBSET').
1224		simp_rule(subset_strict(_,empty_set),falsity,'SIMP_SPECIAL_SUBSET_R').
1225		simp_rule(subset_strict(empty_set,S),negation(equal(S,empty_set)),'SIMP_SPECIAL_SUBSET_L').
1226		simp_rule(subset_strict(S,T),falsity,'SIMP_MULTI_SUBSET') :- equal_terms(S,T).
1227		simp_rule(C,Res,'DISTRI_PROD_PLUS') :- distri(C,Res,multiplication,add).
1228		simp_rule(C,Res,'DISTRI_PROD_MINUS') :- distri(C,Res,multiplication,minus).
1229	?	simp_rule(C,Res,'DISTRI_AND_OR') :- distri(C,Res,conjunct,disjunct).
1230		simp_rule(C,Res,'DISTRI_OR_AND') :- distri(C,Res,disjunct,conjunct).
1231		simp_rule(implication(P,Q),implication(negation(Q),negation(P)),'DERIV_IMP').
1232		simp_rule(implication(P,implication(Q,R)),implication(conjunct(P,Q),R),'DERIV_IMP_IMP').
1233		simp_rule(implication(P,C),Res,'DISTRI_IMP_AND') :- C = conjunct(_,_), and_imp(C,P,Res,conjunct).
1234		simp_rule(implication(D,R),Res,'DISTRI_IMP_OR') :- D = disjunct(_,_), and_imp(D,R,Res,disjunct).
1235		simp_rule(equivalence(P,Q),conjunct(implication(P,Q),implication(Q,P)),'DEF_EQV').
1236		simp_rule(C,P,'SIMP_SPECIAL_AND_BTRUE') :- C = conjunct(P,truth) ; C = conjunct(truth,P).
1237		simp_rule(D,P,'SIMP_SPECIAL_OR_BFALSE') :- D = disjunct(P,falsity) ; D = disjunct(falsity,P).
1238		simp_rule(implication(NotP,P),P,'SIMP_MULTI_IMP_NOT_L') :- is_negation(P,NotP).
1239		simp_rule(implication(P,NotP),NotP,'SIMP_MULTI_IMP_NOT_R') :- is_negation(P,NotP).
1240		simp_rule(Eq,falsity,'SIMP_MULTI_EQV_NOT') :- is_equivalence(Eq,P,NotP), is_negation(P,NotP).
1241		simp_rule(implication(C,Q),truth,'SIMP_MULTI_IMP_AND') :- member_of(conjunct,Q,C).
1242		simp_rule(negation(truth),falsity,'SIMP_SPECIAL_NOT_BTRUE').
1243		simp_rule(Expr,equal(set_subtraction(I0,C),empty_set),'SIMP_BINTER_SETMINUS_EQUAL_EMPTY') :-
1244		is_empty(Expr,I),
1245		member_of(intersection,set_subtraction(B,C),I),
1246		select_op(minus(B,C),I,B,I0,intersection).
1247		simp_rule(Expr,Res,'SIMP_BUNION_EQUAL_EMPTY') :- is_empty(Expr,Union), Union = union(_,_), and_empty(Union,Res,union).
1248	?	simp_rule(Expr,subset(A,B),'SIMP_SETMINUS_EQUAL_EMPTY') :- is_empty(Expr,set_subtraction(A,B)).
1249		simp_rule(Expr,forall([X],P,equal(E,empty_set)),'SIMP_QUNION_EQUAL_EMPTY') :- is_empty(Expr,quantified_union([X],P,E)).
1250		simp_rule(Expr,falsity,'SIMP_NATURAL_EQUAL_EMPTY') :- is_empty(Expr,Nat), is_natural_set(Nat).
1251		simp_rule(Expr,falsity,'SIMP_NATURAL1_EQUAL_EMPTY') :- is_empty(Expr,Nat), is_natural1_set(Nat).
1252		simp_rule(Expr,disjunct(equal(S,empty_set),equal(T,empty_set)),'SIMP_CPROD_EQUAL_EMPTY') :- is_empty(Expr,cartesian_product(S,T)).
1253		simp_rule(member(X,SetA),equal(X,A),'SIMP_IN_SING') :-
1254		singleton_set(SetA,A).
1255		simp_rule(subset(SetA,S),member(A,S),'SIMP_SUBSETEQ_SING') :- singleton_set(SetA,A).
1256		simp_rule(subset(Union,S),Conj,'DERIV_SUBSETEQ_BUNION') :- Union = union(_,_), union_subset(S,Union,Conj).
1257		simp_rule(subset(S,Inter),Conj,'DERIV_SUBSETEQ_BINTER') :- Inter = intersection(_,_), subset_inter(S,Inter,Conj).
1258		simp_rule(member(_,empty_set),falsity,'SIMP_SPECIAL_IN') .
1259		simp_rule(member(B,S),truth,'SIMP_MULTI_IN') :- S = set_extension(L), length(L,LL), LL > 1, member(B,L).
1260		simp_rule(set_extension(L),set_extension(Res),'SIMP_MULTI_SETENUM') :- remove_duplicates(L,Res).
1261		simp_rule(subset(S,U),truth,'SIMP_SUBSETEQ_BUNION') :- member_of(union,S,U).
1262		simp_rule(subset(I,S),truth,'SIMP_SUBSETEQ_BINTER') :- member_of(intersection,S,I).
1263		simp_rule(implication(C,negation(Q)),negation(C),'SIMP_MULTI_IMP_AND_NOT_R') :- member_of(conjunct,Q,C).
1264		simp_rule(implication(C,Q),negation(C),'SIMP_MULTI_IMP_AND_NOT_L') :- member_of(conjunct,negation(Q),C).
1265		simp_rule(U,S,'SIMP_SPECIAL_BUNION') :- U = union(S,empty_set) ; U = union(empty_set,S).
1266		simp_rule(Eq,subset(NewU,T),'SIMP_MULTI_EQUAL_BUNION') :-
1267		is_equality(Eq,U,T),
1268		member_of(union,T,U),
1269		remove_from_op(T,U,NewU,union).
1270		simp_rule(Eq,subset(T,NewI),'SIMP_MULTI_EQUAL_BINTER') :-
1271		is_equality(Eq,I,T),
1272		member_of(intersection,T,I),
1273		remove_from_op(T,I,NewI,intersection).
1274		simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_EQUAL_RELDOMRAN') :- R=..[Op,empty_set,empty_set],
1275		member(Op,[total_surjection,total_bijection,total_surjection_relation]).
1276		simp_rule(domain(cartesian_product(E,F)),E,'SIMP_MULTI_DOM_CPROD') :- equal_terms(E,F).
1277		simp_rule(range(cartesian_product(E,F)),E,'SIMP_MULTI_RAN_CPROD') :- equal_terms(E,F).
1278		simp_rule(image(cartesian_product(SetE,S),SetF),S,'SIMP_MULTI_RELIMAGE_CPROD_SING') :-
1279		singleton_set(SetE,E),
1280		singleton_set(SetF,F),
1281		equal_terms(E,F).
1282		simp_rule(image(set_extension([couple(E,G)]),SetF),set_extension([G]),'SIMP_MULTI_RELIMAGE_SING_MAPSTO') :-
1283		singleton_set(SetF,F),
1284		equal_terms(E,F).
1285		simp_rule(domain(domain_restriction(A,F)),intersection(domain(F),A),'SIMP_MULTI_DOM_DOMRES').
1286		simp_rule(domain(domain_subtraction(A,F)),set_subtraction(domain(F),A),'SIMP_MULTI_DOM_DOMSUB').
1287		simp_rule(range(range_restriction(F,A)),intersection(range(F),A),'SIMP_MULTI_RAN_RANRES').
1288		simp_rule(range(range_subtraction(F,A)),set_subtraction(range(F),A),'SIMP_MULTI_RAN_RANSUB').
1289		simp_rule(M,exists([Y],member(couple(R,Y),F)),'DEF_IN_DOM') :-
1290		M = member(R,domain(F)),
1291		new_identifier(M,Y).
1292		simp_rule(M,exists([X],member(couple(X,R),F)),'DEF_IN_RAN') :-
1293		M = member(R,range(F)),
1294		new_identifier(M,X).
1295		simp_rule(member(couple(E,F),reverse(R)),member(couple(F,E),R),'DEF_IN_CONVERSE').
1296		simp_rule(member(couple(E,F),domain_restriction(S,R)),conjunct(member(E,S),member(couple(E,F),R)),'DEF_IN_DOMRES').
1297		simp_rule(member(couple(E,F),range_restriction(R,T)),conjunct(member(couple(E,F),R),member(F,T)),'DEF_IN_RANRES').
1298		simp_rule(member(couple(E,F),domain_subtraction(S,R)),conjunct(not_member(E,S),member(couple(E,F),R)),'DEF_IN_DOMSUB').
1299		simp_rule(member(couple(E,F),range_subtraction(R,T)),conjunct(member(couple(E,F),R),not_member(F,T)),'DEF_IN_RANSUB').
1300		simp_rule(member(F,image(R,W)),exists([X],conjunct(member(X,W),member(couple(X,F),R))),'DEF_IN_RELIMAGE') :-
1301		new_identifier(image(R,W),X).
1302		simp_rule(M,exists(Ids,Res),'DEF_IN_FCOMP') :-
1303		M = member(couple(E,F),Comp),
1304		Comp = composition(_,_),
1305		op_to_list(Comp,List,composition),
1306		length(List,Length),
1307		L1 is Length - 1,
1308	?	new_identifiers(M,L1,Ids),
1309	?	member_couples(E,F,List,Ids,ConjList),
1310		list_to_op(ConjList,Res,conjunct).
1311		simp_rule(image(Comp,S),image(Q,image(P,S)),'DERIV_RELIMAGE_FCOMP') :- split_composition(Comp,P,Q).
1312
1313		simp_rule(composition(SetEF,SetGH),set_extension([couple(E,H)]),'DERIV_FCOMP_SING') :-
1314		singleton_set(SetEF,couple(E,F)),
1315		singleton_set(SetGH,couple(G,H)),
1316		equal_terms(F,G).
1317		simp_rule(overwrite(P,Q),union(domain_subtraction(domain(Q),P),Q),'DEF_OVERL').
1318		simp_rule(member(couple(E,F),event_b_identity),equal(E,F),'DEF_IN_ID').
1319		simp_rule(member(couple(E,couple(F,G)),direct_product(P,Q)),conjunct(member(couple(E,F),P),member(couple(E,G),Q)),'DEF_IN_DPROD').
1320		simp_rule(member(couple(couple(E,G),couple(F,H)),parallel_product(P,Q)),conjunct(member(couple(E,F),P),member(couple(G,H),Q)),'DEF_IN_PPROD').
1321		simp_rule(member(R,relations(S,T)),subset(R,cartesian_product(S,T)),'DEF_IN_REL').
1322		simp_rule(member(R,total_relation(S,T)),conjunct(member(R,relations(S,T)),equal(domain(R),S)),'DEF_IN_RELDOM').
1323		simp_rule(member(R,surjection_relation(S,T)),conjunct(member(R,relations(S,T)),equal(range(R),T)),'DEF_IN_RELRAN').
1324		simp_rule(member(R,total_surjection_relation(S,T)),conjunct(conjunct(member(R,relations(S,T)),equal(domain(R),S)),equal(range(R),T)),'DEF_IN_RELDOMRAN').
1325		simp_rule(M,conjunct(Conj1,Conj2),'DEF_IN_FCT') :-
1326		M = member(F,partial_function(S,T)),
1327		Conj1 = member(F,relations(S,T)),
1328		new_identifiers(M,3,Ids),
1329		Ids = [X,Y,Z],
1330		Conj2 = forall(Ids,conjunct(member(couple(X,Y),F),member(couple(X,Z),F)),equal(Y,Z)).
1331		simp_rule(member(X,total_function(Dom,Ran)),conjunct(Conj1,Conj2),'DEF_IN_TFCT') :-
1332		Conj1 = member(X,partial_function(Dom,Ran)),
1333		Conj2 = equal(domain(X),Dom).
1334		simp_rule(member(F,partial_injection(S,T)),conjunct(member(F,partial_function(S,T)),member(reverse(F),partial_function(T,S))),'DEF_IN_INJ').
1335		simp_rule(member(F,total_injection(S,T)),conjunct(member(F,partial_injection(S,T)),equal(domain(F),S)),'DEF_IN_TINJ').
1336		simp_rule(member(F,partial_surjection(S,T)),conjunct(member(F,partial_function(S,T)),equal(range(F),T)),'DEF_IN_SURJ').
1337		simp_rule(member(F,total_surjection(S,T)),conjunct(member(F,partial_surjection(S,T)),equal(domain(F),S)),'DEF_IN_TSURJ').
1338		simp_rule(member(F,total_bijection(S,T)),conjunct(member(F,total_injection(S,T)),equal(range(F),T)),'DEF_IN_BIJ').
1339		simp_rule(C,Res,'DISTRI_BCOMP_BUNION') :- distri_r(C,Res,ring,union).
1340		simp_rule(C,Res,'DISTRI_FCOMP_BUNION') :- distri(C,Res,composition,union).
1341	?	simp_rule(C,Res,'DISTRI_DPROD_BUNION') :- distri_r(C,Res,direct_product,union).
1342		simp_rule(C,Res,'DISTRI_DPROD_BINTER') :- distri_r(C,Res,direct_product,intersection).
1343		simp_rule(C,Res,'DISTRI_DPROD_SETMINUS') :- distri_r(C,Res,direct_product,set_subtraction).
1344		simp_rule(C,Res,'DISTRI_DPROD_OVERL') :- distri_r(C,Res,direct_product,overwrite).
1345		simp_rule(C,Res,'DISTRI_PPROD_BUNION') :- distri_r(C,Res,parallel_product,union).
1346		simp_rule(C,Res,'DISTRI_PPROD_BINTER') :- distri_r(C,Res,parallel_product,intersection).
1347		simp_rule(C,Res,'DISTRI_PPROD_SETMINUS') :- distri_r(C,Res,parallel_product,set_subtraction).
1348		simp_rule(C,Res,'DISTRI_PPROD_OVERL') :- distri_r(C,Res,parallel_product,overwrite).
1349	?	simp_rule(C,Res,'DISTRI_OVERL_BUNION_L') :- distri_l(C,Res,overwrite,union).
1350		simp_rule(C,Res,'DISTRI_OVERL_BINTER_L') :- distri_l(C,Res,overwrite,intersection).
1351		simp_rule(C,Res,'DISTRI_DOMRES_BUNION') :- distri(C,Res,domain_restriction,union).
1352		simp_rule(C,Res,'DISTRI_DOMRES_BINTER') :- distri(C,Res,domain_restriction,intersection).
1353		simp_rule(C,Res,'DISTRI_DOMRES_DPROD') :- distri_r(C,Res,domain_restriction,direct_product).
1354		simp_rule(C,Res,'DISTRI_DOMRES_OVERL') :- distri_r(C,Res,domain_restriction,overwrite).
1355		simp_rule(C,Res,'DISTRI_DOMRES_SETMINUS') :- distri(C,Res,domain_restriction,set_subtraction).
1356		simp_rule(C,Res,'DISTRI_DOMSUB_BUNION_R') :- distri_r(C,Res,domain_subtraction,union).
1357	?	simp_rule(C,Res,'DISTRI_DOMSUB_BUNION_L') :- distri_l(C,Res,domain_subtraction,union,intersection).
1358		simp_rule(C,Res,'DISTRI_DOMSUB_BINTER_R') :- distri_r(C,Res,domain_subtraction,intersection).
1359		simp_rule(C,Res,'DISTRI_DOMSUB_BINTER_L') :- distri_l(C,Res,domain_subtraction,intersection,union).
1360		simp_rule(C,Res,'DISTRI_DOMSUB_DPROD') :- distri_r(C,Res,domain_subtraction,direct_product).
1361		simp_rule(C,Res,'DISTRI_DOMSUB_OVERL') :- distri_r(C,Res,domain_subtraction,overwrite).
1362		simp_rule(C,Res,'DISTRI_RANRES_BUNION') :- distri(C,Res,range_restriction,union).
1363		simp_rule(C,Res,'DISTRI_RANRES_BINTER') :- distri(C,Res,range_restriction,intersection).
1364		simp_rule(C,Res,'DISTRI_RANRES_SETMINUS') :- distri(C,Res,range_restriction,set_subtraction).
1365	?	simp_rule(C,Res,'DISTRI_RANSUB_BUNION_R') :- distri_r(C,Res,range_subtraction,union,intersection).
1366	?	simp_rule(C,Res,'DISTRI_RANSUB_BUNION_L') :- distri_l(C,Res,range_subtraction,union).
1367	?	simp_rule(C,Res,'DISTRI_RANSUB_BINTER_R') :- distri_r(C,Res,range_subtraction,intersection,union).
1368		simp_rule(C,Res,'DISTRI_RANSUB_BINTER_L') :- distri_l(C,Res,range_subtraction,intersection).
1369		simp_rule(C,Res,'DISTRI_CONVERSE_BUNION') :- C = reverse(U), U = union(_,_), distri_reverse(U,Res,union).
1370		simp_rule(C,Res,'DISTRI_CONVERSE_BINTER') :- C = reverse(I), I = intersection(_,_), distri_reverse(I,Res,intersection).
1371		simp_rule(C,Res,'DISTRI_CONVERSE_SETMINUS') :- C = reverse(S), S = set_subtraction(_,_), distri_reverse(S,Res,set_subtraction).
1372		simp_rule(C,Res,'DISTRI_CONVERSE_BCOMP') :- C = reverse(R), R = ring(_,_), distri_reverse_reverse(R,Res,ring).
1373		simp_rule(C,Res,'DISTRI_CONVERSE_FCOMP') :- C = reverse(R), R = composition(_,_), distri_reverse_reverse(R,Res,composition).
1374		simp_rule(reverse(parallel_product(S,R)),parallel_product(reverse(S),reverse(R)),'DISTRI_CONVERSE_PPROD').
1375		simp_rule(reverse(domain_restriction(S,R)),range_restriction(reverse(R),S),'DISTRI_CONVERSE_DOMRES').
1376		simp_rule(reverse(domain_subtraction(S,R)),range_subtraction(reverse(R),S),'DISTRI_CONVERSE_DOMSUB').
1377		simp_rule(reverse(range_restriction(R,S)),domain_restriction(S,reverse(R)),'DISTRI_CONVERSE_RANRES').
1378		simp_rule(reverse(range_subtraction(R,S)),domain_subtraction(S,reverse(R)),'DISTRI_CONVERSE_RANSUB').
1379		simp_rule(domain(U),Res,'DISTRI_DOM_BUNION') :- U = union(_,_), distri_union(U,Res,domain).
1380		simp_rule(range(U),Res,'DISTRI_RAN_BUNION') :- U = union(_,_), distri_union(U,Res,range).
1381		simp_rule(image(R,U),Res,'DISTRI_RELIMAGE_BUNION_R') :- U = union(_,_), image_union(R,U,Res).
1382		simp_rule(image(U,S),Res,'DISTRI_RELIMAGE_BUNION_L') :- U = union(_,_), union_image(U,S,Res).
1383		simp_rule(member(LB,interval(LB,UB)),truth,'lower_bound_in_interval') :- number(LB), number(UB), LB =< UB. % own rule: lower bound in interval
1384		simp_rule(member(Nr,interval(LB,UB)),truth,'SIMP_IN_UPTO') :- number(LB), number(UB), number(Nr), LB =< Nr, Nr =< UB. % own rule
1385		simp_rule(member(Nr,interval(LB,UB)),falsity,'SIMP_IN_UPTO') :- number(LB), number(UB), number(Nr), (Nr =< LB ; UB =< Nr). % own rule
1386		simp_rule(member(E,U),Res,'DEF_IN_BUNION') :- U = union(_,_), member_union(E,U,Res).
1387		simp_rule(member(E,I),Res,'DEF_IN_BINTER') :- I = intersection(_,_), member_intersection(E,I,Res).
1388		simp_rule(member(couple(E,F),cartesian_product(S,T)),conjunct(member(E,S),member(F,T)),'DEF_IN_MAPSTO').
1389		simp_rule(member(E,pow_subset(S)),subset(E,S),'DEF_IN_POW').
1390		simp_rule(member(E,pow1_subset(S)),conjunct(member(E,pow_subset(S)),not_equal(S,empty_set)),'DEF_IN_POW1').
1391		simp_rule(S,forall([X],member(X,A),member(X,B)),'DEF_SUBSETEQ') :- S = subset(A,B), new_identifier(S,X).
1392		simp_rule(member(E,set_subtraction(S,T)),conjunct(member(E,S),negation(member(E,T))),'DEF_IN_SETMINUS').
1393		simp_rule(member(E,set_extension(L)),D,'DEF_IN_SETENUM') :- L = [A,B|T],
1394		or_equal(T,E,disjunct(equal(E,A),equal(E,B)),D).
1395		simp_rule(M,exists([X],conjunct(member(X,S),member(E,X))),'DEF_IN_KUNION') :-
1396		M = member(E,general_union(S)),
1397		new_identifier(M,X).
1398		simp_rule(member(E,general_intersection(S)),forall([X],member(X,S),member(E,X)),'DEF_IN_KINTER') :- new_identifier(S,X).
1399		simp_rule(member(E,quantified_union(Ids,P,T)),exists(NewIds,conjunct(P1,member(E,T1))),'DEF_IN_QUNION') :-
1400		length(Ids,L),
1401		new_identifiers(E,L,NewIds),
1402		rewrite_pairwise(Ids,NewIds,conjunct(P,T),conjunct(P1,T1)).
1403		simp_rule(member(E,quantified_intersection(Ids,P,T)),forall(NewIds,P1,member(E,T1)),'DEF_IN_QINTER') :-
1404		length(Ids,L),
1405		new_identifiers(E,L,NewIds),
1406		rewrite_pairwise(Ids,NewIds,conjunct(P,T),conjunct(P1,T1)).
1407		simp_rule(member(E,interval(L,R)),conjunct(less_equal(L,E),less_equal(E,R)),'DEF_IN_UPTO').
1408		simp_rule(C,Res,'DISTRI_BUNION_BINTER') :- distri(C,Res,union,intersection).
1409		simp_rule(C,Res,'DISTRI_BINTER_BUNION') :- distri(C,Res,intersection,union).
1410	?	simp_rule(C,Res,'DISTRI_BINTER_SETMINUS') :- distri(C,Res,intersection,set_subtraction).
1411		simp_rule(C,Res,'DISTRI_SETMINUS_BUNION') :- distri_setminus(C,Res).
1412		simp_rule(C,Res,'DISTRI_CPROD_BINTER') :- distri(C,Res,cartesian_product,intersection).
1413		simp_rule(C,Res,'DISTRI_CPROD_BUNION') :- distri(C,Res,cartesian_product,union).
1414		simp_rule(C,Res,'DISTRI_CPROD_SETMINUS') :- distri(C,Res,cartesian_product,set_subtraction).
1415		simp_rule(subset(set_subtraction(A,B),S),subset(A,union(B,S)),'DERIV_SUBSETEQ_SETMINUS_L').
1416		simp_rule(subset(S,set_subtraction(A,B)),conjunct(subset(S,A),equal(intersection(S,B),empty_set)),'DERIV_SUBSETEQ_SETMINUS_R').
1417		simp_rule(partition(S,L),Res,'DEF_PARTITION') :-
1418		length(L,LL), LL > 1,
1419		list_to_op(L,U,union),
1420		Eq = equal(S,U),
1421		findall(equal(intersection(X,Y),empty_set),(all_pairs(L,Pairs), member([X,Y],Pairs)), Disjoint),
1422		list_to_op([Eq|Disjoint],Res,conjunct).
1423		simp_rule(partition(S,[]),equal(S,empty_set),'SIMP_EMPTY_PARTITION').
1424		simp_rule(partition(S,[T]),equal(S,T),'SIMP_SINGLE_PARTITION').
1425		simp_rule(domain(set_extension(L)),set_extension(Res),'SIMP_DOM_SETENUM') :-
1426		map_dom(L,Dom),
1427		without_duplicates(Dom,[],Res).
1428		simp_rule(range(set_extension(L)),set_extension(Res),'SIMP_RAN_SETENUM') :-
1429		map_ran(L,Ran),
1430		without_duplicates(Ran,[],Res).
1431		simp_rule(general_union(pow_subset(S)),S,'SIMP_KUNION_POW').
1432		simp_rule(general_union(pow1_subset(S)),S,'SIMP_KUNION_POW1').
1433		simp_rule(general_union(set_extension([empty_set])),empty_set,'SIMP_SPECIAL_KUNION').
1434		simp_rule(quantified_union([_],falsity,_),empty_set,'SIMP_SPECIAL_QUNION').
1435		simp_rule(general_intersection(set_extension([empty_set])),empty_set,'SIMP_SPECIAL_KINTER').
1436		simp_rule(general_intersection(pow_subset(S)),S,'SIMP_KINTER_POW').
1437		simp_rule(pow_subset(empty_set),set_extension([empty_set]),'SIMP_SPECIAL_POW').
1438		simp_rule(pow1_subset(empty_set),empty_set,'SIMP_SPECIAL_POW1').
1439		simp_rule(event_b_comprehension_set(Ids,X,member(X,S)),S,'SIMP_COMPSET_IN') :-
1440		used_identifiers(X,Ids),
1441		free_identifiers(S,Free),
1442		list_intersection(Ids,Free,[]).
1443		simp_rule(event_b_comprehension_set(Ids,X,subset(X,S)),pow_subset(S),'SIMP_COMPSET_SUBSETEQ') :-
1444		used_identifiers(X,Ids),
1445		free_identifiers(S,Free),
1446		list_intersection(Ids,Free,[]).
1447		simp_rule(event_b_comprehension_set(_,_,falsity),empty_set,'SIMP_SPECIAL_COMPSET_BFALSE').
1448		simp_rule(Expr,forall(Ids,truth,negation(P)),'SIMP_SPECIAL_EQUAL_COMPSET') :-
1449		is_empty(Expr,event_b_comprehension_set(Ids,_,P)).
1450		simp_rule(event_b_comprehension_set(Ids,F,Conj),event_b_comprehension_set(Ids0,F1,Conj0),'SIMP_COMPSET_EQUAL') :-
1451		op_to_list(Conj,ConjList,conjunct),
1452	?	select(Eq,ConjList,ConjList0),
1453	?	is_equality(Eq,X,E),
1454	?	list_to_op(ConjList0,Conj0,conjunct),
1455		free_identifiers(conjunct(E,Conj0),Free),
1456		op_to_list(X,CIds,couple),
1457		list_intersection(CIds,Free,[]),
1458		list_subset(CIds,Ids),
1459		list_difference(Ids,CIds,Ids0),
1460		Ids0 \= [],
1461		rewrite(X,E,F,F1).
1462		simp_rule(member(E,event_b_comprehension_set(BIds,X,P)),Q,'SIMP_IN_COMPSET_ONEPOINT') :-
1463		op_to_list(X,IdsX,couple),
1464		IdsX = BIds,
1465		op_to_list(E,IdsE,couple),
1466		length(IdsX,LengthX),
1467		length(IdsE,LengthE),
1468		LengthE =:= LengthX,
1469		rewrite_pairwise(IdsX,IdsE,P,Q).
1470		simp_rule(member(F,event_b_comprehension_set(Ids,E,P)),exists(Ids,conjunct(P,equal(E,F))),'SIMP_IN_COMPSET') :-
1471		free_identifiers(F,FreeInF),
1472		list_intersection(Ids,FreeInF,[]).
1473		simp_rule(function(event_b_comprehension_set([X],couple(X,E),_),Y),F,'SIMP_FUNIMAGE_LAMBDA') :- rewrite(X,Y,E,F).
1474		simp_rule(Hyp,New,Rule) :-
1475		CompSet = event_b_comprehension_set(Ids,couple(E,F),P),
1476		NewComp = event_b_comprehension_set(Ids,E,P),
1477		(Hyp = finite(CompSet), New = finite(NewComp), Rule = 'SIMP_FINITE_LAMBDA' ;
1478		Hyp = card(CompSet), New = card(NewComp), Rule = 'SIMP_CARD_LAMBDA' ),
1479		used_identifiers(E,IdsE),
1480		list_subset(Ids,IdsE),
1481		used_identifiers(F,IdsF),
1482		list_intersection(IdsF,Ids,BoundF),
1483		list_subset(BoundF,IdsE).
1484		simp_rule(R,S,'SIMP_SPECIAL_OVERL') :- R = overwrite(S,empty_set) ; R = overwrite(empty_set,S).
1485		simp_rule(domain(reverse(R)),range(R),'SIMP_DOM_CONVERSE').
1486		simp_rule(range(reverse(R)),domain(R),'SIMP_RAN_CONVERSE').
1487		simp_rule(domain_restriction(empty_set,_),empty_set,'SIMP_SPECIAL_DOMRES_L').
1488		simp_rule(domain_restriction(_,empty_set),empty_set,'SIMP_SPECIAL_DOMRES_R').
1489		simp_rule(domain_restriction(domain(R),R),R,'SIMP_MULTI_DOMRES_DOM').
1490		simp_rule(domain_restriction(range(R),reverse(R)),reverse(R),'SIMP_MULTI_DOMRES_RAN').
1491		simp_rule(domain_restriction(S,domain_restriction(T,event_b_identity)),domain_restriction(intersection(S,T),event_b_identity),'SIMP_DOMRES_DOMRES_ID').
1492		simp_rule(domain_restriction(S,domain_subtraction(T,event_b_identity)),domain_restriction(set_subtraction(S,T),event_b_identity),'SIMP_DOMRES_DOMSUB_ID').
1493		simp_rule(range_restriction(_,empty_set),empty_set,'SIMP_SPECIAL_RANRES_R').
1494		simp_rule(range_restriction(empty_set,_),empty_set,'SIMP_SPECIAL_RANRES_L').
1495		simp_rule(range_restriction(domain_restriction(S,event_b_identity),T),domain_restriction(intersection(S,T),event_b_identity),'SIMP_RANRES_DOMRES_ID').
1496		simp_rule(range_restriction(domain_subtraction(S,event_b_identity),T),domain_restriction(set_subtraction(T,S),event_b_identity),'SIMP_RANRES_DOMSUB_ID').
1497		simp_rule(range_restriction(R,range(R)),R,'SIMP_MULTI_RANRES_RAN').
1498		simp_rule(range_restriction(reverse(R),domain(R)),reverse(R),'SIMP_MULTI_RANRES_DOM').
1499		simp_rule(range_restriction(event_b_identity,S),domain_restriction(S,event_b_identity),'SIMP_RANRES_ID').
1500		simp_rule(range_subtraction(event_b_identity,S),domain_subtraction(S,event_b_identity),'SIMP_RANSUB_ID').
1501		simp_rule(domain_subtraction(empty_set,R),R,'SIMP_SPECIAL_DOMSUB_L').
1502		simp_rule(domain_subtraction(_,empty_set),empty_set,'SIMP_SPECIAL_DOMSUB_R').
1503		simp_rule(domain_subtraction(domain(R),R),empty_set,'SIMP_MULTI_DOMSUB_DOM').
1504		simp_rule(domain_subtraction(range(R),reverse(R)),empty_set,'SIMP_MULTI_DOMSUB_RAN').
1505		simp_rule(domain_subtraction(S,domain_restriction(T,event_b_identity)),domain_restriction(set_subtraction(T,S),event_b_identity),'SIMP_DOMSUB_DOMRES_ID').
1506		simp_rule(domain_subtraction(S,domain_subtraction(T,event_b_identity)),domain_subtraction(union(S,T),event_b_identity),'SIMP_DOMSUB_DOMSUB_ID').
1507		simp_rule(range_subtraction(R,empty_set),R,'SIMP_SPECIAL_RANSUB_R').
1508		simp_rule(range_subtraction(empty_set,_),empty_set,'SIMP_SPECIAL_RANSUB_L').
1509		simp_rule(range_subtraction(reverse(R),domain(R)),empty_set,'SIMP_MULTI_RANSUB_DOM').
1510		simp_rule(range_subtraction(R,range(R)),empty_set,'SIMP_MULTI_RANSUB_RAN').
1511		simp_rule(range_subtraction(domain_restriction(S,event_b_identity),T),domain_restriction(set_subtraction(S,T),event_b_identity),'SIMP_RANSUB_DOMRES_ID').
1512		simp_rule(range_subtraction(domain_subtraction(S,event_b_identity),T),domain_subtraction(union(S,T),event_b_identity),'SIMP_RANSUB_DOMSUB_ID').
1513		simp_rule(C,R,'SIMP_TYPE_FCOMP_ID') :- C = composition(R,event_b_identity) ; C = composition(event_b_identity,R).
1514		simp_rule(C,R,'SIMP_TYPE_BCOMP_ID') :- C = ring(R,event_b_identity) ; C = ring(event_b_identity,R).
1515		simp_rule(direct_product(_,empty_set),empty_set,'SIMP_SPECIAL_DPROD_R').
1516		simp_rule(direct_product(empty_set,_),empty_set,'SIMP_SPECIAL_DPROD_L').
1517		simp_rule(direct_product(cartesian_product(S,T),cartesian_product(U,V)),
1518		cartesian_product(intersection(S,U),cartesian_product(T,V)),'SIMP_DPROD_CPROD').
1519		simp_rule(PP,empty_set,'SIMP_SPECIAL_PPROD') :- PP = parallel_product(_,empty_set) ; PP = parallel_product(empty_set,_).
1520		simp_rule(parallel_product(cartesian_product(S,T),cartesian_product(U,V)),
1521		cartesian_product(cartesian_product(S,U),cartesian_product(T,V)),'SIMP_PPROD_CPROD').
1522		simp_rule(image(_,empty_set),empty_set,'SIMP_SPECIAL_RELIMAGE_R').
1523		simp_rule(image(empty_set,_),empty_set,'SIMP_SPECIAL_RELIMAGE_L').
1524		simp_rule(image(R,domain(R)),range(R),'SIMP_MULTI_RELIMAGE_DOM').
1525		simp_rule(image(event_b_identity,T),T,'SIMP_RELIMAGE_ID').
1526		simp_rule(image(domain_restriction(S,event_b_identity),T),intersection(S,T),'SIMP_RELIMAGE_DOMRES_ID').
1527		simp_rule(image(domain_subtraction(S,event_b_identity),T),set_subtraction(T,S),'SIMP_RELIMAGE_DOMSUB_ID').
1528		simp_rule(image(reverse(range_subtraction(_,S)),S),empty_set,'SIMP_MULTI_RELIMAGE_CONVERSE_RANSUB').
1529		simp_rule(image(reverse(range_restriction(R,S)),S),image(reverse(R),S),'SIMP_MULTI_RELIMAGE_CONVERSE_RANRES').
1530		simp_rule(image(reverse(domain_subtraction(S,R)),T),
1531		set_subtraction(image(reverse(R),T),S),'SIMP_RELIMAGE_CONVERSE_DOMSUB').
1532		simp_rule(image(range_subtraction(R,S),T),set_subtraction(image(R,T),S),'DERIV_RELIMAGE_RANSUB').
1533		simp_rule(image(range_restriction(R,S),T),intersection(image(R,T),S),'DERIV_RELIMAGE_RANRES').
1534		simp_rule(image(domain_subtraction(S,_),S),empty_set,'SIMP_MULTI_RELIMAGE_DOMSUB').
1535		simp_rule(image(domain_subtraction(S,R),T),image(R,set_subtraction(T,S)),'DERIV_RELIMAGE_DOMSUB').
1536		simp_rule(image(domain_restriction(S,R),T),image(R,intersection(S,T)),'DERIV_RELIMAGE_DOMRES').
1537		simp_rule(reverse(empty_set),empty_set,'SIMP_SPECIAL_CONVERSE').
1538		simp_rule(reverse(event_b_identity),event_b_identity,'SIMP_SPECIAL_ID').
1539		simp_rule(member(couple(E,F),set_subtraction(_,event_b_identity)),falsity,'SIMP_SPECIAL_IN_SETMINUS_ID') :- equal_terms(E,F).
1540		simp_rule(member(couple(E,F),domain_restriction(S,event_b_identity)),member(E,S),'SIMP_SPECIAL_IN_DOMRES_ID') :-
1541		equal_terms(E,F).
1542		simp_rule(member(couple(E,F),set_subtraction(R,domain_restriction(S,event_b_identity))),
1543		member(couple(E,F),domain_subtraction(S,R)),'SIMP_SPECIAL_IN_DOMRES_ID') :- equal_terms(E,F).
1544		simp_rule(reverse(cartesian_product(S,T)),cartesian_product(T,S),'SIMP_CONVERSE_CPROD').
1545		simp_rule(reverse(set_extension(L)),set_extension(NewL),'SIMP_CONVERSE_SETENUM') :- convert_map_to(L,NewL).
1546		simp_rule(reverse(event_b_comprehension_set(Ids,couple(X,Y),P)),
1547		event_b_comprehension_set(Ids,couple(Y,X),P),'SIMP_CONVERSE_COMPSET').
1548		simp_rule(composition(domain_restriction(S,event_b_identity),R),domain_restriction(S,R),'SIMP_FCOMP_ID_L').
1549		simp_rule(composition(R,domain_restriction(S,event_b_identity)),range_restriction(R,S),'SIMP_FCOMP_ID_R').
1550		simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_REL_R') :- R=..[Op,_,empty_set],
1551	?	member(Op,[relations,surjection_relation,partial_function,partial_injection,partial_surjection]).
1552		simp_rule(R,set_extension([empty_set]),'SIMP_SPECIAL_REL_L') :- R=..[Op,empty_set,_],
1553		member(Op,[relations,total_relation,partial_function,total_function,partial_injection,total_injection]).
1554		simp_rule(function(event_b_first_projection_v2,couple(E,_)),E,'SIMP_FUNIMAGE_PRJ1').
1555		simp_rule(function(event_b_second_projection_v2,couple(_,F)),F,'SIMP_FUNIMAGE_PRJ2').
1556		simp_rule(member(couple(E,function(F,E)),F),truth,'SIMP_IN_FUNIMAGE').
1557		simp_rule(member(couple(function(reverse(F),E),E),F),truth,'SIMP_IN_FUNIMAGE_CONVERSE_L').
1558		simp_rule(member(couple(function(F,E),E),reverse(F)),truth,'SIMP_IN_FUNIMAGE_CONVERSE_R').
1559		simp_rule(function(set_extension(L),_),E,'SIMP_MULTI_FUNIMAGE_SETENUM_LL') :- all_map_to(L,E).
1560	?	simp_rule(function(set_extension(L),X),Y,'SIMP_MULTI_FUNIMAGE_SETENUM_LR') :- member(couple(Z,Y),L), equal_terms(X,Z).
1561		simp_rule(function(Over,X),Y,'SIMP_MULTI_FUNIMAGE_OVERL_SETENUM') :-
1562		Over = overwrite(_,_),
1563		last_overwrite(Over,set_extension(L)),
1564		member(couple(Z,Y),L),
1565		equal_terms(X,Z).
1566		simp_rule(function(U,X),Y,'SIMP_MULTI_FUNIMAGE_BUNION_SETENUM') :-
1567	?	member_of(union,set_extension(L),U),
1568	?	member(couple(Z,Y),L),
1569		equal_terms(X,Z).
1570		simp_rule(function(cartesian_product(_,set_extension([F])),_),F,'SIMP_FUNIMAGE_CPROD').
1571		simp_rule(function(F,function(reverse(F),E)),E,'SIMP_FUNIMAGE_FUNIMAGE_CONVERSE').
1572		simp_rule(function(reverse(F),function(F,E)),E,'SIMP_FUNIMAGE_CONVERSE_FUNIMAGE').
1573		simp_rule(function(set_extension(L),function(set_extension(L2),E)),E,'SIMP_FUNIMAGE_FUNIMAGE_CONVERSE_SETENUM') :-
1574		convert_map_to(L,LConverted),
1575		equal_terms(LConverted,L2).
1576	?	simp_rule(Eq,member(couple(X,Y),F),'DEF_EQUAL_FUNIMAGE') :- is_equality(Eq,function(F,X),Y).
1577		simp_rule(domain_restriction(SetE,event_b_identity),set_extension([couple(E,E)]),'DERIV_ID_SING') :- singleton_set(SetE,E).
1578		simp_rule(domain(empty_set),empty_set,'SIMP_SPECIAL_DOM').
1579		simp_rule(range(empty_set),empty_set,'SIMP_SPECIAL_RAN').
1580		simp_rule(reverse(reverse(R)),R,'SIMP_CONVERSE_CONVERSE').
1581		simp_rule(function(event_b_identity,X),X,'SIMP_FUNIMAGE_ID').
1582		simp_rule(member(E,Nat),less_equal(0,E),'DEF_IN_NATURAL') :- is_natural_set(Nat).
1583		simp_rule(member(E,Nat),less_equal(1,E),'DEF_IN_NATURAL1') :- is_natural1_set(Nat).
1584		simp_rule(div(E,1),E,'SIMP_SPECIAL_DIV_1').
1585		simp_rule(div(0,_),0,'SIMP_SPECIAL_DIV_0').
1586		simp_rule(power_of(E,1),E,'SIMP_SPECIAL_EXPN_1_R').
1587		simp_rule(power_of(1,_),1,'SIMP_SPECIAL_EXPN_1_L').
1588		simp_rule(power_of(_,0),1,'SIMP_SPECIAL_EXPN_0').
1589		simp_rule(A,S,'SIMP_SPECIAL_PLUS') :- A = add(S,0) ; A = add(0,S).
1590		simp_rule(Prod,Res,Rule) :-
1591		Prod = multiplication(_,_),
1592		op_to_list(Prod,L,multiplication),
1593		change_sign(L,NL,Nr),
1594		list_to_op(NL,New,multiplication),
1595		(Nr mod 2 =:= 0 -> Rule = 'SIMP_SPECIAL_PROD_MINUS_EVEN', Res = New
1596		; Rule = 'SIMP_SPECIAL_PROD_MINUS_ODD', Res = unary_minus(New)).
1597		simp_rule(unary_minus(I),J,'SIMP_LIT_MINUS') :- number(I), J is I * (-1).
1598		simp_rule(minus(E,0),E,'SIMP_SPECIAL_MINUS_R').
1599		simp_rule(minus(0,E),unary_minus(E),'SIMP_SPECIAL_MINUS_L').
1600	?	simp_rule(unary_minus(F),E,'SIMP_MINUS_MINUS') :- is_minus(F,E).
1601		simp_rule(minus(E,F),add(E,F2),'SIMP_MINUS_UNMINUS') :- is_minus(F,F2).
1602		simp_rule(minus(E,F),0,'SIMP_MULTI_MINUS') :- equal_terms(E,F).
1603		simp_rule(minus(S,C),S0,'SIMP_MULTI_MINUS_PLUS_L') :- select_op(C,S,S0,add).
1604		simp_rule(minus(C,S),unary_minus(S0),'SIMP_MULTI_MINUS_PLUS_R') :- select_op(C,S,S0,add).
1605		simp_rule(minus(S1,S2),minus(S01,S02),'SIMP_MULTI_MINUS_PLUS_PLUS') :-
1606		member_of(add,El,S1),
1607		select_op(El,S1,S01,add),
1608		select_op(El,S2,S02,add),
1609		S01 = add(_,_),
1610		S02 = add(_,_).
1611		simp_rule(S,S1,'SIMP_MULTI_PLUS_MINUS') :-
1612		member_of(add,minus(C,D),S),
1613		select_op(D,S,S0,add),
1614		select_op(minus(C,D),S0,C,S1,add).
1615		simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_PLUS') :-
1616		Ex=..[Rel,L,R],
1617		comparison(Rel),
1618		R = add(_,_),
1619		member_of(add,El,L),
1620		select_op(El,L,L0,add),
1621		select_op(El,R,R0,add),
1622		Res=..[Rel,L0,R0].
1623		simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_R') :-
1624		Ex=..[Rel,C,R],
1625		comparison(Rel),
1626		R = add(_,_),
1627		select_op(C,R,R0,add),
1628		Res=..[Rel,0,R0].
1629		simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_PLUS_L') :-
1630		Ex=..[Rel,L,C],
1631		comparison(Rel),
1632		L = add(_,_),
1633		select_op(C,L,L0,add),
1634		Res=..[Rel,L0,0].
1635		simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_R') :-
1636		Ex=..[Rel,L,R],
1637		comparison(Rel),
1638		L = minus(A,C1),
1639		R = minus(B,C2),
1640		equal_terms(C1,C2),
1641		Res=..[Rel,A,B].
1642		simp_rule(Ex,Res,'SIMP_MULTI_ARITHREL_MINUS_MINUS_L') :-
1643		Ex=..[Rel,L,R],
1644		comparison(Rel),
1645		L = minus(C1,A),
1646		R = minus(C2,B),
1647		equal_terms(C1,C2),
1648		Res=..[Rel,B,A].
1649		simp_rule(P,E,'SIMP_SPECIAL_PROD_1') :- P = multiplication(E,1) ; P = multiplication(1,E).
1650		simp_rule(min(set_extension(L)),min(set_extension(Res)),'SIMP_LIT_MIN') :-
1651		min_list(L,I),
1652	?	remove_greater(L,I,Res).
1653		simp_rule(max(set_extension(L)),max(set_extension(Res)),'SIMP_LIT_MAX') :-
1654		max_list(L,I),
1655		remove_smaller(L,I,Res).
1656		simp_rule(card(empty_set),0,'SIMP_SPECIAL_CARD').
1657		simp_rule(card(set_extension([_])),1,'SIMP_CARD_SING').
1658		simp_rule(Eq,equal(S,empty_set),'SIMP_SPECIAL_EQUAL_CARD') :- is_equality(Eq,card(S),0).
1659		simp_rule(card(pow_subset(S)),power_of(2,card(S)),'SIMP_CARD_POW').
1660		simp_rule(card(union(S,T)),minus(add(card(S),card(T)),card(intersection(S,T))),'SIMP_CARD_BUNION').
1661		simp_rule(card(reverse(R)),card(R),'SIMP_CARD_CONVERSE').
1662		simp_rule(card(domain_restriction(S,event_b_identity)),S,'SIMP_CARD_ID_DOMRES').
1663		simp_rule(card(domain_restriction(E,event_b_first_projection_v2)),E,'SIMP_CARD_PRJ1_DOMRES').
1664		simp_rule(card(domain_restriction(E,event_b_second_projection_v2)),E,'SIMP_CARD_PRJ2_DOMRES').
1665		simp_rule(P,falsity,'SIMP_MULTI_LT') :- is_less(P,E,F), equal_terms(E,F). % covers SIMP_MULTI_GT too
1666	?	simp_rule(div(NE,NF),div(E,F),'SIMP_DIV_MINUS') :- is_minus(NE,E), is_minus(NF,F).
1667		simp_rule(div(E,F),1,'SIMP_MULTI_DIV') :- equal_terms(E,F).
1668		simp_rule(modulo(0,_),0,'SIMP_SPECIAL_MOD_0').
1669		simp_rule(modulo(_,1),0,'SIMP_SPECIAL_MOD_1').
1670		simp_rule(modulo(E,F),1,'SIMP_MULTI_MOD') :- equal_terms(E,F).
1671		simp_rule(min(SetE),E,'SIMP_MIN_SING') :- singleton_set(SetE,E).
1672		simp_rule(max(SetE),E,'SIMP_MAX_SING') :- singleton_set(SetE,E).
1673		simp_rule(div(P1,E2),P0,'SIMP_MULTI_DIV_PROD') :-
1674	?	member_of(multiplication,E1,P1),
1675		equal_terms(E1,E2),
1676		select_op(E1,P1,P0,multiplication).
1677		simp_rule(card(set_extension(L)),LL,'SIMP_TYPE_CARD') :- length(L,LL).
1678		simp_rule(card(interval(I,J)),Res,'SIMP_LIT_CARD_UPTO') :- number(I), number(J), I =< J, Res is J - I + 1.
1679		simp_rule(card(interval(I,J)),0,'SIMP_LIT_CARD_UPTO') :- number(I), number(J), I > J. % from "Proposal for an extensible rule-based prover for Event-B", pg. 7
1680		simp_rule(P,negation(equal(S,empty_set)),'SIMP_LIT_LE_CARD_1') :- is_less_eq(P,1,card(S)).
1681		simp_rule(P,negation(equal(S,empty_set)),'SIMP_LIT_LT_CARD_0') :- is_less(P,0,card(S)).
1682		simp_rule(Eq,exists([X],equal(S,set_extension([X]))),'SIMP_LIT_EQUAL_CARD_1') :-
1683		is_equality(Eq,card(S),1),
1684		new_identifier(S,X).
1685		simp_rule(member(card(S),Nat),negation(equal(S,empty_set)),'SIMP_CARD_NATURAL1') :- is_natural1_set(Nat).
1686		simp_rule(Eq,exists([F],member(F,total_bijection(interval(1,K),S))),'DEF_EQUAL_CARD') :-
1687		is_equality(Eq,card(S),K),
1688		new_function(conjunct(S,K),F).
1689		simp_rule(equal(card(S),card(T)),exists([F],member(F,total_bijection(S,T))),'SIMP_EQUAL_CARD') :-
1690		new_function(conjunct(S,T),F).
1691		simp_rule(member(0,Nat),falsity,'SIMP_SPECIAL_IN_NATURAL1') :- is_natural1_set(Nat).
1692		simp_rule(interval(I,J),empty_set,'SIMP_LIT_UPTO') :- number(I), number(J), I > J.
1693		simp_rule(member(NI,Nat),falsity,'SIMP_LIT_IN_MINUS_NATURAL') :-
1694		is_natural_set(Nat),
1695		(NI = unary_minus(I), number(I), I > 0
1696		; number(NI), NI < 0).
1697		simp_rule(member(NI,Nat),falsity,'SIMP_LIT_IN_MINUS_NATURAL1') :-
1698		is_natural1_set(Nat),
1699		(NI = unary_minus(I), number(I), I >= 0
1700		; number(NI), NI < 0).
1701		simp_rule(min(Nat),0,'SIMP_MIN_NATURAL') :- is_natural_set(Nat).
1702		simp_rule(min(Nat),1,'SIMP_MIN_NATURAL1') :- is_natural1_set(Nat).
1703		simp_rule(max(interval(_,F)),F,'SIMP_MAX_UPTO').
1704		simp_rule(min(interval(E,_)),E,'SIMP_MIN_UPTO').
1705		simp_rule(Eq,conjunct(member(E,S),forall([X],member(X,S),less_equal(E,X))),'DEF_EQUAL_MIN') :-
1706		is_equality(Eq,E,min(S)),
1707		new_identifier(member(E,S),X).
1708		simp_rule(Eq,conjunct(member(E,S),forall([X],member(X,S),greater_equal(E,X))),'DEF_EQUAL_MAX') :-
1709		is_equality(Eq,E,max(S)),
1710		new_identifier(member(E,S),X).
1711		simp_rule(min(U),min(New),'SIMP_MIN_BUNION_SING') :- U = union(_,_), select_op(set_extension([min(T)]),U,T,New,union).
1712		simp_rule(max(U),max(New),'SIMP_MAX_BUNION_SING') :- U = union(_,_), select_op(set_extension([max(T)]),U,T,New,union).
1713		simp_rule(Expr,falsity,'SIMP_POW_EQUAL_EMPTY') :- is_empty(Expr,pow_subset(_)).
1714		simp_rule(Expr,equal(S,empty_set),'SIMP_POW1_EQUAL_EMPTY') :- is_empty(Expr,pow1_subset(S)).
1715		simp_rule(Expr,subset(S,set_extension([empty_set])),'SIMP_KUNION_EQUAL_EMPTY') :- is_empty(Expr,general_union(S)).
1716
1717		simp_rule(negation(P),Q,'Propagate negation') :-
1718		negate(P,Q), Q \= negation(_). % De-Morgan and similar rules to propagate negation
1719	?	simp_rule(P,truth,'Evaluate tautology') :- is_true(P).
1720
1721		%simp_rule(X,X,'EQ'(F,N,X)) :- functor(X,F,N).
1722
1723		% simp_rule/4
1724		simp_rule(D,implication(negation(P),D0),'DEF_OR',OuterOp) :- OuterOp \= disjunct, D = disjunct(_,_), select_op(P,D,D0,disjunct).
1725		simp_rule(C,falsity,'SIMP_SPECIAL_AND_BFALSE',OuterOp) :- OuterOp \= conjunct, member_of(conjunct,falsity,C).
1726	?	simp_rule(D,truth,'SIMP_SPECIAL_OR_BTRUE',OuterOp) :- OuterOp \= disjunct, member_of(disjunct,truth,D).
1727	?	simp_rule(C,Res,'SIMP_MULTI_AND',OuterOp) :- OuterOp \= conjunct, remove_duplicates(C,Res,conjunct).
1728	?	simp_rule(D,Res,'SIMP_MULTI_OR',OuterOp) :- OuterOp \= disjunct, remove_duplicates(D,Res,disjunct).
1729		simp_rule(C,falsity,'SIMP_MULTI_AND_NOT',OuterOp) :-
1730		OuterOp \= conjunct,
1731	?	member_of(conjunct,Q,C),
1732	?	member_of(conjunct,NotQ,C),
1733		is_negation(Q,NotQ).
1734		simp_rule(D,truth,'SIMP_MULTI_OR_NOT',OuterOp) :-
1735		OuterOp \= disjunct,
1736	?	member_of(disjunct,Q,D),
1737	?	member_of(disjunct,NotQ,D),
1738		is_negation(Q,NotQ).
1739	?	simp_rule(I,empty_set,'SIMP_SPECIAL_BINTER',OuterOp) :- OuterOp \= intersection, member_of(intersection,empty_set,I).
1740		simp_rule(I,Res,'SIMP_MULTI_BINTER',OuterOp) :- OuterOp \= intersection, remove_duplicates(I,Res,intersection).
1741		simp_rule(U,Res,'SIMP_MULTI_BUNION',OuterOp) :- OuterOp \= union, remove_duplicates(U,Res,union).
1742		simp_rule(C,empty_set,'SIMP_SPECIAL_CPROD',OuterOp) :- OuterOp \= cartesian_product, member_of(cartesian_product,empty_set,C).
1743		simp_rule(C,empty_set,'SIMP_SPECIAL_FCOMP',OuterOp) :- OuterOp \= composition, member_of(composition,empty_set,C).
1744		simp_rule(Comp,empty_set,'SIMP_SPECIAL_BCOMP',OuterOp) :- OuterOp \= ring, member_of(ring,empty_set,Comp).
1745	?	simp_rule(C,Res,'DEF_BCOMP',OuterOp) :- OuterOp \= ring, C = ring(_,_), bwd_to_fwd_comp(C,Comp), reorder(Comp,Res,composition).
1746	?	simp_rule(P,0,'SIMP_SPECIAL_PROD_0',OuterOp) :- OuterOp \= multiplication, member_of(multiplication,0,P).
1747		simp_rule(Comp,Res,'SIMP_BCOMP_ID',OuterOp) :- OuterOp \= ring,
1748		op_to_list(Comp,List,ring),
1749	?	rewrite_comp_id(List,List2),
1750	?	list_to_op(List2,Res,ring),
1751		Comp \= Res.
1752		simp_rule(Comp,Res,'SIMP_FCOMP_ID',OuterOp) :- OuterOp \= composition,
1753		op_to_list(Comp,List,composition),
1754	?	rewrite_comp_id(List,List2),
1755	?	list_to_op(List2,Res,composition),
1756		Comp \= Res.
1757	?	simp_rule(Comp,Res,'DERIV_FCOMP_DOMRES',OuterOp) :- OuterOp \= composition, deriv_fcomp_dom(Comp,domain_restriction,Res).
1758	?	simp_rule(Comp,Res,'DERIV_FCOMP_DOMSUB',OuterOp) :- OuterOp \= composition, deriv_fcomp_dom(Comp,domain_subtraction,Res).
1759	?	simp_rule(Comp,Res,'DERIV_FCOMP_RANRES',OuterOp) :- OuterOp \= composition, deriv_fcomp_ran(Comp,range_restriction,Res).
1760		simp_rule(Comp,Res,'DERIV_FCOMP_RANSUB',OuterOp) :- OuterOp \= composition, deriv_fcomp_ran(Comp,range_subtraction,Res).
1761
1762
1763
1764		% simp_rule_with_info/4
1765		simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_DOMSUB_EQUAL_TYPE',Info) :-
1766		is_equality(Eq,domain_subtraction(S,R),Ty),
1767		type_expression(Ty,Info).
1768		simp_rule_with_info(Eq,conjunct(equal(S,empty_set),equal(R,Ty)),'SIMP_RANSUB_EQUAL_TYPE',Info) :-
1769		is_equality(Eq,range_subtraction(R,S),Ty),
1770		type_expression(Ty,Info).
1771		simp_rule_with_info(Eq,equal(R,reverse(Ty)),'SIMP_CONVERSE_EQUAL_TYPE',Info) :-
1772		is_equality(Eq,reverse(R),Ty),
1773		type_expression(Ty,Info).
1774	?	simp_rule_with_info(subset(_,Ty),truth,'SIMP_TYPE_SUBSETEQ',Info) :- type_expression(Ty,Info).
1775	?	simp_rule_with_info(set_subtraction(_,Ty),empty_set,'SIMP_TYPE_SETMINUS',Info) :- type_expression(Ty,Info).
1776	?	simp_rule_with_info(set_subtraction(Ty,set_subtraction(Ty,S)),S,'SIMP_TYPE_SETMINUS_SETMINUS',Info) :- type_expression(Ty,Info).
1777		simp_rule_with_info(member(_,Ty),truth,'SIMP_TYPE_IN',Info) :- type_expression(Ty,Info).
1778		simp_rule_with_info(subset_strict(S,Ty),not_equal(S,Ty),'SIMP_TYPE_SUBSET_L',Info) :- type_expression(Ty,Info).
1779		simp_rule_with_info(Eq,conjunct(equal(A,Ty),equal(B,empty_set)),'SIMP_SETMINUS_EQUAL_TYPE',Info) :-
1780		is_equality(Eq,set_subtraction(A,B),Ty),
1781		type_expression(Ty,Info).
1782		simp_rule_with_info(Eq,Res,'SIMP_BINTER_EQUAL_TYPE',Info) :-
1783		is_equality(Eq,I,Ty),
1784		I = intersection(_,_),
1785		type_expression(Ty,Info),
1786		and_equal_type(I,Ty,Res).
1787		simp_rule_with_info(Eq,equal(S,set_extension([Ty])),'SIMP_KINTER_EQUAL_TYPE',Info) :-
1788		is_equality(Eq,general_intersection(S),Ty),
1789		type_expression(Ty,Info).
1790		simp_rule_with_info(Expr,falsity,'SIMP_TYPE_EQUAL_EMPTY',Info) :- is_empty(Expr,Ty), type_expression(Ty,Info).
1791		simp_rule_with_info(Eq,forall([X],P,equal(E,Ty)),'SIMP_QINTER_EQUAL_TYPE',Info) :-
1792		is_equality(Eq,quantified_intersection([X],P,E),Ty),
1793		type_expression(Ty,Info).
1794	?	simp_rule_with_info(I,S,'SIMP_TYPE_BINTER',Info) :- (I = intersection(S,Ty) ; I = intersection(Ty,S)), type_expression(Ty,Info).
1795		simp_rule_with_info(Eq,falsity,'SIMP_TYPE_EQUAL_RELDOMRAN',Info) :-
1796		is_equality(Eq,R,Ty),
1797		type_expression(Ty,Info),
1798		is_rel(R,_,_,_),
1799		R=..[Op,_,_],
1800		\+ member(Op,[relations,partial_function,partial_injection]).
1801		simp_rule_with_info(member(Prj,RT),truth,Rule,Info) :-
1802		(Prj = event_b_first_projection_v2, Rule = 'DERIV_PRJ1_SURJ'
1803		; Prj = event_b_second_projection_v2, Rule = 'DERIV_PRJ2_SURJ'),
1804		is_rel(RT,_,Ty1,Ty2),
1805		\+ is_inj(RT,Ty1,Ty2),
1806		type_expression(Ty1,Info),
1807		type_expression(Ty2,Info).
1808		simp_rule_with_info(member(event_b_identity,RT),truth,'DERIV_ID_BIJ',Info) :- is_rel(RT,_,Ty,Ty), type_expression(Ty,Info).
1809		simp_rule_with_info(domain_restriction(Ty,R),R,'SIMP_TYPE_DOMRES',Info) :- type_expression(Ty,Info).
1810		simp_rule_with_info(range_restriction(R,Ty),R,'SIMP_TYPE_RANRES',Info) :- type_expression(Ty,Info).
1811		simp_rule_with_info(domain_subtraction(Ty,R),R,'SIMP_TYPE_DOMSUB',Info) :- type_expression(Ty,Info).
1812		simp_rule_with_info(range_subtraction(R,Ty),R,'SIMP_TYPE_RANSUB',Info) :- type_expression(Ty,Info).
1813		simp_rule_with_info(image(R,Ty),range(R),'SIMP_TYPE_RELIMAGE',Info) :- type_expression(Ty,Info).
1814		simp_rule_with_info(composition(R,Ty),cartesian_product(domain(R),Tb),'SIMP_TYPE_FCOMP_R',Info) :-
1815	?	type_expression(Ty,Info),
1816		Ty = cartesian_product(_,Tb).
1817		simp_rule_with_info(composition(Ty,R),cartesian_product(Ta,range(R)),'SIMP_TYPE_FCOMP_L',Info) :-
1818		type_expression(Ty,Info),
1819		Ty = cartesian_product(Ta,_).
1820		simp_rule_with_info(ring(Ty,R),cartesian_product(domain(R),Tb),'SIMP_TYPE_BCOMP_L',Info) :-
1821		type_expression(Ty,Info),
1822		Ty = cartesian_product(_,Tb).
1823		simp_rule_with_info(ring(R,Ty),cartesian_product(Ta,range(R)),'SIMP_TYPE_BCOMP_R',Info) :-
1824		type_expression(Ty,Info),
1825		Ty = cartesian_product(Ta,_).
1826	?	simp_rule_with_info(domain(Ty),Ta,'SIMP_TYPE_DOM',Info) :- type_expression(Ty,Info), Ty = cartesian_product(Ta,_).
1827	?	simp_rule_with_info(range(Ty),Tb,'SIMP_TYPE_RAN',Info) :- type_expression(Ty,Info), Ty = cartesian_product(_,Tb).
1828		simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(T,Tb)),'SIMP_CPROD_EQUAL_TYPE',Info) :-
1829		is_equality(Eq,cartesian_product(S,T),Ty),
1830		type_expression(Ty,Info),
1831		Ty = cartesian_product(Ta,Tb).
1832		simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(T,Tb)),'SIMP_TYPE_EQUAL_REL',Info) :-
1833		is_equality(Eq,relations(S,T),Ty),
1834		type_expression(Ty,Info),
1835		Ty = cartesian_product(Ta,Tb).
1836		simp_rule_with_info(Eq,conjunct(equal(S,Ta),equal(R,Ty)),'SIMP_DOMRES_EQUAL_TYPE',Info) :-
1837		is_equality(Eq,domain_restriction(S,R),Ty),
1838		type_expression(Ty,Info),
1839		Ty = cartesian_product(Ta,_).
1840		simp_rule_with_info(Eq,conjunct(equal(S,Tb),equal(R,Ty)),'SIMP_RANRES_EQUAL_TYPE',Info) :-
1841		is_equality(Eq,range_restriction(R,S),Ty),
1842		type_expression(Ty,Info),
1843		Ty = cartesian_product(_,Tb).
1844		simp_rule_with_info(Eq,conjunct(equal(P,cartesian_product(Ta,Tb)),equal(Q,cartesian_product(Ta,Tc))),'SIMP_DPROD_EQUAL_TYPE',Info) :-
1845		is_equality(Eq,direct_product(P,Q),Ty),
1846		type_expression(Ty,Info),
1847		Ty = cartesian_product(Ta,cartesian_product(Tb,Tc)).
1848		simp_rule_with_info(Eq,conjunct(equal(P,cartesian_product(Ta,Tc)),equal(Q,cartesian_product(Tb,Td))),'SIMP_PPROD_EQUAL_TYPE',Info) :-
1849		is_equality(Eq,parallel_product(P,Q),Ty),
1850		type_expression(Ty,Info),
1851		Ty = cartesian_product(cartesian_product(Ta,Tb),cartesian_product(Tc,Td)).
1852		simp_rule_with_info(C,Res,'DERIV_TYPE_SETMINUS_BINTER',Info) :-
1853		C= set_subtraction(Ty,_),
1854		type_expression(Ty,Info),
1855		distri_r(C,Res,set_subtraction,intersection,union).
1856		simp_rule_with_info(C,Res,'DERIV_TYPE_SETMINUS_BUNION',Info) :-
1857		C= set_subtraction(Ty,_),
1858		type_expression(Ty,Info),
1859		distri_r(C,Res,set_subtraction,union,intersection).
1860		simp_rule_with_info(set_subtraction(Ty,set_subtraction(S,T)),union(set_subtraction(Ty,S),T),'DERIV_TYPE_SETMINUS_SETMINUS',Info) :-
1861		type_expression(Ty,Info).
1862		simp_rule_with_info(Ex,disjunct(greater('$'(E),F),less('$'(E),F)),'DERIV_NOT_EQUAL',Info) :-
1863	?	is_no_equality(Ex,'$'(E),F),
1864		(number(F) ; of_integer_type(E,Info)).
1865		simp_rule_with_info(equal(S,T),conjunct(subset(S,T),subset(T,S)),'DERIV_EQUAL',Info) :-
1866		get_meta_info(ids_types,Info,IdsTypes),
1867	?	check_type(S,T,IdsTypes,set(_)).
1868		simp_rule_with_info(subset(S,T),subset(set_subtraction(Ty,T),set_subtraction(Ty,S)),'DERIV_SUBSETEQ',Info) :-
1869		get_meta_info(ids_types,Info,IdsTypes),
1870	?	check_type(S,T,IdsTypes,Type),
1871		get_type_expression(Type,pow_subset(Ty)).
1872		simp_rule_with_info(event_b_comprehension_set(Ids,E,truth),Ty,'SIMP_SPECIAL_COMPSET_BTRUE',Info) :-
1873		get_meta_info(ids_types,Info,IdsTypes),
1874		pairwise_distict(E,Ids),
1875		check_type(E,IdsTypes,Type),
1876		get_type_expression(Type,Ty).
1877
1878		simp_rule_with_descr(couple(function(event_b_first_projection_v2,E),function(event_b_second_projection_v2,F)),E,Rule,Rule) :-
1879		Rule = 'SIMP_MAPSTO_PRJ1_PRJ2',
1880		equal_terms(E,F).
1881		simp_rule_with_descr(domain(successor),Z,Rule,Rule) :- Rule = 'SIMP_DOM_SUCC', is_integer_set(Z).
1882		simp_rule_with_descr(range(successor),Z,Rule,Rule) :- Rule = 'SIMP_RAN_SUCC', is_integer_set(Z).
1883		simp_rule_with_descr(predecessor,reverse(successor),Rule,Rule) :- Rule = 'DEF_PRED'.
1884		simp_rule_with_descr(Expr,negation(member(A,SetB)),'SIMP_BINTER_SING_EQUAL_EMPTY'(A),Descr) :-
1885		is_empty(Expr,Inter),
1886		is_inter(Inter,SetA,SetB),
1887		singleton_set(SetA,A),
1888		create_descr('SIMP_BINTER_SING_EQUAL_EMPTY',A,Descr).
1889
1890
1891
1892		% simp_rule_with_hyps/4 without info
1893		simp_rule_with_hyps(domain(R),E,'DERIV_DOM_TOTALREL',Hyps) :- member_hyps(member(R,FT),Hyps), is_rel(FT,total,E,_).
1894		simp_rule_with_hyps(range(R),F,'DERIV_RAN_SURJREL',Hyps) :- member_hyps(member(R,FT),Hyps), is_surj(FT,_,F).
1895		simp_rule_with_hyps(function(domain_restriction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMRES',Hyps) :-
1896		member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
1897		simp_rule_with_hyps(function(domain_subtraction(_,F),G),function(F,G),'SIMP_FUNIMAGE_DOMSUB',Hyps) :-
1898		member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
1899		simp_rule_with_hyps(function(range_restriction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANRES',Hyps) :-
1900		member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
1901		simp_rule_with_hyps(function(range_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_RANSUB',Hyps) :-
1902		member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
1903		simp_rule_with_hyps(function(set_subtraction(F,_),G),function(F,G),'SIMP_FUNIMAGE_SETMINUS',Hyps) :-
1904		member_hyps(member(F,FT),Hyps), is_fun(FT,_,_,_).
1905		simp_rule_with_hyps(card(set_subtraction(S,T)),minus(card(S),card(T)),'SIMP_CARD_SETMINUS',Hyps) :-
1906		member_hyps(subset(T,S),Hyps),
1907		(member_hyps(finite(T),Hyps)
1908		; member_hyps(finite(S),Hyps)).
1909		simp_rule_with_hyps(card(set_subtraction(S,set_extension(L))),minus(card(S),card(set_extension(L))),Rule,Hyps) :-
1910		Rule = 'SIMP_CARD_SETMINUS_SETENUM',
1911	?	all_in_set(L,S,Hyps).
1912	?	simp_rule_with_hyps(L,less(A,B),'DERIV_LESS',Hyps) :- is_less_eq(L,A,B), is_no_equality(Ex,A,B), member(Ex,Hyps).
1913		% allow simplifications deeper inside the term:
1914		simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,P], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,Q].
1915		simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,P,R], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,Q,R].
1916	?	simp_rule_with_hyps(C,NewC,Rule,Hyps) :- C=..[F,R,P], simp_rule_with_hyps(P,Q,Rule,Hyps), NewC=..[F,R,Q].
1917
1918
1919		is_true(equal(X,Y)) :- equal_terms(X,Y).
1920		is_true(less_equal(X,Y)) :- equal_terms(X,Y).
1921		is_true(greater_equal(X,Y)) :- equal_terms(X,Y).
1922		is_true(negation(falsity)).
1923		is_true(subset(empty_set,_)).
1924		is_true(subset(S,T)) :- equal_terms(S,T).
1925		is_true(implication(_P,truth)).
1926		is_true(implication(falsity,_P)).
1927		is_true(implication(P,Q)) :- equal_terms(P,Q).
1928		is_true(equivalence(P,Q)) :- equal_terms(P,Q).
1929		is_true(member(card(_S),Nat)) :- is_natural_set(Nat).
1930		is_true(P) :- is_less_eq(P,0,card(_S)).
1931		is_true(member(min(S),T)) :- equal_terms(S,T).
1932		is_true(member(max(S),T)) :- equal_terms(S,T).
1933		is_true(member(couple(E,F), event_b_identity)) :- equal_terms(E,F).
1934		is_true(finite(bool_set)).
1935		is_true(finite(set_extension(_))).
1936		is_true(finite(interval(_,_))).
1937		is_true(finite(empty_set)).
1938		is_true(member(I,Nat)) :- is_natural_set(Nat), number(I), I >= 0.
1939		is_true(member(I,Nat)) :- is_natural1_set(Nat), number(I), I >= 1.
1940
1941		compute(Expr,Res) :- evaluate(Expr,Res), Expr \= Res.
1942
1943		evaluate(I,I) :- number(I).
1944		evaluate(add(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI + NewJ.
1945		evaluate(minus(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI - NewJ.
1946		evaluate(multiplication(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI * NewJ.
1947		evaluate(div(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), J =\= 0, Res is NewI // NewJ.
1948		evaluate(modulo(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), J =\= 0, Res is NewI mod NewJ.
1949		evaluate(power_of(I,J),Res) :- evaluate(I,NewI), evaluate(J,NewJ), Res is NewI ^ NewJ.
1950
1951
1952		add_wd_pos(Hyps,POs,Sequent,NewSequent) :-
1953		reverse(POs,List),
1954		add_pos(Hyps,Sequent,NewSequent,List).
1955
1956		add_pos(_,Sequent,Sequent,[]) :- !.
1957		add_pos(Hyps,InnerSequent,NewSequent,[PO|R]) :- add_pos(Hyps,sequent(Hyps,PO,InnerSequent),NewSequent,R).
1958
1959		% add a sequent per disjunct
1960		extract_disjuncts(Q,Hyps0,Goal,Cont,sequent(Hyps,Goal,Cont)) :- Q \= disjunct(_,_), add_hyp(Q,Hyps0,Hyps).
1961		extract_disjuncts(disjunct(L,R),Hyps0,Goal,Cont,LRSequent) :-
1962		extract_disjuncts(L,Hyps0,Goal,success(PO_Nr),LSequent),
1963		extract_disjuncts(R,Hyps0,Goal,Cont,RSequent),
1964		append_sequents(LSequent,RSequent,LRSequent,PO_Nr).
1965
1966		% add sequents as last continuation
1967		append_sequents(sequent(Hyps,Goal,Cont),InnerCont,sequent(Hyps,Goal,Sequent),PO_Nr) :-
1968		(Cont = success(PO_Nr) -> Sequent = InnerCont
1969		; append_sequents(Cont,InnerCont,Sequent,PO_Nr)).
1970
1971		animation_function_result(state(counter_example(_),_),[((1,1),'Counter example found.')]).
1972		animation_function_result(state(success(Nr),_),[((1,1),Txt)]) :-
1973		(get_po_description(Nr,PO) -> ajoin(['Proof of ',PO,' succeeded.'],Txt)
1974		; Txt = 'Proof succeeded.').
1975		animation_function_result(state(Sequent,_),Matrix) :-
1976		Sequent = sequent(_,_,Cont),
1977		cont_length(Cont,LCont),
1978		findall(((RowNr,ColNr),Cell), (cell_content(RowNr,ColNr,Sequent,Cell,LCont)), Matrix).
1979
1980		cell_content(Row,1,sequent(Hyps,_,_),Cell,_) :- nth1(Row,Hyps,RowHyp), translate_term(RowHyp,Cell).
1981		cell_content(Row,1,sequent(Hyps,_,_),'---------------------',_) :- length(Hyps,LHyps), Row is LHyps + 1.
1982		cell_content(Row,1,sequent(Hyps,Goal,_),Cell,_) :- length(Hyps,LHyps), Row is LHyps + 2, translate_term(Goal,Cell).
1983
1984		cell_content(Row,Col,Sequent,Cell,LCont) :-
1985		extract_continuations(Sequent,LCont,Cont,Col),
1986		cell_content(Row,1,Cont,Cell,LCont).
1987
1988		extract_continuations(sequent(_,_,Cont),LCont,Cont,ColNr) :-
1989		cont_length(Cont,ActualLCont),
1990		ColNr is LCont - ActualLCont + 2.
1991		extract_continuations(sequent(_,_,Cont),LCont,FoundCont,ColNr) :-
1992		extract_continuations(Cont,LCont,FoundCont,ColNr).
1993
1994		get_continuations(success(_),[]).
1995		get_continuations(sequent(_,_,success(_)),[]).
1996		get_continuations(sequent(_,_,sequent(Hyps,Goal,NxtCont)),[sequent(Hyps,Goal)|CT]) :-
1997		get_continuations(NxtCont,CT).
1998
1999		find_transitions(Sequent,Info,Trans) :-
2000		findall(T,( sequent_prover_trans(T,state(Sequent,Info),_)
2001		; sequent_prover_trans_desc(T,state(Sequent,Info),_,_)),TransL),
2002		remove_dups(TransL,Trans).
2003
2004		animation_image_right_click_transition(Row,1,Trans,state(sequent(Hyps,Goal,Cont),Info)) :- nth1(Row,Hyps,Hyp),
2005		select(Hyp,Hyps,Hyps0),
2006		find_transitions(sequent(Hyps,Goal,Cont),Info,AllTransitions),
2007		find_transitions(sequent(Hyps0,Goal,Cont),Info,Transitions0),
2008		member(Trans,AllTransitions),
2009		Trans \= mon_deselect(_),
2010		\+ member(Trans,Transitions0).
2011		animation_image_right_click_transition(Row,1,Trans,state(sequent(Hyps,Goal,Cont),Info)) :-
2012		length(Hyps,LHyps),
2013		Row is LHyps + 2,
2014		find_transitions(sequent([],Goal,Cont),Info,Transitions),
2015		member(Trans,Transitions),
2016		Trans \= reselect_hyp(_).
2017		animation_image_right_click_transition(Row,1,mon_deselect(Row)).
2018
2019		% ------------------------
2020
2021		is_natural_set(natural_set).
2022		is_natural_set('NATURAL').
2023
2024		is_natural1_set(natural1_set).
2025		is_natural1_set('NATURAL1').
2026
2027		is_integer_set(integer_set).
2028		is_integer_set('INTEGER').
2029
2030		is_less_eq(less_equal(P,Q),P,Q).
2031		is_less_eq(greater_equal(Q,P),P,Q).
2032
2033		is_less(less(P,Q),P,Q).
2034		is_less(greater(Q,P),P,Q).
2035
2036		is_equality(equal(A,B),A,B).
2037		is_equality(equal(B,A),A,B).
2038
2039		is_no_equality(negation(equal(A,B)),A,B).
2040		is_no_equality(negation(equal(B,A)),A,B).
2041		is_no_equality(not_equal(A,B),A,B).
2042		is_no_equality(not_equal(B,A),A,B).
2043
2044		is_equivalence(equivalence(A,B),A,B).
2045		is_equivalence(equivalence(B,A),A,B).
2046
2047		is_inter(intersection(A,B),A,B). % TODO: extend to nested inter
2048		is_inter(intersection(B,A),A,B).
2049
2050		is_minus(NE,E) :- number(NE), NE < 0, E is abs(NE) ; NE = unary_minus(E).
2051
2052	?	is_empty(Expr,Term) :- is_equality(Expr,Term,empty_set).
2053		is_empty(Expr,Term) :- Expr = subset(Term,empty_set).
2054
2055		is_negation(Q,negation(P)) :- equal_terms(P,Q).
2056
2057		of_integer_type('$'(E),Info) :-
2058		atomic(E),
2059		of_integer_type(E,Info).
2060
2061		of_integer_type(E,Info) :-
2062		get_meta_info(ids_types,Info,STypes),
2063		member(b(identifier(E),integer,_),STypes).
2064
2065		singleton_set(set_extension([X]),X).
2066
2067		rewrite_comp_id([X],[X]).
2068		rewrite_comp_id([domain_restriction(S,event_b_identity),domain_restriction(T,event_b_identity)|R],Res) :- !,
2069	?	rewrite_comp_id([domain_restriction(intersection(S,T),event_b_identity)|R],Res).
2070		rewrite_comp_id([domain_restriction(S,event_b_identity),domain_subtraction(T,event_b_identity)|R],Res) :- !,
2071	?	rewrite_comp_id([domain_restriction(set_subtraction(S,T),event_b_identity)|R],Res).
2072		rewrite_comp_id([domain_subtraction(S,event_b_identity),domain_subtraction(T,event_b_identity)|R],Res) :- !,
2073	?	rewrite_comp_id([domain_subtraction(union(S,T),event_b_identity)|R],Res).
2074	?	rewrite_comp_id([E,F|R], [E|Res]) :- rewrite_comp_id([F|R],Res).
2075
2076		bwd_to_fwd_comp(ring(R,S),Res) :-
2077	?	bwd_to_fwd_comp(R,R2),
2078		bwd_to_fwd_comp(S,S2),
2079		Res = composition(S2,R2).
2080		bwd_to_fwd_comp(X,X) :- X \= ring(_,_).
2081
2082		% change order of operation if Op is associative
2083		reorder(C,Res,Op) :-
2084		C=..[Op,A,B],
2085		B=..[Op,L,Rest],!,
2086		R=..[Op,A,L],
2087		append_to_op(Rest,R,Res,Op).
2088		reorder(C,C,Op) :- C=..[Op,_,_].
2089
2090		append_to_op(C,R,Res,Op) :-
2091		C=..[Op,A,B],
2092		Inner=..[Op,R,A],!,
2093		append_to_op(B,Inner,Res,Op).
2094		append_to_op(B,R,C,Op) :- C=..[Op,R,B].
2095
2096	?	member_of(Op,X,Term) :- Term=..[Op,A,B], !, (el_of_op(A,X,Op) ; el_of_op(B,X,Op)).
2097		el_of_op(Term,X,Op) :- Term=..[Op,A,B], !, (el_of_op(A,X,Op) ; el_of_op(B,X,Op)).
2098		el_of_op(P,P,_).
2099
2100		remove_from_op(El,Term,NewTerm,Op) :-
2101		op_to_list(Term,List,Op),
2102		remove_from_list(El,List,List0),
2103		list_to_op(List0,NewTerm,Op).
2104
2105		remove_from_list(_,[],[]).
2106		remove_from_list(E,[E|T],T2) :- remove_from_list(E,T,T2).
2107		remove_from_list(E,[X|T],[X|T2]) :- X \= E, remove_from_list(E,T,T2).
2108
2109		op_to_list(Term,NList,Op) :- op_to_list(Term,[],NList,Op).
2110		op_to_list(Term,OList,NList,Op) :-
2111		Term=..[Op,A,B],!,
2112		op_to_list(B,OList,L1,Op),
2113		op_to_list(A,L1,NList,Op).
2114		op_to_list(Term,L,[Term|L],_).
2115
2116		list_to_op([A],A,_).
2117		list_to_op([A,B|L],Res,Op) :- C=..[Op,A,B], list_to_op(L,C,Res,Op).
2118
2119		list_to_op([],C,C,_).
2120		list_to_op([X|T],C,Res,Op) :- NC=..[Op,C,X], list_to_op(T,NC,Res,Op).
2121
2122		or_equal([],_,D,D).
2123		or_equal([A|L],E,D,Res) :- or_equal(L,E,disjunct(D,equal(E,A)),Res).
2124
2125		and_empty(C,Conj,Op) :- C=..[Op,A,B], and_empty(A,ConjA,Op), and_empty(B,ConjB,Op), !, Conj = conjunct(ConjA,ConjB).
2126		and_empty(A,equal(A,empty_set),_).
2127
2128		and_imp(C,R,Conj,Op) :- C=..[Op,A,B], and_imp(A,R,ConjA,Op), and_imp(B,R,ConjB,Op), !, Conj = conjunct(ConjA,ConjB).
2129		and_imp(A,R,implication(R,A),conjunct).
2130		and_imp(A,R,implication(A,R),disjunct).
2131
2132		union_subset(S,union(A,B),Conj) :- union_subset(S,A,ConjA), union_subset(S,B,ConjB), !, Conj = conjunct(ConjA,ConjB).
2133		union_subset(S,A,subset(A,S)).
2134
2135		union_subset_member(T,union(A,B),Conj) :-
2136		union_subset_member(T,A,ConjA),
2137		union_subset_member(T,B,ConjB),!,
2138		Conj = conjunct(ConjA,ConjB).
2139		union_subset_member(T,SetF,member(F,T)) :- singleton_set(SetF,F), !.
2140		union_subset_member(T,A,subset(A,T)).
2141
2142		member_union(E,union(A,B),Disj) :- member_union(E,A,DisjA), member_union(E,B,DisjB), !, Disj = disjunct(DisjA,DisjB).
2143		member_union(E,A,member(E,A)).
2144
2145		subset_inter(S,intersection(A,B),Conj) :- subset_inter(S,A,ConjA), subset_inter(S,B,ConjB), Conj = conjunct(ConjA,ConjB), !.
2146		subset_inter(S,A,subset(S,A)).
2147
2148		member_intersection(E,intersection(A,B),Conj) :-
2149		member_intersection(E,A,ConjA),
2150		member_intersection(E,B,ConjB),!,
2151		Conj = conjunct(ConjA,ConjB).
2152		member_intersection(E,A,member(E,A)).
2153
2154		distribute_exists(X,disjunct(A,B),Disj) :- distribute_exists(X,A,DisjA), distribute_exists(X,B,DisjB), !, Disj = disjunct(DisjA,DisjB).
2155		distribute_exists(X,P,exists(X,P)).
2156
2157		distribute_forall(X,P,conjunct(A,B),Conj) :-
2158		distribute_forall(X,P,A,ConjA),
2159		distribute_forall(X,P,B,ConjB),!,
2160		Conj = conjunct(ConjA,ConjB).
2161		distribute_forall(X,P,A,forall(X,P,A)).
2162
2163		member_couples(E,F,[Q],_,[member(couple(E,F),Q)]).
2164	?	member_couples(E,F,[P|Q],[X|T],[member(couple(E,X),P)|R]) :- member_couples(X,F,Q,T,R).
2165
2166		distri_reverse(C,U,Op) :- C=..[Op,A,B], distri_reverse(A,UA,Op), distri_reverse(B,UB,Op), !, U=..[Op,UA,UB].
2167		distri_reverse(A,reverse(A),_).
2168
2169		distri_reverse_reverse(C,U,Op) :- C=..[Op,A,B], distri_reverse_reverse(A,UA,Op), distri_reverse_reverse(B,UB,Op), !, U=..[Op,UB,UA].
2170		distri_reverse_reverse(A,reverse(A),_).
2171
2172		distri_union(union(A,B),Union,Op) :- distri_union(A,L,Op), distri_union(B,R,Op), !, Union = union(L,R).
2173		distri_union(A,C,Op) :- C=..[Op,A].
2174
2175		image_union(F,union(A,B),Union) :- image_union(F,A,L), image_union(F,B,R), !, Union = union(L,R).
2176		image_union(F,A,image(F,A)).
2177
2178		union_image(union(A,B),S,Union) :- union_image(A,S,L), union_image(B,S,R), !, Union = union(L,R).
2179		union_image(A,S,image(A,S)).
2180
2181		finite_union(union(A,B),Conj) :- finite_union(A,ConjA), finite_union(B,ConjB), !, Conj = conjunct(ConjA,ConjB).
2182		finite_union(S,finite(S)).
2183
2184		finite_intersection(intersection(A,B),Disj) :- finite_intersection(A,DisjA), finite_intersection(B,DisjB), !, Disj = disjunct(DisjA,DisjB).
2185		finite_intersection(S,finite(S)).
2186
2187		last_overwrite(overwrite(_,B),Res) :- !, last_overwrite(B,Res).
2188		last_overwrite(B,B).
2189
2190		and_equal_type(intersection(A,B),Ty,Conj) :- and_equal_type(A,Ty,L), and_equal_type(B,Ty,R), !, Conj = conjunct(L,R).
2191		and_equal_type(A,Ty,equal(A,Ty)).
2192
2193		distri(C,Res,Op1,Op2) :-
2194		C=..[Op1,A,B],
2195		(X = A ; X = B),
2196		functor(X,Op2,2),
2197	?	distribute_op(C,X,Op1,Op2,Res).
2198
2199		distri_r(C,Res,Op1,Op2) :-
2200		C=..[Op1,_,X],
2201		functor(X,Op2,2),
2202	?	distribute_op(C,X,Op1,Op2,Res).
2203
2204		distri_l(C,Res,Op1,Op2) :-
2205		C=..[Op1,X,_],
2206		functor(X,Op2,2),
2207	?	distribute_op(C,X,Op1,Op2,Res).
2208
2209		distribute_op(C,X,Op1,Op2,Res) :-
2210		op_to_list(X,L,Op2),
2211	?	distribute(C,X,L,CN,Op1),
2212		list_to_op(CN,Res,Op2).
2213
2214		distribute(_,_,[],[],_).
2215	?	distribute(C,X,[D|T],[N|R],Op) :- select_op(X,C,D,N,Op), distribute(C,X,T,R,Op).
2216
2217		distri_r(C,Res,Op1,Op2,Op3) :-
2218		C=..[Op1,_,X],
2219	?	distri_and_change(C,X,Op1,Op2,Op3,Res).
2220
2221		distri_l(C,Res,Op1,Op2,Op3) :-
2222		C=..[Op1,X,_],
2223	?	distri_and_change(C,X,Op1,Op2,Op3,Res).
2224
2225		% Op2 changes to Op3
2226		distri_and_change(C,X,Op1,Op2,Op3,Res) :-
2227		functor(X,Op2,2),
2228		op_to_list(X,L,Op2),
2229	?	distribute(C,X,L,CN,Op1),
2230		list_to_op(CN,Res,Op3).
2231
2232		distri_setminus(C,Res) :-
2233		C = set_subtraction(_,X),
2234		X = union(_,_),
2235		select_op(X,C,NewC,set_subtraction),
2236		op_to_list(NewC,CL,set_subtraction),
2237		op_to_list(X,L,union),
2238		append(CL,L,L2),
2239		list_to_op(L2,Res,set_subtraction).
2240
2241		all_pairs(L,Pairs) :- findall([X,Y], (combination(L,[X,Y])), Pairs).
2242
2243		combination(_,[]).
2244		combination([X|T],[X|C]) :- combination(T,C).
2245		combination([_|T],[X|C]) :- combination(T,[X|C]).
2246
2247		all_in_set([E],S,Hyps) :- member_hyps(member(E,S),Hyps).
2248	?	all_in_set([E|R],S,Hyps) :- member_hyps(member(E,S),Hyps), all_in_set(R,S,Hyps).
2249
2250		map_dom([couple(X,_)],[X]) :- !.
2251		map_dom([couple(X,_)|T],[X|R]) :- map_dom(T,R).
2252
2253		map_ran([couple(_,A)],[A]) :- !.
2254		map_ran([couple(_,B)|T],[B|R]) :- map_ran(T,R).
2255
2256		all_map_to([couple(_,F)],E) :- equal_terms(E,F), !.
2257		all_map_to([couple(_,F)|T],E) :- equal_terms(E,F), all_map_to(T,E).
2258
2259		convert_map_to([couple(X,Y)],[couple(Y,X)]) :- !.
2260		convert_map_to([couple(X,Y)|T],[couple(Y,X)|R]) :- convert_map_to(T,R).
2261
2262		list_subset([],_).
2263		list_subset([E|T],L) :- memberchk(E,L), list_subset(T,L).
2264
2265		new_identifier(Expr,I) :-
2266		used_identifiers(Expr,L),
2267	?	possible_identifier(X),
2268		I = '$'(X),
2269	?	\+ member(I,L),!.
2270
2271		used_identifiers(Term,[]) :- atomic(Term), !.
2272		used_identifiers(Term,[Term]) :- Term = '$'(E), atomic(E), !.
2273		used_identifiers(C,Res) :-
2274		C =.. [_|Args],
2275		maplist(used_identifiers,Args,L),
2276		append(L,Res).
2277
2278		free_identifiers(exists(Ids,P),Res) :- !, free_identifiers(P,Free), list_difference(Free,Ids,Res).
2279		free_identifiers(Term,Res) :-
2280		(Term = forall(Ids,P,E)
2281		; Term = event_b_comprehension_set(Ids,E,P)
2282		; Term = quantified_intersection(Ids,P,E)
2283		; Term = quantified_union(Ids,P,E)), !,
2284		free_identifiers(implication(P,E),FreeImp), list_difference(FreeImp,Ids,Res).
2285		free_identifiers(Term,[]) :- atomic(Term), !.
2286		free_identifiers(Term,[Term]) :- Term = '$'(E), atomic(E), !.
2287		free_identifiers(C,Res) :-
2288		C =.. [_|Args],
2289		maplist(free_identifiers,Args,L),
2290		append(L,Res).
2291
2292		identifier(x).
2293		identifier(y).
2294		identifier(z).
2295
2296	?	possible_identifier(Z) :- identifier(Z).
2297		possible_identifier(Z) :- identifier(X), identifier(Y), atom_concat(X,Y,Z).
2298
2299		new_identifiers(Expr,1,[Id]) :- !, new_identifier(Expr,Id).
2300	?	new_identifiers(Expr,Nr,Ids) :- used_identifiers(Expr,L), possible_identifier(X), I = '$'(X), \+ member(I,L), !, range_ids(X,Nr,Ids).
2301
2302	?	range_ids(X,Nr,L) :- range(X,1,Nr,L).
2303		range(X,I,I,['$'(XI)]) :- atom_int_concat(X,I,XI).
2304	?	range(X,I,K,['$'(XI)|L]) :- I < K, I1 is I + 1, atom_int_concat(X,I,XI), range(X,I1,K,L).
2305
2306		atom_int_concat(X,I,XI) :-
2307		atom_codes(X,CX),
2308		number_codes(I,CI),
2309		append(CX,CI,COut),
2310		atom_codes(XI,COut).
2311
2312		new_function(Expr,F) :- used_identifiers(Expr,L), possible_function(X), F = '$'(X), \+ member(F,L), !.
2313
2314		func_id(f).
2315		func_id(g).
2316		func_id(h).
2317
2318		possible_function(Z) :- func_id(Z).
2319		possible_function(Z) :- func_id(X), func_id(Y), atom_concat(X,Y,Z).
2320
2321		remove_duplicates(L,Res) :- without_duplicates(L,[],Res), L \= Res.
2322		remove_duplicates(C,Res,Op) :-
2323		op_to_list(C,List,Op),
2324		remove_duplicates(List,ResL),
2325	?	list_to_op(ResL,Res,Op).
2326
2327		without_duplicates(L,Res) :- without_duplicates(L,[],Res).
2328
2329		without_duplicates([],List,List).
2330		without_duplicates([E|R],Filtered,Res) :-
2331	?	member(F,Filtered),
2332		equal_terms(E,F),!,
2333		without_duplicates(R,Filtered,Res).
2334		without_duplicates([E|R],Filtered, Res) :-
2335		\+ member(E,Filtered),
2336		append(Filtered,[E],New),
2337		without_duplicates(R,New,Res).
2338
2339		min_list([H|T], Min) :- number(H) -> min_list(T,H,Min) ; min_list(T,Min).
2340
2341		min_list([],Min,Min).
2342		min_list([H|T],Min0,Min) :-
2343		number(H),!,
2344		Min1 is min(H,Min0),
2345		min_list(T,Min1,Min).
2346		min_list([_|T],Min0,Min) :-
2347		min_list(T,Min0,Min).
2348
2349	?	remove_greater(L,I,Res) :- only_min(L,I,[],Res), L \= Res.
2350
2351		only_min([],_,List,List).
2352		only_min([E|R],I,Filtered, Res) :-
2353		\+ number(E),!,
2354		append(Filtered,[E],New),
2355	?	only_min(R,I,New,Res).
2356		only_min([E|R],I,Filtered,Res) :-
2357		E > I,
2358	?	only_min(R,I,Filtered,Res).
2359		only_min([E|R],I,Filtered,Res) :-
2360		E =:= I,
2361		member(E,Filtered),
2362		only_min(R,I,Filtered,Res).
2363		only_min([E|R],I,Filtered,Res) :-
2364		E =:= I,
2365		\+ member(E,Filtered),
2366		append(Filtered,[E],New),
2367	?	only_min(R,I,New,Res).
2368
2369		max_list([H|T],Max) :- number(H) -> max_list(T,H,Max) ; max_list(T,Max).
2370
2371		max_list([],Max,Max).
2372		max_list([H|T],Max0,Max) :-
2373		number(H),!,
2374		Max1 is max(H,Max0),
2375		max_list(T,Max1,Max).
2376		max_list([_|T],Max0,Max) :-
2377		max_list(T,Max0,Max).
2378
2379		remove_smaller(L,I,Res) :- only_max(L,I,[],Res), L \= Res.
2380
2381		only_max([],_,List,List).
2382		only_max([E|R],I,Filtered, Res) :-
2383		\+ number(E),!,
2384		append(Filtered,[E],New),
2385		only_max(R,I,New,Res).
2386		only_max([E|R],I,Filtered,Res) :-
2387		E < I,
2388		only_max(R,I,Filtered,Res).
2389		only_max([E|R],I,Filtered,Res) :-
2390		E =:= I,
2391		member(E,Filtered),
2392		only_max(R,I,Filtered,Res).
2393		only_max([E|R],I,Filtered,Res) :-
2394		E =:= I,
2395		\+ member(E,Filtered),
2396		append(Filtered,[E],New),
2397		only_max(R,I,New,Res).
2398
2399	?	overwrite_type([Ty|R],_,ListOut,Info) :- type_expression(Ty,Info), !, overwrite_type(R,[Ty],ListOut,Info).
2400		overwrite_type([S|R],Prev,ListOut,Info) :- append(Prev,[S],ListIn), overwrite_type(R,ListIn,ListOut,Info).
2401		overwrite_type([],L,L,_).
2402
2403		change_sign(L,NL,Nr) :- remove_minus(L,NL,Nr), Nr > 0.
2404
2405	?	remove_minus([NE|R],[E|T],NrN) :- is_minus(NE,E), remove_minus(R,T,Nr), NrN is Nr + 1, !.
2406		remove_minus([E|R],[E|T],Nr) :- remove_minus(R,T,Nr).
2407		remove_minus([],[],0).
2408
2409		remove_unused_identifier(L,P,Used) :-
2410	?	member(Z,L),
2411		used_identifiers(P,Ids),
2412		member(Z,Ids),
2413		list_intersection(L,Ids,Used),
2414		Used \= L.
2415
2416	?	rewrite_once(X,Y,E,NewE) :- is_subterm(X,E), rewrite_once2(X,Y,E,NewE), E \= NewE.
2417
2418		rewrite_once2(X,Y,E,NewE) :- equal_terms(X,E),!, NewE=Y.
2419		rewrite_once2(_X,_Y,E,NewE) :- atomic(E),!, NewE=E.
2420		rewrite_once2(_X,_Y,'$'(E),NewE) :- atomic(E),!, NewE='$'(E).
2421		rewrite_once2(X,Y,C,NewC) :- C=..[Op|Args],
2422	?	select(Arg,Args,NewArg,NewArgs),
2423		rewrite_once2(X,Y,Arg,NewArg),
2424		NewC =.. [Op|NewArgs].
2425
2426		wd_strict_term(T) :- atomic(T), !.
2427		wd_strict_term('$'(E)) :- atomic(E), !.
2428		wd_strict_term(T) :-
2429		\+ with_ids(T,_), % quantified_union, quantified_intersection, event_b_comprehension_set, forall, exists -> not WD strict
2430		T=..[F|Args],
2431		\+ not_wd_strict(F),
2432		wd_strict_args(Args).
2433
2434		wd_strict_args([]).
2435		wd_strict_args([T|Args]) :- wd_strict_term(T), wd_strict_args(Args).
2436
2437		not_wd_strict(implication).
2438		not_wd_strict(conjunct).
2439		not_wd_strict(disjunct).
2440
2441		is_subterm(Term,Term).
2442		is_subterm(Subterm,Term) :-
2443		Term=..[_|Args],
2444	?	member(Arg,Args),
2445	?	is_subterm(Subterm,Arg).
2446
2447		split_composition(Comp,LComp,RComp) :-
2448		op_to_list(Comp,List,composition),
2449		append(L,R,List),
2450	?	list_to_op(L,LComp,composition),
2451	?	list_to_op(R,RComp,composition).
2452
2453		deriv_fcomp_dom(Comp,Functor,Res) :-
2454		Comp = composition(_,_),
2455		op_to_list(Comp,List,composition),
2456		append(L,[At|R],List),
2457		At=..[Functor,P,Q],
2458		list_to_op([Q|R],RComp,composition),
2459		New=..[Functor,P,RComp],
2460		append(L,[New],ResList),
2461	?	list_to_op(ResList,Res,composition),
2462		Comp \= Res.
2463
2464		deriv_fcomp_ran(Comp,Functor,Res) :-
2465		Comp = composition(_,_),
2466		op_to_list(Comp,List,composition),
2467		append(L,[At|R],List),
2468		At=..[Functor,P,Q],
2469		append(L,[P],NewL),
2470	?	list_to_op(NewL,LComp,composition),
2471		New=..[Functor,LComp,Q],
2472	?	list_to_op([New|R],Res,composition),
2473		Comp \= Res.
2474
2475		replace_used_ids([],_,[]).
2476		replace_used_ids(['$'(X)|T],IdsTypes,['$'(Y)|R]) :-
2477	?	member(b(identifier(X),_,_),IdsTypes), !,
2478		new_aux_identifier(IdsTypes,Y),
2479		replace_used_ids(T,[b(identifier(Y),any,[])|IdsTypes],R).
2480		replace_used_ids(['$'(X)|T],IdsTypes,['$'(X)|R]) :-
2481		replace_used_ids(T,[b(identifier(X),any,[])|IdsTypes],R).
2482
2483		rewrite_pairwise_rev(Ids1,Ids2,P,NewP) :-
2484		reverse(Ids1,RevIds1),
2485		reverse(Ids2,RevIds2),
2486		rewrite_pairwise(RevIds1,RevIds2,P,NewP).
2487
2488		rewrite_pairwise([],[],E,E).
2489		rewrite_pairwise([X|TX],[Y|TY],E,Res) :-
2490		rewrite(X,Y,E,NewE),
2491		rewrite_pairwise(TX,TY,NewE,Res).
2492
2493		pairwise_distict(E,Ids) :- pairwise_distict(E,Ids,_).
2494
2495		pairwise_distict(couple(E,F),Ids,Ids1) :- pairwise_distict(E,Ids,Ids0), pairwise_distict(F,Ids0,Ids1).
2496		pairwise_distict(E,Ids,Ids0) :- E = '$'(X), atomic(X), select(E,Ids,Ids0).
2497
2498		same_type('$'(S),'$'(T),List) :-
2499	?	member(b(identifier(S),Type,_),List),
2500		member(b(identifier(T),Type,_),List),
2501		Type \= any.
2502
2503	?	check_type('$'(S),_,IdsTypes,Type) :- !, member(b(identifier(S),Type,_),IdsTypes).
2504		check_type(_,'$'(T),IdsTypes,Type) :- !, member(b(identifier(T),Type,_),IdsTypes).
2505		check_type(S,_,IdsTypes,Type) :- check_type(S,IdsTypes,Type).
2506
2507		check_type(S,IdsTypes,Type) :-
2508		new_aux_identifier(IdsTypes,X),
2509		get_typed_identifiers(equal('$'(X),S),[identifier(IdsTypes)],L),
2510		member(b(identifier(X),Type,_),L).
2511
2512		new_aux_identifier(IdsTypes,X) :-
2513	?	possible_identifier(X),
2514	?	\+ member(b(identifier(X),_,_),IdsTypes),!.
2515
2516		image_intersection(F,intersection(A,B),Inter) :- image_intersection(F,A,L), image_intersection(F,B,R), !, Inter = intersection(L,R).
2517		image_intersection(F,A,image(F,A)).
2518
2519		type_expression(bool_set,_).
2520		type_expression(Z,_) :- is_integer_set(Z).
2521		type_expression(S,Info) :- is_deferred_set(S,Info).
2522	?	type_expression(pow_subset(Ty),Info) :- type_expression(Ty,Info).
2523	?	type_expression(cartesian_product(Ty1,Ty2),Info) :- type_expression(Ty1,Info), type_expression(Ty2,Info).
2524
2525		get_type_expression(integer,'INTEGER').
2526		get_type_expression(boolean,bool_set).
2527		get_type_expression(set(S),pow_subset(T)) :- get_type_expression(S,T).
2528		get_type_expression(couple(A,B),cartesian_product(S,T)) :- get_type_expression(A,S), get_type_expression(B,T).
2529
2530		is_deferred_set('$'(Set),Info) :-
2531		get_meta_info(rawsets,Info,RawSets),
2532		member(deferred_set(_,Set),RawSets).
2533
2534		equal_terms(X,X) :- !.
2535		equal_terms(X,Y) :-
2536		ground(X),
2537		ground(Y),
2538		list_representation(X,LX),
2539		list_representation(Y,LY),
2540		equal_op(LX,LY),
2541		equal_length(LX,LY),
2542		equal_lists(LX,LY).
2543
2544		equal_lists(L1,L2) :- sort_list(L1,SL1), sort_list(L2,SL2), SL1 = SL2.
2545
2546		stronger_list(L1,L2) :- sort_list(L1,SL1), sort_list(L2,SL2), list_implies(SL1,SL2).
2547
2548		list_implies([],[]).
2549		list_implies([H1|T1], [H2|T2]) :-
2550		implies(H1,H2),
2551		list_implies(T1,T2).
2552
2553		% a hypothesis "a > b" is a sufficient condition to discharge the goal "a >= b" with HYP
2554		implies(X,X).
2555		implies(c(L,equal),c(L,greater_equal)).
2556		implies(c(L,equal),c(RL,greater_equal)) :- reverse(L,RL).
2557		implies(c(L,greater),c(L,greater_equal)).
2558		implies(c(L,greater),c(L,not_equal)).
2559
2560		comparable(G1,G2) :- G1=..[T1,_,_], G2=..[T2,_,_], comparison(T1), comparison(T2).
2561		comparable(G1,G2) :- G1=..[F,P], G2=..[F,Q], !, comparable(P,Q).
2562		comparable(G1,G2) :- functor(G1,F,_), functor(G2,F,_).
2563
2564		comparison(equal).
2565		comparison(greater).
2566		comparison(greater_equal).
2567		comparison(less).
2568		comparison(less_equal).
2569		comparison(not_equal).
2570
2571		list_representation(A,B,OList,L3) :-
2572		list_representation(A,OList,L1),
2573		list_representation(B,[],L2),
2574		append(L1,L2,L3).
2575
2576		list_representation(C,L) :- list_representation(C,[],L).
2577		list_representation('$'(X),L,Res) :- !, Res=[X|L].
2578		list_representation(less_equal(A,B),OList,Res) :- !, list_representation(B,A,OList,NList), Res=[c(NList,greater_equal)].
2579		list_representation(greater_equal(A,B),OList,Res) :- !, list_representation(A,B,OList,NList), Res=[c(NList,greater_equal)].
2580		list_representation(less(A,B),OList,Res) :- !, list_representation(B,A,OList,NList), Res=[c(NList,greater)].
2581		list_representation(greater(A,B),OList,Res) :- !, list_representation(A,B,OList,NList), Res=[c(NList,greater)].
2582
2583		list_representation(minus(A,B),OList,NList) :- !,
2584		collect_subtrahend(minus(A,B),Subtraction),
2585		Subtraction = [Minuend, Subtrahend],
2586		exclude(zero, Subtrahend, NSubtrahend),
2587		(NSubtrahend == [] -> NList = [Minuend] ;
2588		append(OList,[c([Minuend, NSubtrahend],minus)],NList)).
2589		list_representation(div(A,B),OList,NList) :- !,
2590		collect_divisor(div(A,B),Division),
2591		Division = [Divident, Divisor],
2592		exclude(one, Divisor, NDivisor),
2593		(NDivisor == [] -> NList = [Divident] ;
2594		append(OList,[c([Divident, NDivisor],div)],NList)).
2595
2596		list_representation(C,OList,Res) :-
2597		C=..[F,A,B],
2598	?	member(F,[conjunct,disjunct,intersection,union]), !,
2599		collect_components(A,B,OList,NList,F),
2600		Res=[c(NList,F)].
2601		list_representation(add(A,B),OList,Res) :- !,
2602		collect_components(A,B,OList,NList,add),
2603		exclude(zero, NList, NList2),
2604		(NList2 == [] -> Res = [0] ;
2605		NList2 \= [_]-> Res = [c(NList2,add)] ;
2606		Res = NList2).
2607		list_representation(multiplication(A,B),OList,Res) :- !,
2608		collect_components(A,B,OList,NList,multiplication),
2609		exclude(one, NList, NList2),
2610		(member(0, NList2) -> Res = [0] ;
2611		NList2 == [] -> Res = [1] ;
2612		NList2 \= [_]-> Res = [c(NList2,multiplication)] ;
2613		Res = NList2).
2614		list_representation(set_extension(A),OList,Res) :- !, list_representation_of_list(A,OList,NList), sort(NList,S), Res=[c(S,set_extension)].
2615		list_representation([A|T],OList,Res) :- !, list_representation_of_list([A|T],OList,NList), Res=[c(NList,list)].
2616		list_representation(C,OList,Res) :- C=..[F,A], !, list_representation(A,OList,NList), Res=[c(NList,F)].
2617		list_representation(C,OList,Res) :-
2618		C=..[F,A,B],!,
2619		list_representation(A,B,OList,NList), Res=[c(NList,F)].
2620		list_representation(X,L,[X|L]) :- atomic(X).
2621
2622		list_representation_of_list([],OList,OList).
2623		list_representation_of_list([A|T],OList,NList) :- list_representation(A,OList,L1), list_representation_of_list(T,[],L2),append(L1,L2,NList).
2624
2625		one(X) :- X is 1.
2626		zero(X) :- X is 0.
2627
2628		collect_components(A,B,OList,NList,T) :-
2629		collect_component(A,OList,L1,T),
2630		collect_component(B,L1,NList,T).
2631
2632		collect_component('$'(X),OList,NList,_) :- !,
2633		append(OList,[X],NList).
2634		collect_component(X,OList,NList,_) :-
2635		atomic(X),!,
2636		append(OList,[X],NList).
2637		collect_component(C,OList,NList,T) :-
2638		C=..[T,A,B],!,
2639		collect_components(A,B,OList,NList,T).
2640		collect_component(X,OList,NList,_) :-
2641		list_representation(X,[],L1),
2642		append(OList,L1,NList).
2643
2644		collect_subtrahend(minus(A, B), [LA, Sub]) :-
2645		A \= minus(_,_), !,
2646		list_representation(A,[LA]),
2647		(B = 0 -> Sub = [] ;
2648		list_representation(B,[LB]), Sub = [LB]).
2649		collect_subtrahend(minus(A, B), [Minuend, NSubtrahends]) :-
2650		collect_subtrahend(A, [Minuend, Subtrahends]),
2651		list_representation(B,LB),
2652		append(Subtrahends, LB, NSubtrahends).
2653
2654		collect_divisor(div(A, B), [LA, Div]) :-
2655		A \= div(_,_), !,
2656		list_representation(A,[LA]),
2657		(B = 1 -> Div = [] ;
2658		list_representation(B,[LB]), Div = [LB]).
2659		collect_divisor(div(A, B), [Divident, NDivisors]) :-
2660		collect_divisor(A, [Divident, Divisors]),
2661		list_representation(B,LB),
2662		append(Divisors, LB, NDivisors).
2663
2664		sort_list(L,R) :- sort_components(L,S), samsort(S,R).
2665		sort_components([],[]).
2666		sort_components([c(L,T)|Rest], Res) :-
2667	?	member(T,[disjunct,conjunct,union,intersection,add,multiplication,equal,not_equal,negation,unary_minus,equivalence,set_extension,list]), !,
2668		sort_list(L,SL),
2669		sort_components(Rest,R),
2670		Res=[c(SL,T)|R].
2671		sort_components([c(L,T)|Rest], Res) :- !, % non-commutative
2672		sort_components(L,L2),
2673		sort_components(Rest,R),
2674		Res=[c(L2,T)|R].
2675		% sort list of subtrahends or divisors
2676		sort_components([E|Rest], [E|R]) :- atomic(E), !, sort_components(Rest,R).
2677		sort_components([E|Rest], [F|R]) :- sort_list(E,F), sort_components(Rest,R).
2678
2679		equal_op(L1,L2) :- L1 = [c(_,T1)], L2 = [c(_,T2)], !, T1 = T2.
2680		equal_op([E1],[E2]) :- E1 \= [c(_,_)], E2 \= [c(_,_)].
2681
2682		equal_length(L1,L2) :- L1 = [c(A1,_)], L2 = [c(A2,_)], !, same_length(A1, A2).
2683		equal_length([_],[_]).
2684
2685		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
2686		:- if(environ(prob_release,true)).
2687		% Don't include tests in release mode.
2688		:- else.
2689		:- use_module(test_sequent_prover).
2690		:- endif.