| author | lcp |
| Tue, 25 Apr 1995 11:14:03 +0200 | |
| changeset 1072 | 0140ff702b23 |
| parent 1048 | 5ba0314f8214 |
| child 1155 | 928a16e02f9f |
| permissions | -rw-r--r-- |
| 1048 | 1 |
(* Title: Confluence.thy |
2 |
ID: $Id$ |
|
3 |
Author: Ole Rasmussen |
|
4 |
Copyright 1995 University of Cambridge |
|
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
8 |
Confluence = Reduction+ |
|
9 |
||
10 |
consts |
|
11 |
confluence :: "i=>o" |
|
12 |
strip :: "o" |
|
13 |
||
14 |
defs |
|
15 |
confluence_def "confluence(R) == \ |
|
16 |
\ ALL x y. <x,y>:R --> (ALL z.<x,z>:R --> \ |
|
17 |
\ (EX u.<y,u>:R & <z,u>:R))" |
|
18 |
strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) --> \ |
|
19 |
\ (EX u.(y =1=> u) & (z===>u)))" |
|
20 |
end |
|
21 |