equal
deleted
inserted
replaced
3 Copyright 1995 TU Muenchen |
3 Copyright 1995 TU Muenchen |
4 |
4 |
5 Commutation theory for proving the Church Rosser theorem. |
5 Commutation theory for proving the Church Rosser theorem. |
6 *) |
6 *) |
7 |
7 |
8 theory Commutation imports Main begin |
8 theory Commutation imports ZF begin |
9 |
9 |
10 definition |
10 definition |
11 square :: "[i, i, i, i] => o" where |
11 square :: "[i, i, i, i] => o" where |
12 "square(r,s,t,u) == |
12 "square(r,s,t,u) == |
13 (\<forall>a b. <a,b> \<in> r \<longrightarrow> (\<forall>c. <a, c> \<in> s \<longrightarrow> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))" |
13 (\<forall>a b. <a,b> \<in> r \<longrightarrow> (\<forall>c. <a, c> \<in> s \<longrightarrow> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))" |