indexing
	description: "Invertible object with an internal + operation"
	note: "The model is that of a commutative group."
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"

deferred class interface
	GROUP_ELEMENT

feature -- Access

	zero: like Current
			-- Neutral element for "+" and "-"
		ensure
			result_exists: Result /= void
	
feature -- Basic operations

	infix "+" (other: like Current): like Current
			-- Sum with other (commutative)
		require
			other_exists: other /= void
		ensure
			result_exists: Result /= void
			commutative: Result.is_equal (other + Current)

	prefix "+": like Current
			-- Unary plus
		ensure
			result_exists: Result /= void
			result_definition: Result.is_equal (Current)

	infix "-" (other: like Current): like Current
			-- Result of subtracting other
		require
			other_exists: other /= void
		ensure
			result_exists: Result /= void

	prefix "-": like Current
			-- Unary minus
		ensure
			result_exists: Result /= void
			result_definition: (Result + Current).is_equal (zero)
	
invariant

	neutral_addition: Current.is_equal (Current + zero)
	self_subtraction: zero.is_equal (Current - Current)
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class GROUP_ELEMENT