problem-set/algebra/groups/ident2.desc created : 07/09/86 revised : 08/12/88 Natural Language Description: Theorem: the right identity axiom is dependant on the rest of the axiom set; i.e., each element has a right identity. Note that this is a corollary to ident1, but also that the proof is different due to the introduction of a skolem function for the right identity of each element of the group. Note: the axioms P(x,e,x) and P(x,g(x),e) must be deleted. Versions : ident2.ver1 : uses UR resolution and a standard p-formulation. created : 7/9/86 from McCharen, Overbeek, & Wos [Aug. 1976]. verified for ITP : 7/11/86 translated for OTTER : caw. verified for OTTER : 08/12/88.