generated(1769247011115,'Sat Jan 24 10:30:11 CET 2026').
project_name('SequentProverExamples').
machine_name(find_ctx).
disprover_po('axm3/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,arr),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,n),integer_set(none)),member(none,identifier(none,mxi),integer_set(none)),member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n)))]),constants(none,[identifier(none,arr),identifier(none,n),identifier(none,mxi)]),sets(none,[])]),forall(none,[identifier(none,j)],implication(none,member(none,identifier(none,j),interval(none,integer(none,1),identifier(none,n))),conjunct(none,[member(none,identifier(none,mxi),domain(none,identifier(none,arr))),member(none,identifier(none,arr),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,j),domain(none,identifier(none,arr)))]))),[member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n)))],[member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n)))],unknown).
disprover_po('thm1/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,arr),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,n),integer_set(none)),member(none,identifier(none,mxi),integer_set(none)),member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n))),forall(none,[identifier(none,j)],implication(none,conjunct(none,[member(none,identifier(none,j),integer_set(none)),member(none,identifier(none,j),interval(none,integer(none,1),identifier(none,n)))]),greater_equal(none,function(none,identifier(none,arr),[identifier(none,mxi)]),function(none,identifier(none,arr),[identifier(none,j)]))))]),constants(none,[identifier(none,arr),identifier(none,n),identifier(none,mxi)]),sets(none,[])]),conjunct(none,[member(none,identifier(none,mxi),domain(none,identifier(none,arr))),member(none,identifier(none,arr),partial_function(none,integer_set(none),integer_set(none))),not_equal(none,range(none,identifier(none,arr)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),range(none,identifier(none,arr))),greater_equal(none,identifier(none,b),identifier(none,x)))))]),[member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n))),forall(none,[identifier(none,j)],implication(none,member(none,identifier(none,j),interval(none,integer(none,1),identifier(none,n))),greater_equal(none,function(none,identifier(none,arr),[identifier(none,mxi)]),function(none,identifier(none,arr),[identifier(none,j)]))))],[member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n))),forall(none,[identifier(none,j)],implication(none,member(none,identifier(none,j),interval(none,integer(none,1),identifier(none,n))),greater_equal(none,function(none,identifier(none,arr),[identifier(none,mxi)]),function(none,identifier(none,arr),[identifier(none,j)]))))],true).
disprover_po('thm1/THM',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,arr),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,n),integer_set(none)),member(none,identifier(none,mxi),integer_set(none)),member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n))),forall(none,[identifier(none,j)],implication(none,conjunct(none,[member(none,identifier(none,j),integer_set(none)),member(none,identifier(none,j),interval(none,integer(none,1),identifier(none,n)))]),greater_equal(none,function(none,identifier(none,arr),[identifier(none,mxi)]),function(none,identifier(none,arr),[identifier(none,j)])))),member(none,identifier(none,mxi),domain(none,identifier(none,arr))),member(none,identifier(none,arr),partial_function(none,integer_set(none),integer_set(none))),not_equal(none,range(none,identifier(none,arr)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,[member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,[member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),range(none,identifier(none,arr)))]),greater_equal(none,identifier(none,b),identifier(none,x))))]))]),constants(none,[identifier(none,arr),identifier(none,n),identifier(none,mxi)]),sets(none,[])]),equal(none,function(none,identifier(none,arr),[identifier(none,mxi)]),max(none,range(none,identifier(none,arr)))),[member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n))),forall(none,[identifier(none,j)],implication(none,member(none,identifier(none,j),interval(none,integer(none,1),identifier(none,n))),greater_equal(none,function(none,identifier(none,arr),[identifier(none,mxi)]),function(none,identifier(none,arr),[identifier(none,j)])))),member(none,identifier(none,mxi),domain(none,identifier(none,arr))),member(none,identifier(none,arr),partial_function(none,integer_set(none),integer_set(none))),not_equal(none,range(none,identifier(none,arr)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),range(none,identifier(none,arr))),greater_equal(none,identifier(none,b),identifier(none,x)))))],[member(none,identifier(none,n),natural1_set(none)),member(none,identifier(none,arr),total_function(none,interval(none,integer(none,1),identifier(none,n)),natural1_set(none))),member(none,identifier(none,mxi),interval(none,integer(none,1),identifier(none,n))),forall(none,[identifier(none,j)],implication(none,member(none,identifier(none,j),interval(none,integer(none,1),identifier(none,n))),greater_equal(none,function(none,identifier(none,arr),[identifier(none,mxi)]),function(none,identifier(none,arr),[identifier(none,j)]))))],true).