equal
deleted
inserted
replaced
21 |
21 |
22 defs |
22 defs |
23 |
23 |
24 is_simulation_def |
24 is_simulation_def |
25 "is_simulation R C A == |
25 "is_simulation R C A == |
26 (!s:starts_of C. R```{s} Int starts_of A ~= {}) & |
26 (!s:starts_of C. R``{s} Int starts_of A ~= {}) & |
27 (!s s' t a. reachable C s & |
27 (!s s' t a. reachable C s & |
28 s -a--C-> t & |
28 s -a--C-> t & |
29 (s,s') : R |
29 (s,s') : R |
30 --> (? t' ex. (t,t'):R & move A ex s' a t'))" |
30 --> (? t' ex. (t,t'):R & move A ex s' a t'))" |
31 |
31 |
32 is_backward_simulation_def |
32 is_backward_simulation_def |
33 "is_backward_simulation R C A == |
33 "is_backward_simulation R C A == |
34 (!s:starts_of C. R```{s} <= starts_of A) & |
34 (!s:starts_of C. R``{s} <= starts_of A) & |
35 (!s t t' a. reachable C s & |
35 (!s t t' a. reachable C s & |
36 s -a--C-> t & |
36 s -a--C-> t & |
37 (t,t') : R |
37 (t,t') : R |
38 --> (? ex s'. (s,s'):R & move A ex s' a t'))" |
38 --> (? ex s'. (s,s'):R & move A ex s' a t'))" |
39 |
39 |