generated(1769246959898,'Sat Jan 24 10:29:19 CET 2026').
project_name('SequentProverExamples').
machine_name('GetPositiveElements').
disprover_po('INITIALISATION/inv1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),subset(none,identifier(none,'ELEMENTS'),identifier(none,'ELEMENTS')),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))],[],true).
disprover_po('INITIALISATION/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),subset(none,typeof(none,empty_set(none),pow_subset(none,integer_set(none))),identifier(none,'ELEMENTS')),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))],[],true).
disprover_po('INITIALISATION/inductive/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),equal(none,typeof(none,empty_set(none),pow_subset(none,integer_set(none))),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,'ELEMENTS')))]))),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))],[],unknown).
disprover_po('INITIALISATION/inv3/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),implication(none,equal(none,identifier(none,'ELEMENTS'),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,typeof(none,empty_set(none),pow_subset(none,integer_set(none))),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS'))],[],true).
disprover_po('step_pos/inv1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,pos),pow_subset(none,integer_set(none))),member(none,identifier(none,e),integer_set(none)),member(none,identifier(none,elements),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))])]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,pos),identifier(none,e),identifier(none,elements),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),subset(none,set_subtraction(none,identifier(none,elements),set_extension(none,[identifier(none,e)])),identifier(none,'ELEMENTS')),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],[subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],true).
disprover_po('step_pos/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,pos),pow_subset(none,integer_set(none))),member(none,identifier(none,e),integer_set(none)),member(none,identifier(none,elements),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))])]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,pos),identifier(none,e),identifier(none,elements),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),subset(none,union(none,identifier(none,pos),set_extension(none,[identifier(none,e)])),identifier(none,'ELEMENTS')),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],[subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],true).
disprover_po('step_pos/inductive/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,pos),pow_subset(none,integer_set(none))),member(none,identifier(none,e),integer_set(none)),member(none,identifier(none,elements),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))])]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,pos),identifier(none,e),identifier(none,elements),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),equal(none,union(none,identifier(none,pos),set_extension(none,[identifier(none,e)])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),set_subtraction(none,identifier(none,elements),set_extension(none,[identifier(none,e)]))))]))),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],[equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],unknown).
disprover_po('step_pos/inv3/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,pos),pow_subset(none,integer_set(none))),member(none,identifier(none,e),integer_set(none)),member(none,identifier(none,elements),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),member(none,identifier(none,'pos\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))])]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,pos),identifier(none,e),identifier(none,elements),identifier(none,'elements\''),identifier(none,'pos\'')]),sets(none,[])]),implication(none,equal(none,set_subtraction(none,identifier(none,elements),set_extension(none,[identifier(none,e)])),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,union(none,identifier(none,pos),set_extension(none,[identifier(none,e)])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],[implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[greater(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],true).
disprover_po('step_neg/inv1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,pos),pow_subset(none,integer_set(none))),member(none,identifier(none,e),integer_set(none)),member(none,identifier(none,elements),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))])]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])])))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,pos),identifier(none,e),identifier(none,elements),identifier(none,'elements\'')]),sets(none,[])]),subset(none,set_subtraction(none,identifier(none,elements),set_extension(none,[identifier(none,e)])),identifier(none,'ELEMENTS')),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],[subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],true).
disprover_po('step_neg/inductive/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,pos),pow_subset(none,integer_set(none))),member(none,identifier(none,e),integer_set(none)),member(none,identifier(none,elements),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))])]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])])))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,pos),identifier(none,e),identifier(none,elements),identifier(none,'elements\'')]),sets(none,[])]),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),set_subtraction(none,identifier(none,elements),set_extension(none,[identifier(none,e)]))))]))),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],[equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],true).
disprover_po('step_neg/inv3/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'ELEMENTS'),pow_subset(none,integer_set(none))),member(none,identifier(none,pos),pow_subset(none,integer_set(none))),member(none,identifier(none,e),integer_set(none)),member(none,identifier(none,elements),pow_subset(none,integer_set(none))),member(none,identifier(none,'elements\''),pow_subset(none,integer_set(none))),subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))])]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[member(none,identifier(none,x),integer_set(none)),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])])))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])]),constants(none,[identifier(none,'ELEMENTS'),identifier(none,pos),identifier(none,e),identifier(none,elements),identifier(none,'elements\'')]),sets(none,[])]),implication(none,equal(none,set_subtraction(none,identifier(none,elements),set_extension(none,[identifier(none,e)])),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),[subset_strict(none,identifier(none,'ELEMENTS'),integer_set(none)),finite(none,identifier(none,'ELEMENTS')),subset(none,identifier(none,elements),identifier(none,'ELEMENTS')),subset(none,identifier(none,pos),identifier(none,'ELEMENTS')),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),set_subtraction(none,identifier(none,'ELEMENTS'),identifier(none,elements)))]))),implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],[implication(none,equal(none,identifier(none,elements),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),equal(none,identifier(none,pos),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,[greater(none,identifier(none,x),integer(none,0)),member(none,identifier(none,x),identifier(none,'ELEMENTS'))])))),conjunct(none,[less_equal(none,identifier(none,e),integer(none,0)),member(none,identifier(none,e),identifier(none,elements))])],true).