well_def_hyps

add_new_hyp_any_vars(H,DollarIDs,H2) :-
    maplist(create_any_type,DollarIDs,TVars),!,
    add_new_hyp_variables(H,TVars,H2).

add_new_hyp_any_vars(H,I,H2) :- add_internal_error('Illegal Ids:',add_new_hyp_any_vars(H,I,H)),
    H2=H.

add_new_hyp_variables(H,[],R) :- !, R=H.

add_new_hyp_variables(hyp_rec(NH,HInfos1),NewAddedTVars,hyp_rec(NH,HInfos3)) :-
    fetch_hyp_typed_vars(HInfos1,TVars),
    list_to_ord_set(NewAddedTVars,SortedNewTVars),
    add_new_hyp_vars(SortedNewTVars,TVars,NewTVars2,ClashTVars),
    (ClashTVars=[] -> HInfos2=HInfos1, NewTVars3=NewTVars2
    ; (debug_mode(off) -> true
    ; add_message(well_def_analyser,'Variable clash, will rename future predicates: ', ClashTVars,ClashTVars)
    ),
    avl_fetch(hyp_clash_vars,HInfos1,clash_rec(GenSymCount,OldClashAVL)),
    ren_clash_variables(ClashTVars,RenClashTVars,GenSymCount,NewGSC,OldClashAVL,NewClashAVL),
    avl_store(hyp_clash_vars,HInfos1,clash_rec(NewGSC,NewClashAVL),HInfos2),
    list_to_ord_set(RenClashTVars,SRenClashTVars),
    ord_union(SRenClashTVars,NewTVars2,NewTVars3)
    ),
    avl_store(hyp_typed_vars,HInfos2,NewTVars3,HInfos3).

add_new_hyp_vars([],TVars,NewTVars,[]) :- !, NewTVars=TVars.

add_new_hyp_vars(AddedTVars,[],NewTVars,[]) :- !,NewTVars=AddedTVars.

add_new_hyp_vars([b(identifier(ID1),Type1,I1)|T1],[b(identifier(ID2),Type2,I2)|T2],NewTVars,Clash) :- !,
    (ID1 @> ID2
    -> NewTVars = [b(identifier(ID2),Type2,I2)|NewT],
    add_new_hyp_vars([b(identifier(ID1),Type1,I1)|T1],T2,NewT,Clash)
    ; ID1 @< ID2
    -> NewTVars = [b(identifier(ID1),Type1,I1)|NewT],
    add_new_hyp_vars(T1,[b(identifier(ID2),Type2,I2)|T2],NewT,Clash)
    ; NewTVars = [b(identifier(ID2),Type2,I2)|NewT],
    Clash = [b(identifier(ID1),Type1,I1)|NewClash],
    add_new_hyp_vars(T1,T2,NewT,NewClash)
).

add_new_hyp_vars(T1,T2,_,_) :- add_internal_error('Illegal call: ',add_new_hyp_vars(T1,T2,_,_)),fail.

avl_store_if_new(NH,H,_,H2) :- avl_fetch(NH,H),!, H2=H.

avl_store_if_new(NH,H1,RH,H3) :- %write(prop_new(NH)),nl, avl_domain(H,H1D), write(H1D),nl,nl,
    propagate_resolution_with_hyp(NH,H1,H2),
    avl_store(NH,H2,RH,H3).

avl_store_with_commutes_if_new(NH,H,_,H2) :- avl_fetch(NH,H),!, H2=H.

avl_store_with_commutes_if_new(NH,H,RH,H3) :- %write(prop_new(NH)),nl, avl_domain(H,H1D), write(H1D),nl,nl,
    propagate_resolution_with_hyp(NH,H,H1),
    push_commutative_hyps(NH,RH,H1,H2),
    avl_store(NH,H2,RH,H3).

can_be_used_for_lookups('$'(_)).

can_be_used_for_lookups(domain(_)). % lookup domain of a function

can_be_used_for_lookups(range(_)).

can_be_used_for_lookups(card(_)).

can_be_used_for_lookups(size(_)). % TO DO: normalize size to card, we assume hyps are WD; so no difference

can_be_used_for_lookups(interval(_,_)).

check_valid_hyp_rec(Hyps,PP) :- var(Hyps),!,
    add_internal_error('Illegal variable hyp_rec: ',check_hyp_rec(Hyps,PP)),fail.

check_valid_hyp_rec(Hyps,PP) :- Hyps \= hyp_rec(_,_),!,
    add_internal_error('Illegal hyp_rec: ',check_valid_hyp_rec(Hyps,PP)),fail.

check_valid_hyp_rec(_,_).

commute_bin_op(equal(A,B),Pred) :- compute_bin_op_equal(A,B,Pred).

commute_bin_op(greater_equal(A,B),less_equal(B,A)) :- can_be_used_for_lookups(B).

commute_bin_op(greater(A,B),Pred) :- compute_bin_op_less(B,A,Pred).

commute_bin_op(less_equal(A,B),Pred) :- compute_bin_op_less_equal(A,B,Pred).

commute_bin_op(less(A,B),Pred) :- compute_bin_op_less(A,B,Pred).

commute_bin_op(less_real(A,B),not_equal(A,B)). % TO DO: extend

commute_bin_op(subset_strict(A,B),Pred) :- gen_subset(A,B,Pred).

commute_bin_op(subset_strict(A,B),not_equal(A,B)).

commute_bin_op(subset(A,B),superset(B,A)) :- % new operator, for efficient lookups !
    can_be_used_for_lookups(B).

commute_bin_op(not_subset(A,B),not_equal(A,B)). % also implies not_subset_strict

commute_bin_op(member(_,Set),not_equal(Set,empty_set)).

commute_bin_op(member(couple(A,B),C),NewHyp) :-
    ( NewHyp = member(A,domain(C)) % A|->B : C ==> A : dom(C)
    ; NewHyp = member(B,range(C)) ). % A|->B : C ==> B : ran(C)

commute_bin_op(member(X,interval(Low,Up)),NewHyp) :-
    (NewHyp = less_equal(Low,Up) % x : Low..Up => Low <= Up
    ; NewHyp = less_equal(Low,X) % Low <= X if X: Low..UP
    ; can_be_used_for_lookups(X), NewHyp = greater_equal(X,Low)
    ; NewHyp = less_equal(X,Up) % X <= UP if X: Low..UP
    ; can_be_used_for_lookups(Up), NewHyp = greater_equal(Up,X)
).

commute_bin_op(member(X,Rel),NewHyp) :- is_total_relation(Rel,Domain),
    % we cannot efficiently lookup this info from Domain
    can_be_used_for_lookups(Domain),
    NewHyp = equal(Domain,domain(X)).

commute_bin_op(member(X,Rel),NewHyp) :- is_surjective_relation(Rel,Range),
    % we cannot efficiently lookup this info from Range
    can_be_used_for_lookups(Range),
    NewHyp = equal(Range,range(X)).

commute_bin_op(member(card(X),_),NewHyp) :- can_be_used_for_lookups(X),
    NewHyp=finite(X).

commute_bin_op(disjunct(LHS,RHS),NewHyp) :- get_member_pred(LHS,X,A), get_member_pred(RHS,X,B),
    NewHyp = member(X,union(A,B)).

commute_bin_op(disjunct(LHS,RHS),NewHyp) :- get_subset_pred(LHS,X,A), get_subset_pred(RHS,X,B),
    NewHyp = subset(X,union(A,B)).

commute_bin_op(partition(A,List),equal(A,UNION)) :- gen_union(List,UNION).

commute_bin_op(forall(['$'(X)],LHSPred,RHSPred), Pred) :-
    get_member_lhs(LHSPred,'$'(X),Set),
    get_member_rhs(RHSPred,'$'(X),SET2),
    useful_forall_superset(SET2),
    % !x.(x:SET => x:dom(F)) => SET <: dom(F)
    % !x.(x:SET => x:SET2) => SET <: SET2
    not_occurs(Set,X),
    not_occurs(SET2,X), %print(subset1(Set,SET2)),nl,
    gen_subset(Set,SET2,Pred).

commute_bin_op(forall(['$'(X),'$'(Y)],LHSPred,RHSPred), Pred) :- % TO DO: generalise
    get_member_lhs(LHSPred,couple('$'(X),'$'(Y)),Set), %TO DO: generalise -> domain/range
    get_member_rhs(RHSPred,'$'(X),SET2),
    useful_forall_superset(SET2),
    % !x,y.(x|->y:SET => x:dom(F)) => dom(SET) <: dom(F)
    % !x,y.(x|->y:SET => x:SET2) => dom(SET) <: SET2
    not_occurs(Set,X),
    not_occurs(Set,Y),
    not_occurs(SET2,X), %print(subset2(Set,SET2)),nl,
    gen_subset(domain(Set),SET2,Pred).

commute_bin_op(not_equal(A,B),equal(A,NB)) :- negate_boolean_like_value(B,NB).

commute_bin_op(not_equal(intersection(Set1,Set2),empty_set), Pred) :-
    % Set /\ {a} /= {} => a : Set
    (Set1=set_extension([A]),B=Set2 -> true ; Set2=set_extension([A]),B=Set1),
    Pred = member(A,B).

compute_bin_op_equal(A,B,equal(B,A)) :-
    can_be_used_for_lookups(B).

compute_bin_op_equal(A,B,falsity) :- % sometimes we have FALSE=TRUE as an alternative to falsity
    is_explicit_value(A,VA),
    is_explicit_value(B,VB),
    VA \= VB.

compute_bin_op_equal(Set,A,Pred) :-
    % e.g., A = B \ C => A <: B, useful for examples/B/Alstom/etcs/actions_scn_f6_372_bis.mch
    derive_superset(Set,B), B \= A,
    gen_superset(B,A,Pred). % only generate superset rule; for subset there are rules to treat set_subtraction

compute_bin_op_equal(A,Set,Pred) :- % interchange args
    derive_superset(Set,B), B \= A,
    gen_superset(B,A,Pred).

compute_bin_op_equal(A,Set,subset(B,A)) :- % A = B \/ C => B <: A ; useful to allow lookups of B
    derive_subset(Set,B),
    can_be_used_for_lookups(B), B \= A.

compute_bin_op_equal(A,Add,Res) :- is_add_with_nr(Add,B,Nr),
    % A = B+Nr => B < A
    (Nr>0 -> compute_bin_op_less(B,A,Res)
    ; Nr<0 -> compute_bin_op_less(A,B,Res)
    ; Res = equal(A,B)).

compute_bin_op_equal(A,B,finite(X)) :-
    (A=card(X);B=card(X)), can_be_used_for_lookups(X). % actually: if any sub-expression uses card(.) we could add it?

compute_bin_op_less(A,B,less_equal(A,B)).

compute_bin_op_less(A,B,greater_equal(B,A)) :- can_be_used_for_lookups(B). % we do not lookup greater

compute_bin_op_less(A,B,not_equal(A,B)). % for not_equal we only need to store one direction

compute_bin_op_less(card(X),_,finite(X)) :- can_be_used_for_lookups(X). % actually card(X)>1 also implies finite(X)

compute_bin_op_less_equal(A,B,greater_equal(B,A)) :- can_be_used_for_lookups(B).

compute_bin_op_less_equal(card(X),_,finite(X)) :- can_be_used_for_lookups(X).

convert_norm_expr_to_raw('$'(ID),Res) :- !, Res=identifier(unknown,ID).

convert_norm_expr_to_raw(Int,Res) :- integer(Int),!,Res=integer(unknown,Int).

convert_norm_expr_to_raw(Nr,Res) :- float(Nr),!,Res=real(unknown,Nr).

convert_norm_expr_to_raw(set_extension(List),Res) :- !,
    Res = set_extension(unknown,RList),
    l_convert_norm(List,RList).

convert_norm_expr_to_raw(sequence_extension(List),Res) :- !,
    Res = sequence_extension(unknown,RList),
    l_convert_norm(List,RList).

convert_norm_expr_to_raw(Term,Res) :- Term =.. [Functor|Args],
    l_convert_norm(Args,RawArgs),
    Res =.. [Functor,unknown|RawArgs].

copy_hyp_variables(hyp_rec(NH,HInfos1),ExistingVars,Hyp2) :-
    fetch_hyp_typed_vars(HInfos1,TVars),
    list_to_ord_set(ExistingVars,SortedIds),
    get_existing_tids(SortedIds,TVars,ResTVars),
    add_new_hyp_variables(hyp_rec(NH,HInfos1),ResTVars,Hyp2).

create_any_type($(ID),b(identifier(ID),any,[])).

create_negation_aux(truth,I,R) :- !, R=b(falsity,pred,I).

create_negation_aux(falsity,I,R) :- !, R=b(truth,pred,I).

create_negation_aux(disjunct(A,B),I,R) :- !,
    negate_hyp(A,NA), negate_hyp(B,NB), R = b(conjunct(NA,NB),pred,I).

create_negation_aux(implication(A,B),I,R) :- !, % not(A=>B) <===> A & not(B)
    negate_hyp(B,NB), R = b(conjunct(A,NB),pred,I).

create_negation_aux(negation(Pred),_,R) :- !, R=Pred.

create_negation_aux(BOP,I,R) :- negate_op_aux(BOP,NBOP), R=b(NBOP,pred,I).

derive_subset(union(B,_),B). % B <: B \/ C

derive_subset(union(_,C),C). % C <: B /\ C

derive_superset(set_subtraction(B,_),B). % B \ C <: B

derive_superset(intersection(B,_),B). % B /\ C <: B

derive_superset(intersection(_,C),C). % B /\ C <: C

empty_hyps(hyp_rec(E,HI2)) :- empty_avl(E),
    avl_store(hyp_typed_vars,E,[],HI1), % typed variables of the hypotheses (implicitly universally quantified)
    avl_store(hyp_clash_vars,HI1,clash_rec(0,E),HI2). % variables which are currently in clash

fetch_hyp_typed_vars(HInfos,Vars) :-
    avl_fetch(hyp_typed_vars,HInfos,Vars).

fetch_hyp_vars(HInfos,Vars) :- avl_fetch(hyp_typed_vars,HInfos,TVars),
    def_get_texpr_ids(TVars,Vars).

gen_subset(A,B,subset(A,B)) :- can_be_used_for_lookups(A).

gen_subset(A,B,superset(B,A)) :- can_be_used_for_lookups(B).

gen_superset(A,B,superset(A,B)) :- can_be_used_for_lookups(A).

gen_union([],emptyset).

gen_union([X],R) :- !, R=X.

gen_union([X|T],union(X,UT)) :- gen_union(T,UT).

get_aux([],ID,_,Res) :- add_internal_error('Cannot find existing hyp variable:',ID), Res=[].

get_aux([TID|TT],ID,TI,Res) :-
    (get_texpr_id(TID,ID) -> Res=[TID|ResT], get_existing_tids(TI,TT,ResT)
    ; get_aux(TT,ID,TI,Res)
).

get_clash_renaming(HInfos,Renamings) :- avl_fetch(hyp_clash_vars,HInfos,clash_rec(_,AVL)),
    findall(rename(ID,FreshID), avl_member(ID,AVL,FreshID), Renamings).

get_clash_renaming_subst(hyp_rec(_,HInfos),ClashRenaming) :- !,
    get_clash_renaming(HInfos,ClashRenaming).

get_clash_renaming_subst(H,R) :- add_internal_error('Illegal hyps:',get_clash_renaming_subst(H,R)),fail.

get_clashed_vars(HInfos,Vars) :- avl_fetch(hyp_clash_vars,HInfos,clash_rec(_,AVL)),
    avl_domain(AVL,Vars).

get_existing_tids([],_,[]).

get_existing_tids([ID|TI],TIDs,Res) :- get_aux(TIDs,ID,TI,Res).

get_hyp_var_type(Var,hyp_rec(_,HInfos),Type) :- atomic(Var),!,
    fetch_hyp_typed_vars(HInfos,TVars),
    TVar = b(identifier(Var),Type,_),
    ord_member_nonvar_chk(TVar,TVars).

get_hyp_var_type(V,H,T) :- add_internal_error('Illegal call: ',is_hyp_var_type(V,H,T)),fail.

get_hyp_vars(hyp_rec(_,HInfos),Res) :- get_hyp_vars(HInfos,Vars),!,Res=Vars.

get_hyp_vars(H,R) :- add_internal_error('Illegal hyps: ',get_hyp_vars(H,R)), R=[].

get_member_lhs(member(X,Set),X,Set).

get_member_lhs(truth,_,typeset).

get_member_pred(member(X,A),X,A).

get_member_pred(equal(X,A),X,set_extension([A])).

get_member_pred(equal(A,X),X,set_extension([A])).

get_member_pred(disjunct(LHS,RHS),X,union(A,B)) :- get_member_pred(LHS,X,A), get_member_pred(RHS,X,B).

get_member_rhs(member(X,Set),X,Set).

get_member_rhs(conjunct(A,B),X,Set) :- get_member_rhs(A,X,Set) ; get_member_rhs(B,X,Set).

get_member_rhs(not_equal(empty_set,X),X,pow1_subset(typeset)).

get_member_rhs(not_equal(X,empty_set),X,pow1_subset(typeset)).

get_member_rhs(finite(X),X,fin_subset(typeset)).

get_normalized_and_renamed_predicate(Pred,Hyps,RenPred,NormPred) :-
    get_clash_renaming_subst(Hyps,ClashRenaming),
    normalize_and_rename_predicate(ClashRenaming,Pred,RenPred,NormPred).

get_renamed_expression(Expr,Hyps,RenExpr) :-
    get_clash_renaming_subst(Hyps,ClashRenaming),
    rename_bt(Expr,ClashRenaming,RenExpr).

get_subset_pred(subset(X,A),X,A).

get_subset_pred(subset_strict(X,A),X,A).

get_subset_pred(disjunct(LHS,RHS),X,union(A,B)) :- get_subset_pred(LHS,X,A), get_subset_pred(RHS,X,B).

hyp_portray_hook(X) :- nonvar(X), X= hyp_rec(AVL,HInfos),
    avl_size(AVL,Size),
    avl_size(HInfos,ISize),
    format('hyp_rec(#~w,#~w)',[Size,ISize]).

install_hyp_portray_hook :- % mainly for the Prolog debugger
    assertz(( user:portray(X) :- well_def_hyps:hyp_portray_hook(X) )).

is_add_with_nr(add(A,B),X,Nr) :- (number(B) -> (X,Nr)=(A,B) ; number(A) -> (X,Nr)=(B,A)).

is_add_with_nr(minus(A,B),A,Nr) :- number(B), Nr is -B.

is_empty_set_alternative(empty_sequence).

is_empty_set_alternative(value(V)) :- V==[]. % should now be handled in norm_expr / norm_value

is_explicit_value(boolean_true,pred_true).

is_explicit_value(boolean_false,pred_false).

is_explicit_value(string(A),A).

is_explicit_value(Nr,Nr) :- number(Nr).

is_finite_type_for_wd(Type,_) :-
    get_preference(wd_analysis_for_animation,true),!,
    is_finite_type_in_context(animation,Type).

is_finite_type_for_wd(Type,_Hyps) :-
    is_finite_type_in_context(proving,Type).

is_hyp_var(Var,hyp_rec(_,HInfos)) :- atomic(Var), nonvar(HInfos),!,
    fetch_hyp_vars(HInfos,Vars),
    ord_member(Var,Vars).

is_hyp_var(V,H) :- add_internal_error('Illegal call: ',is_hyp_var(V,H)),fail.

is_surjective_relation(partial_surjection(_,B),B).

is_surjective_relation(surjection_relation(_,B),B).

is_surjective_relation(total_surjection(_,B),B).

is_surjective_relation(total_bijection(_,B),B).

is_surjective_relation(total_surjection_relation(_,B),B).

is_surjective_relation(perm(B),B).

is_total_relation(total_function(A,_),A).

is_total_relation(total_injection(A,_),A).

is_total_relation(total_surjection(A,_),A).

is_total_relation(total_bijection(A,_),A).

is_total_relation(total_surjection_relation(A,_),A).

l_avl_store_nhyps([],NHyps,_,NHyps).

l_avl_store_nhyps([NH1|TNH],NHyps1,RenH,NHyps3) :-
    avl_store_if_new(NH1,NHyps1,RenH,NHyps2),
    l_avl_store_nhyps(TNH,NHyps2,RenH,NHyps3).

l_convert_norm([],[]).

l_convert_norm([H|T],[RH|RT]) :- convert_norm_expr_to_raw(H,RH), l_convert_norm(T,RT).

negate_boolean_like_value(boolean_true,boolean_false).

negate_boolean_like_value(boolean_false,boolean_true).

negate_hyp(b(P,pred,I),Res) :- create_negation_aux(P,I,R),!,Res=R.

negate_hyp(Pred,b(negation(Pred),pred,Infos)) :-
    extract_info(Pred,Infos).

negate_op(truth,falsity).

negate_op(falsity,truth).

negate_op(equal(A,B),not_equal(A,B)).

negate_op(not_equal(A,B),equal(A,B)).

negate_op(less(A,B),less_equal(B,A)).

negate_op(greater(A,B),less_equal(A,B)).

negate_op(less_equal(A,B),less(B,A)).

negate_op(greater_equal(A,B),less(A,B)).

negate_op(less_real(A,B),less_equal_real(B,A)).

negate_op(less_equal_real(A,B),less_real(B,A)).

negate_op(negation(P),P).

negate_op(not_member(A,B),member(A,B)).

negate_op(member(A,B),not_member(A,B)). % should we do this?

negate_op(not_subset(A,B),subset(A,B)).

negate_op(subset(A,B),not_subset(A,B)).

negate_op(not_subset_strict(A,B),subset_strict(A,B)).

negate_op(subset_strict(A,B),not_subset_strict(A,B)).

negate_op_aux(equal(A,B),not_equal(A,B)).

negate_op_aux(not_equal(A,B),equal(A,B)).

negate_op_aux(less(A,B),greater_equal(A,B)).

negate_op_aux(less_equal(A,B),greater(A,B)).

negate_op_aux(greater(A,B),less_equal(A,B)).

negate_op_aux(greater_equal(A,B),less(A,B)).

norm_aux(equal(Val,'$'(ID)),Res) :- Val \= '$'(_), !, Res=equal('$'(ID),Val).

norm_aux(greater(Val,Nr),greater_equal(Val,N1)) :- integer(Nr),!, N1 is Nr+1.

norm_aux(greater(Nr,Val),greater_equal(N1,Val)) :- integer(Nr),!, N1 is Nr-1.

norm_aux(greater(A,B),less(B,A)) :- !. % we only look up less (when both args are known)

norm_aux(less(Val,Nr),less_equal(Val,N1)) :- integer(Nr),!, N1 is Nr-1.

norm_aux(less(Nr,Val),less_equal(N1,Val)) :- integer(Nr),!, N1 is Nr+1.

norm_aux(not_equal(Val,EMPTY),not_equal(Val,empty_set)) :- is_empty_set_alternative(EMPTY),!.

norm_aux(not_equal(EMPTY,Val),not_equal(Val,empty_set)) :- is_empty_set_alternative(EMPTY),!.

norm_aux(negation(Pred),NormPred) :- negate_op(Pred,NP),!, norm_aux(NP,NormPred).

norm_aux(implication(Pred1,Pred2),implication(NormPred1,NormPred2)) :- !,
    norm_aux(Pred1,NormPred1),norm_aux(Pred2,NormPred2).

norm_aux(V,V).

normalize_and_rename_predicate(_,H,_,_) :- var(H),!,
    add_internal_error('Unbound predicate: ',normalize_and_rename_predicate(H)),fail.

normalize_and_rename_predicate([],H,RenH,NH) :- !, RenH=H,
    normalize_predicate(H,NH).

normalize_and_rename_predicate(ClashRenaming,H,RenH,NH) :- !,
    %format('Rename Hyp: ~w ',[ClashRenaming]),translate:print_bexpr(H),nl,
    rename_bt(H,ClashRenaming,RenH),
    %print(' > renamed Hyp: '),translate:print_bexpr(RenH),nl,
    normalize_predicate(RenH,NH).

normalize_predicate(Pred,NormPred) :-
    b_interpreter_check:norm_pred_check(Pred,NP),
    norm_aux(NP,NormPred).

portray_hyp_vars(hyp_rec(_,HInfos)) :- fetch_hyp_typed_vars(HInfos,TVars),!,
    length(TVars,Len),
    format('Typed vars in hyps (~w):~n',[Len]),
    maplist(print_tvar,TVars).

portray_hyp_vars(H) :- !, format('** ILLEGAL Hypotheses: ~w~n',[H]).

portray_hyps(hyp_rec(AVL,HInfos)) :- fetch_hyp_vars(HInfos,Vars),
    get_clashed_vars(HInfos,CVars),
    (debug_mode(on) -> portray_hyp_vars(hyp_rec(AVL,HInfos)),nl ; true),
    %b_global_sets:portray_global_sets,
    !,
    format('Hypotheses over ~w (clashes: ~w):~n',[Vars,CVars]),
    %avl_domain(AVL,D), lists:maplist(well_def_hyps:println_nhyp,D),
    avl_range(AVL,Hyp),
    conjunct_predicates(Hyp,HypC),
    translate:nested_print_bexpr(HypC),nl,nl.

portray_hyps(H) :- !, format('** ILLEGAL Hypotheses: ~w~n',[H]).

potentially_useful_for_hyp_rule(less(_,_)).

potentially_useful_for_hyp_rule(less_real(_,_)).

potentially_useful_for_hyp_rule(not_subset(_,_)).

potentially_useful_for_hyp_rule(not_subset_strict(_,_)).

potentially_useful_for_hyp_rule(subset_strict(_,_)).

potentially_useful_for_hyp_rule(partition(_,_)).

print_tvar(b(identifier(ID),Type,_)) :- format(' ~w : ~w~n',[ID,Type]).

propagate_implications([],_,Hyps,Hyps).

propagate_implications([NRHS|TR],NLHS,NHyps1,NHyps4) :-
    %write(trigger_implication(NRHS)),nl, %trace,
    (avl_delete(implication(NLHS,NRHS),NHyps1,TE,NHyps2)
    -> %translate:print_bexpr(TE),nl,
    (TE=b(implication(_,RHS),_,_) -> true
    ; NHyps2=NHyps1, RHS = b(unknown,pred,[trigger_implication]),
    add_warning(wd_prover,'Unexpected un-normalised hyp: ',TE)
    ),
    avl_store_with_commutes_if_new(NRHS,NHyps2,RHS,NHyps3)
    ; % implication has already been triggered by processing a previous NRHS in the list
    NHyps3=NHyps1
    ),
    propagate_implications(TR,NLHS,NHyps3,NHyps4).

propagate_resolution_with_hyp(NormHyp,Hyps,H2) :- negate_op(NormHyp,NegNH),
    norm_aux(NegNH,NegNormHyp),
    avl_fetch(NegNormHyp,Hyps),!,
    debug_println(9,contradiction_found_in_hypotheses(NormHyp)),
    avl_store(falsity,Hyps,b(falsity,pred,[neg_hyp]),H2). % false_hyp rule can later trigger

propagate_resolution_with_hyp(NH,Hyps,H2) :- % write(fetch_impl),nl, avl_domain(Hyps,D), write(d(D)),nl,
    findall(NRHS,avl_fetch_bin(NH,implication,Hyps,NRHS),TriggeredImplications),
    propagate_implications(TriggeredImplications,NH,Hyps,H2).

push_commutative_hyps(NH,RenH,NHyps1,NHyps2) :-
    commute_bin_op(NH,_), % somehow faster than using findall directly
    !,
    findall(NH3,commute_bin_op(NH,NH3),NH3s),
    %length(NH3s,Len),hit_profiler:add_profile_hit(hyp(NH,Len)),
    l_avl_store_nhyps(NH3s,NHyps1,RenH,NHyps2).

push_commutative_hyps(_,_,NHyps,NHyps).

push_hyp(Hyps,H,Options,NewHyps) :-
    check_valid_hyp_rec(Hyps,push_hyp),
    conjunction_to_list(H,Hs),
    push_hyps(Hyps,Hs,Options,NewHyps).

push_hyp_aux(Hyps,_,_,_,_) :- var(Hyps),!, add_internal_error('Unbound hyps: ',push_hyps(Hyps)),fail.

push_hyp_aux([],_,_,NH,NH).

push_hyp_aux([H|T],ClashRenaming,Options,NHyps,NewNHyps) :-
    ((var(NHyps) ; NHyps=hyp_rec(_,_)) -> add_internal_error('Illegal AVL: ',NHyps),fail ; true),
    push_individual_hyp(H,ClashRenaming,Options,NHyps,NHyps3),
    push_hyp_aux(T,ClashRenaming,Options,NHyps3,NewNHyps).

push_hyps(hyp_rec(NHyps,HInfos),Hs,Options,hyp_rec(NewNHyps,HInfos)) :- !,
    get_clash_renaming(HInfos,ClashRenaming),
    push_hyp_aux(Hs,ClashRenaming,Options,NHyps,NewNHyps).

push_hyps(A,B,C,D) :- add_internal_error('Illegal call: ', push_hyps(A,B,C,D)),fail.

push_hyps_wo_renaming(hyp_rec(NHyps,HInfos),Hs,Options,hyp_rec(NewNHyps,HInfos)) :- !, ClashRenaming=[],
    push_hyp_aux(Hs,ClashRenaming,Options,NHyps,NewNHyps).

push_hyps_wo_renaming(A,B,C,D) :- add_internal_error('Illegal call: ', push_hyps(A,B,C,D)),fail.

push_individual_hyp(b(conjunct(H1,H2),_,_),ClashRenaming,Options,NHyps,NHyps3) :- !,
    push_individual_hyp(H1,ClashRenaming,Options,NHyps,NHyps2),
    push_individual_hyp(H2,ClashRenaming,Options,NHyps2,NHyps3).

push_individual_hyp(H,ClashRenaming,Options,NHyps,NHyps3) :-
    normalize_and_rename_predicate(ClashRenaming,H,RenH,NH),
    % print('PUSH: '),nl, debug:print_quoted_with_max_depth(NH,6), print(' '), error_manager:print_message_span(H),nl,
    push_normalized_hyp_aux(NH,RenH,Options,NHyps,NHyps3).

push_normalized_hyp_aux(NH,RenH,Options,NHyps,NHyps2) :-
    ((useful_hyp(NH) ; safe_ord_member(create_full_po,Options)
    ; potentially_useful_for_hyp_rule(NH), safe_ord_member(push_more_hyps,Options)
    ; useful_implication(NH),
    true %safe_ord_member(push_more_hyps,Options) % seems useful for Event-B benchmark models, enable by default?
    )
    -> avl_store_with_commutes_if_new(NH,NHyps,RenH,NHyps2)
    ; push_commutative_hyps(NH,RenH,NHyps,NHyps2)
% hypothesis not directly used by prover, but there could be alternatives e.g., for disjunct
%,functor(NH,FF,NN), print(not_pushing(FF,NN)),nl
).

ren_clash_variables([],[],C,C,Avl,Avl).

ren_clash_variables([b(identifier(ID1),Type1,I1)|T1],
    [b(identifier(RenamedID),Type1,[was(ID1)|I1])|T2], Cin,Cout,AvlIn,AvlOut) :-
    number_codes(Cin,NC), atom_codes(Ain,NC),
    atom_concat('$wd_rename_',Ain,RenamedID), % print(rename(ID,RenamedID)),nl,
    C1 is Cin+1,
    avl_store(ID1,AvlIn,RenamedID,Avl2),
    ren_clash_variables(T1,T2,C1,Cout,Avl2,AvlOut).

safe_ord_member(El,List) :- var(List),!, add_internal_error('Illegal call: ',safe_ord_member(El,List)),fail.

safe_ord_member(El,List) :- ord_member(El,List).

translate_norm_expr_with_limit(NormExpr,Limit,Str) :-
    (convert_norm_expr_to_raw(NormExpr,RawExpr)
    -> translate_raw_bexpr_with_limit(RawExpr,Limit,Str)
    ; add_error(translate_norm_expr,'Cannot translate norm expression:',NormExpr),
    Str = '???'
).

useful_forall_superset(domain(_)).

useful_forall_superset(range(_)).

useful_forall_superset(finite(_)).

useful_forall_superset(seq(_)).

useful_forall_superset(seq1(_)).

useful_forall_superset(iseq(_)).

useful_forall_superset(iseq1(_)).

useful_forall_superset(perm(_)).

useful_forall_superset(partial_function(_,_)).

useful_forall_superset(total_function(_,_)).

useful_forall_superset(total_injection(_,_)).

useful_forall_superset(total_surjection(_,_)).

useful_forall_superset('$'(_)).

useful_forall_superset(pow1_subset(_)). % not empty

useful_forall_superset(fin1_subset(_)). % not empty and finite

useful_forall_superset(fin_subset(_)). % finite info

useful_hyp(finite(_)).

useful_hyp(member(_,_)).

useful_hyp(subset(_,_)).

useful_hyp(equal(_,_)).

useful_hyp(greater_equal(_,_)).

useful_hyp(less_equal(_,_)).

useful_hyp(less_equal_real(_,_)).

useful_hyp(not_equal(_,_)).

useful_hyp(not_member(_,_)). % used in check_not_member_of_set

useful_implication(implication(_,RHS)) :-
    (useful_hyp(RHS) -> true ; useful_implication(RHS)). % useful upon pushing hyps in propagate_resolution_with_hyp