src/ZF/Resid/Confluence.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 11319 8b84ee2cc79c
permissions -rw-r--r--
expanded tabs
     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