equal
deleted
inserted
replaced
6 Partial ordering for the strict sum ++ |
6 Partial ordering for the strict sum ++ |
7 *) |
7 *) |
8 |
8 |
9 Ssum1 = Ssum0 + |
9 Ssum1 = Ssum0 + |
10 |
10 |
|
11 instance "++"::(pcpo,pcpo)sq_ord |
|
12 |
11 defs |
13 defs |
12 less_ssum_def "less == (%s1 s2.@z. |
14 less_ssum_def "(op <<) == (%s1 s2.@z. |
13 (! u x.s1=Isinl u & s2=Isinl x --> z = u << x) |
15 (! u x.s1=Isinl u & s2=Isinl x --> z = u << x) |
14 &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y) |
16 &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y) |
15 &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU)) |
17 &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU)) |
16 &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))" |
18 &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))" |
17 |
19 |