1		% (c) 2020-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html
4
5		:- module(well_def_prover, [prove_po/3]).
6
7		:- use_module(probsrc(module_information),[module_info/2]).
8		:- module_info(group,well_def_prover).
9		:- module_info(description,'This module proves WD POs.').
10
11		:- use_module(library(avl)).
12		:- use_module(library(lists)).
13
14		:- use_module(wdsrc(well_def_hyps),[get_hyp_var_type/3, portray_hyps/1, get_clash_renaming_subst/2,
15		is_hyp_var/2, is_finite_type_for_wd/2, add_new_hyp_any_vars/3, negate_op/2]).
16
17		:- use_module(wdsrc(well_def_tools), [rename_norm_term/3, member_in_norm_conjunction/2, not_occurs/2, occurs/2]).
18		:- use_module(probsrc(debug)).
19		:- use_module(probsrc(error_manager),[add_error/3, add_internal_error/2]).
20
21		:- use_module(probsrc(custom_explicit_sets),[domain_of_explicit_set_wf/3, equal_avl_tree/2,
22		range_of_explicit_set_wf/3,
23		invert_explicit_set/2,check_interval_in_custom_set/4, is_interval_closure/5,
24		check_avl_in_interval/3, check_avl_subset/2, is_one_element_avl/2,
25		avl_is_interval/3,
26		expand_custom_set_to_list/2, quick_definitely_maximal_set_avl/1,
27		expand_and_convert_to_avl_set/4, safe_is_avl_sequence/1, is_avl_partial_function/1]).
28
29		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
30
31		% PROVING:
32		% --------
33
34		% some more rules are covered in process_sequent_aux of prove_sequent/3
35		prove_po(truth,_,truth).
36		prove_po(_NormTarget,hyp_rec(AVL,_),false_hyp) :- avl_fetch(falsity,AVL).
37		prove_po(NormTarget,hyp_rec(AVL,_),hyp) :- avl_fetch(NormTarget,AVL).
38		prove_po(member(X,Y),Hyps,mem(PT)) :- % Y is usually domain(Func)
39		simplify_expr(Y,Hyps,SY),
40		simplify_expr(X,Hyps,SX),
41		check_member_of_set(SY,SX,Hyps,PT).
42		prove_po(not_member(X,Y),Hyps,mem(PT)) :-
43		simplify_expr(Y,Hyps,SY),
44		simplify_expr(X,Hyps,SX),
45		check_not_member_of_set(SY,SX,Hyps,PT).
46		prove_po(finite(Set),Hyp,finite_set(PT)) :- check_finite(Set,Hyp,PT).
47		prove_po(not_equal(A,B),Hyp,not_equal) :-
48		simplify_expr(A,Hyp,SA),
49		simplify_expr(B,Hyp,SB),
50		check_not_equal(SA,SB,Hyp).
51		prove_po(equal(A,B),Hyp,equal) :- % not generated by our POG
52		simplify_expr(A,Hyp,SA),
53		simplify_expr(B,Hyp,SB),
54		check_equal(SA,SB,Hyp,_).
55		prove_po(greater(A,B),Hyp,PT) :- prove_po(less(B,A),Hyp,PT).
56		prove_po(greater_equal(A,B),Hyp,greater_equal) :- % print(check_leq(B,A)),nl,
57		check_leq(B,A,Hyp).
58		prove_po(less_equal(A,B),Hyp,less_equal) :-
59		check_leq(A,B,Hyp).
60		%prove_po(less_equal_real(A,B),Hyp,less_equal_real) :-
61		% check_leq(A,B,Hyp). % TODO: check that all proof rules are sound for reals, ditto for less
62		prove_po(less(A,B),Hyp,less) :-
63		check_leq(A,B,Hyp),!,
64		check_not_equal(A,B,Hyp).
65		prove_po(subset(A,B),Hyp,PT) :-
66		check_is_subset(A,B,Hyp,PT).
67		prove_po(subset_strict(A,B),Hyp,subset_strict(PT)) :-
68		check_is_subset_strict(A,B,Hyp,PT).
69		prove_po(not_subset_strict(A,B),Hyp,not_subset_strict(PT)) :-
70		check_not_is_subset_strict(A,B,Hyp,PT).
71		prove_po(not_subset(A,B),Hyp,not_subset(PT)) :-
72		check_not_subset(A,B,Hyp,PT).
73		prove_po(conjunct(A,B),Hyp,conj(T1,T2)) :- % generated by Rodin
74		prove_po(A,Hyp,T1),
75		!,
76		prove_po(B,Hyp,T2).
77		prove_po(disjunct(A,B),Hyp,conj(T1,T2)) :- % could be generated by Rodin
78		(% push_normalized_hyp(NotB,Hyp,Hyp2), % % OR_R rule allows to add not(B) as hypothesis
79		prove_po(A,Hyp,T1) -> true
80		; prove_po(B,Hyp,T2)). % OR_R rule allows to add not(A) as hypothesis, this is done in prove_sequent_goal
81		prove_po(implication(A,B),Hyp,imply(T2)) :- % generated by Rodin; now treated in prove_sequent_goal
82		% also generated for power_of_real
83		(prove_negated_po(A,Hyp,PT) -> T2=false_lhs(PT)
84		; debug_println(19,not_pushing_lhs_for_implication(A)),
85		%push_normalized_hyp(A,Hyp,Hyp2), % TODO: activate this
86		prove_po(B,Hyp,T2)
87		).
88		prove_po(exists([$(B0)],forall([$(X)],member($(X),Set),less_equal($(X),$(B0)))),Hyp,finite_max(PT)) :- X \= B0,
89		% generated by Rodin for max(Set)
90		debug_println(19,checking_finite_for_max(Set)),
91		check_finite(Set,Hyp,PT).
92		prove_po(exists([$(B0)],forall([$(X)],member($(X),Set),less_equal($(B0),$(X)))),Hyp,finite_min(PT)) :- X \= B0,
93		% generated by Rodin for min(Set)
94		debug_println(19,checking_finite_for_min(Set)),
95		check_finite(Set,Hyp,PT).
96		prove_po(negation(Goal),Hyp,negation(PT)) :- prove_negated_po(Goal,Hyp,PT).
97		%prove_po(NT,_,_) :- format('Unproven by WD Prover: ~w~n~n',[NT]),fail.
98
99		% some redundancy wrt negate_hyp; but negate_hyp currently does not go inside conjunction
100		prove_negated_po(falsity,_,falsity) :- !.
101		prove_negated_po(disjunct(A,B),Hyp,negdisj(T1,T2)) :- !,
102		(prove_negated_po(A,Hyp,T1) -> prove_negated_po(B,Hyp,T2)).
103		prove_negated_po(conjunct(A,B),Hyp,negconj(T1,T2)) :- !, % could be generated by Rodin
104		(prove_negated_po(A,Hyp,T1) -> true
105		; prove_negated_po(B,Hyp,T2)). % we could add not(A) as hypothesis,
106		prove_negated_po(negation(Goal),Hyp,negation(PT)) :-!, prove_po(Goal,Hyp,PT).
107		prove_negated_po(OP,Hyp,negated_op(PT)) :- negate_op(OP,NOP), prove_po(NOP,Hyp,PT).
108
109
110		simple_value(Nr) :- number(Nr).
111		simple_value('$'(_)).
112		simple_value(boolean_true).
113		simple_value(boolean_false).
114		simple_value(record_field('$'(_),_)).
115		simple_value(value(_)).
116		simple_value(string(_)).
117		simple_value(function(F,_)) :- simple_value(F).
118		simple_value(couple(A,B)) :- simple_value(A), simple_value(B).
119
120		%get_set_of_possible_values(X,Hyps,XSet) :-
121		% if(try_get_set_of_possible_values(X,Hyps,R), XSet=R,
122		% XSet=set_extension([X])). % was typeset
123
124		try_get_set_of_possible_values(Nr,Hyps,R,Hyps) :- number(Nr),!,R=interval(Nr,Nr).
125		try_get_set_of_possible_values(X,Hyps,R,Hyps) :-
126		avl_fetch_binop_from_hyps_no_loop_check(X,equal,Hyps,Nr), number(Nr),!, % TODO: also treat is_explicit_value
127		R=interval(Nr,Nr).
128		try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :-
129		avl_fetch_worthwhile_mem_from_hyps(X,Hyps,XSet1,Hyps1),
130		(improve_integer_set_precision(X,XSet1,Hyps1,XSet,Hyps2)
131		-> true ; Hyps2=Hyps1, XSet=XSet1).
132		try_get_set_of_possible_values(X,Hyps,Res,Hyps3) :-
133		avl_fetch_equal_from_hyps(X,Hyps,X2,Hyps1),
134		quick_not_occurs_check(X,X2),
135		rewrite_local_loop_check(X,try_get_set_of_possible_values,X2,Hyps1,Hyps2),
136		(X2='$'(_) -> X = '$'(_) ; true), % avoid rewriting x -> card(...) -> x; TO DO: better cyclic equality prevention
137		try_get_set_of_possible_values(X2,Hyps2,Res,Hyps3), !.
138		try_get_set_of_possible_values(function(Func,_),Hyps,RangeSet,Hyps2) :- !,
139		get_range_or_superset(Func,Hyps,RangeSet,Hyps2).
140		try_get_set_of_possible_values(first(Seq),Hyps,RangeSet,Hyps2) :- !, % first(S) === S(1)
141		get_range_or_superset(Seq,Hyps,RangeSet,Hyps2).
142		try_get_set_of_possible_values(last(Seq),Hyps,RangeSet,Hyps2) :- !, % last(S) === S(size(S))
143		get_range_or_superset(Seq,Hyps,RangeSet,Hyps2).
144		% TO DO other sequence operations
145		try_get_set_of_possible_values(couple(A,B),Hyps,cartesian_product(SA,SB),Hyps2) :- !,
146		try_get_set_of_possible_values(A,Hyps,SA,Hyps1),
147		try_get_set_of_possible_values(B,Hyps1,SB,Hyps2).
148		try_get_set_of_possible_values(max(set_extension([V1,V2|_])),H,'NATURAL',H) :- % max({x,-x}) >= 0
149		( V1 = unary_minus(V2), \+ number(V1) -> true
150		; V2 = unary_minus(V1), \+ number(V2) -> true), !. % instead of NATURAL we could try and infer values for V1/V2
151		try_get_set_of_possible_values(max(Set),H,Set,H).
152		try_get_set_of_possible_values(min(Set),H,Set,H).
153		try_get_set_of_possible_values(mu(Set),H,Set,H).
154		try_get_set_of_possible_values(max_int,H,'NATURAL1',H).
155		% TO DO: min_int
156		try_get_set_of_possible_values(value(avl_set(A1)),Hyps,value(avl_set(A2)),Hyps) :- !,
157		expand_and_convert_to_avl_set([avl_set(A1)],A2,get_set_of_possible_values,'WD(?)').
158		try_get_set_of_possible_values(add(X,Y),Hyps,Set,Hyps2) :-
159		add_with_number(add(X,Y),A,Nr),
160		try_get_set_of_possible_values(A,Hyps,ValA,Hyps2),
161		add_to_value_set(ValA,Nr,Set),!.
162		try_get_set_of_possible_values(minus(A,Nr),Hyps,Set,Hyps2) :- number(Nr), Nr1 is -Nr,
163		try_get_set_of_possible_values(A,Hyps,ValA,Hyps2),
164		add_to_value_set(ValA,Nr1,Set),!.
165		% TO DO : add unary_minus, multiplication with nr
166		try_get_set_of_possible_values(Seq,Hyps,Set,Hyps) :-
167		infer_sequence_type_of_expr(Seq,Hyps,SeqType),!,
168		(SeqType=seq1 -> Set=seq1(typeset) ; Set=seq(typeset)). % TO DO: examine type of list elements
169		try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :-
170		avl_fetch_binop_from_hyps(X,greater_equal,Hyps,Low,Hyps1), !,
171		(avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2) -> XSet = interval(Low,Up)
172		; Low=0 -> XSet = 'NATURAL', Hyps2=Hyps1
173		; number(Low),Low>0 -> XSet= 'NATURAL1', Hyps2=Hyps1). % TO DO: improve precision
174		try_get_set_of_possible_values(X,Hyps,XSet,Hyps2) :-
175		rewrite_integer(X,Hyps,X2,Hyps1),!,
176		try_get_set_of_possible_values(X2,Hyps1,XSet,Hyps2).
177		try_get_set_of_possible_values(size(A),Hyps,XSet,Hyps) :-
178		(check_not_empty_set(A,Hyps) -> XSet = 'NATURAL1' ; XSet='NATURAL').
179		try_get_set_of_possible_values(card(A),Hyps,XSet,Hyps) :-
180		(check_not_empty_set(A,Hyps) -> XSet = 'NATURAL1' ; XSet='NATURAL').
181		try_get_set_of_possible_values(if_then_else(_,A,B),Hyps,R,Hyps) :-
182		(try_get_set_of_possible_values(A,Hyps,AV,Hyps1)
183		-> try_get_set_of_possible_values(B,Hyps1,BV,Hyps2)),
184		construct_union(AV,BV,Hyps2,R).
185		try_get_set_of_possible_values(modulo(A,B),Hyps1,XSet,Hyps2) :-
186		number(B), B>0,
187		B1 is B-1,
188		XSet1 = interval(0,B1), % value of A mod B must be in 0..B1
189		% note: this also holds in z_or_tla_minor_mode, we have (-3) mod 2 = 1
190		(try_get_set_of_possible_values(A,Hyps1,XSet2,Hyps2),
191		maximal_value(XSet2,Up)
192		-> intersect_sets(XSet1,interval(0,Up),XSet)
193		% we were able to reduce the interval further by finding possible upper-bound for A
194		% we could call improve_upper_bound
195		; Hyps2=Hyps1, XSet=XSet1).
196
197		maximal_value(interval(_,Up),Up).
198		maximal_value(value(avl_set(A)),Up) :- avl_max(A,int(Up)).
199		% TO DO: add avl_set
200
201
202		is_integer_set(interval(_,_)).
203		is_integer_set('NATURAL').
204		is_integer_set('NATURAL1').
205		is_integer_set('INTEGER').
206		% TO DO: add avl_set
207
208		% detect sets which can profit from narrowing down:
209		is_infinite__or_large_integer_set('NATURAL',0,inf).
210		is_infinite__or_large_integer_set('NATURAL1',1,inf).
211		%is_infinite__or_large_integer_set('INTEGER',-inf,inf).
212		is_infinite__or_large_integer_set(interval(Low,max_int),Low,max_int). % one cannot prove a lot with max_int anyway!?
213
214		% try and improve precision of integer set
215		% limitation: only looks for one other hypotheses; maybe we should do this in well_defs_hyps.pl
216		improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps3) :-
217		is_integer_set(XSet1),
218		avl_fetch_worthwhile_mem_from_hyps(X,Hyps1,XSet2,Hyps2),
219		XSet2 \= XSet1,
220		!,
221		intersect_sets(XSet1,XSet2,XSet12),
222		try_improve_interval(XSet12,X,Hyps2,NewSet,Hyps3). % TO DO: we could try and find another member
223		% TO DO: also look at less_equal, greater_equal constraints
224		improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps3) :-
225		is_infinite__or_large_integer_set(XSet1,Low,LargeUp),
226		avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2),
227		Up \= LargeUp, % we really improve upon earlier value
228		!,
229		try_improve_interval(interval(Low,Up),X,Hyps2,NewSet,Hyps3).
230		improve_integer_set_precision(X,XSet1,Hyps1,NewSet,Hyps2) :-
231		try_improve_interval(XSet1,X,Hyps1,NewSet,Hyps2).
232
233		try_improve_interval(interval(OldLow,OldUp),X,Hyps1,interval(NewLow,NewUp),Hyps2) :- !,
234		improve_interval(X,OldLow,OldUp,Hyps1,NewLow,NewUp,Hyps2).
235		try_improve_interval(Set,_,Hyps,Set,Hyps).
236
237		% phase 1: try improve upper bound
238		improve_interval(X,OldLow,OldUp,Hyps1,NewLow,NewUp,Hyps3) :-
239		improve_upper_bound(X,OldUp,Hyps1,NewUp1,Hyps2),!,
240		improve_interval(X,OldLow,NewUp1,Hyps2,NewLow,NewUp,Hyps3).
241		improve_interval(X,OldLow,Up,Hyps1,NewLow,Up,Hyps2) :-
242		improve_interval2(X,OldLow,Hyps1,NewLow,Hyps2).
243		%
244		improve_upper_bound(X,OldUp,Hyps1,NewUp,Hyps2) :-
245		avl_fetch_binop_from_hyps(X,less_equal,Hyps1,Up,Hyps2),
246		order_values(OldUp,Up,NewUp,OldUp),
247		NewUp \= OldUp.
248
249		% now try and improve lower bound:
250		improve_interval2(X,OldLow,Hyps1,NewLow,Hyps3) :-
251		improve_lower_bound(X,OldLow,Hyps1,Low1,Hyps2),!,
252		improve_interval2(X,Low1,Hyps2,NewLow,Hyps3).
253		improve_interval2(_,Low,Hyps,Low,Hyps).
254		%
255		improve_lower_bound(X,OldLow,Hyps1,NewLow,Hyps2) :-
256		avl_fetch_binop_from_hyps(X,greater_equal,Hyps1,Low,Hyps2),
257		order_values(Low,OldLow,OldLow,NewLow),
258		NewLow \= OldLow.
259
260
261		% try and intersect two sets:
262		intersect_sets(interval(L1,U1),B,Res) :- !, intersect_interval(B,L1,U1,Res).
263		intersect_sets(B,interval(L1,U1),Res) :- intersect_interval(B,L1,U1,Res).
264		intersect_sets('NATURAL1','NATURAL','NATURAL1').
265		intersect_sets('NATURAL','NATURAL1','NATURAL1').
266		% TODO: support avl_set
267
268		intersect_interval(interval(L2,U2),L1,U1,interval(L3,U3)) :-
269		order_values(L1,L2,_,L3), % choose larger value as lower bound
270		order_values(U1,U2,U3,_). % choose smaller value as upper bound
271		intersect_interval('NATURAL1',L1,U1,interval(L3,U1)) :- order_values(L1,1,L3,_).
272		intersect_interval('NATURAL',L1,U1,interval(L3,U1)) :- order_values(L1,0,L3,_).
273
274		% order values for interval intersection
275		order_values(N1,N2,R1,R2) :- number(N1),!, order_aux_nr(N2,N1,R1,R2).
276		order_values(N1,N2,R1,R2) :- number(N2),!, order_aux_nr(N1,N2,R1,R2).
277		order_values(min_int,N2,R1,R2) :- !, R1=min_int,R2=N2.
278		order_values(max_int,N2,R1,R2) :- !, R1=N2,R2=max_int.
279		order_values(N1,N2,N1,N2). % just choose N1
280
281		order_aux_nr(N2,N1,R1,R2) :- number(N2),!,
282		(N2>N1 -> R1=N1,R2=N2 ; R1=N2,R2=N1).
283		order_aux_nr(max_int,N1,R1,R2) :- N1 < 1, !, R1=N1, R2=max_int.
284		order_aux_nr(_N2,N1,N1,N1). % choose the number as the bound
285
286
287		%try_get_set_of_possible_values(X,_,_,_) :- print(try_get_set_of_possible_values_failed(X)),nl,fail.
288		% TO DO: more precise representation of open-ended intervals interval(Low,'$infinity'))
289		% TO DO: intersect multiple solutions; e.g., intervals and >=, <= constraints
290
291		add_to_value_set(interval(L,U),Nr,interval(L2,U2)) :-
292		add_nr(L,Nr,L2),
293		(add_nr(U,Nr,U2) -> true ; Nr =< 0, U2=U). % e.g., if U = size(x) we create an over-approximation
294		add_to_value_set('NATURAL',1,'NATURAL1'). % TO DO: extend
295		%add_to_value_set(value(avl_set(A1),Nr,value(avl_set(A2)) :- TO DO: add Nr to all values in A2
296
297		% adding a known number to an arithmetic expression; could be extended
298		% this is mainly for dealing with index arithmetic for arrays
299		add_nr(Nr1,ToAdd,Nr2) :- number(Nr1),!, Nr2 is Nr1+ToAdd.
300		add_nr(minus(Expr,Nr1),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1-ToAdd,
301		(Nr2=0 -> Res=Expr ; Res= minus(Expr,Nr2)).
302		add_nr(add(Expr,Nr1),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1+ToAdd,
303		(Nr2=0 -> Res=Expr ; Res= add(Expr,Nr2)).
304		add_nr(add(Nr1,Expr),ToAdd,Res) :- number(Nr1),!, Nr2 is Nr1+ToAdd,
305		(Nr2=0 -> Res=Expr ; Res= add(Expr,Nr2)).
306
307
308		% check if an expression is a sequence
309		check_is_sequence(El,Hyps) :- check_is_sequence(El,Hyps,_).
310		check_is_non_empty_sequence(El,Hyps) :- check_is_sequence(El,Hyps,seq1).
311
312		check_is_sequence(S,_,seq) :- is_empty_set_direct(S),!.
313		check_is_sequence(El,Hyps,RequiredType) :-
314		infer_sequence_type_of_expr(El,Hyps,Type),
315		(Type=seq1 -> true ; RequiredType=seq -> true
316		; check_not_equal_empty_set(El,Hyps,_)).
317		check_is_sequence(A,Hyps,RequiredType) :-
318		avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),
319		check_is_sequence(Value,Hyps2,RequiredType).
320		check_is_sequence(domain_restriction(Dom,S),Hyps,Res) :- !,
321		is_interval(Dom,Hyps,1,N),
322		check_is_sequence(S,Hyps,SeqType),
323		(SeqType=seq1, check_leq(1,N,Hyps) -> Res=seq1 ; Res=seq).
324		check_is_sequence(El,Hyps,RequiredType) :-
325		avl_fetch_mem_or_struct(El,Hyps,Set,Hyps2),
326		is_set_of_sequences_type(Set,Hyps2,Type), % should we move this to subset? dealt with in subset_transitivity_rule
327		% required for :wd Right:seq(BOOL) & (Right/=[] => tail(Right)=res) in test 2018
328		(Type=seq1 -> true ; RequiredType=seq -> true
329		; check_not_equal_empty_set(El,Hyps2,_)),
330		!.
331		check_is_sequence(X,Hyps,RequiredType) :- try_get_set_of_possible_values(X,Hyps,XSet,Hyps2),
332		(RequiredType==seq1 -> check_is_subset(XSet,seq1(typeset),Hyps2,_PT)
333		; check_is_subset(XSet,seq(typeset),Hyps2,_PT)).
334		% check if something is an interval
335		is_interval(Expr,Hyps,A,B) :- simplify_expr(Expr,Hyps,SE), is_interval_aux(SE,A,B).
336		is_interval_aux(interval(A,B),A,B).
337		is_interval_aux(value(CS),A,B) :- nonvar(CS), CS= avl_set(AVL), avl_is_interval(AVL,A,B).
338
339		is_set_of_sequences_type(seq1(_),_,seq1) :- !.
340		is_set_of_sequences_type(seq(_),_,seq) :- !.
341		is_set_of_sequences_type(iseq(_),_,seq) :- !.
342		is_set_of_sequences_type(iseq1(_),_,seq) :- !.
343		is_set_of_sequences_type(perm(A),Hyps,Type) :- !,
344		(check_not_equal_empty_set(A,Hyps,_) -> Type=seq1 ; Type=seq).
345		is_set_of_sequences_type(Func,Hyps,Type) :- % a total function 1..Up --> Range is a sequence
346		get_exact_domain_of_func_or_rel_type(Func,Hyps,Dom,Hyps1),
347		check_equal_pattern(Dom,interval(1,Up),Hyps1,Hyps2),
348		% we could call check_equal for Low; relevant for :wd BV=16 & II=1 & BIdx = II..BV & s:BIdx --> BOOL & res=size(s)
349		is_partial_function_type(Func,Hyps2,_),
350		(number(Up), Up>0 % we could call check_leq
351		-> Type=seq1 ; Type=seq).
352
353		% a simple equality check
354		check_equal_pattern(A,Target,Hyps,Hyps1) :-
355		check_equal_h(A,Target,not_ground,[],Hyps,Hyps1).
356		check_equal(A,Target,Hyps,Hyps1) :-
357		check_equal_h(A,Target,ground,[],Hyps,Hyps1).
358
359		% TargetGround=ground means Target is a ground, fully known expressions and not a pattern with variables
360		check_equal_h(A,Target,_,_,Hyps,Hyps1) :- A=Target,!, Hyps1=Hyps.
361		check_equal_h(union(A1,A2),union(B1,B2),TGr,History,Hyps,Hyps2) :-
362		check_equal_h(A1,B1,TGr,History,Hyps,Hyps1),!, % TO DO: add other rules, e.g., check A1 and B2
363		check_equal_h(A2,B2,TGr,History,Hyps1,Hyps2).
364		check_equal_h(couple(A1,A2),couple(B1,B2),TGr,History,Hyps,Hyps2) :- % TO DO: records, ...
365		check_equal_h(A1,B1,TGr,History,Hyps,Hyps1),!,
366		check_equal_h(A2,B2,TGr,History,Hyps1,Hyps2).
367		check_equal_h(A,Target,TGr,History,Hyps,Hyps2) :-
368		avl_fetch_equal_from_hyps(A,Hyps,A2,Hyps1), nonmember(A2,History),
369		check_equal_h(A2,Target,TGr,[A|History],Hyps1,Hyps2).
370		check_equal_h(A,Target,TGr,History,Hyps,Hyps2) :- Target = '$'(_),
371		avl_fetch_equal_from_hyps(Target,Hyps,T2,Hyps1), nonmember(T2,History),
372		check_equal_h(A,T2,TGr,[A|History],Hyps1,Hyps2).
373		check_equal_h(A,Target,ground,_,Hyps,Hyps) :-
374		avl_fetch_from_hyps(subset(A,Target),Hyps),
375		avl_fetch_from_hyps(subset(Target,A),Hyps).
376		check_equal_h(A,Empty,ground,_,Hyps,Hyps) :- is_empty_set_direct(Empty), !, check_empty_set(A,Hyps,_).
377		check_equal_h(Empty,A,ground,_,Hyps,Hyps) :- is_empty_set_direct(Empty), !, check_empty_set(A,Hyps,_).
378
379		infer_sequence_type_of_expr(sequence_extension([_|_]),_,seq1).
380		infer_sequence_type_of_expr(sorted_set_extension(SList),_,seq1) :-
381		sorted_set_extension_is_seq(SList,1).
382		infer_sequence_type_of_expr(set_extension(List),_,seq1) :- sort(List,SList),
383		sorted_set_extension_is_seq(SList,1).
384		infer_sequence_type_of_expr(insert_tail(_,_),_,seq1).
385		% we do not need to check Seq is a sequence; this will be checked in its own PO, ditto for operators below
386		infer_sequence_type_of_expr(insert_front(_,_),_,seq1).
387		infer_sequence_type_of_expr(concat(A,B),Hyps,R) :-
388		( infer_sequence_type_of_expr(A,Hyps,seq1) -> R=seq1
389		; infer_sequence_type_of_expr(B,Hyps,seq1) -> R=seq1
390		; R=seq).
391		infer_sequence_type_of_expr(restrict_front(_,_),_,seq).
392		infer_sequence_type_of_expr(restrict_tail(_,_),_,seq).
393		infer_sequence_type_of_expr(rev(A),Hyps,R) :-
394		(infer_sequence_type_of_expr(A,Hyps,seq1) -> R=seq1 ; R=seq).
395		infer_sequence_type_of_expr(front(_),_,seq). % we could call check_not_empty_set(front(A),Hyps)
396		infer_sequence_type_of_expr(tail(_),_,seq). % ditto
397		infer_sequence_type_of_expr(general_concat(_),_,seq).
398		infer_sequence_type_of_expr(value(avl_set(SeqAVL)),_,seq1) :- !, SeqAVL \= empty,
399		safe_is_avl_sequence(SeqAVL).
400		infer_sequence_type_of_expr(if_then_else(_,A,B),Hyps,Type) :- !,
401		(infer_sequence_type_of_expr(A,Hyps,S1)
402		-> infer_sequence_type_of_expr(B,Hyps,S2), lub_seq(S1,S2,Type)).
403		infer_sequence_type_of_expr(S,_,seq) :- is_empty_set_direct(S).
404		infer_sequence_type_of_expr(Expr,Hyps,R) :-
405		is_lambda_function_with_domain(Expr,Domain),
406		Domain = interval(1,N),
407		(check_leq(1,N,Hyps) -> R = seq1 ; R=seq).
408		% TO DO: rule for composition
409
410		lub_seq(seq1,seq1,seq1).
411		lub_seq(seq1,seq,seq).
412		lub_seq(seq,seq1,seq).
413		lub_seq(seq,seq,seq).
414
415		% check if a sorted set extension represent a proper sequence
416		sorted_set_extension_is_seq([],_).
417		sorted_set_extension_is_seq([couple(Nr,_)|T],Nr) :- N1 is Nr+1, sorted_set_extension_is_seq(T,N1).
418
419		% --------
420		% DOMAIN
421
422		% compute exact domain
423		% currently there can be multiple solutions for $(_) case below; first one is usually more precise
424		%compute_exact_domain(Value,Hyps2,Res) :- debug:print_quoted_with_max_depth(compute_exact_domain(Value,Hyps2,Res),4),nl,fail.
425
426
427		compute_exact_domain(assertion_expression(_,_,Func),Hyps,Res,Hyps2) :- !,
428		compute_exact_domain(Func,Hyps,Res,Hyps2).
429		compute_exact_domain(reverse(Func),Hyps,Res,Hyps2) :- !,
430		compute_exact_range(Func,Hyps,Res,Hyps2).
431		compute_exact_domain(rev(Func),Hyps,Res,Hyps2) :- !, % reverse of a sequence; domain identical
432		compute_exact_domain(Func,Hyps,Res,Hyps2).
433		compute_exact_domain(identity(Domain),Hyps,Res,Hyps2) :- !, Hyps2=Hyps, Res=Domain.
434		compute_exact_domain(restrict_front(_Seq,N),Hyps,Res,Hyps2) :- !,
435		% WD Condition requires N : 0..size(Seq)
436		Hyps2=Hyps, Res = interval(1,N). % TODO: similar rule for restrict_tail
437		compute_exact_domain(Func,Hyps,Res,Hyps2) :-
438		compute_exact_domain_direct(Func,Hyps,Res,Hyps2),!. % No recursive application of equal or hyp
439		compute_exact_domain(Func,Hyps,Domain,Hyps2) :-
440		avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
441		compute_exact_domain(Func2,Hyps1,Domain,Hyps2).
442		%compute_exact_domain(Expr,_,Domain,_) :- print(compute_exact_domain_failed(Expr,_,Domain)),nl,fail.
443
444
445		compute_exact_domain_direct(Func,Hyps,Res,Hyps2) :-
446		avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1), % look for Func : Res --> Range ; e.g. Func:perm(1..10) -> DomSet=1..10
447		% f : _ +-> ( Dom --> _ ) & x:Dom ==> x:dom(f(_))
448		% f : _ +-> ( Dom --> _ ) => dom(f(_)) = Dom
449		get_exact_domain_of_func_or_rel_type(Function,Hyps1,Res,Hyps2),!. % is thus also minimal domain
450		compute_exact_domain_direct(Func,Hyps,Res,Hyps3) :- Func = '$'(_), % Look for Func = Value definition
451		avl_fetch_equal_from_hyps(Func,Hyps,Value,Hyps2),
452		compute_exact_domain(Value,Hyps2,Res,Hyps3).
453		compute_exact_domain_direct(value(CS),Hyps,value(Res),Hyps) :- !, nonvar(CS),
454		domain_of_explicit_set_wf(CS,Res,no_wf_available).
455		compute_exact_domain_direct(overwrite(F1,F2),Hyps,D12,Hyps2) :- !, % dom(F1 <+ F2) = dom(F1) \/ dom(F2)
456		compute_exact_domain(F1,Hyps,D1,Hyps1), compute_exact_domain(F2,Hyps1,D2,Hyps2),
457		construct_union(D1,D2,Hyps2,D12).
458		compute_exact_domain_direct(domain_restriction(S,F),Hyps,intersection(S,D),Hyps2) :- !, % dom(S <| F) = S /\ dom(F)
459		compute_exact_domain(F,Hyps,D,Hyps2). % SIMP_MULTI_DOM_DOMRES
460		compute_exact_domain_direct(domain_subtraction(S,F),Hyps,set_subtraction(D,S),Hyps2) :- !, % dom(S <<| F) = dom(F) - S
461		compute_exact_domain(F,Hyps,D,Hyps2). % SIMP_MULTI_DOM_DOMSUB
462		compute_exact_domain_direct(direct_product(F,G),Hyps,intersection(DF,DG),Hyps2) :- !, % dom(F><G) = dom(F) /\ dom(G)
463		compute_exact_domain(F,Hyps,DF,Hyps1),
464		compute_exact_domain(G,Hyps1,DG,Hyps2).
465		compute_exact_domain_direct(composition(F1,F2),Hyps,Domain,Hyps4) :- !, % dom((F1;F2)) = dom(F1) if ran(F1) <: dom(F2)
466		compute_exact_domain(F1,Hyps,Domain,Hyps2),
467		compute_exact_domain(F2,Hyps2,D2,Hyps3), % or_subset would also be ok
468		(maximal_set(D2,Hyps3) -> Hyps4=Hyps3
469		; get_range_or_superset(F1,Hyps3,R1,Hyps4),
470		check_is_subset(R1,D2,Hyps4,_PT)
471		).
472		compute_exact_domain_direct(union(F,G),Hyps,UnionDFDG,Hyps2) :- !, % dom(F \/ G) = dom(F) \/ dom(G)
473		compute_exact_domain(F,Hyps,DF,Hyps1),
474		compute_exact_domain(G,Hyps1,DG,Hyps2),
475		construct_union(DF,DG,Hyps2,UnionDFDG).
476		compute_exact_domain_direct(sorted_set_extension(List),Hyps,Res,Hyps2) :- !,
477		compute_exact_domain_direct(set_extension(List),Hyps,Res,Hyps2).
478		compute_exact_domain_direct(set_extension(List),Hyps,Res,Hyps) :- !, maplist(get_dom_el,List,Domain),
479		construct_set_extension(Domain,Hyps,Res).
480		compute_exact_domain_direct(Expr,Hyps,Domain,Hyps) :- is_lambda_function_with_domain(Expr,Domain),!.
481		compute_exact_domain_direct(Func,Hyps,Domain,Hyps2) :-
482		avl_fetch_equal_from_hyps(domain(Func),Hyps,Domain,Hyps2).
483
484		% get domain element of a couple
485		get_dom_el(couple(A,_),A).
486		% get range element of a couple
487		get_ran_el(couple(_,B),B).
488
489		% construct union term with a few optimisations
490		construct_union(empty_set,B,_Hyps,Res) :- !,Res=B.
491		construct_union(set_extension(A),set_extension(B),Hyps,Res) :- !,
492		append(A,B,AB),
493		construct_set_extension(AB,Hyps,Res).
494		construct_union(A,empty_set,_,Res) :- !,Res=A.
495		construct_union(A,B,_,union(A,B)).
496
497		% get maximal domain of a function (i.e., domain or superset thereof)
498		:- if(environ(prob_safe_mode,true)).
499		get_domain_or_superset(F,H,R,H2) :- nonvar(H2),
500		add_internal_error('Instantiated hyps:',get_domain_or_superset(F,H,R,H2)),fail.
501		:- endif.
502		get_domain_or_superset(reverse(Func),Hyps,Res,Hyps2) :- !,
503		get_range_or_superset(Func,Hyps,Res,Hyps2).
504		get_domain_or_superset(Func,Hyps,Res,Hyps3) :-
505		compute_exact_domain_direct(Func,Hyps,Res,Hyps2),
506		rewrite_local_loop_check(Func,get_domain_or_superset,Res,Hyps2,Hyps3),
507		!.
508		get_domain_or_superset(domain_restriction(A,_),Hyps,Res,Hyps) :- Res=A. % in case compute_exact_domain_direct fails
509		get_domain_or_superset(Func,Hyps,Res,Hyps1) :-
510		function_restriction(Func,LargerFunc),
511		get_domain_or_superset(LargerFunc,Hyps,Res,Hyps1).
512		get_domain_or_superset(composition(F1,_),Hyps,Res,Hyps1) :- get_domain_or_superset(F1,Hyps,Res,Hyps1).
513		get_domain_or_superset(direct_product(A,B),Hyps,Res,Hyps2) :- % dom(A >< B) = dom(A) /\ dom (B)
514		(get_domain_or_superset(A,Hyps,Res,Hyps2) -> true
515		; get_domain_or_superset(B,Hyps,Res,Hyps2) -> true).
516		get_domain_or_superset(tail(Seq),Hyps,Res,Hyps2) :- !, % dom(tail(S)) <: dom(S)
517		get_domain_or_superset(Seq,Hyps,Res,Hyps2).
518		get_domain_or_superset(front(Seq),Hyps,Res,Hyps2) :- !, % dom(front(S)) <: dom(S)
519		get_domain_or_superset(Seq,Hyps,Res,Hyps2).
520		get_domain_or_superset(restrict_front(Seq,_),Hyps,Res,Hyps2) :- !, % dom(S /|\ k) <: dom(S)
521		get_domain_or_superset(Seq,Hyps,Res,Hyps2).
522		get_domain_or_superset(restrict_tail(Seq,_),Hyps,Res,Hyps2) :- !, % dom(S \|/ k) <: dom(S)
523		get_domain_or_superset(Seq,Hyps,Res,Hyps2).
524		get_domain_or_superset(Func,Hyps,DomSet,Hyps2) :- simple_value(Func),
525		avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps1),
526		get_domain_or_superset_of_func_or_rel_type(FunctionType,Hyps1,DomSet,Hyps2),
527		\+ maximal_set(DomSet,Hyps2). % inference useless
528		get_domain_or_superset(Func,Hyps,Domain,Hyps2) :-
529		avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
530		get_domain_or_superset(Func2,Hyps1,Domain,Hyps2).
531		get_domain_or_superset(Func,Hyps,DomSuperSet,Hyps2) :-
532		avl_fetch_binop_from_hyps(domain(Func),subset,Hyps,DomSuperSet,Hyps2).
533
534
535		% get exact (thus also minimal) domain of a function type
536		:- if(environ(prob_safe_mode,true)).
537		get_exact_domain_of_func_or_rel_type(F,H,R,H2) :-
538		nonvar(H2), add_internal_error('Instantiated hyps:',get_exact_domain_of_func_or_rel_type(F,H,R,H2)),fail.
539		:- endif.
540		get_exact_domain_of_func_or_rel_type(FunType,Hyps,A,Hyps) :-
541		get_possible_domain_of_func_or_rel_type(FunType,Hyps,A,exact),!.
542		get_exact_domain_of_func_or_rel_type(FunType,Hyps,Domain,Hyps2) :-
543		avl_fetch_worthwhile_equal_from_hyps(FunType,Hyps,FunType2,Hyps1), % in case we have a definition like X = 1..n --> R
544		get_exact_domain_of_func_or_rel_type(FunType2,Hyps1,Domain,Hyps2).
545		get_exact_domain_of_func_or_rel_type(sorted_set_extension(F),Hyps,Domain,Hyps2) :- !,
546		get_exact_domain_of_func_or_rel_type(set_extension(F),Hyps,Domain,Hyps2).
547		get_exact_domain_of_func_or_rel_type(set_extension([Func|TF]),Hyps,Domain,Hyps2) :-
548		compute_exact_domain(Func,Hyps,Domain,Hyps2), % now check that all other functions have the same domain
549		(member(Func2,TF), \+ compute_exact_domain(Func2,Hyps2,Domain,_) -> fail
550		; true).
551
552		get_possible_domain_of_func_or_rel_type(iseq(_),_,'NATURAL1',subset).
553		get_possible_domain_of_func_or_rel_type(iseq1(_),_,'NATURAL1',subset).
554		get_possible_domain_of_func_or_rel_type(partial_bijection(A,_),_,A,subset).
555		get_possible_domain_of_func_or_rel_type(partial_function(A,_),_,A,subset).
556		get_possible_domain_of_func_or_rel_type(partial_injection(A,_),_,A,subset).
557		get_possible_domain_of_func_or_rel_type(partial_surjection(A,_),_,A,subset).
558		get_possible_domain_of_func_or_rel_type(perm(A),Hyps,Domain,Type) :-
559		(compute_card_of_set(A,Hyps,CardA,_) % we could do check_finite and use card(A) instead of CardA
560		-> Domain = interval(1,CardA), Type=exact
561		; check_finite(A,Hyps,_) -> Domain = interval(1,card(A)), Type=exact
562		; %print(could_not_compute_card_for_perm(A)),nl,
563		Domain = 'NATURAL1', Type=subset
564		).
565		get_possible_domain_of_func_or_rel_type(relations(A,_),_,A,subset).
566		get_possible_domain_of_func_or_rel_type(seq(_),_,'NATURAL1',subset).
567		get_possible_domain_of_func_or_rel_type(seq1(_),_,'NATURAL1',subset).
568		get_possible_domain_of_func_or_rel_type(surjection_relation(A,_),_,A,subset).
569		get_possible_domain_of_func_or_rel_type(total_bijection(A,_),_,A,exact).
570		get_possible_domain_of_func_or_rel_type(total_function(A,_),_,A,exact).
571		get_possible_domain_of_func_or_rel_type(total_injection(A,_),_,A,exact).
572		get_possible_domain_of_func_or_rel_type(total_relation(A,_),_,A,exact).
573		get_possible_domain_of_func_or_rel_type(total_surjection_relation(A,_),_,A,exact).
574		get_possible_domain_of_func_or_rel_type(total_surjection(A,_),_,A,exact).
575
576
577		% variation of get_possible_domain_of_func_or_rel_type, which uses Hyps and can deal with set_extensions
578		:- if(environ(prob_safe_mode,true)).
579		get_domain_or_superset_of_func_or_rel_type(F,H,R,H2) :- nonvar(H2),
580		add_internal_error('Instantiated hyps:',get_domain_or_superset_of_func_or_rel_type(F,H,R,H2)),fail.
581		:- endif.
582		get_domain_or_superset_of_func_or_rel_type(sorted_set_extension(List),Hyps,Dom,Hyps2) :- !,
583		get_domain_or_superset_of_func_or_rel_type(set_extension(List),Hyps,Dom,Hyps2).
584		get_domain_or_superset_of_func_or_rel_type(set_extension(List),Hyps,Dom,Hyps2) :- !,
585		% if we have f: {f1,f2,...} => dom(f) <: dom(f1) \/ dom(f2) \/ ...
586		merge_possible_domains_of_list(List,Hyps,empty_set,Dom,Hyps2).
587		get_domain_or_superset_of_func_or_rel_type(Func,Hyps,Res,Hyps) :-
588		get_possible_domain_of_func_or_rel_type(Func,Hyps,D,_),!,Res=D.
589
590		% merge domains of a list of possible functions
591		merge_possible_domains_of_list([],Hyps,Acc,Acc,Hyps).
592		merge_possible_domains_of_list([H|T],Hyps,Acc,Res,Hyps2) :-
593		get_domain_or_superset(H,Hyps,Domain,Hyps1),!,
594		construct_union(Acc,Domain,Hyps1,Acc1),
595		merge_possible_domains_of_list(T,Hyps1,Acc1,Res,Hyps2).
596
597		% RANGE
598		% -----
599
600		% compute range or subset thereof
601
602		compute_exact_range(assertion_expression(_,_,Func),Hyps,Res,Hyps2) :- !,
603		compute_exact_range(Func,Hyps,Res,Hyps2).
604		compute_exact_range(reverse(Func),Hyps,Res,Hyps2) :-
605		compute_exact_domain(Func,Hyps,Res,Hyps2).
606		compute_exact_range(rev(Func),Hyps,Res,Hyps2) :- % reverse of a sequence: same range
607		compute_exact_range(Func,Hyps,Res,Hyps2).
608		compute_exact_range(identity(Domain),Hyps,Res,Hyps2) :- !, Hyps2=Hyps, Res=Domain.
609		compute_exact_range(Func,Hyps,Res,Hyps2) :-
610		compute_exact_range_direct(Func,Hyps,Res,Hyps2),!. % No recursive application of equal or hyp
611		compute_exact_range(Func,Hyps,Res,Hyps2) :- Func = '$'(_),
612		avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps2), % Func : _ --> Res
613		get_exact_range_of_func_type_direct(FunctionType,Res).
614		compute_exact_range(Func,Hyps,Range,Hyps2) :-
615		avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
616		compute_exact_range(Func2,Hyps1,Range,Hyps2).
617		%compute_exact_range(Expr,H,Domain) :- nl,portray_hyps(H),nl,print(compute_range_failed(Expr,_,Domain)),nl,fail.
618		% TO DO: rule for composition (exact case)
619
620
621		compute_exact_range_direct(S,Hyps,empty_set,Hyps) :- is_empty_set_direct(S),!.
622		compute_exact_range_direct(function(Func2,_),Hyps,Res,Hyps2) :-
623		% f : _ +-> ( _ --> Ran ) & x:Ran ==> x:ran(f(_))
624		% f : _ +-> ( _ -->> Ran ) => ran(f(_)) = Ran
625		get_range_or_superset(Func2,Hyps,Range,Hyps2),
626		get_exact_range_of_func_type_direct(Range,Res). % is thus also minimal domain
627		compute_exact_range_direct(value(CS),Hyps,value(Res),Hyps) :- !, nonvar(CS), % TO DO: maybe only if small enough
628		range_of_explicit_set_wf(CS,Res,no_wf_available).
629		compute_exact_range_direct(sequence_extension(L),Hyps,Res,Hyps) :- !,
630		construct_set_extension(L,Hyps,Res).
631		compute_exact_range_direct(union(F,G),Hyps,UnionRFRG,Hyps2) :- !, % ran(F \/ G) = ran(F) \/ ran(G)
632		compute_exact_range(F,Hyps,RF,Hyps1),
633		compute_exact_range(G,Hyps1,RG,Hyps2),
634		construct_union(RF,RG,Hyps2,UnionRFRG).
635		compute_exact_range_direct(sorted_set_extension(List),Hyps,Res,Hyps2) :- !,
636		compute_exact_range_direct(set_extension(List),Hyps,Res,Hyps2).
637		compute_exact_range_direct(set_extension(List),Hyps,Res,Hyps) :- !, maplist(get_ran_el,List,Domain),
638		construct_set_extension(Domain,Hyps,Res).
639		compute_exact_range_direct(Func,Hyps,Range,Hyps2) :-
640		avl_fetch_equal_from_hyps(range(Func),Hyps,Range,Hyps2).
641
642		% get maximal range of a function (i.e., range or superset thereof)
643		:- if(environ(prob_safe_mode,true)).
644		get_range_or_superset(P,H,R,H1) :- nonvar(H1), add_internal_error('Illegal hyps:',get_range_or_superset(P,H,R,H1)),fail.
645		:- endif.
646		get_range_or_superset(reverse(Func),Hyps,Res,Hyps2) :- !,
647		get_domain_or_superset(Func,Hyps,Res,Hyps2).
648		get_range_or_superset(Func,Hyps,Res,Hyps3) :-
649		compute_exact_range_direct(Func,Hyps,Res,Hyps2),
650		rewrite_local_loop_check(Func,get_range_or_superset,Res,Hyps2,Hyps3),
651		!. % can be a loop dom(f) = ran(g)
652		get_range_or_superset(function(Func2,_),Hyps,Res,Hyps2) :-
653		% f2 : _ +-> ( _ --> Res ) ==> ran(f2(.)) <: Res
654		get_range_or_superset(Func2,Hyps,Range,Hyps1),
655		get_possible_range_of_func_or_rel_type(Range,Hyps1,Res,_,Hyps2).
656		get_range_or_superset(range_restriction(_,B),Hyps,Res,Hyps) :- Res=B. % in case compute_exact_range_direct fails
657		get_range_or_superset(Func,Hyps,Res,Hyps1) :-
658		function_restriction(Func,LargerFunc),
659		get_range_or_superset(LargerFunc,Hyps,Res,Hyps1).
660		get_range_or_superset(Func,Hyps,RangeSet,Hyps2) :- simple_value(Func),
661		avl_fetch_mem_or_struct(Func,Hyps,FunctionType,Hyps1),
662		get_possible_range_of_func_or_rel_type(FunctionType,Hyps1,RangeSet,_,Hyps2),
663		\+ maximal_set(RangeSet,Hyps2). % inference useless.
664		get_range_or_superset(tail(Seq),Hyps,Res,Hyps2) :- !, % ran(tail(S)) <: ran(S)
665		get_range_or_superset(Seq,Hyps,Res,Hyps2).
666		get_range_or_superset(front(Seq),Hyps,Res,Hyps2) :- !, % ran(front(S)) <: ran(S)
667		get_range_or_superset(Seq,Hyps,Res,Hyps2).
668		get_range_or_superset(restrict_front(Seq,_),Hyps,Res,Hyps2) :- !, % /|\
669		get_range_or_superset(Seq,Hyps,Res,Hyps2).
670		get_range_or_superset(restrict_tail(Seq,_),Hyps,Res,Hyps2) :- !,
671		get_range_or_superset(Seq,Hyps,Res,Hyps2).
672		get_range_or_superset(concat(Seq1,Seq2),Hyps,Res12,Hyps2) :- !, % ran(S1^S2) = ran(S1) \/ ran(S2)
673		get_range_or_superset(Seq1,Hyps,Res1,Hyps2),
674		get_range_or_superset(Seq2,Hyps,Res2,Hyps2),
675		construct_union(Res1,Res2,Hyps2,Res12).
676		get_range_or_superset(composition(_,Func2),Hyps,Res2,Hyps2) :- !, % ran((F1;F2)) <: ran(F2)
677		get_range_or_superset(Func2,Hyps,Res2,Hyps2).
678		get_range_or_superset(Func,Hyps,Range,Hyps2) :-
679		avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
680		get_range_or_superset(Func2,Hyps1,Range,Hyps2).
681		get_range_or_superset(Func,Hyps,RangeSuperSet,Hyps2) :-
682		avl_fetch_binop_from_hyps(range(Func),subset,Hyps,RangeSuperSet,Hyps2).
683		get_range_or_superset(comprehension_set(IDS,Body),Hyps,RangeSuperSet,Hyps2) :-
684		get_lambda_args_and_body(IDS,Body,_,Expr,RestIDs,_), % TO DO: add RestIDs and typing to hyps
685		add_new_hyp_any_vars(Hyps,RestIDs,Hyps1), % do not infer anything about lambda vars; TO DO: push RestBody
686		get_clash_renaming_subst(Hyps1,Renaming),
687		rename_norm_term(Expr,Renaming,RNExpr),
688		try_get_set_of_possible_values(RNExpr,Hyps1,RangeSuperSet,Hyps2).
689		% get_range_or_superset(Func,_,_,_) :- print(get_range_or_superset_failed(Func)),nl,fail.
690		% to do: more sequence operations: insert_front, insert_tail
691
692		% get exact range without equality rewrites
693		get_exact_range_of_func_type_direct(Func,R) :-
694		get_possible_range_of_func_or_rel_type_direct(Func,R,exact).
695		% TO DO: maybe do same treatment for set_extension as in get_exact_domain_of_func_or_rel_type
696
697		% get possible range with equality rewrites
698		get_possible_range_of_func_or_rel_type(Func,Hyps,Range,ResType,Hyps2) :-
699		get_possible_range_of_func_or_rel_type_direct(Func,Range,Type),!, ResType=Type,Hyps2=Hyps.
700		get_possible_range_of_func_or_rel_type(Func,Hyps,Range,ResType,Hyps2) :-
701		avl_fetch_worthwhile_equal_from_hyps(Func,Hyps,Func2,Hyps1),
702		get_possible_range_of_func_or_rel_type(Func2,Hyps1,Range,ResType,Hyps2).
703
704		% get possible range without equality rewrites
705		get_possible_range_of_func_or_rel_type_direct(total_function(_,B),B,subset).
706		get_possible_range_of_func_or_rel_type_direct(total_injection(_,B),B,subset).
707		get_possible_range_of_func_or_rel_type_direct(total_surjection(_,B),B,exact).
708		get_possible_range_of_func_or_rel_type_direct(total_bijection(_,B),B,exact).
709		get_possible_range_of_func_or_rel_type_direct(total_relation(_,B),B,subset).
710		get_possible_range_of_func_or_rel_type_direct(total_surjection_relation(_,B),B,exact).
711		get_possible_range_of_func_or_rel_type_direct(partial_function(_,B),B,subset).
712		get_possible_range_of_func_or_rel_type_direct(partial_injection(_,B),B,subset).
713		get_possible_range_of_func_or_rel_type_direct(partial_surjection(_,B),B,exact).
714		get_possible_range_of_func_or_rel_type_direct(partial_bijection(_,B),B,exact).
715		get_possible_range_of_func_or_rel_type_direct(perm(B),B,exact).
716		get_possible_range_of_func_or_rel_type_direct(iseq(B),B,subset).
717		get_possible_range_of_func_or_rel_type_direct(iseq1(B),B,subset).
718		get_possible_range_of_func_or_rel_type_direct(seq(B),B,subset).
719		get_possible_range_of_func_or_rel_type_direct(seq1(B),B,subset).
720		get_possible_range_of_func_or_rel_type_direct(relations(_,B),B,subset).
721		get_possible_range_of_func_or_rel_type_direct(surjection_relation(_,B),B,exact).
722
723
724		% EXACT REWRITING/SIMPLIFICATION RULES
725
726		% simplifier, useful rules independent of context
727		simplify_expr(A,Hyps,Res) :-
728		rewrite_set_expression_exact(A,Hyps,A2,_),!, Res=A2.
729		simplify_expr(A,Hyps,Res) :-
730		rewrite_integer(A,Hyps,A2,_),!, Res=A2.
731		simplify_expr(record_field(rec(Fields),Field),Hyps,SExpr) :-
732		member(field(Field,Expr),Fields),!,
733		simplify_expr(Expr,Hyps,SExpr).
734		simplify_expr(domain(reverse(A)),_,range(A)) :- !.
735		simplify_expr(range(reverse(A)),_,domain(A)) :- !.
736		simplify_expr(E,_,E).
737
738
739		get_lambda_args_and_body(IDS,Body,LambdaID,LambdaExpr,RestArgs,RestBodyList) :-
740		LambdaID='$'(Lambda),
741		append(RestArgs,[LambdaID],IDS), % TO DO: pass lambda info from typed unnormalized expression!
742		conj_to_list(Body,BodyList,[]),
743		select(equal(A,B),BodyList,RestBodyList),
744		( A=LambdaID, not_occurs(B,Lambda), LambdaExpr=B
745		; B=LambdaID, not_occurs(A,Lambda), LambdaExpr=A
746		).
747
748		% just check if something is a lambda function or similar, without computing exact domain
749		is_lambda_function(comprehension_set(IDS,Body)) :- !,
750		get_lambda_args_and_body(IDS,Body,_,_,_,_).
751		is_lambda_function(Expr) :- is_lambda_function_with_domain(Expr,_).
752
753		% determine if something is a lambda function and determine exact domain:
754		is_lambda_function_with_domain(comprehension_set(IDS,Body),Set) :-
755		get_lambda_args_and_body(IDS,Body,_,_,Args,RestBodyList),
756		get_argument_types(Args,Args,RestBodyList,ArgTypes),
757		create_cartesian_product(ArgTypes,Set).
758		is_lambda_function_with_domain(cartesian_product(Domain,Set),Domain) :-
759		singleton_set(Set,_).
760		is_lambda_function_with_domain(set_extension([couple(El,_)]),set_extension([El])).
761		is_lambda_function_with_domain(Set,singleton_set([El])) :- singleton_set(Set,couple(El,_)). % TO DO: longer lists and check no multiple domain elements
762		is_lambda_function_with_domain(sequence_extension(List),interval(1,Len)) :- length(List,Len).
763		% we could treat domain_restriction, domain_subtraction here
764
765		singleton_set(set_extension([El]),El).
766		singleton_set(sorted_set_extension([El]),El).
767
768		conj_to_list(conjunct(A,B)) --> !, conj_to_list(A),conj_to_list(B).
769		conj_to_list(X) --> [X].
770
771		:- use_module(probsrc(tools),[map_split_list/4]).
772		% we support Arg:Set and we support an argument not appearing at all (equivalent to Arg:typeset)
773		get_argument_types([],_,[],[]). % no other conjuncts remain in body
774		get_argument_types(['$'(ID1)|T],AllArgs,BodyList,[Set1|TS]) :-
775		map_split_list(typing_predicate_for(ID1,AllArgs),BodyList,TypingSetList,RestBody),
776		create_intersection(TypingSetList,Set1),
777		get_argument_types(T,AllArgs,RestBody,TS).
778
779		% check if we have a typing predicate for a given identifier
780		typing_predicate_for(ID1,AllArgs,member('$'(ID1),Set1),Set1) :- l_not_occurs(Set1,AllArgs).
781		typing_predicate_for(ID1,AllArgs,subset('$'(ID1),SSet1),pow_subset(SSet1)) :- l_not_occurs(SSet1,AllArgs).
782
783		% check if any argument appears in expression; if so we have a link between arguments and no proper type
784		l_not_occurs(Expr,AllArgs) :- member('$'(ID),AllArgs), occurs(Expr,ID),!,fail.
785		l_not_occurs(_,_).
786
787		create_intersection([],typeset). % no constraints on identifier: use typeset
788		create_intersection([A],Res) :- !, Res=A.
789		create_intersection([A|T],intersection(A,Rest)) :- create_intersection(T,Rest).
790
791		create_cartesian_product([Type],Res) :- !, Res=Type.
792		create_cartesian_product([Type|T],Res) :- create_cartesian_product3(T,Type,Res).
793
794		create_cartesian_product3([],Res,Res).
795		create_cartesian_product3([Type|T],Acc,Res) :-
796		create_cartesian_product3(T,cartesian_product(Acc,Type),Res).
797		% Note: dom(%(x,y,z).(x:BOOL & y:1..2 & z:BOOL|1)) = (BOOL*(1..2))*BOOL
798
799		% ------------------------
800
801		% Partial Function Check:
802
803		% check if Func : Domain +-> Range
804		check_is_partial_function_with_type(Func,_,_,Hyps,empty_set(PT)) :- check_equal_empty_set(Func,Hyps,PT),!.
805		check_is_partial_function_with_type(Func,Domain,Range,Hyps,pfun(PTD,PTR)) :-
806		check_is_partial_function(Func,Hyps),!,
807		(maximal_set(Domain,Hyps) -> PTD=maximal_domain ; check_is_subset(domain(Func),Domain,Hyps,PTD)),!,
808		(maximal_set(Range,Hyps) -> PTR=maximal_range ; check_is_subset(range(Func),Range,Hyps,PTR)).
809
810		% various way to make a function smaller, related to subset
811		function_restriction(domain_subtraction(_,F),F).
812		function_restriction(domain_restriction(_,F),F).
813		function_restriction(range_subtraction(F,_),F).
814		function_restriction(range_restriction(F,_),F).
815		function_restriction(set_subtraction(F,_),F).
816
817		% check if Func : DomTYPE +-> RanTYPE
818		% check if we can deduce from the Hypotheses that something is a partial function
819		check_is_partial_function(Func,Hyps) :-
820		avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1),
821		% also deals with function(_) f : _ +-> ( _ +-> _ ) => f(_) : _ +-> _
822		is_partial_function_type(Function,Hyps1,_),!.
823		check_is_partial_function(reverse(Func),Hyps) :-
824		check_is_injective(Func,Hyps),!.
825		check_is_partial_function(value(avl_set(AVL)),_) :- !,
826		nonvar(AVL),
827		is_avl_partial_function(AVL).
828		check_is_partial_function(composition(F1,F2),Hyp) :- !,
829		% composition of two partial functions is a partial function
830		(check_is_partial_function(F1,Hyp)
831		-> check_is_partial_function(F2,Hyp)
832		).
833		check_is_partial_function(overwrite(F1,F2),Hyp) :- !,
834		% overwrite of two partial functions is a partial function
835		(check_is_partial_function(F1,Hyp)
836		-> check_is_partial_function(F2,Hyp)
837		).
838		check_is_partial_function(direct_product(F1,F2),Hyp) :- !,
839		% direct_product of two partial functions is a partial function a:A+->B & b:A+->C => a><b : A+->(B*C)
840		(check_is_partial_function(F1,Hyp)
841		-> check_is_partial_function(F2,Hyp)
842		).
843		check_is_partial_function(identity(_),_Hyp) :- !.
844		check_is_partial_function(Func,Hyp) :- function_restriction(Func,LargerFunc), !,
845		check_is_partial_function(LargerFunc,Hyp).
846		check_is_partial_function(intersection(F1,F2),Hyp) :- !,
847		(check_is_partial_function(F1,Hyp) -> true ; check_is_partial_function(F2,Hyp)).
848		check_is_partial_function(sorted_set_extension(List),Hyp) :- !,
849		check_set_extension_is_partial_function(List,Hyp).
850		check_is_partial_function(set_extension(List),Hyp) :- !,
851		check_set_extension_is_partial_function(List,Hyp).
852		check_is_partial_function(Expr,_) :-
853		is_lambda_function(Expr),!. % also treats cartesian_product and sequence_extension
854		% check_is_partial_function(X,_Hyp) :- is_empty_set_direct(X),!. % covered by infer_sequence_type_of_expr below
855		check_is_partial_function(Expr,Hyps) :-
856		infer_sequence_type_of_expr(Expr,Hyps,_),!. % any sequence expression is a partial function; e.g. a <- b, front(.)
857		check_is_partial_function(Func,Hyps) :- rewrite_set_expression_exact(Func,Hyps,NewFunc,Hyps2),!,
858		check_is_partial_function(NewFunc,Hyps2).
859		check_is_partial_function(union(F1,F2),Hyps) :-
860		check_is_subset(F1,F2,Hyps,_),!,
861		check_is_partial_function(F2,Hyps).
862		check_is_partial_function(union(F1,F2),Hyps) :-
863		check_is_subset(F2,F1,Hyps,_),!,
864		check_is_partial_function(F1,Hyps).
865		check_is_partial_function(union(F1,F2),Hyps) :- !,
866		check_domain_disjoint(F1,F2,Hyps,Hyps2), % domain must be disjoint, not F1 and F2
867		check_is_partial_function(F1,Hyps2),
868		check_is_partial_function(F2,Hyps2).
869		check_is_partial_function(Func,Hyps) :- % f<:g & g: A +-> B => f : A +-> B
870		(Op = equal ; Op = subset),
871		avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1),
872		quick_not_occurs_check(Func,Func2),
873		check_is_partial_function(Func2,Hyps1).
874
875		check_domain_disjoint(F1,F2,Hyps,Hyps2) :-
876		compute_exact_domain(F1,Hyps,DF1,Hyps2),
877		% example: :prove f:BOOL +-> BOOL & x /: dom(f) => f \/ {x|->TRUE} : BOOL +-> BOOL
878		is_set_extension(DF1,List1),!,
879		l_check_not_member_of_set(List1,domain(F2),Hyps2). % we could try and compute domain(F2) first
880		check_domain_disjoint(F2,F1,Hyps,Hyps2) :-
881		compute_exact_domain(F1,Hyps,DF1,Hyps2),
882		is_set_extension(DF1,List1),!,
883		l_check_not_member_of_set(List1,domain(F2),Hyps2).
884		check_domain_disjoint(F1,F2,Hyps,Hyps2) :-
885		get_domain_or_superset(F1,Hyps,DomFunc1,Hyps1),
886		get_domain_or_superset(F2,Hyps1,DomFunc2,Hyps2),
887		check_disjoint(DomFunc1,DomFunc2,Hyps2).
888
889		%check_is_partial_function(Func,_) :- print(check_is_partial_function_failed(Func)),nl,fail.
890
891		% check if this is a partial function type or something defined to be equal to a function type
892		:- if(environ(prob_safe_mode,true)).
893		is_partial_function_type(P,H,H1) :- nonvar(H1),
894		add_internal_error('Illegal hyps:',is_partial_function_type(P,H,H1)),fail.
895		:- endif.
896		is_partial_function_type(PF,Hyps,Hyps1) :- is_partial_function(PF,_,_),!,Hyps1=Hyps.
897		is_partial_function_type(range(Func),Hyps,Hyps2) :-
898		get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!,
899		is_partial_function_type(RanFunc,Hyps1,Hyps2).
900		is_partial_function_type(domain(Func),Hyps,Hyps2) :-
901		get_domain_or_superset(Func,Hyps,DomFunc,Hyps1),!,
902		is_partial_function_type(DomFunc,Hyps1,Hyps2).
903		is_partial_function_type(sorted_set_extension(Funcs),Hyps,Hyps2) :- !,
904		is_partial_function_type(set_extension(Funcs),Hyps,Hyps2).
905		is_partial_function_type(set_extension(Funcs),Hyps,Hyps2) :- !,
906		(member(F,Funcs), \+ check_is_partial_function(F,Hyps) -> fail
907		; Hyps2=Hyps). % all elements of Funcs are partial functions
908		is_partial_function_type(Func,Hyps,Hyps2) :-
909		get_superset(Func,Hyps,SuperSet,Hyps1),!,
910		is_partial_function_type(SuperSet,Hyps1,Hyps2).
911		is_partial_function_type(PF,Hyps,Hyps2) :-
912		avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R
913		is_partial_function_type(PF2,Hyps1,Hyps2).
914
915		% get worthwhile superset
916		get_superset(comprehension_set([ID],Body),Hyps,Set,Hyps) :-
917		get_parameter_superset_in_body(ID,[ID],Body,Set).
918		get_superset(set_subtraction(A,_),Hyps,A,Hyps).
919		get_superset(intersection(A,B),Hyps,R,Hyps) :- (R=A ; R=B).
920
921		is_partial_function(total_function(A,B),A,B).
922		is_partial_function(partial_function(A,B),A,B).
923		is_partial_function(total_injection(A,B),A,B).
924		is_partial_function(partial_injection(A,B),A,B).
925		is_partial_function(total_surjection(A,B),A,B).
926		is_partial_function(partial_surjection(A,B),A,B).
927		is_partial_function(total_bijection(A,B),A,B).
928		is_partial_function(partial_bijection(A,B),A,B).
929		is_partial_function(perm(A),'NATURAL1',A).
930		is_partial_function(seq(B),'NATURAL1',B).
931		is_partial_function(seq1(B),'NATURAL1',B).
932		is_partial_function(iseq(B),'NATURAL1',B).
933		is_partial_function(iseq1(B),'NATURAL1',B).
934
935		% if First = f(1,GS) -> we can check if function is total; we could store summary of set_extension in hyps
936		check_set_extension_is_partial_function([_],_) :- !. % one element set extension is a function
937		check_set_extension_is_partial_function(List,Hyps) :-
938		maplist(get_explicit_dom_value(Hyps),List,VList),!,
939		sort(VList,SList),
940		SList = [couple(First,_)|TS],
941		check_set_ext_pf(TS,First,Hyps).
942		check_set_extension_is_partial_function([couple(A,_),couple(B,_)],Hyps) :-
943		check_not_equal(A,B,Hyps). % TO DO: all_different for longer lists
944
945		check_set_ext_pf([],_,_).
946		check_set_ext_pf([couple(Next,_)|TS],Last,Hyp) :-
947		Next \= Last,
948		check_set_ext_pf(TS,Next,Hyp).
949
950		get_explicit_dom_value(Hyps,couple(Val,RanVal),couple(Val2,RanVal)) :- get_explicit_value(Val,Hyps,Val2).
951
952		get_explicit_value(couple(A,B),Hyps,couple(A2,B2)) :- !,
953		get_explicit_value(A,Hyps,A2), get_explicit_value(B,Hyps,B2).
954		get_explicit_value(rec(Fields),Hyps,rec(SFields2)) :- !,
955		maplist(get_field_value(Hyps),Fields,Fields2),
956		sort(Fields2,SFields2).
957		get_explicit_value(Val,Hyps,R) :- is_explicit_value(Val,AVal,Hyps),!,R=AVal.
958		get_explicit_value('$'(ID),Hyps,Res) :-
959		avl_fetch_equal_from_hyps('$'(ID),Hyps,Val2,Hyps2),
960		is_explicit_value(Val2,Res,Hyps2). % should we allow recursion through multiple equations?
961
962		% is value which can be compared using Prolog equality
963		% cf. avl_can_fetch
964		is_explicit_value(boolean_true,pred_true,_).
965		is_explicit_value(boolean_false,pred_false,_).
966		is_explicit_value(Nr,Nr,_) :- number(Nr). % integers and floats
967		is_explicit_value(integer(Nr),Nr,_) :- integer(Nr). % normally already replaced by norm_expr2
968		is_explicit_value(string(Atom),Atom,_).
969		is_explicit_value(real(Atom),Res,_) :- atom(Atom),
970		construct_real(Atom,term(floating(Res))). % c.f. is_real/1 in kernel_reals
971		is_explicit_value(couple(A,B),(AV,BV),Hyp) :- is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp).
972		is_explicit_value('$'(ID),'$'(ID),Hyp) :- is_global_constant_id(ID,Hyp).
973		is_explicit_value(value(R),Nr,_) :- nonvar(R),R=int(Nr), integer(Nr). % TODO: more values, strings, reals, ...
974
975
976		get_field_value(Hyps,field(Name,Val),field(Name,Val2)) :- get_explicit_value(Val,Hyps,Val2).
977
978		:- use_module(probsrc(b_global_sets), [lookup_global_constant/2]).
979		% enumerated set element name
980		is_global_constant_id(ID,Hyp) :-
981		lookup_global_constant(ID,_),
982		\+ is_hyp_var(ID,Hyp). % global enumerated set constant visible
983
984		is_enumerated_set(ID,Hyp) :-
985		enumerated_set(ID),
986		\+ is_hyp_var(ID,Hyp). % global enumerated set constant visible
987
988		% Disjoint check:
989		check_disjoint(A,B,Hyps) :- %print(disj(A,B)),nl, portray_hyps(Hyps),nl,
990		(check_disjoint_aux(A,B,Hyps) -> true ; check_disjoint_aux(B,A,Hyps)).
991		check_disjoint_aux(S,_,Hyps) :- check_equal_empty_set(S,Hyps,_),!.
992		check_disjoint_aux(A,B,Hyps) :-
993		avl_fetch_from_hyps(equal(intersection(A,B),empty_set),Hyps),!.
994		check_disjoint_aux(domain_subtraction(A,_),B,Hyps) :- !, % A <<| f /\ B = {} if dom(B) <: A
995		get_domain_or_superset(B,Hyps,DomB,Hyps2),
996		check_is_subset(DomB,A,Hyps2,_).
997		check_disjoint_aux(set_subtraction(AA,A),B,Hyps) :- !,
998		(check_is_subset(B,A,Hyps,_) -> true % x \ A /\ B = {} if B <: A
999		; check_disjoint(AA,B,Hyps) -> true). % AA-A /\ B ={} if AA /\ B = {}
1000		check_disjoint_aux(set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps).
1001		check_disjoint_aux(sorted_set_extension(As),B,Hyps) :- !, l_check_not_member_of_set(As,B,Hyps).
1002		check_disjoint_aux(A,B,Hyps) :-
1003		avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A1,Hyps1),
1004		check_disjoint(A1,B,Hyps1).
1005		% TO DO: move union of set_extension here?
1006
1007		l_check_not_member_of_set([],_,_).
1008		l_check_not_member_of_set([El|T],Set,Hyps) :-
1009		check_not_member_of_set(Set,El,Hyps,_PT),
1010		l_check_not_member_of_set(T,Set,Hyps).
1011
1012		% Injective check:
1013
1014		check_is_injective(Func,Hyps) :-
1015		get_type_from_hyps(Func,Hyps,Function,Hyps1),
1016		%print(check_rev_fun(Func,Function)),nl,
1017		is_injective_function_type(Function,Hyps1,_).
1018		check_is_injective(value(avl_set(AVL)),_) :- !,
1019		nonvar(AVL), invert_explicit_set(avl_set(AVL),Inv),
1020		Inv=avl_set(AVL2), is_avl_partial_function(AVL2).
1021		check_is_injective(identity(_),_).
1022		check_is_injective(Set,_) :- singleton_set(Set,_). % TO DO: extend to more than singleton set_extension
1023		check_is_injective(sequence_extension([_]),_). % TO DO: check all elements are different
1024		check_is_injective(Func, Hyps) :-
1025		avl_fetch_equal_from_hyps(Func,Hyps,Value,Hyps2),
1026		%print(check_inj_value(Func,Value)),nl,
1027		check_is_injective(Value,Hyps2).
1028
1029		% check if this is a partial function type or something defined to be equal to a function type
1030		is_injective_function_type(PF,Hyps,Hyps1) :- is_injective(PF),!,Hyps1=Hyps.
1031		is_injective_function_type(PF,Hyps,Hyps2) :-
1032		avl_fetch_worthwhile_equal_from_hyps(PF,Hyps,PF2,Hyps1), % in case we have a definition like X = 1..n --> R
1033		is_injective_function_type(PF2,Hyps1,Hyps2).
1034
1035		is_injective(total_injection(_,_)).
1036		is_injective(partial_injection(_,_)).
1037		is_injective(total_bijection(_,_)).
1038		is_injective(partial_bijection(_,_)).
1039		is_injective(iseq(_)).
1040		is_injective(iseq1(_)).
1041
1042		% A /<: B <=> A/<<: B & A /= B
1043		check_not_subset(A,B,Hyps,PT) :-
1044		check_not_is_subset_strict(A,B,Hyps,PT),!,
1045		check_not_equal(A,B,Hyps).
1046
1047		% check_not_is_subset_strict(A,B,Hyps,PT) check if A is not a strict subset of B
1048		% not really used for WD proofs at the moment; mainly as top-level goal in prove_po
1049		% (now used for proving set_subtraction is not empty; test 2469)
1050		% probably quite a few more rules necessary to make it useful
1051		check_not_is_subset_strict(A,B,Hyps,hyp) :-
1052		avl_fetch_from_hyps(not_subset_strict(A,B),Hyps),!. % hyp; currently not marked as useful by default!
1053		check_not_is_subset_strict(A,B,Hyps,hyp2) :-
1054		avl_fetch_from_hyps(not_subset(A,B),Hyps),!. % not(A <: B) => not (A<<:B)
1055		check_not_is_subset_strict(A,B,Hyps,equal(PT)) :-
1056		check_equal(A,B,Hyps,PT),!. % A=B => not (A<<:B)
1057		check_not_is_subset_strict(_,B,Hyps,empty_set(PT)) :- % A /<<: {}
1058		check_equal_empty_set(B,Hyps,PT).
1059		check_not_is_subset_strict(MAX,_,Hyps,maximal_set) :- % MAX /<<: B
1060		maximal_set(MAX,Hyps),!.
1061		check_not_is_subset_strict(A,B,Hyps,not_empty_singleton(PT)) :- % x <<: {A} <=> x={}
1062		singleton_set(B,_),!,
1063		check_not_equal_empty_set(A,Hyps,PT).
1064		check_not_is_subset_strict(A,B,Hyps,superset_eq1(PT)) :-
1065		(Operator = equal ; Operator = superset), % A :> S2 & S2 /<<: B => A /<<: B
1066		avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2),
1067		rewrite_local_loop_check(A,check_not_is_subset_strict,S2,Hyps2,Hyps3),
1068		check_not_is_subset_strict(S2,B,Hyps3,PT),!.
1069		check_not_is_subset_strict(A,B,Hyps,subset_eq2(PT)) :-
1070		(Operator = equal ; Operator = subset), % B <: S2 & A /<<: S2 => A /<<: B
1071		avl_fetch_binop_from_hyps(B,Operator,Hyps,S2,Hyps2),
1072		rewrite_local_loop_check(B,check_not_is_subset_strict,S2,Hyps2,Hyps3),
1073		check_not_is_subset_strict(A,S2,Hyps3,PT),!.
1074		%check_not_is_subset_strict(A,B,H,_) :- print(check_not_is_subset_strict_failed(A,B)),nl, portray_hyps(H),nl,fail.
1075
1076
1077		check_is_subset_strict(A,B,Hyp,empty_singleton(PT)) :- % x <<: {A} <=> x={}
1078		singleton_set(B,_),!,
1079		check_equal_empty_set(A,Hyp,PT).
1080		check_is_subset_strict(A,B,Hyp,PT) :- % A <<: B <=> A <: B & A /= B
1081		check_is_subset(A,B,Hyp,PT),!,
1082		check_not_equal(A,B,Hyp).
1083
1084		% check if something is a subset of something else
1085		check_is_subset(H,H,_,equal).
1086		check_is_subset(A,B,Hyps,hyp) :-
1087		avl_fetch_from_hyps(subset(A,B),Hyps),!. % hyp
1088		check_is_subset(_,MAX,Hyps,maximal_set) :- maximal_set(MAX,Hyps),!.
1089		check_is_subset(S,_,Hyps,empty_set(PT)) :- check_equal_empty_set(S,Hyps,PT),!. % {} <: B
1090		check_is_subset(cartesian_product(A,B),cartesian_product(A2,B2),Hyps,cart(PTA,PTB)) :- !,
1091		% A <: A2 & B <: B2 => (A*B) <: (A2*B2)
1092		(check_is_subset(A,A2,Hyps,PTA)
1093		-> check_is_subset(B,B2,Hyps,PTB)).
1094		check_is_subset('NATURAL1','NATURAL',_,nat1_nat) :- !.
1095		check_is_subset(interval(L,U),B,Hyps,interval(PT)) :- !, check_subset_interval(B,L,U,Hyps,PT).
1096		check_is_subset(intersection(A,B),Super,Hyps,intersection(PT)) :- !,
1097		( check_is_subset(A,Super,Hyps,PT) -> true ; check_is_subset(B,Super,Hyps,PT)).
1098		check_is_subset(union(A,B),Super,Hyps,union(PTA,PTB)) :- !,
1099		( check_is_subset(A,Super,Hyps,PTA) -> check_is_subset(B,Super,Hyps,PTB)).
1100		check_is_subset(domain_subtraction(_,B),Super,Hyps,dom_sub(PT)) :- !,check_is_subset(B,Super,Hyps,PT).
1101		check_is_subset(domain_restriction(_,B),Super,Hyps,dom_res(PT)) :- !,check_is_subset(B,Super,Hyps,PT).
1102		check_is_subset(range_subtraction(A,_),Super,Hyps,ran_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT).
1103		check_is_subset(range_restriction(A,_),Super,Hyps,ran_res(PT)) :- !,check_is_subset(A,Super,Hyps,PT).
1104		check_is_subset(set_subtraction(A,_),Super,Hyps,set_sub(PT)) :- !,check_is_subset(A,Super,Hyps,PT).
1105		check_is_subset(value(avl_set(AVL)),B,Hyps,avl) :- !,check_subset_avl(B,AVL,Hyps).
1106		check_is_subset(A,B,Hyps,subset_eq(PT)) :-
1107		(Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyps
1108		% TO DO: similar rule for B
1109		avl_fetch_binop_from_hyps(A,Operator,Hyps,S2,Hyps2),
1110		rewrite_local_loop_check(A,check_is_subset,S2,Hyps2,Hyps3),
1111		check_is_subset(S2,B,Hyps3,PT),!.
1112		check_is_subset('$'(ID),B,Hyps,eq(ID,PT)) :-
1113		get_type_from_hyps('$'(ID),Hyps,Set,Hyps2),
1114		extract_element_super_set_type(Set,Hyps2,S2),
1115		rewrite_local_loop_check(ID,check_is_subset,S2,Hyps2,Hyps3),
1116		check_is_subset(S2,B,Hyps3,PT),!.
1117		check_is_subset(domain(Func),B,Hyps,domain(PT)) :-
1118		get_domain_or_superset(Func,Hyps,DomFunc,Hyps2),
1119		%rewrite_local_loop_check(domain(Func),check_is_subset,DomFunc,Hyps2,Hyps3),
1120		check_is_subset(DomFunc,B,Hyps2,PT),!.
1121		check_is_subset(range(Func),B,Hyps,range(PT)) :-
1122		get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
1123		%rewrite_local_loop_check(range(Func),check_is_subset,RanFunc,Hyps2,Hyps3),
1124		check_is_subset(RanFunc,B,Hyps2,PT),!.
1125		check_is_subset(function(Func,_),B,Hyps,function_range(PT)) :- !,
1126		get_range_or_superset(Func,Hyps,RanFunc,Hyps2), % f : _ +-> POW(Ran) & Ran <: B => f(.) <: B
1127		subset_transitivity_rule(RanFunc,pow_subset(B),A2,B2), % extract pow_subset from Range
1128		check_is_subset(A2,B2,Hyps2,PT).
1129		check_is_subset(image(Func,_),B,Hyps,image(PT)) :- % or B=range(Range)
1130		(B = range(FuncB),check_equal(Func,FuncB,Hyps,_) -> !, PT=range_of_same_func % f[.] <: ran(f)
1131		; get_range_or_superset(Func,Hyps,Range,Hyps2) -> !, check_is_subset(Range,B,Hyps2,PT)).
1132		check_is_subset(A,B,Hyps,transitivity(PT)) :- subset_transitivity_rule(A,B,A2,B2),
1133		!, % unary subset rules like POW(A2) <: POW(B2) if A2 <: B2
1134		check_is_subset(A2,B2,Hyps,PT).
1135		check_is_subset(A,B,Hyps,transitivity(PT1,PT2)) :- subset_bin_transitivity_rule(A,B,A1,A2,B1,B2),
1136		!, % binary subset rules like A1+->B1 <: A2+->B2 if A1 <:B1 & A2 <: B2
1137		(check_is_subset(A1,B1,Hyps,PT1) -> check_is_subset(A2,B2,Hyps,PT2)).
1138		check_is_subset(sorted_set_extension(List),B,Hyps,PT) :- !,
1139		check_is_subset(set_extension(List),B,Hyps,PT).
1140		check_is_subset(set_extension(List),B,Hyps,set_extension) :-
1141		simplify_expr(B,Hyps,BS), % simplify expression once
1142		%portray_hyps(Hyps),nl,
1143		l_check_is_member(List,BS,Hyps).
1144		check_is_subset(Sub,union(A,B),Hyps,sub_union(PT)) :- !,
1145		( check_is_subset(Sub,A,Hyps,PT) -> true ; check_is_subset(Sub,B,Hyps,PT)).
1146		% get_set_of_possible_values; treat sequence_extension
1147		%check_is_subset(A,B,_,_) :- print(check_is_subset_failed(A,B)),nl,nl,fail.
1148
1149		l_check_is_member([],_,_).
1150		l_check_is_member([El|T],B,Hyps) :- check_member_of_set(B,El,Hyps,_ProofTree), l_check_is_member(T,B,Hyps).
1151
1152		% extract set type of the elements of a set: x: POW(A) ==> x<:A
1153		extract_element_super_set_type(FuncType,Hyps,cartesian_product(A,B)) :-
1154		get_possible_domain_of_func_or_rel_type(FuncType,Hyps,A,_),!,
1155		get_possible_range_of_func_or_rel_type_direct(FuncType,B,_).
1156		extract_element_super_set_type(fin_subset(A),_,A).
1157		extract_element_super_set_type(fin1_subset(A),_,A).
1158		extract_element_super_set_type(pow_subset(A),_,A).
1159		extract_element_super_set_type(pow1_subset(A),_,A).
1160
1161
1162		% simple not member of set check
1163		check_not_member_of_set(Set,_,Hyps,empty_set) :- check_equal_empty_set(Set,Hyps,_),!.
1164		check_not_member_of_set(Set,El,Hyps,hyp) :-
1165		avl_fetch_from_hyps(not_member(El,Set),Hyps),!. % hyp
1166		check_not_member_of_set(if_then_else(_,A,B),El,Hyps,if_then_else(PTA,PTB)) :-
1167		(check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!.
1168		check_not_member_of_set(intersection(A,B),El,Hyps,inter(PT)) :-
1169		(check_not_member_of_set(A,El,Hyps,PT) -> true ; check_not_member_of_set(B,El,Hyps,PT)),!.
1170		check_not_member_of_set(set_subtraction(A,B),El,Hyps,inter(PT)) :-
1171		(check_not_member_of_set(A,El,Hyps,PT) -> true ; check_member_of_set(B,El,Hyps,PT)),!.
1172		check_not_member_of_set(union(A,B),El,Hyps,inter(PTA,PTB)) :-
1173		(check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!.
1174		check_not_member_of_set(overwrite(A,B),El,Hyps,overwrite(PTA,PTB)) :-
1175		(check_not_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)),!.
1176		check_not_member_of_set('NATURAL1',El,Hyps,nat1) :-
1177		check_leq(El,0,Hyps).
1178		check_not_member_of_set('NATURAL',El,Hyps,nat1) :-
1179		check_leq(El,-1,Hyps).
1180		check_not_member_of_set(interval(From,To),El,Hyps,interval) :-
1181		(check_leq(El,minus(From,1),Hyps) -> true
1182		; check_leq(add(To,1),El,Hyps) -> true). % TODO: or interval empty
1183		check_not_member_of_set(domain(Func),El,Hyps,not_in_domain(PT)) :-
1184		check_not_member_of_domain(Func,El,Hyps,PT),!.
1185		check_not_member_of_set(range(Func),El,Hyps,not_in_range(PT)) :-
1186		check_not_member_of_range(Func,El,Hyps,PT),!.
1187		check_not_member_of_set(Set,couple(From,_),Hyps,not_in_dom(PT)) :-
1188		% x /: dom(f) => x|->y /: f
1189		avl_fetch_binop_from_hyps(From,not_member,Hyps,Set2,Hyps2),
1190		check_is_subset(domain(Set),Set2,Hyps2,PT),
1191		!.
1192		check_not_member_of_set(Set,couple(_,To),Hyps,not_in_range) :-
1193		avl_fetch_from_hyps(not_member(To,range(Set)),Hyps), % y /: ran(f) => x|->y /: f
1194		!. % TODO: generalise this rule somewhat, see domain above
1195		check_not_member_of_set(A,El,Hyps,eq(ProofTree)) :-
1196		avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),
1197		rewrite_local_loop_check(A,check_member_of_set,Value,Hyps2,Hyps3),
1198		check_not_member_of_set(Value,El,Hyps3,ProofTree).
1199		check_not_member_of_set(Set,El,Hyps,not_in_set_extension) :-
1200		is_set_extension(Set,List),
1201		check_not_member_of_list(List,El,Hyps).
1202		%check_not_member_of_set(Set,El,Hyps,_) :- print(not_mem_failed(Set,El)),nl,fail.
1203		% TO DO: process equalities, set_extension?, value(avl_set(AVL)), ...
1204
1205		% check if an element is not in the domain of a function
1206		check_not_member_of_domain(domain_subtraction(DS,Func),El,Hyps,not_dom_sub(PT)) :-
1207		(check_member_of_set(DS,El,Hyps,PT) -> true
1208		; check_not_member_of_domain(Func,El,Hyps,PT)).
1209		check_not_member_of_domain(domain_restriction(DS,Func),El,Hyps,not_dom_sub(PT)) :-
1210		(check_not_member_of_set(DS,El,Hyps,PT) -> true
1211		; check_not_member_of_domain(Func,El,Hyps,PT)).
1212		check_not_member_of_domain(Func,El,Hyps,PT) :-
1213		get_domain_or_superset(Func,Hyps,DomFunc,Hyps1),!,
1214		check_not_member_of_set(DomFunc,El,Hyps1,PT).
1215
1216		% check if an element is not in the domain of a function
1217		check_not_member_of_range(range_subtraction(Func,DS),El,Hyps,not_dom_sub(PT)) :-
1218		(check_member_of_set(DS,El,Hyps,PT) -> true
1219		; check_not_member_of_range(Func,El,Hyps,PT)).
1220		check_not_member_of_range(range_restriction(Func,DS),El,Hyps,not_dom_sub(PT)) :-
1221		(check_not_member_of_set(DS,El,Hyps,PT) -> true
1222		; check_not_member_of_range(Func,El,Hyps,PT)).
1223		check_not_member_of_range(Func,El,Hyps,PT) :-
1224		get_range_or_superset(Func,Hyps,RanFunc,Hyps1),!,
1225		check_not_member_of_set(RanFunc,El,Hyps1,PT).
1226
1227
1228
1229		% check that an element does not occur in a list of values/expressions
1230		check_not_member_of_list([],_,_).
1231		check_not_member_of_list([H|T],El,Hyps) :-
1232		check_not_equal(H,El,Hyps),
1233		check_not_member_of_list(T,El,Hyps).
1234
1235		is_set_extension(set_extension(List),List).
1236		is_set_extension(sorted_set_extension(List),List).
1237
1238
1239		% check_member_of_set(Set,Element,Hyps,ProofTree)
1240		% check_member_of_set(A,B,_H,_ProofTree) :- print(check_member_of_set(A,B)),nl,fail.
1241		check_member_of_set(Set,_,Hyps,maximal_set) :- maximal_set(Set,Hyps), !.
1242		check_member_of_set(Set,if_then_else(_,A,B),Hyps,if(P1,P2)) :- !, % if-then-else exprssion
1243		(check_member_of_set(Set,A,Hyps,P1) -> check_member_of_set(Set,B,Hyps,P2)).
1244		check_member_of_set(Set,El,Hyps,hyp) :-
1245		% we could do avl_fetch_binop_from_hyps(El,member,Hyps,Set2,Hyps2), and check_subset(Set2,Set)
1246		avl_fetch_from_hyps(member(El,Set),Hyps),!. % hyp
1247		% TO DO: sometimes value(El) stored !
1248		check_member_of_set(sorted_set_extension(List),El,Hyps,PT) :- !, % ordsets:ord_member(El,List),!.
1249		check_member_of_set(set_extension(List),El,Hyps,PT).
1250		check_member_of_set(set_extension(List),El,Hyps,set_extension) :- member(El2,List),
1251		check_equal(El,El2,Hyps,_),!. % TO DO: avoid multiple equality rewriting of El for long lists ?
1252		check_member_of_set(partial_function(T1,T2),El,Hyps,partial_function(PT)) :-
1253		check_is_partial_function_with_type(El,T1,T2,Hyps,PT).
1254		check_member_of_set(range(Func),El,Hyps,mem_range(PT)) :-
1255		check_member_of_range(El,Func,Hyps,PT),!. % check before function application below, can do symbolic range check
1256		check_member_of_set(image(Func,set_extension([S1|_])),El,Hyps,mem_range_for_image(PT0,PT1)) :-
1257		% El:ran(F) & S /\ dom(F) \= {} => El:F[S]
1258		check_member_of_set(range(Func),El,Hyps,PT0),!,
1259		check_member_of_set(domain(Func),S1,Hyps,PT1). % TO DO: more general check S /\ dom(F) \= {}
1260		check_member_of_set(A,ElFunc,Hyps,typing_membership(PT)) :-
1261		get_type_from_hyps(ElFunc,Hyps,Range,Hyps2), % !, % moving cut later proves on additional PO for test 2039
1262		% e.g. f(.) : A if ran(f) <: Range & Range <: A
1263		%rewrite_local_loop_check(A,check_member_of_set,Range,Hyps2,Hyps3),
1264		check_is_subset(Range,A,Hyps2,PT),!.
1265		check_member_of_set(A,El,Hyps,eq(ProofTree)) :-
1266		avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),
1267		rewrite_local_loop_check(A,check_member_of_set,Value,Hyps2,Hyps3),
1268		check_member_of_set(Value,El,Hyps3,ProofTree).
1269		check_member_of_set(interval(L,U),El,Hyps,interval(PT)) :- !, check_in_interval(El,L,U,Hyps,PT).
1270		check_member_of_set('NATURAL1',El,Hyps,nat1(PT)) :- !, check_subset_interval('NATURAL1',El,El,Hyps,PT).
1271		check_member_of_set('NATURAL',El,Hyps,nat(PT)) :- !, check_subset_interval('NATURAL',El,El,Hyps,PT).
1272		check_member_of_set(union(A,B),El,Hyps,union(PTA,PTB)) :- !,
1273		(check_member_of_set(A,El,Hyps,PTA) -> true ; check_member_of_set(B,El,Hyps,PTB)).
1274		check_member_of_set(intersection(A,B),El,Hyps,intersection(PTA,PTB)) :- !,
1275		(check_member_of_set(A,El,Hyps,PTA) -> check_member_of_set(B,El,Hyps,PTB)).
1276		check_member_of_set(set_subtraction(A,B),El,Hyps,set_subtraction(PTA,PTB)) :- !,
1277		(check_member_of_set(A,El,Hyps,PTA) -> check_not_member_of_set(B,El,Hyps,PTB)).
1278		check_member_of_set(pow_subset(T1),El,Hyps,pow(PT)) :- !,
1279		check_is_subset(El,T1,Hyps,PT).
1280		check_member_of_set(fin_subset(T1),El,Hyps,fin(PT1,PT2)) :- !,
1281		check_is_subset(El,T1,Hyps,PT1),!,
1282		check_finite(El,Hyps,PT2).
1283		check_member_of_set(pow1_subset(T1),El,Hyps,pow1(PT)) :- !,
1284		check_not_empty_set(El,Hyps),!,
1285		check_is_subset(El,T1,Hyps,PT).
1286		check_member_of_set(fin1_subset(T1),El,Hyps,fin1(PT1,PT2)) :- !,
1287		check_not_empty_set(El,Hyps),!,
1288		check_is_subset(El,T1,Hyps,PT1),!,
1289		check_finite(El,Hyps,PT2).
1290		check_member_of_set(seq(T1),El,Hyps,seq(PT)) :- !,
1291		check_is_sequence(El,Hyps),
1292		check_is_subset(range(El),T1,Hyps,PT).
1293		check_member_of_set(seq1(T1),El,Hyps,seq1(PT)) :- !,
1294		check_is_non_empty_sequence(El,Hyps),
1295		check_is_subset(range(El),T1,Hyps,PT).
1296		check_member_of_set(cartesian_product(T1,T2),couple(El1,El2),Hyps,cart(PT1,PT2)) :- !,
1297		check_member_of_set(T1,El1,Hyps,PT1),
1298		check_member_of_set(T2,El2,Hyps,PT2).
1299		check_member_of_set(value(avl_set(AVL)),El,Hyps,PT) :-
1300		(avl_can_fetch(El,BVal) -> !,PT=avl_fetch(El),avl_fetch(BVal,AVL)
1301		; avl_is_interval(AVL,Min,Max) -> !, PT=avl_interval(PT2),
1302		% useful is El is not a number, but e.g. an arithmetic expression
1303		% print(avl_interval(Min,Max,El)),nl,
1304		check_integer(El,check_member_of_set_avl_interval),
1305		check_in_interval(El,Min,Max,Hyps,PT2)
1306		).
1307		check_member_of_set(A,El,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
1308		check_member_of_set(A2,El,Hyps2,PT).
1309		check_member_of_set(domain(Func),Index,Hyps,mem_domain(PT)) :-
1310		check_member_of_domain(Index,Func,Hyps,PT),!.
1311		check_member_of_set(Set,X,Hyps,value_set(PT)) :- try_get_set_of_possible_values(X,Hyps,XSet,Hyps2),
1312		check_is_subset(XSet,Set,Hyps2,PT),!.
1313		%check_member_of_set(Set,X,Hyps,eq(PT)) :- Set = '$'(_),
1314		% avl_fetch_equal_from_hyps(Set,Hyps,Set2,Hyps2), % maybe perform direct rewrite ancestor cycle check here
1315		% check_member_of_set(Set2,X,Hyps2,PT),!.
1316		check_member_of_set(Set,X,Hyps,trans(PT)) :-
1317		avl_fetch_binop_from_hyps(Set,superset,Hyps,SubSet,Hyps2), % X:B & B <: A => X:A
1318		check_member_of_set(SubSet,X,Hyps2,PT),!.
1319		check_member_of_set(Set2,max(Set1),Hyps,mem_max(PT)) :- !, check_is_subset(Set1,Set2,Hyps,PT).
1320		check_member_of_set(Set2,min(Set1),Hyps,mem_min(PT)) :- !, check_is_subset(Set1,Set2,Hyps,PT).
1321		check_member_of_set(Set,ID,Hyps,member_subset(PT)) :-
1322		avl_fetch_worthwhile_member_from_hyps(ID,Hyps,SubSet,Hyps2), %write(sub(ID,SubSet,Set)),nl,
1323		check_is_subset(SubSet,Set,Hyps2,PT).
1324		%check_member_of_set(A,B,_H,_ProofTree) :- print(check_member_of_set_failed(A,B)),nl,fail.
1325
1326
1327		:- use_module(probsrc(kernel_reals),[construct_real/2]).
1328		% check if we can fetch an expression as a B value (second arg) in an AVL set
1329		avl_can_fetch(El,Res) :- number(El),!, Res=int(El).
1330		avl_can_fetch(boolean_true,pred_true).
1331		avl_can_fetch(boolean_false,pred_false).
1332		avl_can_fetch(real(Atom),R) :- construct_real(Atom,R).
1333		avl_can_fetch(string(S),string(S)) :- ground(S).
1334		avl_can_fetch(couple(A,B),(VA,VB)) :- avl_can_fetch(A,VA), avl_can_fetch(B,VB).
1335
1336		check_member_of_domain(El,reverse(Func2),Hyps,reverse(PT)) :- !,check_member_of_range(El,Func2,Hyps,PT).
1337		check_member_of_domain(Index,Func,Hyps,size_in_dom_seq) :- % x:seq1(T) => size(x) : dom(x)
1338		index_in_non_empty_sequence(Index,Func,Hyps),
1339		check_is_non_empty_sequence(Func,Hyps),!.
1340		% TO DO: f~(x) : dom(f) ??
1341		check_member_of_domain(El,union(A,B),Hyps,dom_of_union(PT)) :-
1342		check_member_of_union(domain(A),domain(B),El,Hyps,PT).
1343		check_member_of_domain(El,overwrite(A,B),Hyps,dom_of_overwrite(PT)) :-
1344		check_member_of_union(domain(A),domain(B),El,Hyps,PT).
1345		check_member_of_domain(El,direct_product(A,B),Hyps,dom_of_direct_product(PT)) :- % dom(A >< B) = dom(A) /\ dom (B)
1346		check_member_of_set(domain(A),El,Hyps,PT),
1347		check_member_of_set(domain(B),El,Hyps,PT).
1348		check_member_of_domain(El,A,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
1349		check_member_of_domain(El,A2,Hyps2,PT).
1350		check_member_of_domain(El,Func,Hyps,dom_of_subset(PT)) :- % Func2 <: Func & El:dom(Func2) => El:dom(Func)
1351		% counter part of rule with superset for check_member_of_set
1352		(Op = equal ; Op = superset),
1353		avl_fetch_binop_from_hyps(Func,Op,Hyps,Func2,Hyps1),
1354		rewrite_local_loop_check(Func,check_member_of_domain,Func2,Hyps1,Hyps2),
1355		check_member_of_set(domain(Func2),El,Hyps2,PT).
1356		check_member_of_domain(El,comprehension_set(IDS,Body),Hyps,dom_of_lambda(PTs)) :-
1357		get_lambda_args_and_body(IDS,Body,_,_,Args,RestBodyList),
1358		%nl,print(lambda(Args,El,RestBodyList)),nl,
1359		generate_funapp_binding(Args,El,Subst),
1360		% we rename the local variables of the comprehension set; no need to call add_new_hyp_any_vars
1361		l_rename_and_prove_goals(RestBodyList,Subst,Hyps,PTs).
1362		%check_member_of_domain(Index,Func,Hyps,_) :-
1363		% write(check_member_of_domain_failed(Index,Func)),nl,fail.
1364
1365		% we could do intersection, subtraction
1366
1367		% check if an element is an element of a union of two sets
1368		check_member_of_union(Set1,_,El,Hyps,PT) :- check_member_of_set(Set1,El,Hyps,PT),!.
1369		check_member_of_union(_,Set2,El,Hyps,PT) :- check_member_of_set(Set2,El,Hyps,PT),!.
1370		check_member_of_union(Set1,Set2,El,Hyps,union(PT1,PT2)) :-
1371		% x : A \/ B & A <: S1 & B <: S2 => x : S1 \/ S2
1372		avl_fetch_mem_from_hyps(El,Hyps,union(A,B),Hyps2), % TO DO: other conditions ?
1373		(check_is_subset(A,Set1,Hyps2,PT1) -> check_is_subset(B,Set2,Hyps2,PT2)
1374		; check_is_subset(A,Set2,Hyps2,PT1) -> check_is_subset(B,Set1,Hyps2,PT2)).
1375
1376		generate_funapp_binding(['$'(X)],El,[rename(X,El)]).
1377		generate_funapp_binding(['$'(X),'$'(Y)],couple(El1,El2),[rename(X,El1),rename(Y,El2)]).
1378		generate_funapp_binding(['$'(X),'$'(Y),'$'(Z)],couple(couple(El1,El2),El3),[rename(X,El1),rename(Y,El2),rename(Z,El3)]).
1379		% TO DO: create substitution for more arguments and other parameters
1380
1381
1382		check_member_of_range(El,reverse(Func2),Hyps,reverse(PT)) :- !,check_member_of_domain(El,Func2,Hyps,PT).
1383		check_member_of_range(El,A,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
1384		check_member_of_range(El,A2,Hyps2,PT).
1385		check_member_of_range('$'(ID),Func2,Hyps,PT) :-
1386		avl_fetch_worthwhile_equal_from_hyps('$'(ID),Hyps,Value,Hyps2),
1387		check_member_of_range(Value,Func2,Hyps2,PT).
1388		check_member_of_range(function(Func1,_),Func2,Hyps,func_app_in_range) :- % f(.) : ran(f)
1389		check_equal(Func1,Func2,Hyps,_).
1390
1391
1392		% subset transitivity for unary operators:
1393		subset_transitivity_rule(pow_subset(A),pow_subset(B),A,B).
1394
1395		subset_transitivity_rule(pow1_subset(A),pow1_subset(B),A,B).
1396		subset_transitivity_rule(pow1_subset(A),pow_subset(B),A,B).
1397
1398		subset_transitivity_rule(fin_subset(A),fin_subset(B),A,B).
1399		subset_transitivity_rule(fin_subset(A),pow_subset(B),A,B).
1400
1401		subset_transitivity_rule(fin1_subset(A),fin1_subset(B),A,B).
1402		subset_transitivity_rule(fin1_subset(A),fin_subset(B),A,B).
1403		subset_transitivity_rule(fin1_subset(A),pow1_subset(B),A,B).
1404		subset_transitivity_rule(fin1_subset(A),pow_subset(B),A,B).
1405
1406		subset_transitivity_rule(seq(A),seq(B),A,B).
1407		subset_transitivity_rule(seq(A),partial_function(typeset,B),A,B).
1408
1409		subset_transitivity_rule(seq1(A),seq1(B),A,B).
1410		subset_transitivity_rule(seq1(A),seq(B),A,B).
1411		subset_transitivity_rule(seq1(A),partial_function(typeset,B),A,B).
1412
1413		subset_transitivity_rule(iseq(A),iseq(B),A,B).
1414		subset_transitivity_rule(iseq(A),seq(B),A,B).
1415		subset_transitivity_rule(iseq(A),partial_function(typeset,B),A,B).
1416
1417		subset_transitivity_rule(iseq1(A),iseq1(B),A,B).
1418		subset_transitivity_rule(iseq1(A),iseq(B),A,B).
1419		subset_transitivity_rule(iseq1(A),seq1(B),A,B).
1420		subset_transitivity_rule(iseq1(A),seq(B),A,B).
1421		subset_transitivity_rule(iseq1(A),partial_function(typeset,B),A,B).
1422
1423		subset_transitivity_rule(perm(A),perm(B),A,B).
1424		subset_transitivity_rule(perm(A),iseq(B),A,B).
1425		subset_transitivity_rule(perm(A),seq(B),A,B).
1426		subset_transitivity_rule(perm(A),partial_function(typeset,B),A,B).
1427
1428
1429		subset_transitivity_rule(range(A),domain(reverse(B)),A,B).
1430		subset_transitivity_rule(range(A),range(B),A,B).
1431		subset_transitivity_rule(range(reverse(A)),domain(B),A,B).
1432		subset_transitivity_rule(domain(reverse(A)),range(B),A,B).
1433		subset_transitivity_rule(domain(A),domain(B),A,B). % dom(A) <: dom(B) if A <:B
1434		subset_transitivity_rule(domain(A),range(reverse(B)),A,B).
1435		subset_transitivity_rule(reverse(A),reverse(B),A,B).
1436		subset_transitivity_rule(rev(A),rev(B),A,B).
1437		subset_transitivity_rule(identity(A),identity(B),A,B).
1438
1439		% TO DO: add rules for more binary operators, like surjective relations, ...
1440		subset_bin_transitivity_rule(relations(A1,A2),relations(B1,B2),A1,A2,B1,B2). % <->
1441		subset_bin_transitivity_rule(total_relation(A1,A2),relations(B1,B2),A1,A2,B1,B2). % <<->
1442		subset_bin_transitivity_rule(total_relation(A1,A2),total_relation(B1,B2),A1,A2,B1,B2) :- A1=B1.
1443		subset_bin_transitivity_rule(partial_function(A1,A2),relations(B1,B2),A1,A2,B1,B2). % +->
1444		subset_bin_transitivity_rule(partial_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2).
1445		subset_bin_transitivity_rule(partial_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+>
1446		subset_bin_transitivity_rule(partial_injection(A1,A2),partial_injection(B1,B2),A1,A2,B1,B2).
1447		subset_bin_transitivity_rule(partial_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % -+>>
1448		subset_bin_transitivity_rule(partial_surjection(A1,A2),partial_surjection(B1,B2),A1,A2,B1,B2) :- A2=B2.
1449		subset_bin_transitivity_rule(partial_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+>>
1450		subset_bin_transitivity_rule(total_function(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % -->
1451		subset_bin_transitivity_rule(total_function(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1.
1452		subset_bin_transitivity_rule(total_injection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >->
1453		subset_bin_transitivity_rule(total_injection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1.
1454		subset_bin_transitivity_rule(total_surjection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % -->>
1455		subset_bin_transitivity_rule(total_surjection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1.
1456		subset_bin_transitivity_rule(total_bijection(A1,A2),partial_function(B1,B2),A1,A2,B1,B2). % >+>>
1457		subset_bin_transitivity_rule(total_bijection(A1,A2),partial_injection(B1,B2),A1,A2,B1,B2).
1458		subset_bin_transitivity_rule(total_bijection(A1,A2),partial_surjection(B1,B2),A1,A2,B1,B2) :- A2=B2.
1459		subset_bin_transitivity_rule(total_bijection(A1,A2),total_function(B1,B2),A1,A2,B1,B2) :- A1=B1.
1460		subset_bin_transitivity_rule(total_bijection(A1,A2),total_injection(B1,B2),A1,A2,B1,B2) :- A1=B1.
1461		subset_bin_transitivity_rule(total_bijection(A1,A2),total_surjection(B1,B2),A1,A2,B1,B2) :- A1=B1, A2=B2.
1462		subset_bin_transitivity_rule(image(A1,A2),image(B1,B2),A1,A2,B1,B2). % A1[A2] <: B1[B2] if A1 <: B1 & A2 <: B2
1463		subset_bin_transitivity_rule(domain_restriction(A1,A2),domain_restriction(B1,B2),A1,A2,B1,B2). % A1 <| A2 <: B1 <| B2 if A1 <: B1 & A2 <: B2
1464		subset_bin_transitivity_rule(range_restriction(A1,A2),range_restriction(B1,B2),A1,A2,B1,B2).
1465		subset_bin_transitivity_rule(domain_subtraction(A1,A2),domain_subtraction(B1,B2),B1,A2,A1,B2). % A1 <<| A2 <: B1 <<| B2 if B1 <: A1 & A2 <: B2
1466		subset_bin_transitivity_rule(range_subtraction(A1,A2),range_subtraction(B1,B2),A1,B2,A2,B1). % A1 |>> A2 <: B1|>> B2 if A1 <: B1 & B2 <: A2
1467		%subset_bin_transitivity_rule(A,B,A1,A2,B1,B2) :- write(subset_bin_transitivity_rule(A,B,A1,A2,B1,B2)),nl,fail.
1468		% TO DO: add more
1469
1470		% TO DO: instead of is_set_of_sequences_type
1471		%subset_mixed_transitivity_rule(total_function(A1,A2),seq(B2),A2,B2) :- is_interval(A1).
1472
1473
1474		check_in_interval(El,Min,Max,Hyps,PT) :-
1475		check_subset_interval(interval(Min,Max),El,El,Hyps,PT). % calls check_sub_intervals(Min,Max,El,El,Hyps)
1476
1477		% check if an interval is a subset of the first argument
1478		check_subset_interval(union(A,B),L1,U1,Hyps,union(PT)) :- !,
1479		% TO DO: try and merge A,B : union(interval(1,10),set_extension([11]))
1480		(check_subset_interval(A,L1,U1,Hyps,PT) -> true ; check_subset_interval(B,L1,U1,Hyps,PT)).
1481		check_subset_interval(sorted_set_extension(L),L1,U1,Hyps,PT) :- !,
1482		check_subset_interval(set_extension(L),L1,U1,Hyps,PT).
1483		check_subset_interval(set_extension(L),L1,U1,Hyps,set_extension(Nr)) :- !,
1484		% TO DO: maybe merge L into an interval
1485		nth1(Nr,L,El), check_sub_intervals(L1,U1,El,El,Hyps),!.
1486		check_subset_interval(intersection(A,B),L1,U1,Hyps,inter(PTA,PTB)) :- !,
1487		% L1..U1 <: A /\ B if L1..U1 <: A & L1..U1 <: B
1488		(check_subset_interval(A,L1,U1,Hyps,PTA) -> check_subset_interval(B,L1,U1,Hyps,PTB)).
1489		check_subset_interval(interval(L2,U2),L1,U1,Hyps,interval) :-
1490		!,check_sub_intervals(L1,U1,L2,U2,Hyps).
1491		check_subset_interval('NATURAL',L1,_,Hyps,nat) :- !, check_leq(0,L1,Hyps).
1492		check_subset_interval('NATURAL1',L1,_,Hyps,nat1) :- !, check_leq(1,L1,Hyps).
1493		check_subset_interval(value(avl_set(A)),L1,U1,Hyps,avl(PT)) :- !,
1494		(number(L1), number(U1)
1495		-> PT=in(L1,U1),
1496		check_interval_in_custom_set(L1,U1,avl_set(A),no_wf_available)
1497		; avl_min(A,int(L2)), avl_max(A,int(U2)), PT=min_max(L2,U2,PT2),
1498		check_subset_interval(interval(L2,U2),L1,U1,Hyps,PT2)
1499		).
1500		check_subset_interval(A,L1,U1,Hyps,rewrite(PT)) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
1501		check_subset_interval(A2,L1,U1,Hyps2,PT).
1502		check_subset_interval(domain(Expr),Low,Up,Hyps,dom_seq1) :- % a special rule when using SEQ(1) rather than first(SEQ)
1503		(check_leq(1,Low,Hyps), check_leq(Up,size(Expr),Hyps) % 1..size(s) <: dom(s)
1504		-> check_is_sequence(Expr,Hyps)
1505		; index_in_non_empty_sequence(Low,Expr,Hyps),
1506		index_in_non_empty_sequence(Up,Expr,Hyps) % 1..1 or size(s)..size(s) <: dom(s) if s:seq1(.)
1507		-> check_is_non_empty_sequence(Expr,Hyps)
1508		).
1509		check_subset_interval(range(reverse(Expr)),Low,Up,Hyps,PT) :- !,
1510		check_subset_interval(domain(Expr),Low,Up,Hyps,PT).
1511		check_subset_interval(A,Low,Up,Hyps,eq(PT)) :-
1512		avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2),
1513		rewrite_local_loop_check(A,check_subset_interval,A2,Hyps2,Hyps3),
1514		check_subset_interval(A2,Low,Up,Hyps3,PT).
1515		%check_subset_interval(A,L1,U1,_,_) :- print(check_subset_interval_failed(A,L1,U1)),nl,fail.
1516
1517		% s:seq1(.) => 1:dom(s) & size(s):dom(s)
1518		index_in_non_empty_sequence(1,_,_).
1519		index_in_non_empty_sequence(card(E),E,_).
1520		index_in_non_empty_sequence(size(E),E,_).
1521		index_in_non_empty_sequence('$'(X),E,Hyps) :-
1522		avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
1523		rewrite_local_loop_check(X,index_in_non_empty_sequence,Y,Hyps2,Hyps3),
1524		index_in_non_empty_sequence(Y,E,Hyps3).
1525		index_in_non_empty_sequence(X,E,Hyps) :- \+ useful_value(X), % do not rewrite 10 to interval(10,10)
1526		try_get_set_of_possible_values(X,Hyps,XSet,Hyps2),
1527		rewrite_local_loop_check(X,index_in_non_empty_sequence,XSet,Hyps2,Hyps3),
1528		all_in_non_empty_sequence(XSet,E,Hyps3).
1529
1530		all_in_non_empty_sequence(interval(A,B),E,Hyps) :-
1531		index_in_non_empty_sequence(A,E,Hyps),
1532		index_in_non_empty_sequence(B,E,Hyps).
1533		% TODO: avl_set, ...
1534
1535		% check if L1..U1 <: L2..U2
1536		check_sub_intervals(L1,L1,L2,U2,Hyps) :- (L1=L2 ; L1=U2),!,
1537		check_not_empty_set(interval(L2,U2),Hyps).
1538		check_sub_intervals(L1,U1,L2,U2,Hyps) :- % L1..U1 <: L2..U2 if L2 <= L1 & U1 <= U2
1539		check_leq(L2,L1,Hyps),!,
1540		check_leq(U1,U2,Hyps).
1541
1542
1543
1544		% some exact rewrite steps
1545		rewrite_set_expression_exact(domain(A),Hyps,Res,Hyps2) :- compute_exact_domain(A,Hyps,Dom,Hyps2),!,
1546		%print(rewrote(domain(A))),nl, print(Dom),nl,
1547		(A='$'(ID) -> not_occurs(Dom,ID) ; true), % prevent silly rewrites
1548		Res=Dom.
1549		rewrite_set_expression_exact(range(A),Hyps,Res,Hyps2) :- compute_exact_range(A,Hyps,Ran,Hyps2),!,
1550		%print(rewrote(range(A))),nl, print(Ran),nl,
1551		(A='$'(ID) -> not_occurs(Ran,ID) ; true), % prevent silly rewrites
1552		Res=Ran.
1553		rewrite_set_expression_exact(intersection(A,B),Hyps,Res,Hyps) :-
1554		(is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=empty_set).
1555		rewrite_set_expression_exact(set_subtraction(A,B),Hyps,Res,Hyps) :-
1556		(is_empty_set_direct(A) -> Res=empty_set ; is_empty_set_direct(B) -> Res=A).
1557		rewrite_set_expression_exact(union(A,B),Hyps,Res,Hyps1) :-
1558		(check_equal(A,B,Hyps,Hyps1) -> Res=A
1559		; Hyps1=Hyps, merge_set_extensions(union(A,B),List,[]),
1560		construct_set_extension(List,Hyps,Res)).
1561		rewrite_set_expression_exact(value(closure(P,T,B)),Hyps,Res,Hyps) :- nonvar(P),
1562		is_interval_closure(P,T,B,LOW,UP), number(LOW),number(UP),!,
1563		Res = interval(LOW,UP).
1564		rewrite_set_expression_exact(assertion_expression(_,_,Expr),Hyps,Res,Hyps2) :- % TO DO: add Predicate to Hyps ?
1565		(rewrite_set_expression_exact(Expr,Hyps,Expr2,Hyps2) -> Res=Expr2
1566		; Res=Expr, Hyps2=Hyps).
1567		% Note one can have equalities like f = f~~ (in FunLawsWithLambda.mch); hence important to pass Hyps for cycle detection
1568
1569
1570		merge_set_extensions(empty_set) --> [].
1571		merge_set_extensions(empty_sequence) --> [].
1572		merge_set_extensions(set_extension(L)) --> L.
1573		merge_set_extensions(sorted_set_extension(L)) --> L.
1574		merge_set_extensions(union(A,B)) --> merge_set_extensions(A), merge_set_extensions(B).
1575
1576		% check if AVL is a subset of the first argument
1577		check_subset_avl(union(A,B),AVL1,Hyps) :- !, % TO DO: try and merge A,B
1578		(check_subset_avl(A,AVL1,Hyps) -> true ; check_subset_avl(B,AVL1,Hyps)).
1579		check_subset_avl(intersection(A,B),AVL1,Hyps) :- !, % AVL <: A /\ B if AVL <: A & AVL <: B
1580		(check_subset_avl(A,AVL1,Hyps) -> check_subset_avl(B,AVL1,Hyps)).
1581		check_subset_avl(interval(L2,U2),AVL,_) :- number(L2),number(U2),!,
1582		check_avl_in_interval(AVL,L2,U2).
1583		check_subset_avl(value(avl_set(AVL2)),AVL1,_) :- !, check_avl_subset(AVL1,AVL2).
1584		check_subset_avl(seq(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq).
1585		check_subset_avl(seq1(MAX),AVL,Hyps) :- maximal_set(MAX,Hyps), !, is_avl_set_of_sequences(AVL,seq1).
1586		check_subset_avl(seq(seq(MAX)),AVL,Hyps) :- maximal_set(MAX,Hyps),
1587		% comes from general concat
1588		custom_explicit_sets:is_one_element_avl(AVL,Element), % usually one value from try_get_set_of_possible_values
1589		is_sequence(Element,seq),
1590		expand_custom_set_to_list(Element,ListOfSeqs),
1591		maplist(is_subsequence,ListOfSeqs).
1592		check_subset_avl(A,AVL,Hyps) :- rewrite_set_expression_exact(A,Hyps,A2,Hyps2),!,
1593		check_subset_avl(A2,AVL,Hyps2).
1594		check_subset_avl(A,AVL,Hyps) :-
1595		avl_fetch_worthwhile_equal_from_hyps(A,Hyps,A2,Hyps2),
1596		rewrite_local_loop_check(A,check_subset_avl,A2,Hyps2,Hyps3),
1597		check_subset_avl(A2,AVL,Hyps3).
1598		%check_subset_avl(A,AVL,_) :- print(check_subset_avl_failed(A,AVL)),nl,fail.
1599
1600		is_subsequence((int(_Index),Sequence)) :- is_sequence(Sequence,seq).
1601
1602		is_sequence(avl_set(SeqAVL),_) :- safe_is_avl_sequence(SeqAVL).
1603		is_sequence([],seq).
1604
1605		% check if all elements of the AVL are sequences
1606		is_avl_set_of_sequences(AVL,SeqType) :- avl_height(AVL,Height), Height<7,
1607		expand_custom_set_to_list(avl_set(AVL),ListOfSeqs),
1608		l_is_sequence(ListOfSeqs,SeqType).
1609		l_is_sequence([],_).
1610		l_is_sequence([S1|T],SeqType) :- is_sequence(S1,SeqType), l_is_sequence(T,SeqType).
1611
1612
1613		:- use_module(probsrc(b_global_sets),[b_global_set/1]).
1614		maximal_set('INTEGER',_). % integer_set('INTEGER') ?
1615		maximal_set(real_set,_).
1616		maximal_set(string_set,_).
1617		maximal_set(bool_set,_).
1618		maximal_set('typeset',_).
1619		maximal_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_TYPE
1620		maximal_set(A,Hyps), maximal_set(B,Hyps).
1621		maximal_set(relations(A,B),Hyps) :- % SIMP_TYPE_EQUAL_REL
1622		maximal_set(A,Hyps), maximal_set(B,Hyps).
1623		maximal_set(set_subtraction(A,B),Hyps) :- % SIMP_SETMINUS_EQUAL_TYPE
1624		maximal_set(A,Hyps), check_equal_empty_set(B,Hyps,_).
1625		maximal_set(pow_subset(A),Hyps) :- maximal_set(A,Hyps).
1626		maximal_set('$'(ID),Hyps) :- is_global_set_id(ID,Hyps).
1627		maximal_set(value(avl_set(AVL)),_) :-
1628		quick_definitely_maximal_set_avl(AVL).
1629		maximal_set(set_extension(A),Hyps) :- maximal_set_extension(A,Hyps).
1630		% sorted_set_extension is never maximal
1631		maximal_set(comprehension_set(_,truth),_).
1632		%maximal_set(X,_) :- print(max_fail(X)),nl,fail.
1633
1634		construct_set_extension([],_,Res) :- !, Res=empty_set.
1635		construct_set_extension(L,Hyps,Res) :- maximal_set_extension(L,Hyps),!, Res='typeset'.
1636		construct_set_extension(L,_,sorted_set_extension(SL)) :-
1637		%length(L,Len), format('Construct set_extension ~w~n',[Len]),
1638		sort(L,SL).
1639
1640		maximal_set_extension([boolean_true|T],_) :- !, member(boolean_false,T).
1641		maximal_set_extension([boolean_false|T],_) :- !, member(boolean_true,T).
1642		maximal_set_extension(['$'(ID)|T],Hyps) :-
1643		is_global_constant_id(ID,Hyps),
1644		sort(['$'(ID)|T],Sorted),
1645		maplist(is_glob_const_id(Hyps),Sorted), % all elements are global constants
1646		lookup_global_constant(ID,fd(_,GlobalSet)),
1647		enumerated_set(GlobalSet),b_global_set_cardinality(GlobalSet,Size),
1648		length(Sorted,Size).
1649		%maximal_set_extension(X,_) :- print(maximal_failed(X)),nl,fail.
1650
1651		is_glob_const_id(Hyps,'$'(ID)) :- is_global_constant_id(ID,Hyps).
1652
1653
1654		is_global_set_id(ID,Hyps) :-
1655		b_global_set(ID),
1656		\+ is_hyp_var(ID,Hyps). % global enumerated set visible
1657
1658		% often called with 0 or 1 in first position
1659		check_leq(I,I,_) :- !.
1660		check_leq(if_then_else(_,A1,A2),B,Hyp) :- !, % TODO?: treat if-then-else for B
1661		(check_leq(A1,B,Hyp) -> check_leq(A2,B,Hyp)).
1662		check_leq(N1,N2,_) :- number(N1), number(N2), !, N1 =< N2.
1663		check_leq(N1,N2,hyp_rec(AVL,_)) :-
1664		(avl_fetch(less_equal(N1,N2),AVL)
1665		-> true
1666		; avl_fetch(equal(N1,N2),AVL)),!.
1667		check_leq(min(List),N2,Hyps) :- !,
1668		member(N1,List), check_leq(N1,N2,Hyps),!.
1669		check_leq(min_int,N2,Hyps) :- !, % we could look up the value of MININT; but largest possible value is -1
1670		MININT is -1,
1671		check_leq(MININT,N2,Hyps).
1672		check_leq(N1,max_int,Hyps) :- !, % we could look up the value of MAXINT; but smallest possible value is 1
1673		MAXINT = 1,
1674		check_leq(N1,MAXINT,Hyps).
1675		check_leq(N1,N2,Hyps) :-
1676		rewrite_integer(N2,Hyps,RN2,Hyps2),!,
1677		check_leq(N1,RN2,Hyps2).
1678		check_leq(add(N1,1),N2,Hyps) :-
1679		check_not_equal(N1,N2,Hyps),
1680		!, % N1+1 <= N2 if N1 <= N2 & N1 \= N2 ; happens quite often in array traversals
1681		check_leq(N1,N2,Hyps).
1682		check_leq(N1,minus(N2,1),Hyps) :- % variation of rule above
1683		check_not_equal(N1,N2,Hyps),
1684		!, % N1 <= N2-1 if N1 <= N2 & N1 \= N2 ; happens in array traversals
1685		check_leq(N1,N2,Hyps).
1686		check_leq(Nr,X,Hyps) :-
1687		\+ number(X),
1688		try_get_set_of_possible_values(X,Hyps,SetX,Hyps2),
1689		check_all_values_geq_val(SetX,Nr,Hyps2),!.
1690		check_leq(Nr,X,Hyps) :- number(Nr), !,
1691		check_leq_nr(Nr,X,Hyps).
1692		check_leq(N1,N2,Hyps) :- rewrite_integer(N1,Hyps,RN1,Hyps2),!,
1693		check_leq(RN1,N2,Hyps2).
1694		check_leq(Add,N2,Hyps) :- % A+N1 <= N2 <=> A <= N2-N1
1695		number(N2),
1696		add_with_number(Add,A,N1),!,
1697		N21 is N2-N1,
1698		check_leq(A,N21,Hyps).
1699		check_leq(Mul,N2,Hyps) :- % A*N1 <= N2 if A <= N2/N1 if N1>0 and N2 mod N1=0
1700		number(N2),
1701		mul_with_number(Mul,A,N1),
1702		% symmetrical case to check_leq_nr(N1,Mul,Hyps), with N1=-N2
1703		!,
1704		( N1=0 -> check_leq(0,N2,Hyps)
1705		; N1>0 -> N21 is N2 div N1, % A <= 1.5 means we have to have A <= 1;
1706		% A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2
1707		check_leq(A,N21,Hyps)
1708		; cdiv(N2,N1,N21), % A >= 1.5 means we have to have A >= 2 ; cdiv
1709		check_leq(N21,A,Hyps)
1710		).
1711		check_leq(div(A,N1),N2,Hyps) :- % A/N1 <= N2 <=> A <= (N1+1)*N2-1
1712		number(N1),number(N2), N1>0,
1713		!,
1714		N12 is (N2+1)*N1-1,
1715		check_leq(A,N12,Hyps).
1716		check_leq(div(A1,N1),A2,Hyps) :- number(N1), N1>0, % A/N1 <= A if N1>0 & A>=0
1717		check_equal(A1,A2,Hyps,Hyps1),!,
1718		check_leq(0,A1,Hyps1).
1719		check_leq(modulo(A1,A2),B,Hyps) :-
1720		\+ z_or_tla_minor_mode, % args to mod must be non-negative, modulo is between 0..A2-1
1721		((number(A2),A21 is A2-1 -> check_leq(A21,B,Hyps)
1722		; B=minus(B1,1) -> check_leq(A2,B1,Hyps)
1723		; check_leq(A2,B,Hyps)
1724		) -> true
1725		; check_leq(A1,B,Hyps)).
1726		% TO DO: modulo as RHS
1727		check_leq(unary_minus(A),unary_minus(B),Hyps) :- !, % -A <= -B ---> A >= B
1728		check_leq(B,A,Hyps).
1729		check_leq(X,Nr,Hyps) :- \+ number(X),
1730		try_get_set_of_possible_values(X,Hyps,SetX,Hyps2),
1731		check_all_values_leq_val(SetX,Nr,Hyps2),!. % cut here; get set of possible values can give multiple solutions
1732		check_leq(Minus,N2,Hyps) :- minus_with_number(Minus,N1,Nr),
1733		Nr >= 0,!, % N1-Nr <= N2 if N1 <= N2
1734		% Both N1 and N2 are usually not numbers here
1735		check_leq(N1,N2,Hyps).
1736		check_leq(N1,Add,Hyps) :-
1737		add_with_number(Add,N2,Nr),Nr >= 0,!, % N1 <= N2+Nr if N1 <= N2
1738		% Both N1 and N2 are usually not numbers here
1739		check_leq(N1,N2,Hyps).
1740		check_leq(add(A,B),E,Hyps) :- decompose_floor(E,X,Y), % e.g. divide a number E by 2
1741		check_leq(A,X,Hyps), % TO DO: other combinations like A <= 0, B <= Nr; or we could try_get_set_of_possible_values
1742		check_leq(B,Y,Hyps).
1743		check_leq('$'(X),N2,Hyps) :-
1744		avl_fetch_binop_from_hyps('$'(X),less_equal,Hyps,Y,Hyps2),
1745		(number(N2),avl_fetch_not_equal('$'(X),Y,Hyps) % as we know X and Y we can use regular avl_fetch
1746		-> N21 is N2+1 % we have X<Y in the Hypotheses, we just require that Y <= N2+1
1747		; N21=N2),
1748		check_leq(Y,N21,Hyps2).
1749		check_leq(Nr,'$'(X),Hyps) :-
1750		( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
1751		rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3),
1752		check_leq(Nr,Y,Hyps3) -> true
1753		% ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true
1754		; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2),
1755		% note: Nr is not a number, hence probably not useful to check not_equal in Hyps, as we cannot compute Nr-1
1756		check_leq(Nr,Y,Hyps2)
1757		-> true
1758		),
1759		!.
1760		%check_leq(A,B,_H) :- print(check_leq_failed(A,B)),nl, portray_hyps(_H),nl,fail.
1761
1762		% decompose an expression E into A and B so that A+B <= E
1763		decompose_floor(Nr,A,B) :- number(Nr),!,
1764		A is Nr div 2, B=A. % -11 div 2 -> -6, -1 div 2 = -1, 11 div 2 = 5
1765		decompose_floor(add(A,B),A,B). % TO DO: we could try other order
1766		decompose_floor(Mul,A,A) :- mul_with_number(Mul,A,Nr), Nr>=2. % we could divide Nr by 2
1767
1768		% ceiling division utility
1769		cdiv(N1,N2,Res) :-
1770		(N1 mod N2 =:= 0 -> Res is N1//N2
1771		; Res is (N1 div N2)+1).
1772
1773		% Number <= Expression
1774		check_leq_nr(N1,Add,Hyps) :- % N1 <= A+N2 <=> N1-N2 <= A
1775		add_with_number(Add,A,N2), !,
1776		N12 is N1-N2,
1777		check_leq(N12,A,Hyps).
1778		check_leq_nr(Nr,add(N1,N2),Hyps) :- !, % 0 <= A+B if 0 <= A & 0 <= B
1779		% Both N1 and N2 are usually not numbers here
1780		cdiv(Nr,2,Nr2), % Note: cdiv(-3,2) = 1, cdiv(3,2)=2
1781		check_leq(Nr2,N1,Hyps),
1782		check_leq(Nr2,N2,Hyps).
1783		check_leq_nr(N1,minus(N2,B),Hyps) :- % N1 <= N2-B <=> B <= N2-N1
1784		number(N2), !,
1785		N21 is N2-N1,
1786		check_leq(B,N21,Hyps).
1787		check_leq_nr(N1,Mul,Hyps) :- % N1 <= A*N2 if N1/N2 <= A and N2>0
1788		mul_with_number(Mul,A,N2),
1789		!,
1790		( N2=0 -> check_leq(N1,0,Hyps)
1791		; N2>0 -> cdiv(N1,N2,N12), % cdiv
1792		% if 1.5 <= A --> 2 <= A ; if -1.5 <= A --> -1 <= A
1793		check_leq(N12,A,Hyps)
1794		; N12 is N1 div N2,
1795		% if A <= 1.5 --> A <= 1 ; if -1.5 <= A --> -1 <= A
1796		% A <= -1.5 means we have to have A <= -2 -3 div 2 =:= -2
1797		check_leq(A,N12,Hyps)
1798		).
1799		check_leq_nr(0,multiplication(A,B),Hyps) :- !, % 0 <= A*B if A and B have same parity
1800		(check_leq(0,A,Hyps) -> check_leq(0,B,Hyps)
1801		; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)).
1802		check_leq_nr(N1,div(A,N2),Hyps) :- % N1 <= A/N2 <=> N1*N2 <= A
1803		number(N2), N2>0,
1804		!,
1805		N12 is N1*N2,
1806		check_leq(N12,A,Hyps).
1807		check_leq_nr(0,div(A,B),Hyps) :- !, % 0 <= A/B if A and B have same parity
1808		(check_leq(0,A,Hyps) -> check_leq(0,B,Hyps) % B \= 0 checked by other WD condition
1809		; check_leq(A,0,Hyps) -> check_leq(B,0,Hyps)). % ditto
1810		check_leq_nr(Nr,'$'(X),Hyps) :-
1811		( avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
1812		rewrite_local_loop_check(X,check_leq,Y,Hyps2,Hyps3),
1813		check_leq(Nr,Y,Hyps3) -> true
1814		% ; avl_fetch_binop_from_hyps('$'(X),greater,Hyps,Y,Hyps2), N1 is Nr-1, check_leq(N1,Y,Hyps2) -> true
1815		; avl_fetch_binop_from_hyps('$'(X),greater_equal,Hyps,Y,Hyps2),
1816		(avl_fetch_not_equal('$'(X),Y,Hyps2) % we have X < Y => sufficient to prove N-1 <= Y
1817		-> N1 is Nr-1, check_leq(N1,Y,Hyps2)
1818		; check_leq(Nr,Y,Hyps2)
1819		)
1820		),
1821		!.
1822		check_leq_nr(Nr,modulo(A,B),Hyps) :- \+ z_or_tla_minor_mode, % A and B must be non-negative, modulo is between 0..B-1
1823		(Nr =< 0 -> true % modulo always positive or 0
1824		; % Nr <= A mod B if Nr <= A and A < B
1825		check_leq_nr(Nr,A,Hyps), % Nr <= A
1826		check_less(A,B,Hyps)). % and A < B so that modulo does not take effect
1827		check_leq_nr(Nr,size(Seq),Hyps) :- check_leq_nr_size(Nr,Seq,Hyps).
1828		check_leq_nr(1,power_of(A,_),Hyps) :- check_leq(1,A,Hyps). % Nr <= 1 <= x**y if x >= 1
1829		check_leq_nr(Nr,power_of(A,_),Hyps) :- number(Nr), Nr =< 0,
1830		check_leq(0,A,Hyps). % 0 <= x**y if x >= 0
1831		%check_leq_nr(A,B,_H) :- print(check_leq_nr_failed(A,B)),nl,fail.
1832
1833		check_less(A,B,Hyps) :-
1834		check_leq(A,B,Hyps),!,
1835		check_not_equal(A,B,Hyps).
1836
1837		:- use_module(probsrc(specfile),[z_or_tla_minor_mode/0]).
1838
1839
1840		check_leq_nr_size(Nr,restrict_front(_,RestrN),Hyps) :- !, % X <= size( Seq /|\ N) if X <= N as WD condition implies N : 0..size(Seq)
1841		check_leq_nr(Nr,RestrN,Hyps).
1842		check_leq_nr_size(1,Seq,Hyps) :- check_is_non_empty_sequence(Seq,Hyps).
1843
1844		add_with_number(add(A,B),X,Nr) :- (number(A) -> Nr=A, X=B ; number(B) -> Nr=B, X=A).
1845		add_with_number(minus(A,B),A,Nr) :- number(B), Nr is -B.
1846		mul_with_number(multiplication(A,B),X,Nr) :- (number(A) -> Nr=A, X=B ; number(B) -> Nr=B, X=A).
1847		mul_with_number(unary_minus(A),A,Nr) :- Nr is -1.
1848		minus_with_number(add(A,B),A,Nr) :- number(B), Nr is -B.
1849		minus_with_number(minus(A,Nr),A,Nr) :- number(Nr).
1850
1851		%get_possible_values('$'(X),Hyps,SetX,Hyps2) :-
1852		% avl_fetch_binop_from_hyps('$'(X),member,Hyps,SetX,Hyps2).
1853
1854		% a few rewrite rules for integer expressions
1855		% addition/multiplication is dealt with in other places (and is usually done symbolically)
1856		rewrite_integer(size(Seq),Hyps,Size,Hyps2) :- % can happen for sequence POs, like restrict_front,tail
1857		compute_card_of_set(Seq,Hyps,Size,Hyps2),!.
1858		rewrite_integer(card(Seq),Hyps,Size,Hyps2) :- !, rewrite_card_of_set(Seq,Hyps,Size,Hyps2).
1859		rewrite_integer(assertion_expression(_,_,Expr),Hyps,Expr,Hyps). % TO DO: add Predicate to Hyps?
1860		% the following may be done by ast_cleanup, but e.g., when applying functions no cleanup is run in l_rename_and_prove_goals
1861		rewrite_integer(add(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
1862		compute_integer(B,Hyps1,B1,Hyps2), number(B1),
1863		Res is A1+B1.
1864		rewrite_integer(unary_minus(A),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps2), number(A1),
1865		Res is -A1.
1866		rewrite_integer(minus(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
1867		compute_integer(B,Hyps1,B1,Hyps2), number(B1),
1868		Res is A1-B1.
1869		rewrite_integer(power_of(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
1870		compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >=0,
1871		% check if not too large:
1872		(abs(A1) < 2 -> true
1873		; A1=2 -> B1 =< 64
1874		; A1 < 4294967296 -> B1 =< 2
1875		; B1 =< 0
1876		),
1877		Res is A1 ^ B1.
1878		rewrite_integer(modulo(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1),number(A1),
1879		A1 >= 0,
1880		compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 >0,
1881		Res is A1 mod B1.
1882		rewrite_integer(division(A,B),Hyps,Res,Hyps2) :- compute_integer(A,Hyps,A1,Hyps1), number(A1),
1883		compute_integer(B,Hyps1,B1,Hyps2), number(B1), B1 \= 0,
1884		Res is A1 // B1. % Prolog division corresponds to B division
1885		rewrite_integer(integer(X),Hyps,X,Hyps) :- integer(X), write(wd_unnormalised_integer(X)),nl. % should not happen
1886		rewrite_integer(real(X),Hyps,Res,Hyps) :- atom(X), construct_real(X,term(floating(Res))).
1887		rewrite_integer(convert_int_floor(RX),Hyps,X,Hyps1) :-
1888		compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is floor(RX1). %, print(rewr_floor(RX,X)),nl.
1889		rewrite_integer(convert_int_ceiling(RX),Hyps,X,Hyps1) :-
1890		compute_integer(RX,Hyps,RX1,Hyps1), number(RX1), X is ceiling(RX1).
1891		rewrite_integer(convert_real(A),Hyps,RX,Hyps1) :-
1892		compute_integer(A,Hyps,A1,Hyps1), integer(A1), RX is float(A1).
1893
1894		rewrite_card_of_set(Set,Hyps,Size,Hyps2) :-
1895		compute_card_of_set(Set,Hyps,Size,Hyps2),!.
1896		rewrite_card_of_set(interval(1,Up),Hyps,Size,Hyps) :- !, % useful if Up is a symbolic expression
1897		Size=Up.
1898		rewrite_card_of_set(Set,Hyps,Size,Hyps2) :- rewrite_set_expression_exact(Set,Hyps,S2,Hyps1),
1899		rewrite_card_of_set(S2,Hyps1,Size,Hyps2).
1900
1901		compute_integer(A,H,A,H) :- number(A),!.
1902		compute_integer(A,H,Res,H2) :- rewrite_integer(A,H,Res,H2).
1903
1904		:- use_module(probsrc(b_global_sets), [enumerated_set/1, b_global_set_cardinality/2]).
1905		compute_card_of_set(empty_set,Hyps,0,Hyps).
1906		compute_card_of_set(empty_sequence,Hyps,0,Hyps).
1907		compute_card_of_set(bool_set,Hyps,2,Hyps).
1908		compute_card_of_set(interval(L,U),Hyps,Size,Hyps) :- number(L), number(U), Size is U+1-L.
1909		compute_card_of_set(value(Val),Hyps,Size,Hyps) :- get_set_val_size(Val,Size).
1910		compute_card_of_set(sequence_extension(List),Hyps,Size,Hyps) :- length(List,Size).
1911		compute_card_of_set(set_extension([_]),Hyps,Size,Hyps) :- Size=1. % to do check if all elements definitely different
1912		compute_card_of_set(sorted_set_extension([_]),Hyps,Size,Hyps) :- Size=1. % ditto
1913		compute_card_of_set(rev(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(A,Hyps,Size,Hyps2).
1914		compute_card_of_set(front(A),Hyps,Size,Hyps2) :- !, compute_card_of_set(tail(A),Hyps,Size,Hyps2).
1915		compute_card_of_set(tail(A),Hyps,Size,Hyps2) :- !,
1916		compute_card_of_set(A,Hyps,Size1,Hyps2), number(Size1), Size1>0,
1917		Size is Size1-1.
1918		compute_card_of_set(concat(A,B),Hyps,Size,Hyps2) :-
1919		compute_card_of_set(A,Hyps,SA,Hyps1),!,
1920		compute_card_of_set(B,Hyps1,SB,Hyps2),
1921		Size is SA+SB.
1922		compute_card_of_set('$'(ID),Hyps,Size,Hyps) :- is_enumerated_set(ID,Hyps),
1923		!,
1924		b_global_set_cardinality(ID,Size).
1925		compute_card_of_set('$'(ID),Hyps,Size,Hyps2) :-
1926		avl_fetch_equal_from_hyps('$'(ID),Hyps,X2,Hyps1),
1927		compute_card_of_set(X2,Hyps1,Size,Hyps2),!.
1928		compute_card_of_set('$'(ID),Hyps,Size,Hyps4) :- % e.g., f:1..10 --> BOOL --> card(f) = 10
1929		avl_fetch_binop_from_hyps('$'(ID),member,Hyps,FunctionType,Hyps1),
1930		is_partial_function_type(FunctionType,Hyps1,Hyps2),
1931		get_exact_domain_of_func_or_rel_type(FunctionType,Hyps2,Dom,Hyps3),
1932		compute_card_of_set(Dom,Hyps3,Size,Hyps4).
1933		%compute_card_of_set(S,_,_,_) :- print(card_fail(S)),nl,fail.
1934
1935		get_set_val_size([],0).
1936		get_set_val_size(avl_set(AVL),Size) :- avl_size(AVL,Size).
1937
1938
1939		check_all_values_geq_val(intersection(A,B),Nr,Hyps) :-
1940		(check_all_values_geq_val(A,Nr,Hyps) -> true ; check_all_values_geq_val(B,Nr,Hyps)).
1941		check_all_values_geq_val(union(A,B),Nr,Hyps) :-
1942		(check_all_values_geq_val(A,Nr,Hyps) -> check_all_values_geq_val(B,Nr,Hyps)).
1943		check_all_values_geq_val(set_subtraction(A,_),Nr,Hyps) :-
1944		check_all_values_geq_val(A,Nr,Hyps).
1945		check_all_values_geq_val(interval(From,_),Nr,Hyps) :- check_leq(Nr,From,Hyps).
1946		check_all_values_geq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_min(AVL,int(Min)), check_leq(Nr,Min,Hyps).
1947		check_all_values_geq_val('NATURAL',Nr,Hyps) :- check_leq(Nr,0,Hyps).
1948		check_all_values_geq_val('NATURAL1',Nr,Hyps) :- check_leq(Nr,1,Hyps).
1949		check_all_values_geq_val(domain(Func),Nr,Hyps) :-
1950		get_domain_or_superset(Func,Hyps,DomFunc,Hyps2),
1951		check_all_values_geq_val(DomFunc,Nr,Hyps2).
1952		check_all_values_geq_val(range(Func),Nr,Hyps) :-
1953		get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
1954		check_all_values_geq_val(RanFunc,Nr,Hyps2).
1955		check_all_values_geq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_geq_val(set_extension(L),Nr,Hyps).
1956		check_all_values_geq_val(set_extension(L),Nr,Hyps) :-
1957		(member(Val,L), \+ check_leq(Nr,Val,Hyps) -> fail ; true).
1958		check_all_values_geq_val('$'(X),Nr,Hyps) :-
1959		avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
1960		rewrite_local_loop_check(X,check_all_values_geq_val,Y,Hyps2,Hyps3),
1961		check_all_values_geq_val(Y,Nr,Hyps3).
1962		%check_all_values_geq_val(A,B,_) :- print(check_all_values_geq_val_failed(A,B)),nl,fail.
1963
1964		check_all_values_neq_nr(intersection(A,B),Nr,Hyps) :-
1965		(check_all_values_neq_nr(A,Nr,Hyps) -> true ; check_all_values_neq_nr(B,Nr,Hyps)).
1966		check_all_values_neq_nr(union(A,B),Nr,Hyps) :-
1967		(check_all_values_neq_nr(A,Nr,Hyps) -> check_all_values_neq_nr(B,Nr,Hyps)).
1968		check_all_values_neq_nr(set_subtraction(A,_),Nr,Hyps) :-
1969		check_all_values_neq_nr(A,Nr,Hyps).
1970		check_all_values_neq_nr(interval(From,_),Nr,Hyps) :- number(From),F1 is From-1, check_leq(Nr,F1,Hyps).
1971		check_all_values_neq_nr(interval(_,To),Nr,Hyps) :- number(To),T1 is To+1, check_leq(T1,Nr,Hyps).
1972		check_all_values_neq_nr('NATURAL',Nr,Hyps) :- check_leq(Nr,-1,Hyps).
1973		check_all_values_neq_nr('NATURAL1',Nr,Hyps) :- check_leq(Nr,0,Hyps).
1974		check_all_values_neq_nr(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_neq_nr(set_extension(L),Nr,Hyps).
1975		check_all_values_neq_nr(set_extension(L),Nr,Hyps) :-
1976		(member(Val,L), \+ check_not_equal(Val,Nr,Hyps) -> fail ; true).
1977		check_all_values_neq_nr('$'(X),Nr,Hyps) :-
1978		avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
1979		rewrite_local_loop_check(X,check_all_values_neq_nr,Y,Hyps2,Hyps3),
1980		check_all_values_neq_nr(Y,Nr,Hyps3).
1981		%check_all_values_neq_nr(A,B,_) :- print(check_all_values_neq_nr_failed(A,B)),nl,fail.
1982
1983
1984		check_all_values_leq_val(intersection(A,B),Nr,Hyps) :-
1985		(check_all_values_leq_val(A,Nr,Hyps) -> true ; check_all_values_leq_val(B,Nr,Hyps)).
1986		check_all_values_leq_val(union(A,B),Nr,Hyps) :-
1987		(check_all_values_leq_val(A,Nr,Hyps) -> check_all_values_leq_val(B,Nr,Hyps)).
1988		check_all_values_leq_val(set_subtraction(A,_),Nr,Hyps) :-
1989		check_all_values_leq_val(A,Nr,Hyps).
1990		check_all_values_leq_val(interval(_,To),Nr,Hyps) :- check_leq(To,Nr,Hyps).
1991		check_all_values_leq_val(value(avl_set(AVL)),Nr,Hyps) :- avl_max(AVL,int(Max)), check_leq(Max,Nr,Hyps).
1992		check_all_values_leq_val(domain(Func),Nr,Hyps) :-
1993		get_domain_or_superset(Func,Hyps,DomFunc,Hyps2),
1994		check_all_values_leq_val(DomFunc,Nr,Hyps2).
1995		check_all_values_leq_val(range(Func),Nr,Hyps) :-
1996		get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
1997		check_all_values_leq_val(RanFunc,Nr,Hyps2).
1998		check_all_values_leq_val(sorted_set_extension(L),Nr,Hyps) :- !, check_all_values_leq_val(set_extension(L),Nr,Hyps).
1999		check_all_values_leq_val(set_extension(L),Nr,Hyps) :-
2000		(member(Val,L), \+ check_leq(Val,Nr,Hyps) -> fail ; true).
2001		check_all_values_leq_val('$'(X),Nr,Hyps) :-
2002		avl_fetch_equal_from_hyps('$'(X),Hyps,Y,Hyps2),
2003		rewrite_local_loop_check(X,check_all_values_leq_val,Y,Hyps2,Hyps3),
2004		check_all_values_leq_val(Y,Nr,Hyps3).
2005		%check_all_values_leq_val(A,B,_) :- print(check_all_values_leq_val(A,B)),nl,fail.
2006
2007		% check if two expressions are definitely different
2008		% usually called for check_not_equal 0 or empty_set
2009		check_not_equal(A,B,Hyp) :-
2010		is_explicit_value(A,AV,Hyp), is_explicit_value(B,BV,Hyp), !, AV \= BV.
2011		check_not_equal(X,Y,Hyp) :- sym_unify(X,Y,if_then_else(_,A1,A2),B),!,
2012		(check_not_equal(A1,B,Hyp) -> check_not_equal(A2,B,Hyp)).
2013		check_not_equal(N1,N2,Hyps) :-
2014		avl_fetch_not_equal(N1,N2,Hyps),!.
2015		check_not_equal(couple(A1,A2),couple(B1,B2),Hyps) :- !,
2016		(check_not_equal(A1,B1,Hyps) -> true ; check_not_equal(A2,B2,Hyps)).
2017		check_not_equal(X,B,Hyps) :- number(B),
2018		try_get_set_of_possible_values(X,Hyps,SetX,Hyps2),
2019		check_all_values_neq_nr(SetX,B,Hyps2),!.
2020		% TO DO: compute also things like domain(...) for :wd s:perm(1..10) & x:dom(s) & res = 10/x
2021		check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,unary_minus(A),B),number(B),!, BM is -B,
2022		check_not_equal(A,BM,Hyps).
2023		check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,multiplication(A,B),0),!, % A*B /= 0 if A/=0 & B/=0
2024		check_not_equal(A,0,Hyps),check_not_equal(B,0,Hyps).
2025		check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,power_of(A,_),0),!, % A**B /= 0 if A/=0
2026		check_not_equal(A,0,Hyps).
2027		check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,Add,B),
2028		add_with_number(Add,A,Nr),!,
2029		(Nr>0 -> check_leq(B,A,Hyps) % A >= B => A+Nr > B => A+Nr /= B
2030		; Nr=0 -> check_not_equal(A,B,Hyps)
2031		; check_leq(A,B,Hyps)
2032		).
2033		check_not_equal(X,Y,Hyps) :- sym_unify(X,Y,A,B),number(B),!,
2034		B1 is B+1,
2035		(check_leq(B1,A,Hyps) -> true % B < A
2036		; B2 is B-1,
2037		check_leq(A,B2,Hyps)). % A < B
2038		check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B),
2039		avl_fetch_binop_from_hyps('$'(A),less_equal,Hyps,Y,Hyps2),
2040		(number(B) -> (B1 is B-1, check_leq(Y,B1,Hyps2) -> true)
2041		; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B
2042		-> check_leq(Y,B,Hyps2) % we can prove x<y & y<=z => x<z but we cannot yet prove x<=y & y<z => x<z
2043		).
2044		check_not_equal(XX,YY,Hyps) :- sym_unify(XX,YY,'$'(A),B),
2045		avl_fetch_binop_from_hyps('$'(A),greater_equal,Hyps,Y,Hyps2),
2046		(number(B) -> (B1 is B+1, check_leq(B1,Y,Hyps2) -> true)
2047		; avl_fetch_not_equal('$'(A),Y,Hyps) % we have $(A) < Y => prove Y <= B
2048		-> check_leq(B,Y,Hyps2) % see comments above
2049		).
2050		check_not_equal(A,Empty,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp).
2051		check_not_equal(Empty,A,Hyp) :- is_empty_set_direct(Empty), !, check_not_empty_set(A,Hyp).
2052		check_not_equal(value(avl_set(A)),value(avl_set(B)),_) :- nonvar(A), nonvar(B),!, % nonvar should always be true
2053		\+ equal_avl_tree(A,B).
2054		check_not_equal(A,B,Hyps) :-
2055		(A=set_extension(LA) -> check_not_equal_set_extension(B,LA,Hyps)
2056		; B=set_extension(LB) -> check_not_equal_set_extension(A,LB,Hyps)).
2057		check_not_equal(A,B,Hyps) :-
2058		avl_fetch_worthwhile_equal_from_hyps(A,Hyps,Value,Hyps2),!,
2059		check_not_equal(Value,B,Hyps2).
2060		check_not_equal(A,B,Hyps) :-
2061		avl_fetch_worthwhile_equal_from_hyps(B,Hyps,Value,Hyps2),!,
2062		check_not_equal(A,Value,Hyps2).
2063		%check_not_equal(A,B,Hyps) :- print(check_not_equal_failed(A,B)),nl,portray_hyps(Hyps),nl,fail.
2064
2065		check_not_equal_set_extension(set_extension([B|TB]),[A|TA],Hyps) :- (TA=[];TB=[]),!,
2066		check_not_equal(A,B,Hyps). % TO DO: we can generalize this treatment to find one element in one set not in the other
2067		check_not_equal_set_extension(value(avl_set(AVL)),LA,Hyps) :- length(LA,MaxSizeA),
2068		(avl_size(AVL,Sze),Sze>MaxSizeA -> true % AVL has at least one element more
2069		; is_one_element_avl(AVL,B), LA=[A|_], check_not_equal(A,B,Hyps)).
2070
2071		avl_fetch_not_equal(N1,N2,hyp_rec(AVL,_)) :-
2072		(avl_fetch(not_equal(N1,N2),AVL) -> true
2073		; avl_fetch(not_equal(N2,N1),AVL)). % we do not store both directions for not_equal
2074
2075		% unify two variables with other two variables; useful for symmetric rules
2076		sym_unify(A,B,A,B).
2077		sym_unify(A,B,B,A).
2078
2079		% TO DO: get equalities; maybe we should harmonise this for all rules
2080		% we could add rules about min_int, max_int
2081
2082
2083		% we should call this to check if something is the empty set:
2084		% it does equality rewrites, but also calls check_empty_set/3 indirectly
2085		check_equal_empty_set(Set,Hyps,PT) :-
2086		check_equal(Set,empty_set,Hyps,PT). % will also call this below:
2087
2088		is_empty_set_direct(empty_set).
2089		is_empty_set_direct(empty_sequence).
2090		is_empty_set_direct(value(X)) :- X==[].
2091
2092		check_empty_set(Set,_,empty_set) :- is_empty_set_direct(Set),!.
2093		check_empty_set(A,Hyps,hyp) :- avl_fetch_from_hyps(equal(A,empty_set),Hyps),!.
2094		check_empty_set(set_subtraction(A,B),Hyp,subset(PT)) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule
2095		check_is_subset(A,B,Hyp,PT).
2096		check_empty_set(intersection(A,B),Hyps,inter_disjoint) :- !,
2097		check_disjoint(A,B,Hyps).
2098		check_empty_set(union(A,B),Hyps,union_empty(P1,P2)) :- !, % SIMP_BUNION_EQUAL_EMPTY
2099		check_equal_empty_set(A,Hyps,P1),!,
2100		check_equal_empty_set(B,Hyps,P2).
2101		check_empty_set(cartesian_product(A,B),Hyps,cart_empty(PT)) :- !, % SIMP_CPROD_EQUAL_EMPTY
2102		(check_equal_empty_set(A,Hyps,PT) -> true ; check_equal_empty_set(B,Hyps,PT)).
2103		check_empty_set(pow1_subset(A),Hyps,pow1_empty(PT)) :- !, % SIMP_POW1_EQUAL_EMPTY
2104		check_equal_empty_set(A,Hyps,PT).
2105		check_empty_set(interval(From,To),Hyps,interval_empty) :- !, % SIMP_UPTO_EQUAL_EMPTY
2106		check_less(To,From,Hyps).
2107		check_empty_set(domain(A),Hyps,domain_empty(PT)) :- !, % SIMP_DOM_EQUAL_EMPTY
2108		check_equal_empty_set(A,Hyps,PT).
2109		check_empty_set(range(A),Hyps,range_empty(PT)) :- !, % SIMP_RAN_EQUAL_EMPTY
2110		check_equal_empty_set(A,Hyps,PT).
2111		check_empty_set(reverse(A),Hyps,reverse_empty(PT)) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse)
2112		check_equal_empty_set(A,Hyps,PT).
2113		check_empty_set(domain(A),Hyps,domain_empty(PT)) :- !, % SIMP_DOM_EQUAL_EMPTY
2114		check_equal_empty_set(A,Hyps,PT).
2115		check_empty_set(total_relation(A,B),Hyp,trel_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
2116		check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB).
2117		check_empty_set(total_function(A,B),Hyp,tfun_empty(PTA,PTB)) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
2118		check_not_equal_empty_set(A,Hyp,PTA), check_equal_empty_set(B,Hyp,PTB).
2119		check_empty_set(A,Hyps,subset_strict_singleton) :-
2120		avl_fetch_binop_from_hyps(A,subset_strict,Hyps,B,_), % A <<: {Single} => A={}
2121		singleton_set(B,_).
2122		% TODO: add more rules inter(A,Singleton) SIMP_BINTER_SING_EQUAL_EMPTY
2123
2124		% we should call this to check if something is not the empty set:
2125		% it does equality rewrites, but also calls check_not_empty_set/2 indirectly
2126		check_not_equal_empty_set(Set,Hyps,not_equal_empty_set) :-
2127		check_not_equal(Set,empty_set,Hyps).
2128
2129		check_not_empty_set(A,Hyps) :- avl_fetch_from_hyps(not_equal(A,empty_set),Hyps),!.
2130		check_not_empty_set(A,Hyps) :- %Note: size(A) should be changed to card(A) in normalization
2131		(CardA = card(A) ; CardA = size(A)),
2132		avl_fetch_binop_from_hyps(CardA,greater_equal,Hyps,Nr,Hyps2), %Nr \= 0,
2133		check_leq(1,Nr,Hyps2),!. % cut here, relevant for test 2043
2134		check_not_empty_set(set_extension([_|_]),_Hyps).
2135		check_not_empty_set(sorted_set_extension([_|_]),_Hyps).
2136		check_not_empty_set(sequence_extension([_|_]),_Hyps).
2137		check_not_empty_set(cartesian_product(A,B),Hyps) :- % SIMP_CPROD_EQUAL_EMPTY
2138		(check_not_empty_set(A,Hyps) -> check_not_empty_set(B,Hyps)).
2139		check_not_empty_set(interval(A,B),Hyps) :- check_leq(A,B,Hyps).
2140		check_not_empty_set(value(avl_set(AVL)),_) :- AVL \= empty.
2141		check_not_empty_set(union(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)).
2142		check_not_empty_set(general_union(A),Hyp) :- !, % SIMP_KUNION_EQUAL_EMPTY
2143		check_not_subset(A,set_extension([empty_set]),Hyp,_PT).
2144		check_not_empty_set(set_subtraction(A,B),Hyp) :- !, % see SIMP_SETMINUS_EQUAL_EMPTY Rodin proof rule
2145		check_not_subset(A,B,Hyp,_PT).
2146		check_not_empty_set(overwrite(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)).
2147		check_not_empty_set(domain(A),Hyp) :- !, % SIMP_DOM_EQUAL_EMPTY
2148		check_not_empty_set(A,Hyp).
2149		check_not_empty_set(range(A),Hyp) :- !, % SIMP_RAN_EQUAL_EMPTY
2150		check_not_empty_set(A,Hyp).
2151		check_not_empty_set(identity(A),Hyp) :- !, check_not_empty_set(A,Hyp).
2152		check_not_empty_set(image(R,interval(L,U)),Hyp) :- !,
2153		check_not_empty_set(interval(L,U),Hyp),
2154		(check_member_of_set(domain(R),L,Hyp,_) -> true
2155		; check_member_of_set(domain(R),U,Hyp,_)
2156		).
2157		check_not_empty_set(reverse(A),Hyp) :- !, % SIMP_CONVERSE_EQUAL_EMPTY (relational inverse)
2158		check_not_empty_set(A,Hyp).
2159		check_not_empty_set(rev(A),Hyp) :- !, check_not_empty_set(A,Hyp).
2160		check_not_empty_set(concat(A,B),Hyp) :- !, (check_not_empty_set(A,Hyp) -> true ; check_not_empty_set(B,Hyp)).
2161		check_not_empty_set(bool_set,_Hyp) :- !.
2162		check_not_empty_set(float_set,_Hyp) :- !.
2163		check_not_empty_set(real_set,_Hyp) :- !.
2164		check_not_empty_set(string_set,_Hyp) :- !.
2165		check_not_empty_set('NATURAL1',_Hyp) :- !. % SIMP_NATURAL1_EQUAL_EMPTY
2166		check_not_empty_set('NATURAL',_Hyp) :- !. % SIMP_NATURAL_EQUAL_EMPTY
2167		check_not_empty_set(typeset,_Hyp) :- !. % SIMP_TYPE_EQUAL_EMPTY, all basic sets are non empty in B and Event-B
2168		check_not_empty_set(relations(_,_),_Hyp) :- !. % SIMP_SPECIAL_EQUAL_REL
2169		check_not_empty_set(total_function(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
2170		( check_equal_empty_set(A,Hyp,_) -> true
2171		; check_not_equal_empty_set(B,Hyp,_) -> true
2172		; check_equal(A,B,Hyp,_)). % implicit proof by case distinction
2173		check_not_empty_set(total_relation(A,B),Hyp) :- !, % SIMP_SPECIAL_EQUAL_RELDOM
2174		check_not_empty_set(total_function(A,B),Hyp).
2175		check_not_empty_set(Expr,Hyps) :-
2176		is_lambda_function_with_domain(Expr,Domain),!,
2177		check_not_empty_set(Domain,Hyps).
2178		check_not_empty_set('$'(ID),Hyps) :-
2179		enumerated_set(ID),
2180		\+ is_hyp_var(ID,Hyps),!. % global enumerated set visible
2181		check_not_empty_set(Eq,Hyps) :-
2182		(Eq='$'(_) ; Eq=interval(_,_)),
2183		avl_fetch_equal_from_hyps(Eq,Hyps,Value,Hyps2),
2184		rewrite_local_loop_check(Eq,check_not_empty_set,Value,Hyps2,Hyps3),
2185		check_not_empty_set(Value,Hyps3),!.
2186		check_not_empty_set(Seq,Hyp) :- infer_sequence_type_of_expr(Seq,Hyp,seq1),!.
2187		check_not_empty_set(Func,Hyps) :- Func = '$'(_),
2188		avl_fetch_binop_from_hyps(Func,member,Hyps,FunctionType,Hyps2), % Func : . --> .
2189		check_not_empty_elements(FunctionType,Hyps2),!.
2190		check_not_empty_set(function(Func2,_),Hyps) :-
2191		get_range_or_superset(Func2,Hyps,Range,Hyps2),
2192		check_not_empty_elements(Range,Hyps2),!.
2193		check_not_empty_set(tail(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!,
2194		check_leq(2,CardA,Hyps1).
2195		check_not_empty_set(front(A),Hyps) :- rewrite_card_of_set(A,Hyps,CardA,Hyps1),!,
2196		check_leq(2,CardA,Hyps1).
2197		check_not_empty_set(A,Hyps) :-
2198		avl_fetch_binop_from_hyps(A,not_subset_strict,Hyps,B,_), % A <<: {Single} <=> A={}
2199		singleton_set(B,_),!.
2200		check_not_empty_set(A,Hyps) :-
2201		( Lookup = A, Operator = superset
2202		;
2203		(Lookup=domain(A) ; Lookup=range(A)),
2204		(Operator = superset ; Operator = equal)
2205		),
2206		avl_fetch_binop_from_hyps(Lookup,Operator,Hyps,B,Hyps2), % B /= {} & B <: A => A /= {}
2207		rewrite_local_loop_check(A,check_not_empty_set,B,Hyps2,Hyps3),
2208		check_not_empty_set(B,Hyps3),!.
2209		% TO DO: rule for dom(r)<:A and r not empty implies A not empty; problem: we need lookup for A=dom(r), or dom(r)<:A, could be of form: r:A+->B
2210		% check_not_empty_set(A,_) :- print(check_not_empty_set_failed(A)),nl,fail.
2211		% TO DO: more rules for sequence operators; infer_sequence_type_of_expr does not look at values of ids
2212
2213
2214		% check if elements of a function type or set are guaranteed to be not empty
2215
2216		check_not_empty_elements(fin1_subset(_),_).
2217		check_not_empty_elements(pow1_subset(_),_).
2218		check_not_empty_elements(seq1(_),_).
2219		check_not_empty_elements(iseq1(_),_).
2220		check_not_empty_elements(perm(A),Hyps) :- check_not_empty_set(A,Hyps).
2221		check_not_empty_elements(total_function(A,_),Hyps) :- check_not_empty_set(A,Hyps).
2222		check_not_empty_elements(total_injection(A,_),Hyps) :- check_not_empty_set(A,Hyps).
2223		check_not_empty_elements(total_surjection(A,B),Hyps) :-
2224		(check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)).
2225		check_not_empty_elements(total_bijection(A,B),Hyps) :-
2226		(check_not_empty_set(A,Hyps) -> true ; check_not_empty_set(B,Hyps)).
2227		check_not_empty_elements(total_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps).
2228		check_not_empty_elements(total_surjection_relation(A,_),Hyps) :- check_not_empty_set(A,Hyps).
2229		check_not_empty_elements(partial_surjection(_,B),Hyps) :- check_not_empty_set(B,Hyps).
2230		check_not_empty_elements(partial_bijection(_,B),Hyps) :- check_not_empty_set(B,Hyps).
2231		check_not_empty_elements(surjection_relation(_,B),Hyps) :- check_not_empty_set(B,Hyps).
2232		% more cases, set_extension,...
2233
2234		:- use_module(probsrc(b_global_sets),[enumerated_set/1]).
2235		% check if an expression is definitely finite
2236		check_finite(bool_set,_,bool_set) :- !.
2237		check_finite(empty_set,_,empty_set) :- !.
2238		check_finite(empty_sequence,_,empty_sequence) :- !.
2239		check_finite(float_set,_,float_set) :- !.
2240		% check_finite(integer_set(X),_,bool_set) :- !. INT, NAT, NAT1 are translated to intervals
2241		check_finite(set_extension(_),_,set_extension) :- !.
2242		check_finite(sorted_set_extension(_),_,set_extension) :- !.
2243		check_finite(sequence_extension(_),_,seq_extension) :- !.
2244		check_finite(fin_subset(X),Hyps,fin(PT)) :- !, check_finite(X,Hyps,PT).
2245		check_finite(fin1_subset(X),Hyps,fin1(PT)) :- !, check_finite(X,Hyps,PT).
2246		check_finite(pow_subset(X),Hyps,pow(PT)) :- !, check_finite(X,Hyps,PT).
2247		check_finite(pow1_subset(X),Hyps,pow1(PT)) :- !, check_finite(X,Hyps,PT).
2248		check_finite(iseq(X),Hyps,iseq(PT)) :- !, check_finite(X,Hyps,PT).
2249		check_finite(iseq1(X),Hyps,iseq1(PT)) :- !, check_finite(X,Hyps,PT).
2250		check_finite(mu(Set),Hyps,mu) :- !, has_finite_elements(Set,Hyps).
2251		check_finite(perm(X),Hyps,perm(PT)) :- !, check_finite(X,Hyps,PT).
2252		check_finite(Set,Hyps,hyp) :-
2253		avl_fetch_from_hyps(finite(Set),Hyps),!.
2254		check_finite(domain(A),Hyp,dom(PT)) :- !,
2255		(check_finite(A,Hyp,PT) -> true ; finite_domain(A,Hyp,PT)).
2256		check_finite(range(A),Hyp,ran(PT)) :- !,
2257		(check_finite(A,Hyp,PT) -> true ; finite_range(A,Hyp,PT)).
2258		check_finite(reverse(A),Hyp,rev(PT)) :- !, check_finite(A,Hyp,PT).
2259		check_finite(identity(A),Hyp,id(PT)) :- !,check_finite(A,Hyp,PT). % finite(id(A)) if finite(A)
2260		check_finite(function(Func,_),Hyps,function_finite_elements) :- !,
2261		get_range_or_superset(Func,Hyps,RanFunc,Hyps2),
2262		has_finite_elements(RanFunc,Hyps2).
2263		check_finite(image(Func,B),Hyp,image(PT)) :- !,
2264		(check_finite(Func,Hyp,PT) -> true % finite(Func[.]) <= finite(Func)
2265		; check_finite(B,Hyp,PTB)
2266		-> PT = pfun(PTB), check_is_partial_function(Func,Hyp) % finite(Func[B]) <= finite(B) & Func : TD +-> TR
2267		).
2268		check_finite(union(A,B),Hyp,union(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
2269		check_finite(if_then_else(_,A,B),Hyps,if(PTA,PTB)) :- !, (check_finite(A,Hyps,PTA) -> check_finite(B,Hyps,PTB)).
2270		check_finite(intersection(A,B),Hyps,intersection(D,PT)) :- !,
2271		(D=left,check_finite(A,Hyps,PT) -> true ; D=right,check_finite(B,Hyps,PT)).
2272		check_finite(cartesian_product(A,B),Hyp,cart(PT)) :-
2273		(check_finite(A,Hyp,PT) -> (check_equal_empty_set(A,Hyp,_PT2) -> true ; check_finite(B,Hyp,_PT2))
2274		; check_equal_empty_set(B,Hyp,PT)).
2275		check_finite(Rel,Hyp,rel(PTA,PTB)) :- is_relations_type(Rel,A,B),!,
2276		(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)). % add other relations
2277		check_finite(direct_product(A,B),Hyp,direct_product(PTA,PTB)) :- !,
2278		(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
2279		check_finite(parallel_product(A,B),Hyp,parallel_product(PTA,PTB)) :- !,
2280		(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
2281		check_finite(overwrite(A,B),Hyp,overwrite(PTA,PTB)) :- !, (check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)).
2282		check_finite(set_subtraction(A,_),Hyps,set_subtraction(PT)) :- !, check_finite(A,Hyps,PT).
2283		check_finite(domain_restriction(A,BRel),Hyp,domain_restriction(PT)) :- !,
2284		(check_finite(BRel,Hyp,PT) -> true
2285		; check_is_partial_function(BRel,Hyp), check_finite(A,Hyp,PT)
2286		; finite_range(BRel,Hyp,_) -> check_finite(A,Hyp,PT) % finite(a <| brel) if finite(a) & finite(ran(brel))
2287		).
2288		check_finite(domain_subtraction(_,B),Hyp,domain_subtraction(PT)) :- !, check_finite(B,Hyp,PT).
2289		check_finite(range_restriction(ARel,B),Hyp,range_restriction(PT)) :- !,
2290		(check_finite(ARel,Hyp,PT) -> true
2291		; check_is_injective(ARel,Hyp) -> check_finite(B,Hyp,PT)
2292		; finite_domain(ARel,Hyp,_) -> check_finite(B,Hyp,PT) % finite(arel |> b) if finite(b) & finite(dom(arel))
2293		).
2294		check_finite(image(A,B),Hyp,image(PT)) :- % A[B] is finite if A is finite or if B is finite and A a function
2295		(check_finite(A,Hyp,PT) -> true ; check_is_partial_function(A,Hyp), check_finite(B,Hyp,PT)).
2296		check_finite(range_subtraction(A,_),Hyp,range_subtraction(PT)) :- check_finite(A,Hyp,PT).
2297		check_finite(interval(_,_),_,interval) :- !.
2298		check_finite(value(V),_,empty_set_value) :- V==[], !.
2299		check_finite(value(X),_,avl_set) :- nonvar(X),X=avl_set(_),!.
2300		check_finite('$'(ID),Hyps,finite_type) :-
2301		get_hyp_var_type(ID,Hyps,Type), %print(chk_fin(ID,Type)),nl,
2302		(is_finite_type_for_wd(Type,Hyps) -> true
2303		; Type = set(couple(DomType,_)), % in principle an infinite relation type
2304		is_finite_type_for_wd(DomType,Hyps), % we have something like set(couple(boolean,integer))
2305		% note: we treat this here in addition to the case is_partial_function below, as
2306		% sometimes we loose the typing information in the term, e.g., in comprehension_set
2307		avl_fetch_equal_from_hyps('$'(ID),Hyps,Func,_),
2308		is_lambda_function(Func) % we have a function, it is finite if the domain is finite
2309		),!.
2310		check_finite('$'(ID),Hyps,enumerated_set) :-
2311		enumerated_set(ID),
2312		\+ is_hyp_var(ID,Hyps),!. % global enumerated set visible
2313		%check_finite('$'(ID),Hyp,partition) :-
2314		% avl_fetch_binop_from_hyps('$'(ID),partition,Hyp,Values,Hyp2), % is now normalized
2315		% not_occurs(Values,ID),
2316		% l_check_finite(Values,Hyp2),!.
2317		check_finite('$'(ID),Hyps,rewrite(Operator,PT)) :-
2318		(Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp
2319		avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2),
2320		not_occurs(Set2,ID), % avoid silly, cyclic rewrites $x -> reverse(reverse($x)) (FunLawsStrings.mch)
2321		% however, in SetLawsNatural this prevents proving 2 POs due to SS <: min(SS)..max(SS)
2322		rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3),
2323		check_finite(Set2,Hyps3,PT),!.
2324		check_finite(Set,Hyp,finite_elements) :- id_or_record_field(Set),
2325		avl_fetch_mem_or_struct(Set,Hyp,Set2,Hyp2),
2326		Set2 \= Set,
2327		has_finite_elements(Set2,Hyp2).
2328		check_finite(Func,Hyp,pfun(PTA,PTB)) :- is_partial_function(Func,A,B),!,
2329		% a set of partial functions from A to B is finite if both A and B are finite
2330		(check_finite(A,Hyp,PTA) -> check_finite(B,Hyp,PTB)),!.
2331		check_finite(Seq,Hyp,seq_type) :- infer_sequence_type_of_expr(Seq,Hyp,_),!. % a sequence is always finite
2332		check_finite(comprehension_set(Paras,Body),Hyp,comprehension_set) :-
2333		finite_comprehension_set(Paras,Body,Hyp),!.
2334		check_finite(struct(rec(Fields)),Hyp,struct) :- maplist(check_finite_field(Hyp),Fields).
2335		check_finite(general_union(SetOfSets),Hyp,general_union) :-
2336		check_all_finite(SetOfSets,Hyp).
2337		check_finite(general_intersection(SetOfSets),Hyp,general_intersection(PT)) :-
2338		check_some_finite(SetOfSets,Hyp,PT).
2339		% TODO: is_lambda_function_with_domain; improve some proof trees above in style of intersection
2340		%check_finite(F,Hyps,_) :- print(check_finite_failed(F)),nl,portray_hyps(Hyps),nl,fail.
2341
2342		check_finite_field(Hyp,field(_,Set)) :- check_finite(Set,Hyp,_PT).
2343
2344		% we could write a check_all meta_predicate
2345		% check if we have a finite set of finite sets; used to determine if union(Sets) is finite
2346		check_all_finite(empty_set,_).
2347		check_all_finite(empty_sequence,_).
2348		check_all_finite(value(avl_set(_AVL)),_Hyp) :- % currently avl_set can only contain finite values for normalisation
2349		true.
2350		check_all_finite(intersection(A,B),Hyps) :-
2351		(check_all_finite(A,Hyps) -> true ; check_all_finite(B,Hyps)).
2352		check_all_finite(union(A,B),Hyps) :-
2353		(check_all_finite(A,Hyps) -> check_all_finite(B,Hyps)).
2354		check_all_finite(sorted_set_extension(L),Hyps) :- !, check_all_finite(set_extension(L),Hyps).
2355		check_all_finite(set_extension(L),Hyps) :-
2356		(member(Val,L), \+ check_finite(Val,Hyps,_) -> fail % CHECK
2357		; true).
2358		check_all_finite('$'(ID),Hyps) :-
2359		(Operator = equal ; Operator = subset), % for subset_strict we also have subset in Hyp
2360		avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2),
2361		not_occurs(Set2,ID), % avoid silly, cyclic rewrites
2362		rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3),
2363		check_all_finite(Set2,Hyps3),!.
2364		check_all_finite(Op,Hyps) :- pow_subset_operator(Op,Set),!,
2365		% if Set is finite then all subsets of it are finite and there are only finitely many
2366		check_finite(Set,Hyps,_PT).
2367		check_all_finite(Op,Hyps) :- iseq_operator(Op,Set),!,
2368		% if Set is finite then all injective sequences of it are finite and there are only finitely many
2369		check_finite(Set,Hyps,_PT).
2370
2371		% check if some set of a set of sets is finite:
2372		check_some_finite(sorted_set_extension(L),Hyps,PT) :- !, check_some_finite(set_extension(L),Hyps,PT).
2373		check_some_finite(set_extension(L),Hyps,set_extension(PT)) :-
2374		(member(Val,L), check_finite(Val,Hyps,PT) -> true).
2375		check_some_finite('$'(ID),Hyps,rewrite_id(ID,PT)) :-
2376		(Operator = equal ; Operator = superset), % Note: superset not subset as for check_all_finite
2377		avl_fetch_binop_from_hyps('$'(ID),Operator,Hyps,Set2,Hyps2),
2378		not_occurs(Set2,ID), % avoid silly, cyclic rewrites
2379		rewrite_local_loop_check(ID,check_finite,Set2,Hyps2,Hyps3),
2380		check_some_finite(Set2,Hyps3,PT),!.
2381		%check_some_finite(intersection(A,B),Hyps) :- fail. % Note: the intersection could be empty!
2382		check_some_finite(union(A,B),Hyps,union(PT)) :-
2383		(check_some_finite(A,Hyps,PT) -> true ; check_some_finite(B,Hyps,PT)).
2384		% for pow_subset_operator iseq_operator we would still need to check that the sets are not empty
2385		% we cannot currently :prove x<:POW1(INT) & inter({NATURAL}\/x) : FIN(inter({NATURAL}\/x))
2386
2387
2388		pow_subset_operator(fin_subset(X),X).
2389		pow_subset_operator(fin1_subset(X),X).
2390		pow_subset_operator(pow_subset(X),X).
2391		pow_subset_operator(pow1_subset(X),X).
2392		iseq_operator(perm(Set),Set).
2393		iseq_operator(iseq(Set),Set).
2394		iseq_operator(iseq1(Set),Set).
2395
2396		% Note: lambdas already treated in is_partial_function check above
2397		finite_comprehension_set(Paras,Body,Hyp) :-
2398		% first exclude the parameters which can be proven finite on their own
2399		% now deal with the rest; we do not pass AllParas as second arg; as all references to excluded IDs is ok (only finitely many values possible)
2400		finite_comprehension_set_rest(Paras,Body,Hyp,[],Rest),
2401		Rest \= Paras,
2402		finite_comprehension_set_rest(Rest,Body,Hyp,[],[]). % do a second pass, e.g., for {x,y|x:{y,y+1} & y:1..2 & x:INTEGER}
2403
2404		finite_comprehension_set_rest([],_,_,_,[]).
2405		% finite_comprehension_set(['$'(ID)|TID],Body,Hyp) :- finite_type !
2406		finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,Rest) :-
2407		get_parameter_superset_in_body(ParaExpr,[ParaID1|TID],Body,Values),
2408		l_not_occurs(Values,UnProven), % do not rely on not yet finitely proven paras; e.g. for {x,y|x:INTEGER & y=x}
2409		match_parameter(ParaExpr,ParaID1),
2410		check_finite(Values,Hyp,_PT),!,
2411		finite_comprehension_set_rest(TID,Body,Hyp,UnProven,Rest).
2412		finite_comprehension_set_rest([ParaID1|TID],Body,Hyp,UnProven,[ParaID1|Rest]) :-
2413		finite_comprehension_set_rest(TID,Body,Hyp,[ParaID1|UnProven],Rest).
2414
2415		% match_parameter(Expr,ID) -> ID occurs in Expr and finite number of values for Expr implies finite values for ID
2416		match_parameter(ParaID,ParaID).
2417		match_parameter(couple(ParaID,_),ParaID). % x|->y : Values finite implies finitely many values for x
2418		match_parameter(couple(_,ParaID),ParaID).
2419		match_parameter(set_extension(Ext),ParaID) :-
2420		member(El,Ext), match_parameter(El,ParaID). % {x,..} : Values finite implies finitely many values for x
2421		match_parameter(sorted_set_extension(Ext),ParaID) :- match_parameter(set_extension(Ext),ParaID).
2422		match_parameter(sequence_extension(Ext),ParaID) :- member(ParaID,Ext).
2423		match_parameter(rev(RF),ParaID) :- match_parameter(RF,ParaID).
2424		match_parameter(reverse(RF),ParaID) :- match_parameter(RF,ParaID).
2425		match_parameter(unary_minus(RF),ParaID) :- match_parameter(RF,ParaID).
2426		match_parameter(concat(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)).
2427		match_parameter(union(RF1,RF2),ParaID) :- (match_parameter(RF1,ParaID) -> true ; match_parameter(RF2,ParaID)).
2428		match_parameter(overwrite(_,RF),ParaID) :- match_parameter(RF,ParaID). % f <+ RF = (... <<| f ) \/ RF
2429		match_parameter(Add,ParaID) :- add_with_number(Add,A,_Number), match_parameter(A,ParaID).
2430		match_parameter(Mul,ParaID) :- mul_with_number(Mul,A,Number), Number \= 0, match_parameter(A,ParaID).
2431		% TO DO: more injective functions where a solution determines the ParaID, identity? direct_product, ...
2432		% cartesian_product : only if other set not empty
2433
2434		get_parameter_superset_in_body(ParaID,AllParas,Body,Values) :-
2435		( member_in_norm_conjunction(Body,member(ParaID,Values))
2436		; member_in_norm_conjunction(Body,subset(ParaID,Values)) % there are only finitely many subsets of a finite set
2437		; member_in_norm_conjunction(Body,subset_strict(ParaID,Values))
2438		; member_in_norm_conjunction(Body,equal(X,Y)),
2439		sym_unify(X,Y,ParaID,Value), Values=set_extension([Value]) ),
2440		l_not_occurs(Values,AllParas). % as an alternative: check for finite_type of set elements; e.g., detect ID=bool(...)
2441
2442
2443		:- use_module(probsrc(bsyntaxtree),[is_set_type/2]).
2444		%we suppose this has already failed: finite_domain(A,Hyp) :- check_finite(A,Hyp,PT).
2445		finite_domain('$'(ID),Hyps,finite_type) :-
2446		get_hyp_var_type(ID,Hyps,Type),
2447		is_set_type(Type,couple(DomType,_)),
2448		is_finite_type_for_wd(DomType,Hyps),!.
2449		finite_domain(domain_restriction(A,Rel),Hyps,domain_restriction(PT)) :- !,
2450		(check_finite(A,Hyps,PT) -> true ; finite_domain(Rel,Hyps,PT)).
2451		finite_domain(A,Hyp,PT) :- get_domain_or_superset(A,Hyp,DA,Hyp2),!, check_finite(DA,Hyp2,PT).
2452
2453		finite_range('$'(ID),Hyps,finite_type) :-
2454		get_hyp_var_type(ID,Hyps,Type),
2455		is_set_type(Type,couple(_,RanType)),
2456		is_finite_type_for_wd(RanType,Hyps),!.
2457		finite_range(A,Hyp,PT) :- get_range_or_superset(A,Hyp,RA,Hyp2),!, check_finite(RA,Hyp2,PT).
2458
2459		l_check_finite([],_).
2460		l_check_finite([H|T],Hyp) :- (check_finite(H,Hyp,_) -> l_check_finite(T,Hyp)).
2461
2462		% is a set containing only finite sets
2463		has_finite_elements(fin_subset(_),_) :- !.
2464		has_finite_elements(fin1_subset(_),_) :- !.
2465		has_finite_elements(pow_subset(X),Hyps) :- !, check_finite(X,Hyps,_).
2466		has_finite_elements(pow1_subset(X),Hyps) :- !, check_finite(X,Hyps,_).
2467		has_finite_elements(seq(_),_) :- !. % every sequence is always finite (of finite length)
2468		has_finite_elements(seq1(_),_) :- !.
2469		has_finite_elements(iseq(_),_) :- !.
2470		has_finite_elements(iseq1(_),_) :- !.
2471		has_finite_elements(perm(_),_) :- !.
2472		has_finite_elements(union(A,B),Hyps) :- !, has_finite_elements(A,Hyps), has_finite_elements(B,Hyps).
2473		has_finite_elements(intersection(A,B),Hyps) :- !, (has_finite_elements(A,Hyps) -> true ; has_finite_elements(B,Hyps)).
2474		has_finite_elements(set_subtraction(A,_),Hyps) :- !, has_finite_elements(A,Hyps).
2475		has_finite_elements(sorted_set_extension(L),Hyps) :- !, l_check_finite(L,Hyps).
2476		has_finite_elements(set_extension(L),Hyps) :- !, l_check_finite(L,Hyps).
2477		has_finite_elements(S,_) :- is_empty_set_direct(S),!. % has no elements
2478		has_finite_elements(Func,Hyps) :- is_partial_function(Func,A,B),!,
2479		(check_finite(A,Hyps,_) -> true ; is_injective(Func), check_finite(B,Hyps,_)).
2480		has_finite_elements(Rel,Hyps) :- is_relations_type(Rel,A,B),!,check_finite(A,Hyps,_),check_finite(B,Hyps,_).
2481		%has_finite_elements(F,Hs) :- print(has_finite_elements_failed(F)),nl, portray_hyps(Hs),fail.
2482
2483
2484		is_relations_type(relations(A,B),A,B).
2485		is_relations_type(surjection_relation(A,B),A,B).
2486		is_relations_type(total_relation(A,B),A,B).
2487		is_relations_type(total_surjection_relation(A,B),A,B).
2488
2489		% TO DO: more rules for functions
2490		% ------------------------------
2491
2492		:- use_module(probsrc(avl_tools),[avl_fetch_bin/4]).
2493
2494		% fetch member(Ground,Free) construct
2495		%avl_fetch_mem(Key, AVL ,Res) :- avl_fetch_bin(Key, member, AVL ,Res).
2496		%avl_fetch_equal(Key, AVL ,Res) :- avl_fetch_bin(Key, equal, AVL ,Res).
2497
2498
2499		avl_fetch_mem_from_hyps(ID,Hyps,Value,Hyps2) :-
2500		avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2).
2501
2502		avl_fetch_worthwhile_mem_from_hyps(ID,Hyps,Value,Hyps2) :-
2503		avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2),
2504		\+ maximal_set(Value,Hyps).
2505
2506		avl_fetch_equal_from_hyps(ID,Hyps,Value,Hyps2) :-
2507		avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2).
2508
2509		avl_fetch_worthwhile_equal_from_hyps(ID,Hyps,Value,Hyps2) :-
2510		worth_rewriting_with_equal(ID),
2511		avl_fetch_binop_from_hyps(ID,equal,Hyps,Value,Hyps2),
2512		quick_not_occurs_check(ID,Value).
2513
2514		avl_fetch_worthwhile_member_from_hyps(ID,Hyps,Value,Hyps2) :-
2515		worth_rewriting_with_equal(ID),
2516		avl_fetch_binop_from_hyps(ID,member,Hyps,Value,Hyps2).
2517
2518		% fetch member predicate or indirect member via record fields
2519		avl_fetch_mem_or_struct(Func,Hyps,Function,Hyps1) :-
2520		get_type_from_hyps(Func,Hyps,Function,Hyps1).
2521		avl_fetch_mem_or_struct(record_field(Rec,Field),Hyps,FieldType,Hyps2) :-
2522		get_record_type_fields(Rec,Fields,Hyps,Hyps2),
2523		(member(field(Field,FieldType),Fields) -> true).
2524
2525		% find record type and extract fields for a given expression
2526		get_record_type_fields(function(Func,_),Fields,Hyps,Hyps2) :-
2527		get_range_or_superset(Func,Hyps,Range,Hyps1),
2528		check_equal_pattern(Range,struct(rec(Fields)),Hyps1,Hyps2).
2529		get_record_type_fields(Rec,Fields,Hyps,Hyps2) :-
2530		get_type_from_hyps(Rec,Hyps,RecType,Hyps1),
2531		check_equal_pattern(RecType,struct(rec(Fields)),Hyps1,Hyps2).
2532
2533		% get type from hyps x:XType or x:ran(F) with F : A->B
2534		get_type_from_hyps(X,Hyps,XType,Hyps2) :-
2535		avl_fetch_mem_from_hyps(X,Hyps,XSet,Hyps1),
2536		get_type2(XSet,Hyps1,XType,Hyps2).
2537		get_type_from_hyps(function(Func2,_),Hyps,Range,Hyps2) :-
2538		% f : _ +-> ( _ >-> _ ) => f(_) : _ >-> _
2539		get_range_or_superset(Func2,Hyps,Range,Hyps2).
2540		get_type_from_hyps(second_of_pair(X),Hyps,Type,Hyps2) :- %prj2
2541		get_type_from_hyps(X,Hyps,XType,Hyps1),
2542		check_equal_pattern(XType,cartesian_product(_,Type),Hyps1,Hyps2).
2543		get_type_from_hyps(first_of_pair(X),Hyps,Type,Hyps2) :- %prj1
2544		get_type_from_hyps(X,Hyps,XType,Hyps1),
2545		check_equal_pattern(XType,cartesian_product(Type,_),Hyps1,Hyps2).
2546		get_type_from_hyps(assertion_expression(_,_,X),Hyps,XType,Hyps1) :-
2547		get_type_from_hyps(X,Hyps,XType,Hyps1).
2548
2549		get_type2(domain(Func),Hyps,XType,Hyps2) :- !,
2550		get_domain_or_superset(Func,Hyps,XType,Hyps2).
2551		get_type2(range(Func),Hyps,XType,Hyps2) :- !,
2552		get_range_or_superset(Func,Hyps,XType,Hyps2).
2553		get_type2(Type,Hyps,Type,Hyps).
2554
2555		id_or_record_field('$'(_)).
2556		id_or_record_field(record_field(_,_)).
2557
2558		% perform occurs check if first arg is an identifier:
2559		quick_not_occurs_check('$'(ID),Value) :- !, not_occurs(Value,ID).
2560		quick_not_occurs_check(_,_).
2561
2562		% worth rewriting with equality hyps
2563		worth_rewriting_with_equal('$'(_)).
2564		worth_rewriting_with_equal(record_field('$'(_),_)).
2565		worth_rewriting_with_equal(couple(_,_)).
2566		worth_rewriting_with_equal(size(_)).
2567		worth_rewriting_with_equal(card(_)).
2568		worth_rewriting_with_equal(function(_,_)).
2569
2570		% utility to fetch fully ground term from hyp avl
2571		avl_fetch_from_hyps(Term,hyp_rec(AVL,_)) :- avl_fetch(Term,AVL).
2572
2573		% a version without loop check; can be used if processing is finished afterwards
2574		avl_fetch_binop_from_hyps_no_loop_check(ID,BinOp,hyp_rec(AVL,_),Value) :-
2575		avl_fetch_bin(ID,BinOp,AVL,Value).
2576
2577		% lookup a hypothesis ID BinOp Value in logarithmic time; ID and BinOp must be known
2578		avl_fetch_binop_from_hyps(ID,BinOp,hyp_rec(AVL,HInfos),Value,hyp_rec(AVL,HInfos2)) :-
2579		avl_fetch_bin(ID,BinOp,AVL,Value),
2580		(avl_fetch(prevent_cycle_count,HInfos,CycleCount) % avoid cycles x=y, y=x
2581		-> (CycleCount < 5 -> true ; % print(prevented_cycle(ID,CycleCount)),nl,
2582		% in test 2018: :wd target = [2,1,1,2,1] & n=size(target) & i:1..n & target(i)=res requires cycle count < 5
2583		!, fail),
2584		C1 is CycleCount+1
2585		; C1 is 1
2586		),
2587		avl_store(prevent_cycle_count,HInfos,C1,HInfos2).
2588		% detect local loops; should not be used where Hyps are passed to unrelated goals or one has to reset_local_loop_check
2589		rewrite_local_loop_check(_,_,Value,HI,HI1) :- useful_value(Value),!,HI1=HI.
2590		rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_) :- var(Hyps),!,
2591		add_internal_error('Var hyps: ',rewrite_local_loop_check(Term,ProverPredicate,_,Hyps,_)),fail.
2592		rewrite_local_loop_check(Term,ProverPredicate,_,hyp_rec(AVL,HInfos),hyp_rec(AVL,HInfos1)) :- !,
2593		(Term='$'(ID) -> true ; ID=Term),
2594		%(avl_fetch(rewritten(Term,ProverPredicate),HInfos) -> print(loop(Term,ProverPredicate)),nl,fail ; true),
2595		\+ avl_fetch(rewritten(ID,ProverPredicate),HInfos),
2596		avl_store(rewritten(ID,ProverPredicate),HInfos,true,HInfos1).
2597		% :wd a : 1 .. sz --> INTEGER & sz=5 & p : perm(dom(a)) & i : 1 .. sz - 1 & res= p(i) % sz rewritten multiple times
2598		% :wd f: BOOL --> 1..10 & g : 0..20 --> BOOL & bb:BOOL & (f;g)(bb)=res
2599
2600		%reset_local_loop_check()
2601
2602		% values where there is no risk of looping when rewriting to:
2603		useful_value(Value) :- number(Value).
2604		useful_value(interval(A,B)) :- number(A), number(B).
2605		useful_value(value(_)).
2606
2607
2608		% rename and prove a list of goals
2609		l_rename_and_prove_goals([],_,_,[]).
2610		l_rename_and_prove_goals([H|T],Subst,Hyps,[PTH|PTT]) :-
2611		rename_norm_term(H,Subst,RH),!,
2612		prove_po(RH,Hyps,PTH),!, % TO DO: use version of prove_po that does not print info
2613		l_rename_and_prove_goals(T,Subst,Hyps,PTT).
2614
2615
2616		% small utility for sanity checking
2617		check_integer(A,PP) :- not_integer(A),!, add_error(PP,'Not an integer: ',A),fail.
2618		check_integer(_,_).
2619		not_integer(empty_set).
2620		not_integer(empty_sequence).
2621		not_integer(interval(_,_)).
2622		not_integer(couple(_,_)).
2623		not_integer(union(_,_)).
2624		not_integer(intersection(_,_)).
2625		not_integer(domain(_)).
2626		not_integer(range(_)).
2627		% TO DO: extend
2628
2629
2630		% ----------------
2631
2632		% small REPL to inspect hyps
2633		:- public hyp_repl/1.
2634		hyp_repl(Hyps) :- hyp_repl_prompt(Hyps),read(Term), !, hyp_repl(Term,Hyps).
2635		hyp_repl(_).
2636
2637		hyp_repl(end_of_file,_).
2638		hyp_repl(quit,_).
2639		hyp_repl(exit,_).
2640		hyp_repl(help,Hyps) :- write('Use quit to exit, print to portray_hyps, or type an identifier to lookup in hyps'),nl,
2641		hyp_repl(Hyps).
2642		hyp_repl(print,Hyps) :- portray_hyps(Hyps), hyp_repl(Hyps).
2643		hyp_repl(ID,Hyps) :- avl_fetch_equal_from_hyps($(ID),Hyps,Value,_),
2644		format('Value for ~w:~n ~w~n',[ID,Value]),
2645		hyp_repl(Hyps).
2646
2647		hyp_repl_prompt(hyp_rec(AVL,HInfos)) :-
2648		avl_size(AVL,Size),
2649		avl_size(HInfos,ISize),!,
2650		format('hyp_rec(#~w,#~w) >>>',[Size,ISize]).
2651		hyp_repl_prompt(_) :- write('ILLEGAL HYP_REC >>>').