library Units
logic HasCASL
spec S =
%% sorts A,B, R
type t;
var a : Type;
op test : a ->? Unit
op id : a -> a
op id2 : a -> Unit
op id3 : Unit -> a
op id4 : Unit ->? a
op id5 : Unit ->? Unit
op id6 : Unit -> Unit
op id7 : a ->? a
op id8 : ? a ->? a
op id9 : ? a -> a
op c : Unit
op b : ? Unit
op o : t
op p : ?t
. id2 o
. id2 p
. test o
. test p
. def (id o)
. def (id p)
. def (id7 o)
. def (id7 p)
. def (id8 o)
. def (id8 p)
. def (id9 o)
. def (id9 p)
. c
. id true
. id c
. id2 true
. id2 c
. id2 (id3 true : a)
. id2 (id3 c : a)
. id2 (id4 true : a)
. id2 (id4 c : a)
. test (id3 true : a)
. test (id3 c : a)
. test (id4 true : a)
. test (id4 c : a)
. id5 true
. id5 c
. id6 true
. id6 c
. id7 true
. id7 c
. id8 true
. id8 c
. id9 true
. id9 c
. test c
. test b
. test true
%[
op f : A * B -> R
op m : A -> B
op a : ?A
op b : ?B
. m a = b
]%