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