set X = {0,1,2};
set f = QLT_Ex2 ;
thus QLT_Ex2 is commutative :: thesis:

proof

let a, b be Element of {0,1,2}; :: according to BINOP_1:def 2 :: thesis:

per cases ;

suppose A1: ( a = 1 or b = 1 ) ; :: thesis:

then QLT_Ex2 . (a,b) = 1 by QLTEx2Def
.= QLT_Ex2 . (b,a) by A1, QLTEx2Def ;
hence QLT_Ex2 . (a,b) = QLT_Ex2 . (b,a) ; :: thesis:

end;

suppose A2: ( a <> 1 & b <> 1 ) ; :: thesis:

then QLT_Ex2 . (a,b) = min (a,b) by QLTEx2Def
.= QLT_Ex2 . (b,a) by A2, QLTEx2Def ;
hence QLT_Ex2 . (a,b) = QLT_Ex2 . (b,a) ; :: thesis:

end;

end;

end;

thus QLT_Ex2 is associative :: thesis:

proof

let a, b, c be Element of {0,1,2}; :: according to BINOP_1:def 3 :: thesis:

per cases ;

suppose A1: ( a = 1 & ( b = 1 or c = 1 ) ) ; :: thesis:

then A2: QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def, A2;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by QLTEx2Def, A3; :: thesis:

end;

suppose A1: ( ( a = 1 or b = 1 ) & c = 1 ) ; :: thesis:

then A5: QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def;
QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by A5, QLTEx2Def; :: thesis:

end;

suppose A1: ( a <> 1 & b = 1 & c <> 1 ) ; :: thesis:

then QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
then A5: QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def;
QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by A5, QLTEx2Def; :: thesis:

end;

suppose A1: ( a = 1 & b <> 1 & c = 1 ) ; :: thesis:

then QLT_Ex2 . (b,c) = 1 by QLTEx2Def;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by QLTEx2Def, A1; :: thesis:

end;

suppose A1: ( a = 1 & b <> 1 & c <> 1 ) ; :: thesis:

then A2: QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = min (b,c) by QLTEx2Def, A1;

per cases by XXREAL_0:15;

suppose min (b,c) = b ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, A3, QLTEx2Def; :: thesis:

end;

suppose min (b,c) = c ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A1, QLTEx2Def, A2; :: thesis:

end;

end;

end;

suppose A1: ( a <> 1 & b = 1 & c <> 1 ) ; :: thesis:

then A2: QLT_Ex2 . (a,b) = 1 by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;
QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = 1 by QLTEx2Def, A2;
hence QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) by QLTEx2Def, A3; :: thesis:

end;

suppose A1: ( a <> 1 & b <> 1 & c = 1 ) ; :: thesis:

then A2: QLT_Ex2 . (a,b) = min (a,b) by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = 1 by QLTEx2Def, A1;

per cases by XXREAL_0:15;

suppose min (a,b) = a ; :: thesis:

QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . (a,1) by QLTEx2Def, A1
.= 1 by QLTEx2Def, A1 ;
hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A1; :: thesis:

end;

suppose min (a,b) = b ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A3, A2; :: thesis:

end;

end;

end;

suppose A1: ( a <> 1 & b <> 1 & c <> 1 ) ; :: thesis:

then A2: QLT_Ex2 . (a,b) = min (a,b) by QLTEx2Def;
A3: QLT_Ex2 . (b,c) = min (b,c) by QLTEx2Def, A1;

per cases by XXREAL_0:15;

suppose C1: min (a,c) = a ; :: thesis:

per cases by XXREAL_0:15;

suppose ( min (a,b) = a & min (b,c) = b ) ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, A3, C1, QLTEx2Def, A1; :: thesis:

end;

suppose ( min (a,b) = a & min (b,c) = c ) ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A1, A2; :: thesis:

end;

suppose ( min (a,b) = b & min (b,c) = b ) ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A3, A2; :: thesis:

end;

suppose B1: ( min (a,b) = b & min (b,c) = c ) ; :: thesis:

then ( a <= c & b <= a & c <= b ) by C1, XXREAL_0:def 9;
then ( a <= c & c <= a ) by XXREAL_0:2;
then a = c by XXREAL_0:1;
hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by B1, A3; :: thesis:

end;

end;

end;

suppose C1: min (a,c) = c ; :: thesis:

per cases by XXREAL_0:15;

suppose B1: ( min (a,b) = a & min (b,c) = b ) ; :: thesis:

then ( c <= a & a <= b & b <= c ) by C1, XXREAL_0:def 9;
then ( a <= c & c <= a ) by XXREAL_0:2;
then a = c by XXREAL_0:1;
hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, B1; :: thesis:

end;

suppose ( min (a,b) = a & min (b,c) = c ) ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by QLTEx2Def, A1, A2; :: thesis:

end;

suppose ( min (a,b) = b & min (b,c) = b ) ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by A2, A3; :: thesis:

end;

suppose ( min (a,b) = b & min (b,c) = c ) ; :: thesis:

hence QLT_Ex2 . ((QLT_Ex2 . (a,b)),c) = QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) by C1, QLTEx2Def, A1, A3, A2; :: thesis:

end;

end;

end;

end;

end;

end;

end;

let a be Element of {0,1,2}; :: according to BINOP_1:def 4 :: thesis:

per cases ;

suppose a = 1 ; :: thesis:

hence QLT_Ex2 . (a,a) = a by QLTEx2Def; :: thesis:

end;

suppose a <> 1 ; :: thesis:

then QLT_Ex2 . (a,a) = min (a,a) by QLTEx2Def
.= a ;
hence QLT_Ex2 . (a,a) = a ; :: thesis:

end;

end;