rewrite_rule_mandatory(tree(A), set(set(couple(seq(integer),B))), C, [set(B)], comprehension_set([b(identifier(tr),set(couple(seq(integer),B)),[])],b(conjunct(b(conjunct(b(member(b(empty_sequence,seq(integer),[]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(forall([b(identifier(tt),seq(integer),[introduced_by(forall)])],b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(conjunct(b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(seq(b(integer_set('NATURAL1'),set(integer),[])),set(seq(integer)),[])),pred,[]),b(implication(b(not_equal(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(empty_sequence,seq(integer),[])),pred,[]),b(conjunct(b(member(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition]),b(implication(b(greater(b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition]),b(integer(1),integer,[])),pred,[contains_wd_condition]),b(member(b(insert_tail(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(minus(b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition]),b(integer(1),integer,[])),integer,[contains_wd_condition])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[used_ids([tr]),contains_wd_condition])),pred,[contains_wd_condition]),b(subset(b(range(b(identifier(tr),set(couple(seq(integer),B)),[])),set(B),[]),A),pred,[])),pred,[contains_wd_condition])), set(set(couple(seq(integer),B))), [was(tree),prob_annotation('SYMBOLIC')|C], tree).
rewrite_rule_mandatory(btree(A), set(set(couple(seq(integer),B))), C, [set(B)], comprehension_set([b(identifier(tr),set(couple(seq(integer),B)),[])],b(conjunct(b(conjunct(b(member(b(empty_sequence,seq(integer),[]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(forall([b(identifier(tt),seq(integer),[introduced_by(forall)])],b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[]),b(conjunct(b(member(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(seq(b(integer_set('NATURAL1'),set(integer),[])),set(seq(integer)),[])),pred,[]),b(implication(b(not_equal(b(identifier(tt),seq(integer),[introduced_by(forall)]),b(empty_sequence,seq(integer),[])),pred,[]),b(conjunct(b(conjunct(b(member(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition]),b(member(b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition]),b(interval(b(integer(1),integer,[]),b(integer(2),integer,[])),set(integer),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition]),b(member(b(insert_tail(b(front(b(identifier(tt),seq(integer),[introduced_by(forall)])),seq(integer),[contains_wd_condition]),b(minus(b(integer(3),integer,[]),b(last(b(identifier(tt),seq(integer),[introduced_by(forall)])),integer,[contains_wd_condition])),integer,[contains_wd_condition])),seq(integer),[contains_wd_condition]),b(domain(b(identifier(tr),set(couple(seq(integer),B)),[])),set(seq(integer)),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[used_ids([tr]),contains_wd_condition])),pred,[contains_wd_condition]),b(subset(b(range(b(identifier(tr),set(couple(seq(integer),B)),[])),set(B),[]),A),pred,[])),pred,[contains_wd_condition])), set(set(couple(seq(integer),B))), [was(btree),prob_annotation('SYMBOLIC')|C], btree).
rewrite_rule_mandatory(top(A), B, C, [set(couple(seq(integer),B))], function(A,b(empty_sequence,seq(integer),[])), B, [was(top)|C], top).
rewrite_rule_mandatory(rank(A,B), integer, C, [set(couple(seq(integer),_)),seq(integer)], assertion_expression(b(member(B,b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: rank',b(last(B),integer,[contains_wd_condition])), integer, [was(rank)|C], rank).
rewrite_rule_mandatory(father(A,B), seq(integer), C, [set(couple(seq(integer),_)),seq(integer)], assertion_expression(b(member(B,b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: father',b(front(B),seq(integer),[contains_wd_condition])), seq(integer), [was(father)|C], father).
rewrite_rule_mandatory(son(A,B,C), seq(integer), D, [set(couple(seq(integer),_)),seq(integer),integer], assertion_expression(b(conjunct(b(member(B,b(domain(A),set(seq(integer)),[])),pred,[]),b(member(b(insert_tail(B,C),seq(integer),[contains_wd_condition]),b(domain(A),set(seq(integer)),[])),pred,[contains_wd_condition])),pred,[contains_wd_condition]),'WD Error for: son',b(insert_tail(B,C),seq(integer),[contains_wd_condition])), seq(integer), [was(son)|D], son).
rewrite_rule_mandatory(const(A,B), set(couple(seq(integer),C)), D, [C,seq(set(couple(seq(integer),C)))], union(b(general_union(b(range(b(comprehension_set([b(identifier(const_i),integer,[]),b(identifier('_lambda_result_'),set(couple(seq(integer),C)),[lambda_result])],b(conjunct(b(member(b(identifier(const_i),integer,[]),b(domain(B),set(integer),[])),pred,[]),b(equal(b(identifier('_lambda_result_'),set(couple(seq(integer),C)),[lambda_result]),b(domain(b(comprehension_set([b(identifier(pi),seq(integer),[]),b(identifier(a),C,[]),b(identifier(p),seq(integer),[])],b(conjunct(b(member(b(couple(b(identifier(p),seq(integer),[]),b(identifier(a),C,[])),couple(seq(integer),C),[]),b(function(B,b(identifier(const_i),integer,[])),set(couple(seq(integer),C)),[contains_wd_condition])),pred,[contains_wd_condition]),b(equal(b(identifier(pi),seq(integer),[]),b(insert_front(b(identifier(const_i),integer,[]),b(identifier(p),seq(integer),[])),seq(integer),[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),set(couple(couple(seq(integer),C),seq(integer))),[contains_wd_condition])),set(couple(seq(integer),C)),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),set(couple(integer,set(couple(seq(integer),C)))),[contains_wd_condition,generated(quantified_union)])),set(set(couple(seq(integer),C))),[contains_wd_condition,generated(quantified_union)])),set(couple(seq(integer),C)),[contains_wd_condition]),b(set_extension([b(couple(b(empty_sequence,seq(integer),[]),A),couple(seq(integer),C),[])]),set(couple(seq(integer),C)),[])), set(couple(seq(integer),C)), [was(const)|D], const).
rewrite_rule_mandatory(sons(A), seq(set(couple(seq(integer),B))), C, [set(couple(seq(integer),B))], assertion_expression(b(member(b(empty_sequence,seq(integer),[]),b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: sons',b(domain(b(comprehension_set([b(identifier(son_x),integer,[]),b(identifier(r),set(couple(seq(integer),B)),[]),b(identifier(si),seq(integer),[])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(si),seq(integer),[]),b(domain(A),set(seq(integer)),[])),pred,[]),b(not_equal(b(identifier(si),seq(integer),[]),b(empty_sequence,seq(integer),[])),pred,[])),pred,[]),b(equal(b(identifier(son_x),integer,[]),b(first(b(identifier(si),seq(integer),[])),integer,[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition]),b(equal(b(identifier(r),set(couple(seq(integer),B)),[]),b(comprehension_set([b(identifier(p),seq(integer),[]),b(identifier(a),B,[])],b(member(b(couple(b(insert_front(b(identifier(son_x),integer,[]),b(identifier(p),seq(integer),[])),seq(integer),[contains_wd_condition]),b(identifier(a),B,[])),couple(seq(integer),B),[contains_wd_condition]),A),pred,[contains_wd_condition])),set(couple(seq(integer),B)),[contains_wd_condition])),pred,[contains_wd_condition])),pred,[contains_wd_condition])),set(couple(couple(integer,set(couple(seq(integer),B))),seq(integer))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition])), seq(set(couple(seq(integer),B))), [was(sons)|C], sons).
rewrite_rule_mandatory(bin(A), set(couple(seq(integer),B)), C, [B], const(A,b(empty_sequence,seq(set(couple(seq(integer),B))),[])), set(couple(seq(integer),B)), [was(bin)|C], bin).
rewrite_rule_mandatory(bin(A,B,C), set(couple(seq(integer),D)), E, [set(couple(seq(integer),D)),D,set(couple(seq(integer),D))], const(B,b(sequence_extension([A,C]),seq(set(couple(seq(integer),D))),[])), set(couple(seq(integer),D)), [was(bin)|E], bin).
rewrite_rule_mandatory(left(A), set(couple(seq(integer),B)), C, [set(couple(seq(integer),B))], first(b(sons(A),seq(set(couple(seq(integer),B))),[])), set(couple(seq(integer),B)), [was(left)|C], left).
rewrite_rule_mandatory(right(A), set(couple(seq(integer),B)), C, [set(couple(seq(integer),B))], last(b(sons(A),seq(set(couple(seq(integer),B))),[])), set(couple(seq(integer),B)), [was(right)|C], right).
rewrite_rule_mandatory(subtree(A,B), set(couple(seq(integer),C)), D, [set(couple(seq(integer),C)),seq(integer)], composition(b(comprehension_set([b(identifier(u),set(couple(integer,integer)),[]),b(identifier('_lambda_result_'),seq(integer),[lambda_result])],b(equal(b(identifier('_lambda_result_'),seq(integer),[lambda_result]),b(concat(B,b(identifier(u),seq(integer),[])),seq(integer),[contains_wd_condition])),pred,[prob_annotation('LAMBDA'),lambda_result,contains_wd_condition])),set(couple(set(couple(integer,integer)),seq(integer))),[contains_wd_condition]),A), set(couple(seq(integer),C)), [was(subtree)|D], subtree).
rewrite_rule_mandatory(arity(A,B), integer, C, [set(couple(seq(integer),D)),seq(integer)], size(b(sons(b(subtree(A,B),set(couple(seq(integer),D)),[])),seq(set(couple(seq(integer),D))),[])), integer, [was(arity)|C], arity).
rewrite_rule_mandatory(sizet(A), integer, B, [set(couple(seq(integer),_))], assertion_expression(b(member(b(empty_sequence,seq(integer),[]),b(domain(A),set(seq(integer)),[])),pred,[]),'WD Error for: sizet',b(card(A),integer,[contains_wd_condition])), integer, [was(sizet)|B], sizet).
rewrite_rule_mandatory(prefix(A), seq(B), C, [set(couple(seq(integer),B))], function(b(image(
b(closure(
b(comprehension_set(
[b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(identifier(sn),set(couple(integer,B)),[]),b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result])],
b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(sn),set(couple(integer,B)),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(range(A),set(B),[])),set(set(couple(integer,B))),[])),pred,[]),b(not_equal(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])),pred,[])),pred,[]),b(member(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(pow_subset(b(cartesian_product(b(relations(b(integer_set('INTEGER'),set(integer),[]),b(integer_set('INTEGER'),set(integer),[])),set(set(couple(integer,integer))),[]),b(range(A),set(B),[])),set(couple(set(couple(integer,integer)),B)),[])),set(set(couple(set(couple(integer,integer)),B))),[])),set(seq(set(couple(set(couple(integer,integer)),B)))),[])),pred,[])),pred,[]),b(equal(b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result]),b(couple(b(concat(b(sons(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(tail(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),seq(set(couple(seq(integer),B))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(insert_tail(b(identifier(sn),seq(B),[]),b(top(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),B,[contains_wd_condition])),seq(B),[contains_wd_condition])),couple(seq(set(couple(seq(integer),B))),seq(B)),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),
set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),
[contains_wd_condition,prob_annotation('SYMBOLIC')])),set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),[contains_wd_condition]),b(set_extension([b(couple(b(sequence_extension([A]),seq(set(couple(seq(integer),B))),[]),b(empty_sequence,seq(B),[])),couple(seq(set(couple(seq(integer),B))),seq(B)),[])]),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[])),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[contains_wd_condition]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])), seq(B), [was(prefix)|C], prefix).
rewrite_rule_mandatory(postfix(A), seq(B), C, [set(couple(seq(integer),B))], rev(b(function(b(image(b(closure(b(comprehension_set([b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(identifier(sn),set(couple(integer,B)),[]),b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(sn),set(couple(integer,B)),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(range(A),set(B),[])),set(set(couple(integer,B))),[])),pred,[]),b(not_equal(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])),pred,[])),pred,[]),b(member(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[]),b(relations(b(integer_set('INTEGER'),set(integer),[]),b(pow_subset(b(cartesian_product(b(relations(b(integer_set('INTEGER'),set(integer),[]),b(integer_set('INTEGER'),set(integer),[])),set(set(couple(integer,integer))),[]),b(range(A),set(B),[])),set(couple(set(couple(integer,integer)),B)),[])),set(set(couple(set(couple(integer,integer)),B))),[])),set(seq(set(couple(set(couple(integer,integer)),B)))),[])),pred,[])),pred,[]),b(equal(b(identifier('_lambda_result_'),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),[lambda_result]),b(couple(b(concat(b(rev(b(sons(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(tail(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),seq(set(couple(seq(integer),B))),[contains_wd_condition])),seq(set(couple(seq(integer),B))),[contains_wd_condition]),b(insert_tail(b(identifier(sn),seq(B),[]),b(top(b(first(b(identifier(st),seq(set(couple(set(couple(integer,integer)),B))),[])),set(couple(seq(integer),B)),[contains_wd_condition])),B,[contains_wd_condition])),seq(B),[contains_wd_condition])),couple(seq(set(couple(seq(integer),B))),seq(B)),[contains_wd_condition])),pred,[lambda_result,contains_wd_condition])),pred,[prob_annotation('LAMBDA'),contains_wd_condition])),set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),[contains_wd_condition,prob_annotation('SYMBOLIC')])),set(couple(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))),couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B))))),[contains_wd_condition]),b(set_extension([b(couple(b(sequence_extension([A]),seq(set(couple(seq(integer),B))),[]),b(empty_sequence,seq(B),[])),couple(seq(set(couple(seq(integer),B))),seq(B)),[])]),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[])),set(couple(seq(set(couple(set(couple(integer,integer)),B))),set(couple(integer,B)))),[contains_wd_condition]),b(empty_sequence,seq(set(couple(set(couple(integer,integer)),B))),[])),seq(B),[contains_wd_condition])), seq(B), [was(postfix)|C], postfix).
rewrite_rule_mandatory(trans_function(A), set(couple(B,set(C))), D, [set(couple(B,C))], comprehension_set([b(identifier(fnc_x),B,[]),b(identifier('_lambda_result_'),set(C),[lambda_result])],b(conjunct(b(member(b(identifier(fnc_x),B,[]),b(domain(A),set(B),[])),pred,[]),b(equal(b(identifier('_lambda_result_'),set(C),[lambda_result]),b(image(A,b(set_extension([b(identifier(fnc_x),B,[])]),set(B),[])),set(C),[])),pred,[lambda_result])),pred,[prob_annotation('LAMBDA')])), set(couple(B,set(C))), [was(trans_function)|D], trans_function).
rewrite_rule_mandatory(trans_relation(A), set(couple(B,C)), D, [set(couple(B,set(C)))], comprehension_set([b(identifier(rel_x),B,[]),b(identifier(rel_y),C,[])],b(conjunct(b(member(b(identifier(rel_x),B,[]),b(domain(A),set(B),[])),pred,[]),b(member(b(identifier(rel_y),C,[]),b(general_union(b(image(A,b(set_extension([b(identifier(rel_x),B,[])]),set(B),[])),set(set(C)),[])),set(C),[])),pred,[])),pred,[])), set(couple(B,C)), [was(trans_relation)|D], trans_relation).