Dear Dimitri,
You are right. I didn't checked very carefully the local confluence of my rewriting system. To get confluence, I need to add the fact that the bimorphism f satisfies "fu = vf implies u = 1 and v = 1". So this is enough for f to be a potential isomorphism.
Yes, that does the trick, and is also the best sufficient condition that I have been able to come up with in my thesis. I would guess something similar might work for the general case, but the condition is actually so strong as to be somewhat unsatisfactory. Note in particular that it fails for actual (nontrivial) isomorphisms. I poked around this problem for quite a bit back then but haven't been able to isolate a satisfactory criterion (other than the obvious one that talks explicitly about equality in a non-confluent axiom system). Good luck, Lutz -- -------------------------------------- PD Dr. Lutz Schröder Senior Researcher DFKI Bremen Safe and Secure Cognitive Systems Cartesium, Enrique-Schmidt-Str. 5 D-28359 Bremen phone: (+49) 421-218-64216 Fax: (+49) 421-218-9864216 mail: Lutz.Schroeder@dfki.de www.dfki.de/sks/staff/lschrode -------------------------------------- ------------------------------------------------------------- Deutsches Forschungszentrum für Künstliche Intelligenz GmbH Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern Geschäftsführung: Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender) Dr. Walter Olthoff Vorsitzender des Aufsichtsrats: Prof. Dr. h.c. Hans A. Aukes Amtsgericht Kaiserslautern, HRB 2313 ------------------------------------------------------------- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]