:: BCIALG_1 semantic presentation

definition
attr c1 is strict;
struct BCIStr -> 1-sorted ;
aggr BCIStr(# carrier, InternalDiff #) -> BCIStr ;
sel InternalDiff c1 -> BinOp of the carrier of c1;
end;

registration
cluster non empty strict BCIStr ;
existence
ex b1 being BCIStr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let A be BCIStr ;
let x, y be Element of A;
func x \ y -> Element of A equals :: BCIALG_1:def 1
the InternalDiff of A . x,y;
coherence
the InternalDiff of A . x,y is Element of A
proof end;
end;

:: deftheorem defines \ BCIALG_1:def 1 :
for A being BCIStr
for x, y being Element of A holds x \ y = the InternalDiff of A . x,y;

definition
attr c1 is strict;
struct BCIStr_0 -> BCIStr , ZeroStr ;
aggr BCIStr_0(# carrier, InternalDiff, ZeroF #) -> BCIStr_0 ;
end;

registration
cluster non empty strict BCIStr_0 ;
existence
ex b1 being BCIStr_0 st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let IT be non empty BCIStr_0 ;
let x be Element of IT;
func x ` -> Element of IT equals :: BCIALG_1:def 2
(0. IT) \ x;
coherence
(0. IT) \ x is Element of IT ;
end;

:: deftheorem defines ` BCIALG_1:def 2 :
for IT being non empty BCIStr_0
for x being Element of IT holds x ` = (0. IT) \ x;

definition
let IT be non empty BCIStr_0 ;
attr IT is being_B means :Def3: :: BCIALG_1:def 3
for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT;
attr IT is being_C means :Def4: :: BCIALG_1:def 4
for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT;
attr IT is being_I means :Def5: :: BCIALG_1:def 5
for x being Element of IT holds x \ x = 0. IT;
attr IT is being_K means :Def6: :: BCIALG_1:def 6
for x, y being Element of IT holds (x \ y) \ x = 0. IT;
attr IT is being_BCI-4 means :Def7: :: BCIALG_1:def 7
for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y;
attr IT is being_BCK-5 means :Def8: :: BCIALG_1:def 8
for x being Element of IT holds x ` = 0. IT;
end;

:: deftheorem Def3 defines being_B BCIALG_1:def 3 :
for IT being non empty BCIStr_0 holds
( IT is being_B iff for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT );

:: deftheorem Def4 defines being_C BCIALG_1:def 4 :
for IT being non empty BCIStr_0 holds
( IT is being_C iff for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT );

:: deftheorem Def5 defines being_I BCIALG_1:def 5 :
for IT being non empty BCIStr_0 holds
( IT is being_I iff for x being Element of IT holds x \ x = 0. IT );

:: deftheorem Def6 defines being_K BCIALG_1:def 6 :
for IT being non empty BCIStr_0 holds
( IT is being_K iff for x, y being Element of IT holds (x \ y) \ x = 0. IT );

:: deftheorem Def7 defines being_BCI-4 BCIALG_1:def 7 :
for IT being non empty BCIStr_0 holds
( IT is being_BCI-4 iff for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y );

:: deftheorem Def8 defines being_BCK-5 BCIALG_1:def 8 :
for IT being non empty BCIStr_0 holds
( IT is being_BCK-5 iff for x being Element of IT holds x ` = 0. IT );

notation
let IT be non empty BCIStr_0 ;
synonym IT is_B for being_B IT;
synonym IT is_C for being_C IT;
synonym IT is_I for being_I IT;
synonym IT is_K for being_K IT;
synonym IT is_BCI-4 for being_BCI-4 IT;
synonym IT is_BCK-5 for being_BCK-5 IT;
end;

definition
func BCI-EXAMPLE -> BCIStr_0 equals :: BCIALG_1:def 9
 BCIStr_0(# {{} },op2 ,op0 #);
coherence
BCIStr_0(# {{} },op2 ,op0 #) is BCIStr_0 ;
end;

:: deftheorem defines BCI-EXAMPLE BCIALG_1:def 9 :
BCI-EXAMPLE = BCIStr_0(# {{} },op2 ,op0 #);

registration
cluster BCI-EXAMPLE -> non empty strict ;
coherence
( BCI-EXAMPLE is strict & not BCI-EXAMPLE is empty )
proof end;
end;

Lm1: ( BCI-EXAMPLE is_B & BCI-EXAMPLE is_C & BCI-EXAMPLE is_I & BCI-EXAMPLE is_BCI-4 )
proof end;

registration
cluster non empty strict being_B being_C being_I being_BCI-4 BCIStr_0 ;
existence
ex b1 being non empty BCIStr_0 st
( b1 is strict & b1 is being_B & b1 is being_C & b1 is being_I & b1 is being_BCI-4 ) by Lm1;
end;

definition
mode BCI-algebra is non empty being_B being_C being_I being_BCI-4 BCIStr_0 ;
end;

definition
let X be BCI-algebra;
mode SubAlgebra of X -> BCI-algebra means :Def10: :: BCIALG_1:def 10
( 0. it = 0. X & the carrier of it c= the carrier of X & the InternalDiff of it = the InternalDiff of X || the carrier of it );
existence
ex b1 being BCI-algebra st
( 0. b1 = 0. X & the carrier of b1 c= the carrier of X & the InternalDiff of b1 = the InternalDiff of X || the carrier of b1 )
proof end;
end;

:: deftheorem Def10 defines SubAlgebra BCIALG_1:def 10 :
for X, b2 being BCI-algebra holds
( b2 is SubAlgebra of X iff ( 0. b2 = 0. X & the carrier of b2 c= the carrier of X & the InternalDiff of b2 = the InternalDiff of X || the carrier of b2 ) );

theorem Th1: :: BCIALG_1:1
for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is_I & X is_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) )
proof end;

registration
cluster strict being_BCK-5 BCIStr_0 ;
existence
ex b1 being BCI-algebra st
( b1 is strict & b1 is being_BCK-5 )
proof end;
end;

definition
mode BCK-algebra is being_BCK-5 BCI-algebra;
end;

definition
let IT be non empty BCIStr_0 ;
let x, y be Element of IT;
pred x <= y means :Def11: :: BCIALG_1:def 11
x \ y = 0. IT;
end;

:: deftheorem Def11 defines <= BCIALG_1:def 11 :
for IT being non empty BCIStr_0
for x, y being Element of IT holds
( x <= y iff x \ y = 0. IT );

Lm2: for X being BCI-algebra
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X
proof end;

theorem Th2: :: BCIALG_1:2
for X being BCI-algebra
for x being Element of X holds x \ (0. X) = x
proof end;

theorem Th3: :: BCIALG_1:3
for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
proof end;

theorem Th4: :: BCIALG_1:4
for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
proof end;

theorem :: BCIALG_1:5
for X being BCI-algebra
for x, y, z being Element of X st x <= y holds
( x \ z <= y \ z & z \ y <= z \ x )
proof end;

theorem :: BCIALG_1:6
for X being BCI-algebra
for x, y being Element of X st x \ y = 0. X holds
(y \ x) ` = 0. X
proof end;

theorem Th7: :: BCIALG_1:7
for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
proof end;

theorem Th8: :: BCIALG_1:8
for X being BCI-algebra
for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y
proof end;

theorem Th9: :: BCIALG_1:9
for X being BCI-algebra
for x, y being Element of X holds (x \ y) ` = (x ` ) \ (y ` )
proof end;

theorem Th10: :: BCIALG_1:10
for X being BCI-algebra
for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X
proof end;

theorem :: BCIALG_1:11
for X being non empty BCIStr_0 holds
( X is BCI-algebra iff ( X is_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )
proof end;

theorem :: BCIALG_1:12
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds
X is BCK-algebra
proof end;

theorem :: BCIALG_1:13
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) holds
X is BCK-algebra
proof end;

theorem :: BCIALG_1:14
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) holds
X is BCK-algebra
proof end;

theorem :: BCIALG_1:15
for X being BCI-algebra st ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds
X is BCK-algebra
proof end;

theorem :: BCIALG_1:16
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds
X is BCK-algebra
proof end;

theorem :: BCIALG_1:17
for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds
X is BCK-algebra
proof end;

theorem :: BCIALG_1:18
for X being BCI-algebra holds
( X is_K iff X is BCK-algebra )
proof end;

definition
let X be BCI-algebra;
func BCK-part X -> non empty Subset of X equals :: BCIALG_1:def 12
{ x where x is Element of X : 0. X <= x } ;
coherence
{ x where x is Element of X : 0. X <= x } is non empty Subset of X
proof end;
end;

:: deftheorem defines BCK-part BCIALG_1:def 12 :
for X being BCI-algebra holds BCK-part X = { x where x is Element of X : 0. X <= x } ;

theorem Th19: :: BCIALG_1:19
for X being BCI-algebra holds 0. X in BCK-part X
proof end;

registration
let X be BCI-algebra;
cluster 0. X -> Element of BCK-part X;
coherence
0. X is Element of BCK-part X by Th19;
end;

theorem :: BCIALG_1:20
for X being BCI-algebra
for x, y being Element of BCK-part X holds x \ y in BCK-part X
proof end;

theorem :: BCIALG_1:21
for X being BCI-algebra
for x being Element of X
for y being Element of BCK-part X holds x \ y <= x
proof end;

theorem Th22: :: BCIALG_1:22
for X being BCI-algebra holds X is SubAlgebra of X
proof end;

definition
let X be BCI-algebra;
let IT be SubAlgebra of X;
attr IT is proper means :Def13: :: BCIALG_1:def 13
IT <> X;
end;

:: deftheorem Def13 defines proper BCIALG_1:def 13 :
for X being BCI-algebra
for IT being SubAlgebra of X holds
( IT is proper iff IT <> X );

registration
let X be BCI-algebra;
cluster non proper SubAlgebra of X;
existence
not for b1 being SubAlgebra of X holds b1 is proper
proof end;
end;

definition
let X be BCI-algebra;
let IT be Element of X;
attr IT is atom means :Def14: :: BCIALG_1:def 14
for z being Element of X st z \ IT = 0. X holds
z = IT;
end;

:: deftheorem Def14 defines atom BCIALG_1:def 14 :
for X being BCI-algebra
for IT being Element of X holds
( IT is atom iff for z being Element of X st z \ IT = 0. X holds
z = IT );

definition
let X be BCI-algebra;
func AtomSet X -> non empty Subset of X equals :: BCIALG_1:def 15
{ x where x is Element of X : x is atom } ;
coherence
{ x where x is Element of X : x is atom } is non empty Subset of X
proof end;
end;

:: deftheorem defines AtomSet BCIALG_1:def 15 :
for X being BCI-algebra holds AtomSet X = { x where x is Element of X : x is atom } ;

theorem Th23: :: BCIALG_1:23
for X being BCI-algebra holds 0. X in AtomSet X
proof end;

theorem Th24: :: BCIALG_1:24
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x )
proof end;

theorem :: BCIALG_1:25
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u )
proof end;

theorem :: BCIALG_1:26
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) )
proof end;

theorem :: BCIALG_1:27
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) )
proof end;

theorem Th28: :: BCIALG_1:28
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z ` ) \ (x ` ) = x \ z )
proof end;

theorem Th29: :: BCIALG_1:29
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff (x ` ) ` = x )
proof end;

theorem Th30: :: BCIALG_1:30
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )
proof end;

theorem Th31: :: BCIALG_1:31
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds ((x \ z) ` ) ` = x \ z )
proof end;

theorem :: BCIALG_1:32
for X being BCI-algebra
for x being Element of X holds
( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u )
proof end;

theorem Th33: :: BCIALG_1:33
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of X holds a \ x in AtomSet X
proof end;

definition
let X be BCI-algebra;
let a, b be Element of AtomSet X;
:: original: \
redefine func a \ b -> Element of AtomSet X;
coherence
a \ b is Element of AtomSet X by Th33;
end;

theorem Th34: :: BCIALG_1:34
for X being BCI-algebra
for x being Element of X holds x ` in AtomSet X
proof end;

theorem Th35: :: BCIALG_1:35
for X being BCI-algebra
for x being Element of X ex a being Element of AtomSet X st a <= x
proof end;

definition
let X be BCI-algebra;
attr X is generated_by_atom means :Def16: :: BCIALG_1:def 16
for x being Element of X ex a being Element of AtomSet X st a <= x;
end;

:: deftheorem Def16 defines generated_by_atom BCIALG_1:def 16 :
for X being BCI-algebra holds
( X is generated_by_atom iff for x being Element of X ex a being Element of AtomSet X st a <= x );

definition
let X be BCI-algebra;
let a be Element of AtomSet X;
func BranchV a -> non empty Subset of X equals :: BCIALG_1:def 17
{ x where x is Element of X : a <= x } ;
coherence
{ x where x is Element of X : a <= x } is non empty Subset of X
proof end;
end;

:: deftheorem defines BranchV BCIALG_1:def 17 :
for X being BCI-algebra
for a being Element of AtomSet X holds BranchV a = { x where x is Element of X : a <= x } ;

theorem :: BCIALG_1:36
for X being BCI-algebra holds X is generated_by_atom
proof end;

theorem :: BCIALG_1:37
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV b holds a \ x = a \ b
proof end;

theorem Th38: :: BCIALG_1:38
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BCK-part X holds a \ x = a
proof end;

Lm3: for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BranchV a holds a \ x = 0. X
proof end;

theorem Th39: :: BCIALG_1:39
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b holds x \ y in BranchV (a \ b)
proof end;

theorem :: BCIALG_1:40
for X being BCI-algebra
for a being Element of AtomSet X
for x, y being Element of BranchV a holds x \ y in BCK-part X
proof end;

theorem :: BCIALG_1:41
for X being BCI-algebra
for a, b being Element of AtomSet X
for x being Element of BranchV a
for y being Element of BranchV b st a <> b holds
not x \ y in BCK-part X
proof end;

theorem :: BCIALG_1:42
for X being BCI-algebra
for a, b being Element of AtomSet X st a <> b holds
(BranchV a) /\ (BranchV b) = {}
proof end;

definition
let X be BCI-algebra;
mode Ideal of X -> non empty Subset of X means :Def18: :: BCIALG_1:def 18
( 0. X in it & ( for x, y being Element of X st x \ y in it & y in it holds
x in it ) );
existence
ex b1 being non empty Subset of X st
( 0. X in b1 & ( for x, y being Element of X st x \ y in b1 & y in b1 holds
x in b1 ) )
proof end;
end;

:: deftheorem Def18 defines Ideal BCIALG_1:def 18 :
for X being BCI-algebra
for b2 being non empty Subset of X holds
( b2 is Ideal of X iff ( 0. X in b2 & ( for x, y being Element of X st x \ y in b2 & y in b2 holds
x in b2 ) ) );

definition
let X be BCI-algebra;
let IT be Ideal of X;
attr IT is closed means :Def19: :: BCIALG_1:def 19
for x being Element of IT holds x ` in IT;
end;

:: deftheorem Def19 defines closed BCIALG_1:def 19 :
for X being BCI-algebra
for IT being Ideal of X holds
( IT is closed iff for x being Element of IT holds x ` in IT );

Lm4: for X being BCI-algebra holds {(0. X)} is Ideal of X
proof end;

Lm5: for X being BCI-algebra
for X1 being Ideal of X st X1 = {(0. X)} holds
for x being Element of X1 holds x ` in {(0. X)}
proof end;

registration
let X be BCI-algebra;
cluster non empty closed Ideal of X;
existence
ex b1 being Ideal of X st b1 is closed
proof end;
end;

theorem :: BCIALG_1:43
for X being BCI-algebra holds {(0. X)} is