author | clasohm |
Wed, 02 Nov 1994 11:50:09 +0100 | |
changeset 156 | fd1be45b64bf |
child 168 | 44ff2275d44f |
permissions | -rw-r--r-- |
156 | 1 |
(* Methods of proof for IOA. *) |
2 |
||
3 |
Solve = IOA + |
|
4 |
||
5 |
consts |
|
6 |
||
7 |
is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" |
|
8 |
||
9 |
rules |
|
10 |
||
11 |
is_weak_pmap_def |
|
12 |
"is_weak_pmap(f,C,A) == \ |
|
13 |
\ (!s:starts_of(C). f(s):starts_of(A)) & \ |
|
14 |
\ (!s t a. reachable(C,s) & \ |
|
15 |
\ <s,a,t>:trans_of(C) \ |
|
16 |
\ --> if(a:externals(asig_of(C)), \ |
|
17 |
\ <f(s),a,f(t)>:trans_of(A), \ |
|
18 |
\ f(s)=f(t)))" |
|
19 |
||
20 |
end |