equal
deleted
inserted
replaced
68 I :: comb where |
68 I :: comb where |
69 "I = S\<bullet>K\<bullet>K" |
69 "I = S\<bullet>K\<bullet>K" |
70 |
70 |
71 definition |
71 definition |
72 diamond :: "('a * 'a)set \<Rightarrow> bool" where |
72 diamond :: "('a * 'a)set \<Rightarrow> bool" where |
73 \<comment>\<open>confluence; Lambda/Commutation treats this more abstractly\<close> |
73 \<comment> \<open>confluence; Lambda/Commutation treats this more abstractly\<close> |
74 "diamond(r) = (\<forall>x y. (x,y) \<in> r --> |
74 "diamond(r) = (\<forall>x y. (x,y) \<in> r --> |
75 (\<forall>y'. (x,y') \<in> r --> |
75 (\<forall>y'. (x,y') \<in> r --> |
76 (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))" |
76 (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))" |
77 |
77 |
78 |
78 |