:: BCIALG_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"BCIStr"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"BCIStr":::(# :::"carrier":::, :::"InternalDiff"::: #) -> ($#l1_bcialg_1 :::"BCIStr"::: ) ; sel :::"InternalDiff"::: "c1" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_bcialg_1 :::"strict"::: ) for ($#l1_bcialg_1 :::"BCIStr"::: ) ; end; definitionlet "A" be ($#l1_bcialg_1 :::"BCIStr"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "A")); func "x" :::"\"::: "y" -> ($#m1_subset_1 :::"Element":::) "of" "A" equals :: BCIALG_1:def 1 (Set (Set "the" ($#u1_bcialg_1 :::"InternalDiff"::: ) "of" "A") ($#k5_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::"\"::: BCIALG_1:def 1 : (Bool "for" (Set (Var "A")) "being" ($#l1_bcialg_1 :::"BCIStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_bcialg_1 :::"InternalDiff"::: ) "of" (Set (Var "A"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); definitionattr "c1" is :::"strict"::: ; struct :::"BCIStr_0"::: -> ($#l1_bcialg_1 :::"BCIStr"::: ) "," ($#l2_struct_0 :::"ZeroStr"::: ) ; aggr :::"BCIStr_0":::(# :::"carrier":::, :::"InternalDiff":::, :::"ZeroF"::: #) -> ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_bcialg_1 :::"strict"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "IT")); func "x" :::"`"::: -> ($#m1_subset_1 :::"Element":::) "of" "IT" equals :: BCIALG_1:def 2 (Set (Set "(" ($#k4_struct_0 :::"0."::: ) "IT" ")" ) ($#k1_bcialg_1 :::"\"::: ) "x"); end; :: deftheorem defines :::"`"::: BCIALG_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")))))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; attr "IT" is :::"being_B"::: means :: BCIALG_1:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))); attr "IT" is :::"being_C"::: means :: BCIALG_1:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))); attr "IT" is :::"being_I"::: means :: BCIALG_1:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))); attr "IT" is :::"being_K"::: means :: BCIALG_1:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))); attr "IT" is :::"being_BCI-4"::: means :: BCIALG_1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); attr "IT" is :::"being_BCK-5"::: means :: BCIALG_1:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))); end; :: deftheorem defines :::"being_B"::: BCIALG_1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_bcialg_1 :::"being_B"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) ")" )); :: deftheorem defines :::"being_C"::: BCIALG_1:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_bcialg_1 :::"being_C"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) ")" )); :: deftheorem defines :::"being_I"::: BCIALG_1:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_bcialg_1 :::"being_I"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) ")" )); :: deftheorem defines :::"being_K"::: BCIALG_1:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_bcialg_1 :::"being_K"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) ")" )); :: deftheorem defines :::"being_BCI-4"::: BCIALG_1:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_bcialg_1 :::"being_BCI-4"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); :: deftheorem defines :::"being_BCK-5"::: BCIALG_1:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_bcialg_1 :::"being_BCK-5"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) ")" )); definitionfunc :::"BCI-EXAMPLE"::: -> ($#l2_bcialg_1 :::"BCIStr_0"::: ) equals :: BCIALG_1:def 9 (Set ($#g2_bcialg_1 :::"BCIStr_0"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" ); end; :: deftheorem defines :::"BCI-EXAMPLE"::: BCIALG_1:def 9 : (Bool (Set ($#k3_bcialg_1 :::"BCI-EXAMPLE"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g2_bcialg_1 :::"BCIStr_0"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "#)" )); registration cluster (Set ($#k3_bcialg_1 :::"BCI-EXAMPLE"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_bcialg_1 :::"strict"::: ) ; end; registration cluster (Set ($#k3_bcialg_1 :::"BCI-EXAMPLE"::: ) ) -> ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v8_bcialg_1 :::"being_BCK-5"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_bcialg_1 :::"strict"::: ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v8_bcialg_1 :::"being_BCK-5"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; definitionmode BCI-algebra is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; definitionmode BCK-algebra is ($#v8_bcialg_1 :::"being_BCK-5"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::); end; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); mode :::"SubAlgebra"::: "of" "X" -> ($#l2_bcialg_1 :::"BCI-algebra":::) means :: BCIALG_1:def 10 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) & (Bool (Set "the" ($#u1_bcialg_1 :::"InternalDiff"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_bcialg_1 :::"InternalDiff"::: ) "of" "X") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ); end; :: deftheorem defines :::"SubAlgebra"::: BCIALG_1:def 10 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_bcialg_1 :::"SubAlgebra"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set "the" ($#u1_bcialg_1 :::"InternalDiff"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_bcialg_1 :::"InternalDiff"::: ) "of" (Set (Var "X"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" ) ")" )); theorem :: BCIALG_1:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_bcialg_1 :::"being_I"::: ) ) & (Bool (Set (Var "X")) "is" ($#v7_bcialg_1 :::"being_BCI-4"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ) ")" ) ")" ) ")" )) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "IT")); pred "x" :::"<="::: "y" means :: BCIALG_1:def 11 (Bool (Set "x" ($#k1_bcialg_1 :::"\"::: ) "y") ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")); end; :: deftheorem defines :::"<="::: BCIALG_1:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) ")" ))); theorem :: BCIALG_1:2 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: BCIALG_1:3 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))))) ; theorem :: BCIALG_1:4 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ))) ; theorem :: BCIALG_1:5 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")))) & (Bool (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")))) ")" ))) ; theorem :: BCIALG_1:6 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))))) ; theorem :: BCIALG_1:7 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))))) ; theorem :: BCIALG_1:8 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))))) ; theorem :: BCIALG_1:9 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k2_bcialg_1 :::"`"::: ) ")" ))))) ; theorem :: BCIALG_1:10 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))))) ; theorem :: BCIALG_1:11 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v7_bcialg_1 :::"being_BCI-4"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ")" ) ")" )) ; theorem :: BCIALG_1:12 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::))) ; theorem :: BCIALG_1:13 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::))) ; theorem :: BCIALG_1:14 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::))) ; theorem :: BCIALG_1:15 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::))) ; theorem :: BCIALG_1:16 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::))) ; theorem :: BCIALG_1:17 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) ")" )) "holds" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::))) ; theorem :: BCIALG_1:18 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_bcialg_1 :::"being_K"::: ) ) "iff" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::)) ")" )) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); func :::"BCK-part"::: "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BCIALG_1:def 12 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x"))) "}" ; end; :: deftheorem defines :::"BCK-part"::: BCIALG_1:def 12 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x"))) "}" )); theorem :: BCIALG_1:19 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ; theorem :: BCIALG_1:20 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X")))))) ; theorem :: BCIALG_1:21 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))))) ; theorem :: BCIALG_1:22 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_1 :::"SubAlgebra"::: ) "of" (Set (Var "X")))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "IT" be ($#m1_bcialg_1 :::"SubAlgebra"::: ) "of" (Set (Const "X")); attr "IT" is :::"proper"::: means :: BCIALG_1:def 13 (Bool "IT" ($#r1_hidden :::"<>"::: ) "X"); end; :: deftheorem defines :::"proper"::: BCIALG_1:def 13 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_bcialg_1 :::"SubAlgebra"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_bcialg_1 :::"proper"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r1_hidden :::"<>"::: ) (Set (Var "X"))) ")" ))); registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#~v9_bcialg_1 "non" ($#v9_bcialg_1 :::"proper"::: ) ) for ($#m1_bcialg_1 :::"SubAlgebra"::: ) "of" "X"; end; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "IT" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); attr "IT" is :::"atom"::: means :: BCIALG_1:def 14 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) "IT") ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X"))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) "IT")); end; :: deftheorem defines :::"atom"::: BCIALG_1:def 14 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_bcialg_1 :::"atom"::: ) ) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "IT")))) ")" ))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); func :::"AtomSet"::: "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BCIALG_1:def 15 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool (Set (Var "x")) "is" ($#v10_bcialg_1 :::"atom"::: ) ) "}" ; end; :: deftheorem defines :::"AtomSet"::: BCIALG_1:def 15 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Var "x")) "is" ($#v10_bcialg_1 :::"atom"::: ) ) "}" )); theorem :: BCIALG_1:23 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))))) ; theorem :: BCIALG_1:24 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" ))) ; theorem :: BCIALG_1:25 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u"))))) ")" ))) ; theorem :: BCIALG_1:26 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" ))) ; theorem :: BCIALG_1:27 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" ))) ; theorem :: BCIALG_1:28 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))))) ")" ))) ; theorem :: BCIALG_1:29 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool (Set (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: BCIALG_1:30 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))))) ")" ))) ; theorem :: BCIALG_1:31 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))))) ")" ))) ; theorem :: BCIALG_1:32 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u"))))) ")" ))) ; theorem :: BCIALG_1:33 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))))))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "a", "b" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Const "X"))); :: original: :::"\"::: redefine func "a" :::"\"::: "b" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) "X"); end; theorem :: BCIALG_1:34 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X")))))) ; theorem :: BCIALG_1:35 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "st" (Bool (Set (Var "a")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); attr "X" is :::"generated_by_atom"::: means :: BCIALG_1:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "ex" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) "X") "st" (Bool (Set (Var "a")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"generated_by_atom"::: BCIALG_1:def 16 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v11_bcialg_1 :::"generated_by_atom"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "st" (Bool (Set (Var "a")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x"))))) ")" )); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Const "X"))); func :::"BranchV"::: "a" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: BCIALG_1:def 17 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X" : (Bool "a" ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x"))) "}" ; end; :: deftheorem defines :::"BranchV"::: BCIALG_1:def 17 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) : (Bool (Set (Var "a")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x"))) "}" ))); theorem :: BCIALG_1:36 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set (Var "X")) "is" ($#v11_bcialg_1 :::"generated_by_atom"::: ) )) ; theorem :: BCIALG_1:37 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "b"))) "holds" (Bool (Set (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_bcialg_1 :::"\"::: ) (Set (Var "b"))))))) ; theorem :: BCIALG_1:38 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: BCIALG_1:39 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "a"))) (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "b"))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set "(" (Set (Var "a")) ($#k6_bcialg_1 :::"\"::: ) (Set (Var "b")) ")" ))))))) ; theorem :: BCIALG_1:40 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "a"))) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))))) ; theorem :: BCIALG_1:41 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "a"))) (Bool "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "b"))) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "not" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))))))) ; theorem :: BCIALG_1:42 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_bcialg_1 :::"AtomSet"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "a")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k7_bcialg_1 :::"BranchV"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); mode :::"Ideal"::: "of" "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" means :: BCIALG_1:def 18 (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r2_hidden :::"in"::: ) it) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"Ideal"::: BCIALG_1:def 18 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "IT" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); attr "IT" is :::"closed"::: means :: BCIALG_1:def 19 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "IT" "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem defines :::"closed"::: BCIALG_1:def 19 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "IT")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v12_bcialg_1 :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))); registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_bcialg_1 :::"closed"::: ) for ($#m2_bcialg_1 :::"Ideal"::: ) "of" "X"; end; theorem :: BCIALG_1:43 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ) "is" ($#v12_bcialg_1 :::"closed"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ; theorem :: BCIALG_1:44 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "is" ($#v12_bcialg_1 :::"closed"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ; theorem :: BCIALG_1:45 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) "is" ($#v12_bcialg_1 :::"closed"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) ; theorem :: BCIALG_1:46 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "IT")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "IT")) "is" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "y")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))))) ; begin definitionlet "IT" be ($#l2_bcialg_1 :::"BCI-algebra":::); attr "IT" is :::"associative"::: means :: BCIALG_1:def 20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )))); attr "IT" is :::"quasi-associative"::: means :: BCIALG_1:def 21 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ))); attr "IT" is :::"positive-implicative"::: means :: BCIALG_1:def 22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ")" )))); attr "IT" is :::"weakly-positive-implicative"::: means :: BCIALG_1:def 23 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )))); attr "IT" is :::"implicative"::: means :: BCIALG_1:def 24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))); attr "IT" is :::"weakly-implicative"::: means :: BCIALG_1:def 25 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))); attr "IT" is :::"p-Semisimple"::: means :: BCIALG_1:def 26 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y")))); attr "IT" is :::"alternative"::: means :: BCIALG_1:def 27 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))) ")" )); end; :: deftheorem defines :::"associative"::: BCIALG_1:def 20 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v13_bcialg_1 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"quasi-associative"::: BCIALG_1:def 21 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v14_bcialg_1 :::"quasi-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ))) ")" )); :: deftheorem defines :::"positive-implicative"::: BCIALG_1:def 22 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v15_bcialg_1 :::"positive-implicative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ")" )))) ")" )); :: deftheorem defines :::"weakly-positive-implicative"::: BCIALG_1:def 23 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )))) ")" )); :: deftheorem defines :::"implicative"::: BCIALG_1:def 24 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v17_bcialg_1 :::"implicative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )); :: deftheorem defines :::"weakly-implicative"::: BCIALG_1:def 25 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v18_bcialg_1 :::"weakly-implicative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); :: deftheorem defines :::"p-Semisimple"::: BCIALG_1:def 26 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); :: deftheorem defines :::"alternative"::: BCIALG_1:def 27 : (Bool "for" (Set (Var "IT")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v20_bcialg_1 :::"alternative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))) ")" )) ")" )); registration cluster (Set ($#k3_bcialg_1 :::"BCI-EXAMPLE"::: ) ) -> ($#v13_bcialg_1 :::"associative"::: ) ($#v15_bcialg_1 :::"positive-implicative"::: ) ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) ($#v17_bcialg_1 :::"implicative"::: ) ($#v18_bcialg_1 :::"weakly-implicative"::: ) ($#v19_bcialg_1 :::"p-Semisimple"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v13_bcialg_1 :::"associative"::: ) ($#v15_bcialg_1 :::"positive-implicative"::: ) ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) ($#v17_bcialg_1 :::"implicative"::: ) ($#v18_bcialg_1 :::"weakly-implicative"::: ) ($#v19_bcialg_1 :::"p-Semisimple"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; theorem :: BCIALG_1:47 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v13_bcialg_1 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )) ; theorem :: BCIALG_1:48 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) ")" ) "iff" (Bool (Set (Var "X")) "is" ($#v13_bcialg_1 :::"associative"::: ) ) ")" )) ; theorem :: BCIALG_1:49 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v13_bcialg_1 :::"associative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )) ; theorem :: BCIALG_1:50 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v13_bcialg_1 :::"associative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )) ; theorem :: BCIALG_1:51 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v13_bcialg_1 :::"associative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )) ; begin theorem :: BCIALG_1:52 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) "is" ($#v10_bcialg_1 :::"atom"::: ) )) ")" )) ; theorem :: BCIALG_1:53 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) )) "holds" (Bool (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: BCIALG_1:54 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )) ; theorem :: BCIALG_1:55 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )) ; theorem :: BCIALG_1:56 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))) ")" )) ; theorem :: BCIALG_1:57 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )) ; theorem :: BCIALG_1:58 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))) ")" )) ; theorem :: BCIALG_1:59 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))))) ")" )) ; theorem :: BCIALG_1:60 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))))) ")" )) ; theorem :: BCIALG_1:61 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "u")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u"))))) ")" )) ; theorem :: BCIALG_1:62 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) ")" )) ; theorem :: BCIALG_1:63 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k2_bcialg_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" )))) ")" )) ; theorem :: BCIALG_1:64 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" )))) ")" )) ; theorem :: BCIALG_1:65 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))))) ")" )) ; theorem :: BCIALG_1:66 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" )))) ")" )) ; theorem :: BCIALG_1:67 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ")" )) ; theorem :: BCIALG_1:68 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ")" )) ; theorem :: BCIALG_1:69 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )) ; theorem :: BCIALG_1:70 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_bcialg_1 :::"being_I"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ")" ) ")" )) ; begin theorem :: BCIALG_1:71 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v14_bcialg_1 :::"quasi-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))) ")" )) ; theorem :: BCIALG_1:72 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v14_bcialg_1 :::"quasi-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ))) ")" )) ; theorem :: BCIALG_1:73 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v14_bcialg_1 :::"quasi-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ))) ")" )) ; theorem :: BCIALG_1:74 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v14_bcialg_1 :::"quasi-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) ")" )) ; theorem :: BCIALG_1:75 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v14_bcialg_1 :::"quasi-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" )))) ")" )) ; begin theorem :: BCIALG_1:76 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: BCIALG_1:77 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) ) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: BCIALG_1:78 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) ) & (Bool (Set (Set (Var "a")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: BCIALG_1:79 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) ) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: BCIALG_1:80 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) ) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "a")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "b")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "a")))) ")" ))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v20_bcialg_1 :::"alternative"::: ) -> ($#v13_bcialg_1 :::"associative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v13_bcialg_1 :::"associative"::: ) -> ($#v20_bcialg_1 :::"alternative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v20_bcialg_1 :::"alternative"::: ) -> ($#v17_bcialg_1 :::"implicative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; theorem :: BCIALG_1:81 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: BCIALG_1:82 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) )) "holds" (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v13_bcialg_1 :::"associative"::: ) -> ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v19_bcialg_1 :::"p-Semisimple"::: ) -> ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; theorem :: BCIALG_1:83 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v17_bcialg_1 :::"implicative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ))) ")" )) ")" )) ; theorem :: BCIALG_1:84 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k2_bcialg_1 :::"`"::: ) ")" )))) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v15_bcialg_1 :::"positive-implicative"::: ) -> ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_bcialg_1 :::"being_B"::: ) ($#v4_bcialg_1 :::"being_C"::: ) ($#v5_bcialg_1 :::"being_I"::: ) ($#v7_bcialg_1 :::"being_BCI-4"::: ) ($#v20_bcialg_1 :::"alternative"::: ) -> ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; theorem :: BCIALG_1:85 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v16_bcialg_1 :::"weakly-positive-implicative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))))) ; theorem :: BCIALG_1:86 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_bcialg_1 :::"BCIStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v15_bcialg_1 :::"positive-implicative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "z")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k2_bcialg_1 :::"`"::: ) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))) ")" )) ")" )) ;