Cross Reference: /hets/Static/test/RemoveNodeSpec3.het
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
spec s2 =
sort s, t;
ops a, o : s
. a = o
. o = a %implied
sort u, v
preds p, q : s * v
. forall x : v . p(a, x)
spec t1 =
sort s, t;
ops a, o : s
. a = o
. o = a %implied
spec t2 = t1 then
sort u, v
preds p, q : s * v
. forall x : v . p(a, x)
view v : s2 to t2