logic Hybrid

%% Hard formulas

spec aux =

modality M

nominal N

spec f1 =

aux then

pred p,q,r,s,t : ()

. ( not (( p /\ (not q)) /\ (((((q => p) /\ (r => q)) /\ ((p => (( t => ([M](p => t))) /\ ((not t) =>

([M](p => (not t)))))) /\ (q => ((s => ([M](q => s))) /\ ((not s) => ([M](q => (not s)))))))) /\ ((p /\

(not q)) => (( <M> ((q /\ (not r)) /\ s)) /\ ( <M> ((q /\ (not r)) /\ (not s)))))) /\ ([M] (((( q => p) /\

(r => q)) /\ ((p => ((t => ([M](p => t))) /\ ((not t) => ([M](p => (not t)))))) /\ (q => ((s =>

([M](p => t))) /\ ((not t) => ([M](p => (not t)))))))) /\ ((p /\ (not q)) => (( <M> ((q /\ (not r)) /\ p))

/\ ( <M> ((q /\ (not r)) /\ (not s)))))))))) \/ (not ( [M] s)) %implied