let x, y, z, a be Element of {0,1,2}; :: thesis: ( a = 0 implies ( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) ) )

assume A1: a = 0 ; :: thesis: ( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) )

thus x + (- x) = a :: thesis: ( x + a = x & (x + y) + z = x + (y + z) )

thus (x + y) + z = x + (y + z) :: thesis: verum

assume A1: a = 0 ; :: thesis: ( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) )

thus x + (- x) = a :: thesis: ( x + a = x & (x + y) + z = x + (y + z) )

proof

end;

thus
x + a = x
by A1, Def13; :: thesis: (x + y) + z = x + (y + z)now :: thesis: x + (- x) = a

hence
x + (- x) = a
; :: thesis: verumend;

thus (x + y) + z = x + (y + z) :: thesis: verum

proof

end;

now :: thesis: (x + y) + z = x + (y + z)end;

hence
(x + y) + z = x + (y + z)
; :: thesis: verumper cases
( x = 0 or y = 0 or z = 0 or ( x = 1 & y = 1 & z = 1 ) or ( x = 1 & y = 1 & z = 2 ) or ( x = 1 & y = 2 & z = 1 ) or ( x = 1 & y = 2 & z = 2 ) or ( x = 2 & y = 1 & z = 1 ) or ( x = 2 & y = 1 & z = 2 ) or ( x = 2 & y = 2 & z = 1 ) or ( x = 2 & y = 2 & z = 2 ) )
by ENUMSET1:def 1;

end;

suppose A9:
( x = 1 & y = 1 & z = 2 )
; :: thesis: (x + y) + z = x + (y + z)

then A10:
y + z = 0
by Def13;

x + y = 2 by A9, Def13;

hence (x + y) + z = 1 by A9, Def13

.= x + (y + z) by A9, A10, Def13 ;

:: thesis: verum

end;x + y = 2 by A9, Def13;

hence (x + y) + z = 1 by A9, Def13

.= x + (y + z) by A9, A10, Def13 ;

:: thesis: verum

suppose A11:
( x = 1 & y = 2 & z = 1 )
; :: thesis: (x + y) + z = x + (y + z)

then A12:
y + z = 0
by Def13;

x + y = 0 by A11, Def13;

hence (x + y) + z = 1 by A11, Def13

.= x + (y + z) by A11, A12, Def13 ;

:: thesis: verum

end;x + y = 0 by A11, Def13;

hence (x + y) + z = 1 by A11, Def13

.= x + (y + z) by A11, A12, Def13 ;

:: thesis: verum

suppose A13:
( x = 1 & y = 2 & z = 2 )
; :: thesis: (x + y) + z = x + (y + z)

then A14:
y + z = 1
by Def13;

x + y = 0 by A13, Def13;

hence (x + y) + z = 2 by A13, Def13

.= x + (y + z) by A13, A14, Def13 ;

:: thesis: verum

end;x + y = 0 by A13, Def13;

hence (x + y) + z = 2 by A13, Def13

.= x + (y + z) by A13, A14, Def13 ;

:: thesis: verum

suppose A15:
( x = 2 & y = 1 & z = 1 )
; :: thesis: (x + y) + z = x + (y + z)

then A16:
y + z = 2
by Def13;

x + y = 0 by A15, Def13;

hence (x + y) + z = 1 by A15, Def13

.= x + (y + z) by A15, A16, Def13 ;

:: thesis: verum

end;x + y = 0 by A15, Def13;

hence (x + y) + z = 1 by A15, Def13

.= x + (y + z) by A15, A16, Def13 ;

:: thesis: verum

suppose A17:
( x = 2 & y = 1 & z = 2 )
; :: thesis: (x + y) + z = x + (y + z)

then A18:
y + z = 0
by Def13;

x + y = 0 by A17, Def13;

hence (x + y) + z = 2 by A17, Def13

.= x + (y + z) by A17, A18, Def13 ;

:: thesis: verum

end;x + y = 0 by A17, Def13;

hence (x + y) + z = 2 by A17, Def13

.= x + (y + z) by A17, A18, Def13 ;

:: thesis: verum