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