:: by Yuzhong Ding

::

:: Received February 23, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

definition

attr c_{1} is strict ;

struct BCIStr -> 1-sorted ;

aggr BCIStr(# carrier, InternalDiff #) -> BCIStr ;

sel InternalDiff c_{1} -> BinOp of the carrier of c_{1};

end;
struct BCIStr -> 1-sorted ;

aggr BCIStr(# carrier, InternalDiff #) -> BCIStr ;

sel InternalDiff c

registration
end;

definition

let A be BCIStr ;

let x, y be Element of A;

coherence

the InternalDiff of A . (x,y) is Element of A ;

end;
let x, y be Element of A;

coherence

the InternalDiff of A . (x,y) is Element of A ;

:: 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);

for A being BCIStr

for x, y being Element of A holds x \ y = the InternalDiff of A . (x,y);

definition

attr c_{1} is strict ;

struct BCIStr_0 -> BCIStr , ZeroStr ;

aggr BCIStr_0(# carrier, InternalDiff, ZeroF #) -> BCIStr_0 ;

end;
struct BCIStr_0 -> BCIStr , ZeroStr ;

aggr BCIStr_0(# carrier, InternalDiff, ZeroF #) -> BCIStr_0 ;

registration
end;

definition
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;

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 ;

end;
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;

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;

for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT;

:: 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 );

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 );

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 );

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 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 );

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 );

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 );

for IT being non empty BCIStr_0 holds

( IT is being_BCK-5 iff for x being Element of IT holds x ` = 0. IT );

registration

coherence

( BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) by STRUCT_0:def 10;

end;
( BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) by STRUCT_0:def 10;

registration

existence

ex b_{1} being non empty BCIStr_0 st

( b_{1} is strict & b_{1} is being_B & b_{1} is being_C & b_{1} is being_I & b_{1} is being_BCI-4 & b_{1} is being_BCK-5 )

end;
ex b

( b

proof end;

definition

let X be BCI-algebra;

ex b_{1} being BCI-algebra st

( 0. b_{1} = 0. X & the carrier of b_{1} c= the carrier of X & the InternalDiff of b_{1} = the InternalDiff of X || the carrier of b_{1} )

end;
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 ( 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 );

ex b

( 0. b

proof end;

:: deftheorem Def10 defines SubAlgebra BCIALG_1:def 10 :

for X, b_{2} being BCI-algebra holds

( b_{2} is SubAlgebra of X iff ( 0. b_{2} = 0. X & the carrier of b_{2} c= the carrier of X & the InternalDiff of b_{2} = the InternalDiff of X || the carrier of b_{2} ) );

for X, b

( b

::T1.1.11

theorem Th1: :: BCIALG_1:1

for X being non empty BCIStr_0 holds

( X is BCI-algebra iff ( X is being_I & X is being_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 ) ) ) )

( X is BCI-algebra iff ( X is being_I & X is being_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;

:: deftheorem 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 );

for IT being non empty BCIStr_0

for x, y being Element of IT holds

( x <= y iff x \ y = 0. IT );

Lm1: for X being BCI-algebra

for x being Element of X st x \ (0. X) = 0. X holds

x = 0. 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

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 )

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

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

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 being_BCI-4 & ( for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )

( X is BCI-algebra iff ( X is being_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

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

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

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

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

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

for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds

X is BCK-algebra

proof end;

definition

let X be BCI-algebra;

{ x where x is Element of X : 0. X <= x } is non empty Subset of X

end;
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 } ;

{ x where x is Element of X : 0. X <= x } is non empty Subset of X

proof 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 } ;

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

:: 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 );

for X being BCI-algebra

for IT being SubAlgebra of X holds

( IT is proper iff IT <> X );

registration

let X be BCI-algebra;

existence

not for b_{1} being SubAlgebra of X holds b_{1} is proper

end;
existence

not for b

proof end;

:: deftheorem 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 );

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;

{ x where x is Element of X : x is atom } is non empty Subset of X

end;
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 } ;

{ x where x is Element of X : x is atom } is non empty Subset of X

proof 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 } ;

for X being BCI-algebra holds AtomSet X = { x where x is Element of X : x is atom } ;

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 )

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 )

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) )

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) )

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 )

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 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 )

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 )

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 )

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

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;
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;

definition

let X be BCI-algebra;

end;
attr X is generated_by_atom means :: BCIALG_1:def 16

for x being Element of X ex a being Element of AtomSet X st a <= x;

for x being Element of X ex a being Element of AtomSet X st a <= x;

:: deftheorem 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 );

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;

{ x where x is Element of X : a <= x } is non empty Subset of X

end;
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 } ;

{ x where x is Element of X : a <= x } is non empty Subset of X

proof 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 } ;

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: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

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

for a being Element of AtomSet X

for x being Element of BCK-part X holds a \ x = a

proof end;

Lm2: 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)

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

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

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) = {}

for a, b being Element of AtomSet X st a <> b holds

(BranchV a) /\ (BranchV b) = {}

proof end;

::Ideal

definition

let X be BCI-algebra;

ex b_{1} being non empty Subset of X st

( 0. X in b_{1} & ( for x, y being Element of X st x \ y in b_{1} & y in b_{1} holds

x in b_{1} ) )

end;
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 ( 0. X in it & ( for x, y being Element of X st x \ y in it & y in it holds

x in it ) );

ex b

( 0. X in b

x in b

proof end;

:: deftheorem Def18 defines Ideal BCIALG_1:def 18 :

for X being BCI-algebra

for b_{2} being non empty Subset of X holds

( b_{2} is Ideal of X iff ( 0. X in b_{2} & ( for x, y being Element of X st x \ y in b_{2} & y in b_{2} holds

x in b_{2} ) ) );

for X being BCI-algebra

for b

( b

x in b

:: 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 );

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 );

Lm3: for X being BCI-algebra holds {(0. X)} is Ideal of X

proof end;

Lm4: 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
end;

Lm5: for X being BCI-algebra

for IT being non empty Subset of X st IT is Ideal of X holds

for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT

proof end;

theorem :: BCIALG_1:46

for X being BCI-algebra

for IT being non empty Subset of X st IT is Ideal of X holds

for x, y being Element of X st x in IT & y <= x holds

y in IT

for IT being non empty Subset of X st IT is Ideal of X holds

for x, y being Element of X st x in IT & y <= x holds

y in IT

proof end;

definition

let IT be BCI-algebra;

end;
attr IT is associative means :Def20: :: BCIALG_1:def 20

for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z);

for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z);

attr IT is quasi-associative means :: BCIALG_1:def 21

for x being Element of IT holds (x `) ` = x ` ;

for x being Element of IT holds (x `) ` = x ` ;

attr IT is positive-implicative means :: BCIALG_1:def 22

for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)));

for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)));

attr IT is weakly-positive-implicative means :Def23: :: BCIALG_1:def 23

for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z);

for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z);

attr IT is implicative means :Def24: :: BCIALG_1:def 24

for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x);

for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x);

attr IT is weakly-implicative means :: BCIALG_1:def 25

for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x;

for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x;

attr IT is p-Semisimple means :Def26: :: BCIALG_1:def 26

for x, y being Element of IT holds x \ (x \ y) = y;

for x, y being Element of IT holds x \ (x \ y) = y;

:: deftheorem Def20 defines associative BCIALG_1:def 20 :

for IT being BCI-algebra holds

( IT is associative iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z) );

for IT being BCI-algebra holds

( IT is associative iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z) );

:: deftheorem defines quasi-associative BCIALG_1:def 21 :

for IT being BCI-algebra holds

( IT is quasi-associative iff for x being Element of IT holds (x `) ` = x ` );

for IT being BCI-algebra holds

( IT is quasi-associative iff for x being Element of IT holds (x `) ` = x ` );

:: deftheorem defines positive-implicative BCIALG_1:def 22 :

for IT being BCI-algebra holds

( IT is positive-implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) );

for IT being BCI-algebra holds

( IT is positive-implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) );

:: deftheorem Def23 defines weakly-positive-implicative BCIALG_1:def 23 :

for IT being BCI-algebra holds

( IT is weakly-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) );

for IT being BCI-algebra holds

( IT is weakly-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) );

:: deftheorem Def24 defines implicative BCIALG_1:def 24 :

for IT being BCI-algebra holds

( IT is implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) );

for IT being BCI-algebra holds

( IT is implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) );

:: deftheorem defines weakly-implicative BCIALG_1:def 25 :

for IT being BCI-algebra holds

( IT is weakly-implicative iff for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x );

for IT being BCI-algebra holds

( IT is weakly-implicative iff for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x );

:: deftheorem Def26 defines p-Semisimple BCIALG_1:def 26 :

for IT being BCI-algebra holds

( IT is p-Semisimple iff for x, y being Element of IT holds x \ (x \ y) = y );

for IT being BCI-algebra holds

( IT is p-Semisimple iff for x, y being Element of IT holds x \ (x \ y) = y );

:: deftheorem defines alternative BCIALG_1:def 27 :

for IT being BCI-algebra holds

( IT is alternative iff for x, y being Element of IT holds

( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) );

for IT being BCI-algebra holds

( IT is alternative iff for x, y being Element of IT holds

( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) );

registration

( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) by STRUCT_0:def 10;

end;

cluster BCI-EXAMPLE -> associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple ;

coherence ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) by STRUCT_0:def 10;

registration

ex b_{1} being BCI-algebra st

( b_{1} is implicative & b_{1} is positive-implicative & b_{1} is p-Semisimple & b_{1} is associative & b_{1} is weakly-implicative & b_{1} is weakly-positive-implicative )
end;

cluster non empty being_B being_C being_I being_BCI-4 associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple for BCIStr_0 ;

existence ex b

( b

proof end;

Lm6: for X being BCI-algebra st ( for x, y being Element of X holds y \ x = x \ y ) holds

X is associative

proof end;

Lm7: for X being BCI-algebra st ( for x being Element of X holds x ` = x ) holds

for x, y being Element of X holds x \ y = y \ x

proof end;

theorem Th48: :: BCIALG_1:48

for X being BCI-algebra holds

( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative )

( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative )

proof end;

theorem Th49: :: BCIALG_1:49

for X being non empty BCIStr_0 holds

( X is associative BCI-algebra iff for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )

( X is associative BCI-algebra iff for x, y, z being Element of X holds

( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )

proof end;

theorem Th50: :: BCIALG_1:50

for X being non empty BCIStr_0 holds

( X is associative BCI-algebra iff for x, y, z being Element of X holds

( (x \ y) \ (x \ z) = z \ y & x ` = x ) )

( X is associative BCI-algebra iff for x, y, z being Element of X holds

( (x \ y) \ (x \ z) = z \ y & x ` = x ) )

proof end;

theorem :: BCIALG_1:51

for X being non empty BCIStr_0 holds

( X is associative BCI-algebra iff for x, y, z being Element of X holds

( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) )

( X is associative BCI-algebra iff for x, y, z being Element of X holds

( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) )

proof end;

Lm8: for X being BCI-algebra holds

( ( for x, y being Element of X holds y \ (y \ x) = x ) iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )

proof end;

theorem :: BCIALG_1:55

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) ;

( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) ;

theorem Th56: :: BCIALG_1:56

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )

( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )

proof end;

theorem Th57: :: BCIALG_1:57

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) )

( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) )

proof end;

Lm9: for X being BCI-algebra st X is p-Semisimple holds

for x, y, z, u being Element of X holds

( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )

proof end;

Lm10: for X being BCI-algebra st X is p-Semisimple holds

for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y

proof end;

Lm11: for X being BCI-algebra st X is p-Semisimple holds

for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z

proof end;

Lm12: for X being BCI-algebra st X is p-Semisimple holds

for x, y, z being Element of X st x \ y = x \ z holds

y = z

proof end;

Lm13: for X being BCI-algebra st X is p-Semisimple holds

for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `)

proof end;

Lm14: for X being BCI-algebra st X is p-Semisimple holds

for x, y, z being Element of X st y \ x = z \ x holds

y = z

proof end;

theorem :: BCIALG_1:58

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) )

( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) )

proof end;

theorem Th59: :: BCIALG_1:59

for X being BCI-algebra holds

( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z )

( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z )

proof end;

theorem :: BCIALG_1:60

for X being BCI-algebra holds

( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) `) ` = x \ z )

( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) `) ` = x \ z )

proof end;

theorem :: BCIALG_1:61

for X being BCI-algebra holds

( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u )

( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u )

proof end;

theorem Th62: :: BCIALG_1:62

for X being BCI-algebra holds

( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds

x = 0. X )

( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds

x = 0. X )

proof end;

theorem Th63: :: BCIALG_1:63

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) )

( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) )

proof end;

theorem :: BCIALG_1:64

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) )

( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) )

proof end;

theorem :: BCIALG_1:65

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z )

( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z )

proof end;

theorem :: BCIALG_1:66

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) )

( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) )

proof end;

theorem :: BCIALG_1:67

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds

y = z )

( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds

y = z )

proof end;

theorem :: BCIALG_1:68

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds

y = z )

( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds

y = z )

proof end;

theorem :: BCIALG_1:69

for X being non empty BCIStr_0 holds

( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds

( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) )

( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds

( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) )

proof end;

theorem :: BCIALG_1:70

for X being non empty BCIStr_0 holds

( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) )

( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds

( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) )

proof end;

Lm15: for X being BCI-algebra st ( for x being Element of X holds x ` <= x ) holds

for x, y being Element of X holds (x \ y) ` = (y \ x) `

proof end;

Lm16: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) holds

for x, y being Element of X holds (x `) \ y = (x \ y) `

proof end;

Lm17: for X being BCI-algebra st ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) holds

for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X

proof end;

Lm18: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) holds

X is quasi-associative

proof end;

Lm19: for X being BCI-algebra holds

( ( for x being Element of X holds x ` <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )

proof end;

theorem Th71: :: BCIALG_1:71

for X being BCI-algebra holds

( X is quasi-associative iff for x being Element of X holds x ` <= x )

( X is quasi-associative iff for x being Element of X holds x ` <= x )

proof end;

theorem Th72: :: BCIALG_1:72

for X being BCI-algebra holds

( X is quasi-associative iff for x, y being Element of X holds (x \ y) ` = (y \ x) ` )

( X is quasi-associative iff for x, y being Element of X holds (x \ y) ` = (y \ x) ` )

proof end;

theorem Th73: :: BCIALG_1:73

for X being BCI-algebra holds

( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` )

( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` )

proof end;

theorem :: BCIALG_1:74

for X being BCI-algebra holds

( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )

( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )

proof end;

theorem :: BCIALG_1:75

for X being BCI-algebra holds

( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )

( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )

proof end;

theorem Th76: :: BCIALG_1:76

for X being BCI-algebra

for x, y being Element of X st X is alternative holds

( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )

for x, y being Element of X st X is alternative holds

( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )

proof end;

theorem :: BCIALG_1:77

for X being BCI-algebra

for x, a, b being Element of X st X is alternative & x \ a = x \ b holds

a = b

for x, a, b being Element of X st X is alternative & x \ a = x \ b holds

a = b

proof end;

theorem :: BCIALG_1:78

for X being BCI-algebra

for x, a, b being Element of X st X is alternative & a \ x = b \ x holds

a = b

for x, a, b being Element of X st X is alternative & a \ x = b \ x holds

a = b

proof end;

theorem :: BCIALG_1:80

for X being BCI-algebra

for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds

( a = x \ b & b = x \ a )

for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds

( a = x \ b & b = x \ a )

proof end;

Lm20: for X being BCI-algebra holds

( X is alternative iff X is associative )

proof end;

Lm21: for X being BCI-algebra st X is alternative holds

X is implicative

by Th76;

registration

coherence

for b_{1} being BCI-algebra st b_{1} is alternative holds

b_{1} is associative
by Lm20;

coherence

for b_{1} being BCI-algebra st b_{1} is associative holds

b_{1} is alternative
;

coherence

for b_{1} being BCI-algebra st b_{1} is alternative holds

b_{1} is implicative
by Lm21;

end;
for b

b

coherence

for b

b

coherence

for b

b

theorem :: BCIALG_1:81

for X being BCI-algebra

for x, y being Element of X st X is alternative holds

(x \ (x \ y)) \ (y \ x) = x

for x, y being Element of X st X is alternative holds

(x \ (x \ y)) \ (y \ x) = x

proof end;

theorem :: BCIALG_1:82

for X being BCI-algebra

for x, y being Element of X st X is alternative holds

y \ (y \ (x \ (x \ y))) = y

for x, y being Element of X st X is alternative holds

y \ (y \ (x \ (x \ y))) = y

proof end;

Lm22: for X being BCI-algebra st X is associative holds

X is weakly-positive-implicative

proof end;

Lm23: for X being BCI-algebra st X is p-Semisimple BCI-algebra holds

X is weakly-positive-implicative BCI-algebra

proof end;

registration

for b_{1} being BCI-algebra st b_{1} is associative holds

b_{1} is weakly-positive-implicative
by Lm22;

for b_{1} being BCI-algebra st b_{1} is p-Semisimple holds

b_{1} is weakly-positive-implicative
by Lm23;

end;

cluster non empty being_B being_C being_I being_BCI-4 associative -> weakly-positive-implicative for BCIStr_0 ;

coherence for b

b

cluster non empty being_B being_C being_I being_BCI-4 p-Semisimple -> weakly-positive-implicative for BCIStr_0 ;

coherence for b

b

theorem :: BCIALG_1:83

for X being non empty BCIStr_0 holds

( X is implicative BCI-algebra iff for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) )

( X is implicative BCI-algebra iff for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) )

proof end;

theorem Th84: :: BCIALG_1:84

for X being BCI-algebra holds

( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) )

( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) )

proof end;

Lm24: for X being BCI-algebra

for x, y being Element of X st X is weakly-positive-implicative holds

(x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)

proof end;

Lm25: for X being BCI-algebra holds

( X is positive-implicative iff X is weakly-positive-implicative )

proof end;

registration

for b_{1} being BCI-algebra st b_{1} is positive-implicative holds

b_{1} is weakly-positive-implicative
by Lm25;

for b_{1} being BCI-algebra st b_{1} is alternative holds

b_{1} is weakly-positive-implicative
;

end;

cluster non empty being_B being_C being_I being_BCI-4 positive-implicative -> weakly-positive-implicative for BCIStr_0 ;

coherence for b

b

cluster non empty being_B being_C being_I being_BCI-4 alternative -> weakly-positive-implicative for BCIStr_0 ;

coherence for b

b

theorem :: BCIALG_1:85

theorem :: BCIALG_1:86

for X being non empty BCIStr_0 holds

( X is positive-implicative BCI-algebra iff for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) )

( X is positive-implicative BCI-algebra iff for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) )

proof end;