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