problem-set/algebra/category.theory/p11.desc created : 07/05/89 revised : 07/19/89 Natural Language Description: Lemma 11: dom(dom(x)) = dom(x). Versions : p11.ver1 : uses UR resolution, with axioms from B.Mitchell, "Theory of Categories", Chapter 1. created : from Mitchell, "Theory of Categories", Ch. 1. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/05/89. p11.ver2 : Quaife axioms, using UR resolution, paramodulation into the given clause, and dynamic demodulation; created : from Mitchell, "Theory of Categories", Ch. 1. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/07/89. p11.ver3 : Scott axioms, using UR resolution. created : from Mitchell, "Theory of Categories", Ch. 1. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : no proof.