equal
deleted
inserted
replaced
19 edges :: "(vertex*vertex) set" |
19 edges :: "(vertex*vertex) set" |
20 |
20 |
21 constdefs |
21 constdefs |
22 |
22 |
23 asgt :: "[vertex,vertex] => (state*state) set" |
23 asgt :: "[vertex,vertex] => (state*state) set" |
24 "asgt u v == {(s,s'). s' = s[v:= s u | s v]}" |
24 "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" |
25 |
25 |
26 racts :: "(state*state) set set" |
26 racts :: "(state*state) set set" |
27 "racts == insert id (UN (u,v): edges. {asgt u v})" |
27 "racts == insert id (UN (u,v): edges. {asgt u v})" |
28 |
28 |
29 rinit :: "state set" |
29 rinit :: "state set" |