6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder op o : s ->? s %%partial
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder op o : s -> s %%total
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% make o total
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s1a = s1 with o : s ->? s |-> o : s -> s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s1b = s1 with o : s -> s |-> o : s -> s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s1a equal s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s1as2 : s1a to s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2s1a : s2 to s1a
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s1b equal s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s1bs2 : s1b to s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2s1b : s2 to s1b
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% leave o partial
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s1c = s1 with o : s -> s |-> o : s ->? s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s1d = s1 with o : s ->? s |-> o : s ->? s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s1c equal s1
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s1cs1 : s1c to s1
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s1s1c : s1 to s1c
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s1d equal s1
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s1ds1 : s1d to s1
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s1s1d : s1 to s1d
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% true refinement
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview v1 : s1 to s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s2a = s2 with o : s ->? s |-> o : s -> s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s2b = s2 with o : s -> s |-> o : s -> s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s2c = s2 with o : s -> s |-> o : s ->? s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederspec s2d = s2 with o : s ->? s |-> o : s ->? s
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s2a equal s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2as2 : s2a to s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2s2a : s2 to s2a
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s2b equal s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2bs2 : s2b to s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2s2b : s2 to s2b
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s2c equal s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2cs2 : s2c to s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2s2c : s2 to s2c
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% s2d equal s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2ds2 : s2d to s2
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maederview s2s2d : s2 to s2d
6c27ec0140e8de46f15f7c2aea4761157f9f8bd9Christian Maeder%% view v2 : s2 to s1