1		generated(1585845636643,'Thu Apr 02 18:40:36 CEST 2020').
2		project_name('Test').
3		machine_name('BitFunctions').
4		disprover_po('axm2/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,countLeadingZeroesUI4),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI8),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI16),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])]))]),constants(none,[identifier(none,countLeadingZeroesUI4),identifier(none,countLeadingZeroesUI8),identifier(none,countLeadingZeroesUI16)]),sets(none,[])]),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,8))),[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])]))],[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])]))],true).
5		disprover_po('axm3/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,countLeadingZeroesUI4),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI8),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI16),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,8))]),constants(none,[identifier(none,countLeadingZeroesUI4),identifier(none,countLeadingZeroesUI8),identifier(none,countLeadingZeroesUI16)]),sets(none,[])]),conjunct(none,forall(none,[identifier(none,ui)],implication(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),conjunct(none,less_equal(none,integer(none,0),integer(none,8)),conjunct(none,implication(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,integer(none,0),integer(none,4))),implication(none,conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))),conjunct(none,not_equal(none,power_of(none,integer(none,2),integer(none,4)),integer(none,0)),conjunct(none,member(none,div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4))),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))))))),forall(none,[identifier(none,ui)],implication(none,conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1))))),conjunct(none,member(none,identifier(none,ui),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))),[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,8))],[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none)))],true).
6		disprover_po('axm4\n/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,countLeadingZeroesUI4),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI8),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI16),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,8)),equal(none,identifier(none,countLeadingZeroesUI8),union(none,event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),function(none,identifier(none,countLeadingZeroesUI4),[div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4)))])]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))),event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),add(none,integer(none,4),function(none,identifier(none,countLeadingZeroesUI4),[identifier(none,ui)]))]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))))),forall(none,[identifier(none,ui)],implication(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),conjunct(none,less_equal(none,integer(none,0),integer(none,8)),conjunct(none,implication(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,integer(none,0),integer(none,4))),implication(none,conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))),conjunct(none,not_equal(none,power_of(none,integer(none,2),integer(none,4)),integer(none,0)),conjunct(none,member(none,div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4))),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))))))),forall(none,[identifier(none,ui)],implication(none,conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1))))),conjunct(none,member(none,identifier(none,ui),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))]),constants(none,[identifier(none,countLeadingZeroesUI4),identifier(none,countLeadingZeroesUI8),identifier(none,countLeadingZeroesUI16)]),sets(none,[])]),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,16))),[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,8)),equal(none,identifier(none,countLeadingZeroesUI8),union(none,event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),function(none,identifier(none,countLeadingZeroesUI4),[div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4)))])]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))),event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),add(none,integer(none,4),function(none,identifier(none,countLeadingZeroesUI4),[identifier(none,ui)]))]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))))),forall(none,[identifier(none,ui)],implication(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),conjunct(none,less_equal(none,integer(none,0),integer(none,8)),conjunct(none,implication(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,integer(none,0),integer(none,4))),implication(none,conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))),conjunct(none,not_equal(none,power_of(none,integer(none,2),integer(none,4)),integer(none,0)),conjunct(none,member(none,div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4))),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))))))),forall(none,[identifier(none,ui)],implication(none,conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1))))),conjunct(none,member(none,identifier(none,ui),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))],[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),equal(none,identifier(none,countLeadingZeroesUI8),union(none,event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),function(none,identifier(none,countLeadingZeroesUI4),[div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4)))])]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))),event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),add(none,integer(none,4),function(none,identifier(none,countLeadingZeroesUI4),[identifier(none,ui)]))]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1))))))))],true).
7		disprover_po('axm5\n/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,countLeadingZeroesUI4),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI8),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,countLeadingZeroesUI16),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,8)),equal(none,identifier(none,countLeadingZeroesUI8),union(none,event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),function(none,identifier(none,countLeadingZeroesUI4),[div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4)))])]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))),event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),add(none,integer(none,4),function(none,identifier(none,countLeadingZeroesUI4),[identifier(none,ui)]))]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))))),forall(none,[identifier(none,ui)],implication(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),conjunct(none,less_equal(none,integer(none,0),integer(none,8)),conjunct(none,implication(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,integer(none,0),integer(none,4))),implication(none,conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))),conjunct(none,not_equal(none,power_of(none,integer(none,2),integer(none,4)),integer(none,0)),conjunct(none,member(none,div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4))),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))))))),forall(none,[identifier(none,ui)],implication(none,conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1))))),conjunct(none,member(none,identifier(none,ui),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none)))))),member(none,identifier(none,countLeadingZeroesUI16),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,16)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,16))]),constants(none,[identifier(none,countLeadingZeroesUI4),identifier(none,countLeadingZeroesUI8),identifier(none,countLeadingZeroesUI16)]),sets(none,[])]),conjunct(none,forall(none,[identifier(none,ui)],implication(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),conjunct(none,less_equal(none,integer(none,0),integer(none,16)),conjunct(none,implication(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,16)),integer(none,1)))),less_equal(none,integer(none,0),integer(none,8))),implication(none,conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,16)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),conjunct(none,not_equal(none,power_of(none,integer(none,2),integer(none,8)),integer(none,0)),conjunct(none,member(none,div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,8))),domain(none,identifier(none,countLeadingZeroesUI8))),member(none,identifier(none,countLeadingZeroesUI8),partial_function(none,integer_set(none),integer_set(none))))))))))),forall(none,[identifier(none,ui)],implication(none,conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,16)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))))),conjunct(none,member(none,identifier(none,ui),domain(none,identifier(none,countLeadingZeroesUI8))),member(none,identifier(none,countLeadingZeroesUI8),partial_function(none,integer_set(none),integer_set(none))))))),[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,2)),less_equal(none,integer(none,0),integer(none,8)),equal(none,identifier(none,countLeadingZeroesUI8),union(none,event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),function(none,identifier(none,countLeadingZeroesUI4),[div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4)))])]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))),event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),add(none,integer(none,4),function(none,identifier(none,countLeadingZeroesUI4),[identifier(none,ui)]))]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))))),forall(none,[identifier(none,ui)],implication(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,less_equal(none,integer(none,0),integer(none,2)),conjunct(none,less_equal(none,integer(none,0),integer(none,8)),conjunct(none,implication(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,integer(none,0),integer(none,4))),implication(none,conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))),conjunct(none,not_equal(none,power_of(none,integer(none,2),integer(none,4)),integer(none,0)),conjunct(none,member(none,div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4))),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none))))))))))),forall(none,[identifier(none,ui)],implication(none,conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1))))),conjunct(none,member(none,identifier(none,ui),domain(none,identifier(none,countLeadingZeroesUI4))),member(none,identifier(none,countLeadingZeroesUI4),partial_function(none,integer_set(none),integer_set(none)))))),member(none,identifier(none,countLeadingZeroesUI16),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,16)),integer(none,1))),integer_set(none))),less_equal(none,integer(none,0),integer(none,16))],[equal(none,identifier(none,countLeadingZeroesUI4),set_extension(none,[couple(none,[integer(none,0),integer(none,4)]),couple(none,[integer(none,1),integer(none,3)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,2)]),couple(none,[integer(none,4),integer(none,1)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,6),integer(none,1)]),couple(none,[integer(none,7),integer(none,1)]),couple(none,[integer(none,8),integer(none,0)]),couple(none,[integer(none,9),integer(none,0)]),couple(none,[integer(none,10),integer(none,0)]),couple(none,[integer(none,11),integer(none,0)]),couple(none,[integer(none,12),integer(none,0)]),couple(none,[integer(none,13),integer(none,0)]),couple(none,[integer(none,14),integer(none,0)]),couple(none,[integer(none,15),integer(none,0)])])),member(none,identifier(none,countLeadingZeroesUI8),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1))),integer_set(none))),equal(none,identifier(none,countLeadingZeroesUI8),union(none,event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),function(none,identifier(none,countLeadingZeroesUI4),[div(none,identifier(none,ui),power_of(none,integer(none,2),integer(none,4)))])]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),greater(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))),event_b_comprehension_set(none,[identifier(none,ui)],couple(none,[identifier(none,ui),add(none,integer(none,4),function(none,identifier(none,countLeadingZeroesUI4),[identifier(none,ui)]))]),conjunct(none,member(none,identifier(none,ui),integer_set(none)),conjunct(none,member(none,identifier(none,ui),interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,8)),integer(none,1)))),less_equal(none,identifier(none,ui),minus(none,power_of(none,integer(none,2),integer(none,4)),integer(none,1)))))))),member(none,identifier(none,countLeadingZeroesUI16),total_function(none,interval(none,integer(none,0),minus(none,power_of(none,integer(none,2),integer(none,16)),integer(none,1))),integer_set(none)))],true).
8