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 :: thesis: x + (- x) = a

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 Def12;
hence x + (- x) = a by A1, A2, Def13; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

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

end;

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

proof

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

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 Def13
.= x + (y + z) by A5, Def13 ;
:: thesis: verum

end;

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

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

end;

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

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

end;

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

thus (x + y) + z = 0 by A8, Def13
.= x + (y + z) by A8, Def13 ; :: thesis: verum

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;

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;

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;

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;

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;

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

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

end;

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

thus (x + y) + z = 0 by A21, Def13
.= x + (y + z) by A21, Def13 ; :: thesis: verum

end;

end;

end;

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

end;