%1. not(box a : '$Rp' equivalent (box a : ('$Rq' implies '$Rp') and box a : (not '$Rq' implies '$Rp'))). %not((box a : '$Rp' implies (box a : ('$Rq' implies '$Rp') and box a : %(not '$Rq' implies '$Rp'))) and ((box a : ('$Rq' implies '$Rp') and %box a : (not '$Rq' implies '$Rp')) implies box a : '$Rp')). %%% Axioms of S4: reflexivity and transitivity %# modal_axiom_schema(reflexive,a). %# modal_axiom_schema(transitive,a).