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 y = 0 ; :: thesis: (x + y) + z = x + (y + z)

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;