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