set X = {0,1,2};
set f = QLT_Ex2 ;
thus
QLT_Ex2 is commutative
( QLT_Ex2 is associative & QLT_Ex2 is idempotent )
thus
QLT_Ex2 is associative
QLT_Ex2 is idempotent proof
let a,
b,
c be
Element of
{0,1,2};
BINOP_1:def 3 QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)
per cases
( ( a = 1 & ( b = 1 or c = 1 ) ) or ( ( a = 1 or b = 1 ) & c = 1 ) or ( a <> 1 & b = 1 & c <> 1 ) or ( a = 1 & b <> 1 & c = 1 ) or ( a = 1 & b <> 1 & c <> 1 ) or ( a <> 1 & b = 1 & c <> 1 ) or ( a <> 1 & b <> 1 & c = 1 ) or ( a <> 1 & b <> 1 & c <> 1 ) )
;
suppose A1:
(
a = 1 & (
b = 1 or
c = 1 ) )
;
QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)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;
verum end; suppose A1:
(
a <> 1 &
b = 1 &
c <> 1 )
;
QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)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;
verum end; suppose A1:
(
a <> 1 &
b = 1 &
c <> 1 )
;
QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)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;
verum end; suppose A1:
(
a <> 1 &
b <> 1 &
c = 1 )
;
QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)then A2:
QLT_Ex2 . (
a,
b)
= min (
a,
b)
by QLTEx2Def;
A3:
QLT_Ex2 . (
b,
c)
= 1
by QLTEx2Def, A1;
per cases
( min (a,b) = a or min (a,b) = b )
by XXREAL_0:15;
suppose
min (
a,
b)
= a
;
QLT_Ex2 . (a,(QLT_Ex2 . (b,c))) = QLT_Ex2 . ((QLT_Ex2 . (a,b)),c)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;
verum end; end; end; end;
end;
let a be Element of {0,1,2}; BINOP_1:def 4 QLT_Ex2 . (a,a) = a