ABSTRACT
Let L be a language with the constants c0, Cj, the 2-ary operation symbol + and predicate symbols = and < , and with the abbreviation x < y for x < y v x= y . Let C o2 be the set of axioms
cl. "I x < x c2. x < y A y < z -* x < z c3. x < y v y < x v x = y c4. c0< x v c0= x c4j. c0< c , c6 . x < y -* x + C j< y al. x + ( y + z) = ( x + y ) + z a2 . x + y = y + x a3. x + c 0= x a4. x + y = x + z -* y = z bl. y < z -♦ x + y < x + z b2 . y < z -* 3x y + x = z .
