equal
deleted
inserted
replaced
13 is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" |
13 is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" |
14 |
14 |
15 defs |
15 defs |
16 |
16 |
17 is_weak_pmap_def |
17 is_weak_pmap_def |
18 "is_weak_pmap(f,C,A) == \ |
18 "is_weak_pmap(f,C,A) == |
19 \ (!s:starts_of(C). f(s):starts_of(A)) & \ |
19 (!s:starts_of(C). f(s):starts_of(A)) & |
20 \ (!s t a. reachable(C,s) & \ |
20 (!s t a. reachable(C,s) & |
21 \ <s,a,t>:trans_of(C) \ |
21 <s,a,t>:trans_of(C) |
22 \ --> if(a:externals(asig_of(C)), \ |
22 --> if(a:externals(asig_of(C)), |
23 \ <f(s),a,f(t)>:trans_of(A), \ |
23 <f(s),a,f(t)>:trans_of(A), |
24 \ f(s)=f(t)))" |
24 f(s)=f(t)))" |
25 |
25 |
26 end |
26 end |