logic Hybrid

spec X =

modalities m

preds p : ()

%% this is equivalent to the negation of A (down x <m> not x)

. not (!y not (!x not (@y Here x /\ @y <m> not Here x))) %implied %(ex2)%

%% same of above, this time the formula is the negated version of A (down x <m> (not x /\ <m> x))

. not ! y not (! x not (@y Here x /\ @y <m> (not Here x /\ <m> Here x))) %implied %(ex1)%

end