subtree_compare

add_st_error(MissingClause) :-
    (retract(errors(X)) -> true ; X=[]),
    assertz(errors([MissingClause|X])).

build_map_list([], [], []).

build_map_list([b(identifier(X),Type,_)|T1], [X-F|T2], [b(identifier(F),Type,_)|T3]) :-
    build_map_list(T1,T2, T3).

expressions(b(identifier(op(_)), Type, _), b(identifier(op(_)), Type, _), Before, Before) :- !.

expressions(b(identifier(Val), Type, _), b(identifier(PVal), Type, _), Before, After) :- !,
    (lookup(Val, Before, PVal)-> After=Before; insert(Val, PVal, Before, After)).

expressions(b(identifier(Val)), b(identifier(PVal)), Before, After) :- !,
    (lookup(Val, Before, PVal)-> After=Before; insert(Val, PVal, Before, After)).

expressions(b(unary_minus(Exp), Type,_), b(unary_minus(PExp), Type,_), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(integer(Val), Type, _ ), b(integer(Val), Type, _), Before, Before ) :- !.

expressions(b(boolean_false, Type, _), b(boolean_false, Type, _), Before, Before).

expressions(b(boolean_true, Type, _), b(boolean_true, Type, _), Before, Before).

expressions(b(min_int, Type, _), b(min_int, Type, _), Before, Before).

expressions(b(max_int, Type, _), b(max_int, Type, _), Before, Before).

expressions(b(integer_set(Var), Type, _), b(integer_set(Var), Type, _), Before, Before).

expressions(b(interval(A, B), Type, [was(integer_set('NAT')),_]),
    b(interval(NewA, NewB), Type, [was(integer_set('NAT')),_]), Before, Before) :-
    expressions(A, NewA, _,_),
    expressions(B, NewB, _,_).

expressions(b(interval(A, B), Type, [was(integer_set('INT')),_]),
    b(interval(NewA, NewB), Type, [was(integer_set('INT')),_]), Before, Before) :-
    expressions(A, NewA, _,_),
    expressions(B, NewB, _,_).

expressions(b(bool_set,Type,_), b(bool_set,Type,_), Before, Before).

expressions(b(set_extension(SetElements), Type, _), b(set_extension(PSetElements), Type, _), Before, After) :-
    process_all_expressions(SetElements, PSetElements, Before, After).

expressions(b(relations(Left, Right), Type, _), b(relations(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(couple(Left, Right), Type , _), b(couple(PLeft, PRight), Type , _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(union(Left, Right), Type, Info), b(union(PLeft, PRight), Type, Info), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(event_b_identity, _, _), b(event_b_identity, _, _), Before, Before).

expressions(b(total_function(From, To), Type, _), b(total_function(PFrom, PTo), Type, _), Before, After) :-
    handle_binary_exp(From, To, PFrom, PTo, Before, After).

expressions(b(partial_function(From, To), Type, _), b(partial_function(PFrom, PTo), Type, _), Before, After) :-
    handle_binary_exp(From, To, PFrom, PTo, Before, After).

expressions(b(total_injection(From, To), Type, _), b(total_injection(PFrom, PTo), Type, _), Before, After) :-
    handle_binary_exp(From, To, PFrom, PTo, Before, After).

expressions(b(partial_injection(From, To), Type, _), b(partial_injection(PFrom, PTo), Type, _), Before, After) :-
    handle_binary_exp(From, To, PFrom, PTo, Before, After).

expressions(b(total_surjection(From, To), Type, _), b(total_surjection(PFrom, PTo), Type, _), Before, After) :-
    handle_binary_exp(From, To, PFrom, PTo, Before, After).

expressions(b(partial_surjection(From, To), Type, _), b(partial_surjection(PFrom, PTo), Type, _), Before, After) :-
    handle_binary_exp(From, To, PFrom, PTo, Before, After).

expressions(b(total_bijection(From, To), Type, _), b(total_bijection(PFrom, PTo), Type, _), Before, After) :-
    handle_binary_exp(From, To, PFrom, PTo, Before, After).

expressions(b(partial_bijection(Left, Right), Type, _), b(partial_bijection(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(interval(Left, Right), Type, _), b(interval(PLeft, PRight), Type, _), Before,After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(add(Left, Right), Type, _), b(add(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(minus(Left, Right), Type, _), b(minus(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(Left div Right, Type, _), b(PLeft div PRight, Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(multiplication(Left, Right), Type, _), b(multiplication(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(modulo(Left, Right), Type, _), b(modulo(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(set_subtraction(Left, Right), Type, _), b(set_subtraction(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(intersection(Left, Right), Type, _), b(intersection(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(direct_product(Left, Right), Type, _), b(direct_product(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(composition(Left,Right), Type, _), b(composition(PLeft,PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(cartesian_product(Left, Right), Type, _), b(cartesian_product(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(concat(Left, Right), Type, _), b(concat(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(domain_restriction(Left, Right), Type, _), b(domain_restriction(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(domain_subtraction(Left, Right), Type, _), b(domain_subtraction(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(range_restriction(Left, Right), Type, _), b(range_restriction(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(range_subtraction(Left, Right), Type, _), b(range_subtraction(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(restrict_tail(Left, Right), Type, _), b(restrict_tail(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(restrict_front(Left, Right), Type, _), b(restrict_front(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(function(Left, Right), Type, _), b(function(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(overwrite(Left, Right), Type, _), b(overwrite(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(parallel_product(Left, Right), Type, _), b(parallel_product(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(image(Left, Right), Type, _), b(image(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(first_of_pair(Exp), _, _), b(first_of_pair(PExp), _, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(second_of_pair(Exp), _, _), b(first_of_pair(PExp), _, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(iteration(Left, Right), Type, _), b(iteration(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Right, PLeft, PRight, Before, After).

expressions(b(range(Exp), Type, _), b(range(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(domain(Exp), Type, _), b(domain(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(card(Exp), Type, _), b(card(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(reflexive_closure(Exp), Type, _), b(reflexive_closure(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(closure(Exp), Type, _), b(closure(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(min(Exp), Type, _), b(min(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(max(Exp), Type, _), b(max(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(pow_subset(Exp), Type, _), b(pow_subset(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(pow1_subset(Exp), Type, _), b(pow1_subset(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(fin_subset(Exp), Type, _), b(fin_subset(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(fin1_subset(Exp), Type, _), b(fin1_subset(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(general_concat(Exp), Type, _), b(general_concat(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(first(Exp), Type, _), b(first(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(last(Exp), Type, _), b(last(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(front(Exp), Type, _), b(front(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(tail(Exp), Type, _), b(tail(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(identity(Exp), Type, _), b(identity(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(reverse(Exp), Type, _), b(reverse(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(rev(Exp), Type, _), b(rev(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(size(Exp), Type, _), b(size(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(convert_bool(Pred), Type, _), b(convert_bool(PPred), Type, _), Before, After) :-
    predicates(Pred, PPred, Before, After).

expressions(b(let_expression(Variables, SubValues, Expression), Type, _), b(let_expression(PVariables, PSubValues, PExpression), Type, _), Before, After) :-
    process_all_expressions(Variables, PVariables, [], LetAfter),
    append(Before, LetAfter, BeforeWithLet),
    process_all_predicates(SubValues, PSubValues, BeforeWithLet, After1),
    expressions(Expression, PExpression, After1, After2),
    keys_and_values(LetAfter, LetKeys,_),
    maplist(remove_key, LetKeys, After2, After).

expressions(b(empty_set, Type, _), b(empty_set, Type, _), Before, Before).

expressions(b(empty_sequence, seq(Type), _), b(empty_sequence, seq(Type), _), Before, Before).

expressions(b(surjection_relation(S, T), Type, _), b(surjection_relation(PS, PT), Type, _), Before, After) :-
    handle_binary_exp(S, T, PS, PT, Before, After).

expressions(b(total_relation(S, T), Type, _), b(total_relation(PS, PT), Type, _), Before, After) :-
    handle_binary_exp(S, T, PS, PT, Before, After).

expressions(b(total_surjection_relation(S, T), Type, _), b(total_surjection_relation(PS, PT), Type, _), Before, After) :-
    handle_binary_exp(S, T, PS, PT, Before, After).

expressions(b(record_field(Expr, Id), Type, _), b(record_field(PExpr, PId), Type, _), Before, After) :-
    expressions(Expr, PExpr, Before, After1),
    expressions(Id, PId, After1, After).

expressions(b(rec(Fields), Type, _), b(rec(PFields), Type, _), Before, After) :-
    process_all_expressions(Fields, PFields, Before, After).

expressions(field(Label, Carrier), field(Label, PCarrier), Before, After) :-
    expressions(Carrier, PCarrier, Before, After).

expressions(b(struct(Exp), Type, _), b(struct(PExp), Type, _), Before, After) :-
    process_all_expressions(Exp, PExp, Before, After).

expressions(b(seq(Exp), Type, _), b(seq(PExp), Type, _), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(b(insert_tail(Left, Rigth), Type, _), b(insert_tail(PLeft, PRigth), Type, _), Before, After) :-
    handle_binary_exp(Left, Rigth, PLeft, PRigth, Before, After).

expressions(b(insert_front(Left, Rigth), Type, _), b(insert_front(PLeft, PRight), Type, _), Before, After) :-
    handle_binary_exp(Left, Rigth, PLeft, PRight, Before, After).

expressions(b(general_sum(IdList, Pred, Result), Type, _), b(general_sum(PIdList, PPred, PResult), Type, _), Before, After) :-
    handle_quantified_set_exp(IdList, Pred, Result, PIdList, PPred, PResult, Before, After).

expressions(b(general_product(IdList, Pred, Result), Type, _), b(general_product(PIdList, PPred, PResult), Type, _), Before, After) :-
    handle_quantified_set_exp(IdList, Pred, Result, PIdList, PPred, PResult, Before, After).

expressions(b(general_union(Set), Type, _), b(general_union(PSet), Type, _), Before, After) :-
    expressions(Set, PSet, Before, After).

expressions(b(general_intersection(Set), Type, _), b(general_intersection(PSet), Type, _), Before, After) :-
    expressions(Set, PSet, Before, After).

expressions(b(comprehension_set(VarList, Predicate), Type, _), b(comprehension_set(PVarList, PPredicate), Type, _), Before, After) :-
    process_all_expressions(VarList, PVarList, Before, After1),
    predicates(Predicate, PPredicate, After1, After).

expressions(b(operation_call_in_expr(Id,Paras),_,_), b(operation_call_in_expr(PId,PParas),_,_), Before, After) :- !,
    expressions(Id, PId, Before, After1),
    process_all_expressions(Paras, PParas, After1, After).

expressions(set(Exp), set(PExp), Before, After) :-
    expressions(Exp, PExp, Before, After).

expressions(seq(Exp), seq(PExp), Before, After) :-
    expressions(set(couple(Exp, Exp)), set(couple(PExp, PExp)), Before, After).

expressions(couple(Left, Right), couple(PLeft, PRight), Before, After) :-
    expressions(Left, PLeft, Before, After1),
    expressions(Right, PRight, After1, After).

expressions(empty_set,empty_set, Before, Before).

expressions(X, _,_,_) :- !, add_st_error(X).

get_st_errors(errors(X)) :-
    (retract(errors(X)) -> true
    ; X = []).

handle_binary_exp(Left, Right, PLeft, PRight, Before, After2) :-
    expressions(Left , PLeft, Before, After1),
    expressions(Right, PRight, After1, After2).

handle_if(b(if_elsif(Condition, Then),_ ,_), b(if_elsif(PCondition, PThen),_ ,_), Before, After) :-
    predicates(Condition, PCondition, Before, After1),
    substitutions(Then, PThen, After1, After).

handle_quantified_set_exp(VarList, Predicate, Expressions, PVarList, PPredicate, PExpression, Before, After) :-
    process_all_expressions(VarList, PVarList, Before, After1),
    predicates(Predicate, PPredicate, After1, After2),
    expressions(Expressions, PExpression, After2, After).

handle_rest([b(if_elsif(b(truth,_,_), Then), _,_)], [b(if_elsif(b(truth,_,_), PThen), _,_)], Before, After) :- !,
    substitutions(Then, PThen, Before, After).

handle_rest([b(if_elsif(Condition, Then), _,_) | Rest], [b(if_elsif(PCondition, PThen), _,_) | PRest], Before, After) :- !,
    predicates(Condition, PCondition, Before, After1),
    substitutions(Then, PThen, After1, After2),
    handle_rest(Rest, PRest, After2, After).

handle_two_expr(Left, Right, PLeft, PRight, Before, After2):-
    expressions(Left , PLeft, Before, After1),
    expressions(Right, PRight, After1, After2).

insert(Var, PVal, [], [Var-PVal]) :- !.

insert(Var, PVal, [H1|T], [Var-PVal, H1|T]).

lookup(Variable, [Variable-VAR|_], VAR):-!.

lookup(Variable, [Variable2-_|T], VAR) :-
    Variable \= Variable2,
    lookup(Variable, T, VAR), !.

predicates(b(conjunct(Left, Right), Type, _), b(conjunct(PLeft, PRight), Type,_), Before, After2) :-
    predicates(Left, PLeft, Before, After1),
    predicates(Right, PRight, After1, After2).

predicates(b(disjunct(Left, Right), Type, _), b(disjunct(PLeft, PRight), Type, _), Before, After2) :-
    predicates(Left, PLeft, Before, After1),
    predicates(Right, PRight, After1, After2).

predicates(b(subset(Left, Right), _, _), b(subset(PLeft, PRight), _, _), Before, After) :-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(not_subset(Left, Right), _, _), b(not_subset(PLeft, PRight), _, _), Before, After) :-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(implication(Left, Right), _, _), b(implication(PLeft, PRight), _, _), Before, After) :-
    process_all_predicates([Left, Right], [PLeft, PRight], Before, After).

predicates(b(equivalence(Left, Right), _,_), b(equivalence(PLeft, PRight), _,_), Before, After) :-
    process_all_predicates([Left, Right], [PLeft, PRight], Before, After).

predicates(b(not_member(Left, Right), _, _), b(not_member(PLeft, PRight), _, _), Before, After) :-
    handle_two_expr(Left, Right,PLeft, PRight, Before, After).

predicates(b(member(Left, Right), _, _), b(member(PLeft, PRight), _, _), Before, After) :-
    handle_two_expr(Left, Right,PLeft, PRight, Before, After).

predicates(b(not_subset_strict(Left, Right), _, _), b(not_subset_strict(PLeft, PRight), _, _), Before, After) :-
    handle_two_expr(Left, Right,PLeft, PRight, Before, After).

predicates(b(subset_strict(Left, Right), _, _), b(subset_strict(PLeft, PRight), _, _), Before, After) :-
    handle_two_expr(Left, Right,PLeft, PRight, Before, After).

predicates(b(greater_equal(Left, Right), _, _), b(greater_equal(PLeft, PRight), _, _), Before, After):-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(less_equal(Left, Right), _, _), b(less_equal(PLeft, PRight), _, _), Before, After):-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(less(Left, Right), Type, _), b(less(PLeft, PRight), Type, _), Before, After):-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(greater(Left, Right), Type, _), b(greater(PLeft, PRight), Type, _), Before, After):-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(equal(Left, Right), _,_), b(equal(PLeft, PRight), _,_), Before, After) :-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(not_equal(Left, Right), _,_), b(not_equal(PLeft, PRight), _,_), Before, After) :-
    handle_two_expr(Left, Right, PLeft, PRight, Before, After).

predicates(b(exists(VarList, Predicate), _, _), b(exists(PLeft, PRight), _, _), Before, After) :-
    handle_two_expr(VarList, Predicate, PLeft, PRight, Before, After).

predicates(b(forall(VarList, Predicate1, Predicate2), _, _), b(forall(PVarList, PPredicate1, PPredicate2), _, _), Before, After) :-
    process_all_expressions(VarList, PVarList, Before, After1),
    predicates(Predicate1, PPredicate1, After1, After2),
    predicates(Predicate2, PPredicate2, After2, After).

predicates(b(truth, TruthType,_),b(truth, TruthType,_),Before,Before).

predicates(b(let_predicate(Variables, SubValues, Predicate), _, _), b(let_predicate(PVariables, PSubValues, PPredicate), _, _), Before, After) :-
    process_all_expressions(Variables, PVariables, [], LetAfter),
    append(Before, LetAfter, BeforeWithLet),
    process_all_predicates(SubValues, PSubValues, BeforeWithLet, After1),
    predicates(Predicate, PPredicate, After1, After2),
    keys_and_values(LetAfter, LetKeys,_),
    maplist(remove_key, LetKeys, After2, After).

predicates(b(negation(Predicate), _,_), b(negation(PPredicate), _,_), Before, After) :-
    predicates(Predicate, PPredicate, Before, After).

predicates(X, _,_,_) :- !, add_st_error(X).

prep_operation(b(operation(Name, OutParas, InParas, Body)),
    b(operation(PName, POutParas, PInParas, PBody)), Substitutions) :-
   
    build_map_list(OutParas, MapOut, POutParas),
    build_map_list(InParas, MapIn, PInParas),
    append(MapIn, MapOut, Paras),
    substitutions(Body, PBody, [Name-PName|Paras], Substitutions).

prep_operation(b(initialisation(Body)), b(initialisation(PBody)), Substitutions) :-
    substitutions(Body, PBody, [], Substitutions).

prepare_operation(Old, Preped, FoundVars, FreeVars, Errors) :-
    prep_operation(Old, Preped, Substitutions),!,
    keys_and_values(Substitutions, FoundVars, FreeVars),
    get_st_errors(Errors).

process_all_expressions([], [], Before, Before).

process_all_expressions([Frist|Rest], [PFirst|PRest], Before, After) :-
    expressions(Frist, PFirst, Before, After1),
    process_all_expressions(Rest, PRest, After1, After).

process_all_predicates([], [], Before, Before).

process_all_predicates([Frist|Rest], [PFirst|PRest], Before, After) :-
    predicates(Frist, PFirst, Before, After1),
    process_all_predicates(Rest, PRest, After1, After).

process_all_substitutions([], [], Before, Before).

process_all_substitutions([Frist|Rest], [PFirst|PRest], Before, After) :-
    substitutions(Frist, PFirst, Before, After1),
    process_all_substitutions(Rest, PRest, After1, After).

remove_key(_, [], []) :- !.

remove_key(Key, [NKey-Val| Rest], NewList) :-
    (Key \= NKey ->
    remove_key(Key, Rest, RestOfNew),
    NewList = [NKey-Val|RestOfNew]
    ; NewList = Rest).

substitutions(b(sequence(List), Type, _), b(sequence(PList), Type, _), Before, After) :-
    process_all_substitutions(List, PList, Before, After).

substitutions(b(select(WhenClauses), Type, _), b(select(PWhenClauses), Type, _), Before, After) :-
    process_all_substitutions(WhenClauses, PWhenClauses, Before, After).

substitutions(b(any(IdentifierList, Predicate, Substitution), Type, _), b(any(PIdentifierList, PPredicate, PSubstitution), Type, _), Before, After) :-
    process_all_expressions(IdentifierList, PIdentifierList, Before, After1),
    predicates(Predicate, PPredicate, After1, After2),
    substitutions(Substitution, PSubstitution, After2, After).

substitutions(b(assertion(Condition, Then), Type, _), b(assertion(PCondition, PThen), Type, _), Before, After2) :-
    predicates(Condition, PCondition, Before, After1),
    substitutions(Then, PThen, After1, After2).

substitutions(b(precondition(Condition, Then), Type,_), b(precondition(PCondition, PThen), Type,_), Before, After2) :-
    predicates(Condition, PCondition, Before, After1),
    substitutions(Then, PThen, After1, After2).

substitutions(b(skip, Type, _), b(skip, Type, _), _, _).

substitutions(b(parallel(Substitutions), _, _), b(parallel(PSubstitutions), _, _), Before, After) :-
    process_all_substitutions(Substitutions, PSubstitutions, Before, After).

substitutions(b(select_when(Condition, Then), _, _), b(select_when(PCondition, PThen), _, _), Before, After) :-
    predicates(Condition, PCondition, Before, After1),
    substitutions(Then, PThen, After1, After).

substitutions(b(assign(Vars, Vals), Type, _), b(assign(PVars, PVals), Type, _), Before, After2) :-
    process_all_expressions(Vars, PVars, Before, After1),
    process_all_expressions(Vals, PVals, After1, After2).

substitutions(b(assign_single_id(Var, Val), Type, _), b(assign_single_id(PVar, PVal), Type, _), Before, After2) :-
    expressions(Var, PVar, Before, After1),
    expressions(Val, PVal, After1, After2).

substitutions(b(choice(Choices), _ ,_), b(choice(PChoices), _ ,_), Before, After) :-
    process_all_substitutions(Choices, PChoices, Before, After).

substitutions(b(becomes_such(Variables, Predicate), _ , _), b(becomes_such(PVariables, PPredicate), _ , _), Before, After) :-
    process_all_expressions(Variables, PVariables, Before, After1),
    predicates(Predicate, PPredicate, After1, After).

substitutions(b(becomes_element_of(Variables, Expression), _ , _), b(becomes_element_of(PVariables, PExpression), _ , _), Before, After) :-
    process_all_expressions(Variables, PVariables, Before, After1),
    expressions(Expression, PExpression, After1, After).

substitutions(b(operation_call(ID, Input, Output), _, _), b(operation_call(PID , PInput, POutput), _, _), Before, After) :-
    expressions(ID, PID, Before, After1),
    process_all_expressions(Input, PInput, After1, After2),
    process_all_expressions(Output, POutput, After2, After).

substitutions(b(let(Variables, Values, Body), _, _), b(let(PVariables, PValues, PBody), _, _), Before, After) :-
    process_all_expressions(Variables, PVariables, [], LetAfter),
    append(Before, LetAfter, BeforeWithLet),
    process_all_predicates(Values, PValues, BeforeWithLet, After1),
    substitutions(Body, PBody, After1, After2),
    keys_and_values(LetAfter, LetKeys,_),
    maplist(remove_key, LetKeys, After2, After).

substitutions(b(if([IF | Rest]), _, _), b(if([PIF | PRest]), _, _), Before, After) :-
    handle_if(IF, PIF, Before, After1),
    (Rest = [] -> !,PRest = [], After = After1;
    !, handle_rest(Rest, PRest, After1, After)).

substitutions(b(while(Condition, Body, Invariant, Variant), _,_), b(while(PCondition, PBody, PInvariant, PVariant), _,_), Before, After) :-
    predicates(Condition, PCondition, Before, After1),
    substitutions(Body, PBody, After1, After2),
    predicates(Invariant, PInvariant, After2, After3),
    expressions(Variant, PVariant, After3, After).

substitutions(b(var(Variables, Body), _, _), b(var(PVariables, PBody), _, _), Before, After) :-
    process_all_expressions(Variables, PVariables, Before, After1),
    substitutions(Body, PBody, After1, After).

substitutions(X,_,_,_) :- !, add_st_error(X).

unpack_operation(ListOfOperation, NamesOfOperations) :-
    unpack_operation_aux(ListOfOperation, NamesOfOperations).

unpack_operation_aux([b(operation(Name, _, _, _))|T], [Name|T1]):-
    unpack_operation_aux(T, T1).

unpack_operation_aux([], []).