| 4 | | disprover_po('nothm2/WD',event_b_context(none,'DisproverContext',[axioms(none,[]),constants(none,[]),sets(none,[deferred_set(none,'DS')])]),forall(none,[identifier(none,cc)],implication(none,conjunct(none,member(none,identifier(none,cc),pow_subset(none,cartesian_product(none,identifier(none,'DS'),bool_set(none)))),member(none,identifier(none,cc),relations(none,identifier(none,'DS'),bool_set(none)))),finite(none,identifier(none,cc)))),[],[],unknown). |
| 5 | | disprover_po('nothm2/THM',event_b_context(none,'DisproverContext',[axioms(none,[forall(none,[identifier(none,cc)],implication(none,conjunct(none,member(none,identifier(none,cc),pow_subset(none,cartesian_product(none,identifier(none,'DS'),bool_set(none)))),member(none,identifier(none,cc),relations(none,identifier(none,'DS'),bool_set(none)))),finite(none,identifier(none,cc))))]),constants(none,[]),sets(none,[deferred_set(none,'DS')])]),exists(none,[identifier(none,cc)],conjunct(none,member(none,identifier(none,cc),pow_subset(none,cartesian_product(none,identifier(none,'DS'),bool_set(none)))),conjunct(none,member(none,identifier(none,cc),relations(none,identifier(none,'DS'),bool_set(none))),equal(none,card(none,identifier(none,cc)),integer(none,4))))),[forall(none,[identifier(none,cc)],implication(none,conjunct(none,member(none,identifier(none,cc),pow_subset(none,cartesian_product(none,identifier(none,'DS'),bool_set(none)))),member(none,identifier(none,cc),relations(none,identifier(none,'DS'),bool_set(none)))),finite(none,identifier(none,cc))))],[],unknown). |