|
1478
|
1 |
(* Title: Confluence.thy
|
|
1048
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Ole Rasmussen
|
|
1048
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
Logic Image: ZF
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
Confluence = Reduction+
|
|
|
9 |
|
|
|
10 |
consts
|
|
1478
|
11 |
confluence :: i=>o
|
|
|
12 |
strip :: o
|
|
1048
|
13 |
|
|
|
14 |
defs
|
|
1155
|
15 |
confluence_def "confluence(R) ==
|
|
11319
|
16 |
\\<forall>x y. <x,y>:R --> (\\<forall>z.<x,z>:R -->
|
|
|
17 |
(\\<exists>u.<y,u>:R & <z,u>:R))"
|
|
|
18 |
strip_def "strip == \\<forall>x y. (x ===> y) --> (\\<forall>z.(x =1=> z) -->
|
|
|
19 |
(\\<exists>u.(y =1=> u) & (z===>u)))"
|
|
1048
|
20 |
end
|
|
|
21 |
|