fmod PROP-LOG is protecting QID . sorts Atom Prop . subsorts Qid < Atom < Prop . *** atomic propositions ops tt ff : -> Prop . *** truth values op ~_ : Prop -> Prop . *** negation op _\/_ : Prop Prop -> Prop . *** disjunction op _/\_ : Prop Prop -> Prop . *** conjunction vars P Q : Prop . eq ~ tt = ff . eq ~ ff = tt . eq ~ ~ P = P . *** double negation eq ~ (P \/ Q) = ~ P /\ ~ Q . *** De Morgan laws eq ~ (P /\ Q) = ~ P \/ ~ Q . sorts PropSet Sequent . subsort Prop < PropSet . op _,_ : PropSet PropSet -> PropSet [assoc comm] . op |-_ : PropSet -> Sequent . var S : PropSet . eq S,S = S . endfm red |- ~ (tt /\ ~ (~ ff \/ ~ tt)) . ***( reduce in PROP-LOG : |- ~ (tt /\ ~ (~ ff \/ ~ tt)) . rewrites: 10 in -10ms cpu (0ms real) (~ rewrites/second) result Sequent: |- (ff \/ (tt \/ ff)) )