| 4 | | disprover_po('thm1/THM',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,x),bool_set(none)),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,bool_set(none),bool_set(none)))),member(none,identifier(none,f),partial_function(none,bool_set(none),bool_set(none))),not_member(none,couple(none,[identifier(none,x),boolean_true(none)]),identifier(none,f))]),constants(none,[identifier(none,x),identifier(none,f)]),sets(none,[])]),member(none,union(none,identifier(none,f),set_extension(none,[couple(none,[identifier(none,x),boolean_true(none)])])),partial_function(none,bool_set(none),bool_set(none))),[member(none,identifier(none,f),partial_function(none,bool_set(none),bool_set(none))),not_member(none,couple(none,[identifier(none,x),boolean_true(none)]),identifier(none,f))],[member(none,identifier(none,f),partial_function(none,bool_set(none),bool_set(none))),not_member(none,couple(none,[identifier(none,x),boolean_true(none)]),identifier(none,f))],unknown). |