:: BINOP_1 semantic presentation

definition
let c1 be Function;
let c2, c3 be set ;
func c1 . c2,c3 -> set equals :: BINOP_1:def 1
a1 . [a2,a3];
correctness
coherence
c1 . [c2,c3] is set ;
;
end;

:: deftheorem Def1 defines . BINOP_1:def 1 :
for b1 being Function
for b2, b3 being set holds b1 . b2,b3 = b1 . [b2,b3];

definition
let c1, c2 be non empty set ;
let c3 be set ;
let c4 be Function of [:c1,c2:],c3;
let c5 be Element of c1;
let c6 be Element of c2;
redefine func . as c4 . c5,c6 -> Element of a3;
coherence
c4 . c5,c6 is Element of c3
proof end;
end;

theorem Th1: :: BINOP_1:1
canceled;

theorem Th2: :: BINOP_1:2
for b1, b2, b3 being non empty set
for b4, b5 being Function of [:b1,b2:],b3 st ( for b6 being Element of b1
for b7 being Element of b2 holds b4 . b6,b7 = b5 . b6,b7 ) holds
b4 = b5
proof end;

definition
let c1 be set ;
mode UnOp of a1 is Function of a1,a1;
mode BinOp of a1 is Function of [:a1,a1:],a1;
end;

scheme :: BINOP_1:sch 1
s1{ F1() -> non empty set , P1[ Element of F1(), Element of F1(), Element of F1()] } :
ex b1 being BinOp of F1() st
for b2, b3 being Element of F1() holds P1[b2,b3,b1 . b2,b3]
provided
E1: for b1, b2 being Element of F1() ex b3 being Element of F1() st P1[b1,b2,b3]
proof end;

scheme :: BINOP_1:sch 2
s2{ F1() -> non empty set , F2( Element of F1(), Element of F1()) -> Element of F1() } :
ex b1 being BinOp of F1() st
for b2, b3 being Element of F1() holds b1 . b2,b3 = F2(b2,b3)
proof end;

definition
let c1 be set ;
let c2 be BinOp of c1;
attr a2 is commutative means :Def2: :: BINOP_1:def 2
for b1, b2 being Element of a1 holds a2 . b1,b2 = a2 . b2,b1;
attr a2 is associative means :Def3: :: BINOP_1:def 3
for b1, b2, b3 being Element of a1 holds a2 . b1,(a2 . b2,b3) = a2 . (a2 . b1,b2),b3;
attr a2 is idempotent means :Def4: :: BINOP_1:def 4
for b1 being Element of a1 holds a2 . b1,b1 = b1;
end;

:: deftheorem Def2 defines commutative BINOP_1:def 2 :
for b1 being set
for b2 being BinOp of b1 holds
( b2 is commutative iff for b3, b4 being Element of b1 holds b2 . b3,b4 = b2 . b4,b3 );

:: deftheorem Def3 defines associative BINOP_1:def 3 :
for b1 being set
for b2 being BinOp of b1 holds
( b2 is associative iff for b3, b4, b5 being Element of b1 holds b2 . b3,(b2 . b4,b5) = b2 . (b2 . b3,b4),b5 );

:: deftheorem Def4 defines idempotent BINOP_1:def 4 :
for b1 being set
for b2 being BinOp of b1 holds
( b2 is idempotent iff for b3 being Element of b1 holds b2 . b3,b3 = b3 );

registration
cluster -> empty commutative associative M4([:{} ,{} :], {} );
coherence
for b1 being BinOp of {} holds
( b1 is empty & b1 is associative & b1 is commutative )
proof end;
end;

definition
let c1 be set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
pred c2 is_a_left_unity_wrt c3 means :Def5: :: BINOP_1:def 5
for b1 being Element of a1 holds a3 . a2,b1 = b1;
pred c2 is_a_right_unity_wrt c3 means :Def6: :: BINOP_1:def 6
for b1 being Element of a1 holds a3 . b1,a2 = b1;
end;

:: deftheorem Def5 defines is_a_left_unity_wrt BINOP_1:def 5 :
for b1 being set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_left_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b2,b4 = b4 );

:: deftheorem Def6 defines is_a_right_unity_wrt BINOP_1:def 6 :
for b1 being set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_right_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b4,b2 = b4 );

definition
let c1 be set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
pred c2 is_a_unity_wrt c3 means :: BINOP_1:def 7
( a2 is_a_left_unity_wrt a3 & a2 is_a_right_unity_wrt a3 );
end;

:: deftheorem Def7 defines is_a_unity_wrt BINOP_1:def 7 :
for b1 being set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_unity_wrt b3 iff ( b2 is_a_left_unity_wrt b3 & b2 is_a_right_unity_wrt b3 ) );

theorem Th3: :: BINOP_1:3
canceled;

theorem Th4: :: BINOP_1:4
canceled;

theorem Th5: :: BINOP_1:5
canceled;

theorem Th6: :: BINOP_1:6
canceled;

theorem Th7: :: BINOP_1:7
canceled;

theorem Th8: :: BINOP_1:8
canceled;

theorem Th9: :: BINOP_1:9
canceled;

theorem Th10: :: BINOP_1:10
canceled;

theorem Th11: :: BINOP_1:11
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b3 is_a_unity_wrt b2 iff for b4 being Element of b1 holds
( b2 . b3,b4 = b4 & b2 . b4,b3 = b4 ) )
proof end;

theorem Th12: :: BINOP_1:12
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 st b2 is commutative holds
( b3 is_a_unity_wrt b2 iff for b4 being Element of b1 holds b2 . b3,b4 = b4 )
proof end;

theorem Th13: :: BINOP_1:13
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 st b2 is commutative holds
( b3 is_a_unity_wrt b2 iff for b4 being Element of b1 holds b2 . b4,b3 = b4 )
proof end;

theorem Th14: :: BINOP_1:14
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 st b2 is commutative holds
( b3 is_a_unity_wrt b2 iff b3 is_a_left_unity_wrt b2 )
proof end;

theorem Th15: :: BINOP_1:15
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 st b2 is commutative holds
( b3 is_a_unity_wrt b2 iff b3 is_a_right_unity_wrt b2 )
proof end;

theorem Th16: :: BINOP_1:16
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 st b2 is commutative holds
( b3 is_a_left_unity_wrt b2 iff b3 is_a_right_unity_wrt b2 )
proof end;

theorem Th17: :: BINOP_1:17
for b1 being set
for b2 being BinOp of b1
for b3, b4 being Element of b1 st b3 is_a_left_unity_wrt b2 & b4 is_a_right_unity_wrt b2 holds
b3 = b4
proof end;

theorem Th18: :: BINOP_1:18
for b1 being set
for b2 being BinOp of b1
for b3, b4 being Element of b1 st b3 is_a_unity_wrt b2 & b4 is_a_unity_wrt b2 holds
b3 = b4
proof end;

definition
let c1 be set ;
let c2 be BinOp of c1;
assume E13: ex b1 being Element of c1 st b1 is_a_unity_wrt c2 ;
func the_unity_wrt c2 -> Element of a1 means :: BINOP_1:def 8
a3 is_a_unity_wrt a2;
existence
ex b1 being Element of c1 st b1 is_a_unity_wrt c2 by E13;
uniqueness
for b1, b2 being Element of c1 st b1 is_a_unity_wrt c2 & b2 is_a_unity_wrt c2 holds
b1 = b2 by Th18;
end;

:: deftheorem Def8 defines the_unity_wrt BINOP_1:def 8 :
for b1 being set
for b2 being BinOp of b1 st ex b3 being Element of b1 st b3 is_a_unity_wrt b2 holds
for b3 being Element of b1 holds
( b3 = the_unity_wrt b2 iff b3 is_a_unity_wrt b2 );

definition
let c1 be set ;
let c2, c3 be BinOp of c1;
pred c2 is_left_distributive_wrt c3 means :Def9: :: BINOP_1:def 9
for b1, b2, b3 being Element of a1 holds a2 . b1,(a3 . b2,b3) = a3 . (a2 . b1,b2),(a2 . b1,b3);
pred c2 is_right_distributive_wrt c3 means :Def10: :: BINOP_1:def 10
for b1, b2, b3 being Element of a1 holds a2 . (a3 . b1,b2),b3 = a3 . (a2 . b1,b3),(a2 . b2,b3);
end;

:: deftheorem Def9 defines is_left_distributive_wrt BINOP_1:def 9 :
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_left_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . b4,(b3 . b5,b6) = b3 . (b2 . b4,b5),(b2 . b4,b6) );

:: deftheorem Def10 defines is_right_distributive_wrt BINOP_1:def 10 :
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_right_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . (b3 . b4,b5),b6 = b3 . (b2 . b4,b6),(b2 . b5,b6) );

definition
let c1 be set ;
let c2, c3 be BinOp of c1;
pred c2 is_distributive_wrt c3 means :: BINOP_1:def 11
( a2 is_left_distributive_wrt a3 & a2 is_right_distributive_wrt a3 );
end;

:: deftheorem Def11 defines is_distributive_wrt BINOP_1:def 11 :
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff ( b2 is_left_distributive_wrt b3 & b2 is_right_distributive_wrt b3 ) );

theorem Th19: :: BINOP_1:19
canceled;

theorem Th20: :: BINOP_1:20
canceled;

theorem Th21: :: BINOP_1:21
canceled;

theorem Th22: :: BINOP_1:22
canceled;

theorem Th23: :: BINOP_1:23
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds
( b2 . b4,(b3 . b5,b6) = b3 . (b2 . b4,b5),(b2 . b4,b6) & b2 . (b3 . b4,b5),b6 = b3 . (b2 . b4,b6),(b2 . b5,b6) ) )
proof end;

theorem Th24: :: BINOP_1:24
for b1 being non empty set
for b2, b3 being BinOp of b1 st b3 is commutative holds
( b3 is_distributive_wrt b2 iff for b4, b5, b6 being Element of b1 holds b3 . b4,(b2 . b5,b6) = b2 . (b3 . b4,b5),(b3 . b4,b6) )
proof end;

theorem Th25: :: BINOP_1:25
for b1 being non empty set
for b2, b3 being BinOp of b1 st b3 is commutative holds
( b3 is_distributive_wrt b2 iff for b4, b5, b6 being Element of b1 holds b3 . (b2 . b4,b5),b6 = b2 . (b3 . b4,b6),(b3 . b5,b6) )
proof end;

theorem Th26: :: BINOP_1:26
for b1 being non empty set
for b2, b3 being BinOp of b1 st b3 is commutative holds
( b3 is_distributive_wrt b2 iff b3 is_left_distributive_wrt b2 )
proof end;

theorem Th27: :: BINOP_1:27
for b1 being non empty set
for b2, b3 being BinOp of b1 st b3 is commutative holds
( b3 is_distributive_wrt b2 iff b3 is_right_distributive_wrt b2 )
proof end;

theorem Th28: :: BINOP_1:28
for b1 being non empty set
for b2, b3 being BinOp of b1 st b3 is commutative holds
( b3 is_right_distributive_wrt b2 iff b3 is_left_distributive_wrt b2 )
proof end;

definition
let c1 be set ;
let c2 be UnOp of c1;
let c3 be BinOp of c1;
pred c2 is_distributive_wrt c3 means :Def12: :: BINOP_1:def 12
for b1, b2 being Element of a1 holds a2 . (a3 . b1,b2) = a3 . (a2 . b1),(a2 . b2);
end;

:: deftheorem Def12 defines is_distributive_wrt BINOP_1:def 12 :
for b1 being set
for b2 being UnOp of b1
for b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff for b4, b5 being Element of b1 holds b2 . (b3 . b4,b5) = b3 . (b2 . b4),(b2 . b5) );

definition
let c1 be non empty set ;
let c2 be BinOp of c1;
redefine attr a2 is commutative means :: BINOP_1:def 13
for b1, b2 being Element of a1 holds a2 . b1,b2 = a2 . b2,b1;
correctness
compatibility
( c2 is commutative iff for b1, b2 being Element of c1 holds c2 . b1,b2 = c2 . b2,b1 );
by Def2;
redefine attr a2 is associative means :: BINOP_1:def 14
for b1, b2, b3 being Element of a1 holds a2 . b1,(a2 . b2,b3) = a2 . (a2 . b1,b2),b3;
correctness
compatibility
( c2 is associative iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c2 . b2,b3) = c2 . (c2 . b1,b2),b3 );
by Def3;
redefine attr a2 is idempotent means :: BINOP_1:def 15
for b1 being Element of a1 holds a2 . b1,b1 = b1;
correctness
compatibility
( c2 is idempotent iff for b1 being Element of c1 holds c2 . b1,b1 = b1 );
by Def4;
end;

:: deftheorem Def13 defines commutative BINOP_1:def 13 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( b2 is commutative iff for b3, b4 being Element of b1 holds b2 . b3,b4 = b2 . b4,b3 );

:: deftheorem Def14 defines associative BINOP_1:def 14 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( b2 is associative iff for b3, b4, b5 being Element of b1 holds b2 . b3,(b2 . b4,b5) = b2 . (b2 . b3,b4),b5 );

:: deftheorem Def15 defines idempotent BINOP_1:def 15 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( b2 is idempotent iff for b3 being Element of b1 holds b2 . b3,b3 = b3 );

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
redefine pred c2 is_a_left_unity_wrt c3 means :: BINOP_1:def 16
for b1 being Element of a1 holds a3 . a2,b1 = b1;
correctness
compatibility
( c2 is_a_left_unity_wrt c3 iff for b1 being Element of c1 holds c3 . c2,b1 = b1 );
by Def5;
redefine pred c2 is_a_right_unity_wrt c3 means :: BINOP_1:def 17
for b1 being Element of a1 holds a3 . b1,a2 = b1;
correctness
compatibility
( c2 is_a_right_unity_wrt c3 iff for b1 being Element of c1 holds c3 . b1,c2 = b1 );
by Def6;
end;

:: deftheorem Def16 defines is_a_left_unity_wrt BINOP_1:def 16 :
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_left_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b2,b4 = b4 );

:: deftheorem Def17 defines is_a_right_unity_wrt BINOP_1:def 17 :
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_right_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b4,b2 = b4 );

definition
let c1 be non empty set ;
let c2, c3 be BinOp of c1;
redefine pred c2 is_left_distributive_wrt c3 means :: BINOP_1:def 18
for b1, b2, b3 being Element of a1 holds a2 . b1,(a3 . b2,b3) = a3 . (a2 . b1,b2),(a2 . b1,b3);
correctness
compatibility
( c2 is_left_distributive_wrt c3 iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) );
by Def9;
redefine pred c2 is_right_distributive_wrt c3 means :: BINOP_1:def 19
for b1, b2, b3 being Element of a1 holds a2 . (a3 . b1,b2),b3 = a3 . (a2 . b1,b3),(a2 . b2,b3);
correctness
compatibility
( c2 is_right_distributive_wrt c3 iff for b1, b2, b3 being Element of c1 holds c2 . (c3 . b1,b2),b3 = c3 . (c2 . b1,b3),(c2 . b2,b3) );
by Def10;
end;

:: deftheorem Def18 defines is_left_distributive_wrt BINOP_1:def 18 :
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b2 is_left_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . b4,(b3 . b5,b6) = b3 . (b2 . b4,b5),(b2 . b4,b6) );

:: deftheorem Def19 defines is_right_distributive_wrt BINOP_1:def 19 :
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b2 is_right_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . (b3 . b4,b5),b6 = b3 . (b2 . b4,b6),(b2 . b5,b6) );

definition
let c1 be non empty set ;
let c2 be UnOp of c1;
let c3 be BinOp of c1;
redefine pred c2 is_distributive_wrt c3 means :: BINOP_1:def 20
for b1, b2 being Element of a1 holds a2 . (a3 . b1,b2) = a3 . (a2 . b1),(a2 . b2);
correctness
compatibility
( c2 is_distributive_wrt c3 iff for b1, b2 being Element of c1 holds c2 . (c3 . b1,b2) = c3 . (c2 . b1),(c2 . b2) );
by Def12;
end;

:: deftheorem Def20 defines is_distributive_wrt BINOP_1:def 20 :
for b1 being non empty set
for b2 being UnOp of b1
for b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff for b4, b5 being Element of b1 holds b2 . (b3 . b4,b5) = b3 . (b2 . b4),(b2 . b5) );