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