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) )

proof

now

per cases ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def 1;

suppose A2: x = 0 ; :: thesis: x + (- x) = a

then - x = 0 by Def15;
hence x + (- x) = a by A1, A2, Def16; :: thesis: verum

end;

suppose A3: x = 1 ; :: thesis: x + (- x) = a

then - x = 2 by Def15;
hence x + (- x) = a by A1, A3, Def16; :: thesis: verum

end;

suppose A4: x = 2 ; :: thesis: x + (- x) = a

then - x = 1 by Def15;
hence x + (- x) = a by A1, A4, Def16; :: thesis: verum

end;

end;

end;

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

end;

thus x + a = x by A1, Def16; :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = x + (y + z) :: thesis: verum

proof

now

per 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;

suppose A5: x = 0 ; :: thesis: (x + y) + z = x + (y + z)

hence (x + y) + z = y + z by Def16
.= x + (y + z) by A5, Def16 ;
:: thesis: verum

end;

suppose A6: y = 0 ; :: thesis: (x + y) + z = x + (y + z)

then x + y = x by Def16;
hence (x + y) + z = x + (y + z) by A6, Def16; :: thesis: verum

end;

suppose A7: z = 0 ; :: thesis: (x + y) + z = x + (y + z)

then y + z = y by Def16;
hence (x + y) + z = x + (y + z) by A7, Def16; :: thesis: verum

end;

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

then A9: x + y = 2 by Def16;
hence (x + y) + z = 0 by A8, Def16
.= x + (y + z) by A8, A9, Def16 ;
:: thesis: verum

end;

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

then A11: y + z = 0 by Def16;
x + y = 2 by A10, Def16;
hence (x + y) + z = 1 by A10, Def16
.= x + (y + z) by A10, A11, Def16 ;
:: thesis: verum

end;

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

then A13: y + z = 0 by Def16;
x + y = 0 by A12, Def16;
hence (x + y) + z = 1 by A12, Def16
.= x + (y + z) by A12, A13, Def16 ;
:: thesis: verum

end;

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

then A15: y + z = 1 by Def16;
x + y = 0 by A14, Def16;
hence (x + y) + z = 2 by A14, Def16
.= x + (y + z) by A14, A15, Def16 ;
:: thesis: verum

end;

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

then A17: y + z = 2 by Def16;
x + y = 0 by A16, Def16;
hence (x + y) + z = 1 by A16, Def16
.= x + (y + z) by A16, A17, Def16 ;
:: thesis: verum

end;

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

then A19: y + z = 0 by Def16;
x + y = 0 by A18, Def16;
hence (x + y) + z = 2 by A18, Def16
.= x + (y + z) by A18, A19, Def16 ;
:: thesis: verum

end;

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

then A21: y + z = 0 by Def16;
x + y = 1 by A20, Def16;
hence (x + y) + z = 2 by A20, Def16
.= x + (y + z) by A20, A21, Def16 ;
:: thesis: verum

end;

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

then A23: x + y = 1 by Def16;
hence (x + y) + z = 0 by A22, Def16
.= x + (y + z) by A22, A23, Def16 ;
:: thesis: verum

end;

end;

end;

hence (x + y) + z = x + (y + z) ; :: thesis: verum

end;