mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
23 lines
346 B
Plaintext
23 lines
346 B
Plaintext
|
|
module M
|
|
|
|
use bool.Bool
|
|
|
|
let f (a b : bool)
|
|
ensures {
|
|
(andb (orb a b) (notb (andb a b)) = True)
|
|
<->
|
|
( ( a = True \/ b = True ) /\ not ( a = True /\ b = True) )
|
|
}
|
|
= ()
|
|
|
|
let g (a b : bool)
|
|
ensures {
|
|
(xorb a b = True)
|
|
<->
|
|
( ( a = True \/ b = True ) /\ not ( a = True /\ b = True) )
|
|
}
|
|
= ()
|
|
|
|
end
|