:: BCIALG_2 semantic presentation begin definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "(" "x" "," "y" ")" :::"to_power"::: "n" -> ($#m1_subset_1 :::"Element":::) "of" "X" means :: BCIALG_2:def 1 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) "n")) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "x") & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) "n")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_bcialg_1 :::"\"::: ) "y")) ")" ) ")" )); end; :: deftheorem defines :::"to_power"::: BCIALG_2:def 1 : (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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))) ")" ) ")" )) ")" ))))); theorem :: BCIALG_2:1 (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")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: BCIALG_2:2 (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")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))))) ; theorem :: BCIALG_2:3 (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")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")))))) ; theorem :: BCIALG_2:4 (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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))))) ; theorem :: BCIALG_2:5 (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 "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: BCIALG_2:6 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))))) ; theorem :: BCIALG_2: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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_2: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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_2:9 (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 "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_2: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")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" )))))) ; theorem :: BCIALG_2:11 (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")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) "," (Set (Var "z")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" "(" (Set (Var "x")) "," (Set (Var "z")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m")) ")" ) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_2:12 (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 "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_2:13 (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 "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" )))))) ; theorem :: BCIALG_2:14 (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 "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" )))))) ; theorem :: BCIALG_2:15 (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 "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "m")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )))))) ; theorem :: BCIALG_2:16 (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 "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "holds" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "m")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; theorem :: BCIALG_2:17 (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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: BCIALG_2:18 (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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" )))))) ; theorem :: BCIALG_2:19 (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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "z")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_bcialg_1 :::"<="::: ) (Set "(" (Set (Var "y")) "," (Set (Var "z")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_2:20 (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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set "(" (Set (Var "z")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_bcialg_1 :::"<="::: ) (Set "(" (Set (Var "z")) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_2:21 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "z")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" "(" (Set (Var "y")) "," (Set (Var "z")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))))) ; theorem :: BCIALG_2:22 (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")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set "(" "(" (Set (Var "x")) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))))) ; notationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); synonym :::"minimal"::: "a" for :::"atom"::: ; end; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); attr "a" is :::"positive"::: means :: BCIALG_2:def 2 (Bool (Set ($#k4_struct_0 :::"0."::: ) "X") ($#r1_bcialg_1 :::"<="::: ) "a"); attr "a" is :::"least"::: means :: BCIALG_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool "a" ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))); attr "a" is :::"maximal"::: means :: BCIALG_2:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool "a" ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) "a")); attr "a" is :::"greatest"::: means :: BCIALG_2:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) "a")); end; :: deftheorem defines :::"positive"::: BCIALG_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_bcialg_2 :::"positive"::: ) ) "iff" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a"))) ")" ))); :: deftheorem defines :::"least"::: BCIALG_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v2_bcialg_2 :::"least"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "a")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))) ")" ))); :: deftheorem defines :::"maximal"::: BCIALG_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v3_bcialg_2 :::"maximal"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" ))); :: deftheorem defines :::"greatest"::: BCIALG_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v4_bcialg_2 :::"greatest"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "a")))) ")" ))); registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); cluster ($#v1_bcialg_2 :::"positive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"); end; registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); cluster (Set ($#k4_struct_0 :::"0."::: ) "X") -> ($#v10_bcialg_1 :::"minimal"::: ) ($#v1_bcialg_2 :::"positive"::: ) ; end; theorem :: BCIALG_2:23 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v10_bcialg_1 :::"minimal"::: ) ) "iff" (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"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k2_bcialg_1 :::"`"::: ) ")" )))) ")" ))) ; theorem :: BCIALG_2: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 (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) "is" ($#v10_bcialg_1 :::"minimal"::: ) ) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k2_bcialg_1 :::"`"::: ) ))) ")" ))) ; theorem :: BCIALG_2: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 (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ) "is" ($#v10_bcialg_1 :::"minimal"::: ) ) "iff" (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" )))) ")" ))) ; theorem :: BCIALG_2:26 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))) "is" ($#v3_bcialg_2 :::"maximal"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "a")) "is" ($#v10_bcialg_1 :::"minimal"::: ) ))) ; theorem :: BCIALG_2:27 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) "is" ($#v4_bcialg_2 :::"greatest"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "a")) "is" ($#v1_bcialg_2 :::"positive"::: ) ))) ; theorem :: BCIALG_2: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 (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ")" )) "is" ($#v1_bcialg_2 :::"positive"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))))) ; theorem :: BCIALG_2:29 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v10_bcialg_1 :::"minimal"::: ) ) "iff" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ($#k2_bcialg_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: BCIALG_2:30 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v10_bcialg_1 :::"minimal"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ))) ")" ))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); attr "x" is :::"nilpotent"::: means :: BCIALG_2:def 6 (Bool "ex" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) "X" ")" ) "," "x" ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X"))); end; :: deftheorem defines :::"nilpotent"::: BCIALG_2:def 6 : (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")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) ) "iff" (Bool "ex" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) ")" ))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); attr "X" is :::"nilpotent"::: means :: BCIALG_2:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set (Var "x")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) )); end; :: deftheorem defines :::"nilpotent"::: BCIALG_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_bcialg_2 :::"nilpotent"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) )) ")" )); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); assume (Bool (Set (Const "x")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) ) ; func :::"ord"::: "x" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: BCIALG_2:def 8 (Bool "(" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) "X" ")" ) "," "x" ")" ($#k1_bcialg_2 :::"to_power"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) "X" ")" ) "," "x" ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "X")) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" ) ")" ); end; :: deftheorem defines :::"ord"::: BCIALG_2:def 8 : (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")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_bcialg_2 :::"ord"::: ) (Set (Var "x")))) "iff" (Bool "(" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" ) ")" ) ")" )))); registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); cluster (Set ($#k4_struct_0 :::"0."::: ) "X") -> ($#v5_bcialg_2 :::"nilpotent"::: ) ; end; theorem :: BCIALG_2: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")) "is" ($#v1_bcialg_2 :::"positive"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) ) & (Bool (Set ($#k2_bcialg_2 :::"ord"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ))) ; theorem :: BCIALG_2:32 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::)) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k2_bcialg_2 :::"ord"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) ) ")" )) ")" )) ; theorem :: BCIALG_2:33 (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 "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) "is" ($#v10_bcialg_1 :::"minimal"::: ) )))) ; theorem :: BCIALG_2: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")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_bcialg_2 :::"nilpotent"::: ) )) "holds" (Bool (Set ($#k2_bcialg_2 :::"ord"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_bcialg_2 :::"ord"::: ) (Set "(" (Set (Var "x")) ($#k2_bcialg_1 :::"`"::: ) ")" ))))) ; begin definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); mode :::"Congruence"::: "of" "X" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" means :: BCIALG_2:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "v")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it)); end; :: deftheorem defines :::"Congruence"::: BCIALG_2:def 9 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "v")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) ")" ))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); mode :::"L-congruence"::: "of" "X" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" means :: BCIALG_2:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "u")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "u")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it))); end; :: deftheorem defines :::"L-congruence"::: BCIALG_2:def 10 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_bcialg_2 :::"L-congruence"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "u")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "u")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))))) ")" ))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); mode :::"R-congruence"::: "of" "X" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "X" means :: BCIALG_2:def 11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it))); end; :: deftheorem defines :::"R-congruence"::: BCIALG_2:def 11 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_bcialg_2 :::"R-congruence"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "u")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))))) ")" ))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "A" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); mode :::"I-congruence"::: "of" "X" "," "A" -> ($#m1_subset_1 :::"Relation":::) "of" "X" means :: BCIALG_2:def 12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) "A") ")" ) ")" )); end; :: deftheorem defines :::"I-congruence"::: BCIALG_2:def 12 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "A")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "A"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" )) ")" )))); registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "A" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); cluster -> ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m4_bcialg_2 :::"I-congruence"::: ) "of" "X" "," "A"; end; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); func :::"IConSet"::: "X" -> ($#m1_hidden :::"set"::: ) means :: BCIALG_2:def 13 (Bool "for" (Set (Var "A1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A1")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" "X" "st" (Bool (Set (Var "A1")) "is" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" "X" "," (Set (Var "I")))) ")" )); end; :: deftheorem defines :::"IConSet"::: BCIALG_2:def 13 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_bcialg_2 :::"IConSet"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "A1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A1")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "A1")) "is" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")))) ")" )) ")" ))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); func :::"ConSet"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: BCIALG_2:def 14 "{" (Set (Var "R")) where R "is" ($#m1_bcialg_2 :::"Congruence"::: ) "of" "X" : (Bool verum) "}" ; func :::"LConSet"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: BCIALG_2:def 15 "{" (Set (Var "R")) where R "is" ($#m2_bcialg_2 :::"L-congruence"::: ) "of" "X" : (Bool verum) "}" ; func :::"RConSet"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: BCIALG_2:def 16 "{" (Set (Var "R")) where R "is" ($#m3_bcialg_2 :::"R-congruence"::: ) "of" "X" : (Bool verum) "}" ; end; :: deftheorem defines :::"ConSet"::: BCIALG_2:def 14 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_bcialg_2 :::"ConSet"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "R")) where R "is" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) : (Bool verum) "}" )); :: deftheorem defines :::"LConSet"::: BCIALG_2:def 15 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k5_bcialg_2 :::"LConSet"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "R")) where R "is" ($#m2_bcialg_2 :::"L-congruence"::: ) "of" (Set (Var "X")) : (Bool verum) "}" )); :: deftheorem defines :::"RConSet"::: BCIALG_2:def 16 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k6_bcialg_2 :::"RConSet"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "R")) where R "is" ($#m3_bcialg_2 :::"R-congruence"::: ) "of" (Set (Var "X")) : (Bool verum) "}" )); theorem :: BCIALG_2:35 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ) "is" ($#v12_bcialg_1 :::"closed"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))))) ; theorem :: BCIALG_2:36 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#m3_bcialg_2 :::"R-congruence"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "R")) "is" ($#m2_bcialg_2 :::"L-congruence"::: ) "of" (Set (Var "X"))) ")" ) ")" ))) ; theorem :: BCIALG_2:37 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "RI")) "being" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) "holds" (Bool (Set (Var "RI")) "is" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")))))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "I" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); :: original: :::"I-congruence"::: redefine mode :::"I-congruence"::: "of" "X" "," "I" -> ($#m1_bcialg_2 :::"Congruence"::: ) "of" "X"; end; theorem :: BCIALG_2:38 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "RI")) "being" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "RI")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "I")))))) ; theorem :: BCIALG_2:39 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "RI")) "being" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v12_bcialg_1 :::"closed"::: ) ) "iff" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "RI")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" )) ")" )))) ; theorem :: BCIALG_2:40 (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")) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" )) & (Bool (Set (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" )) ")" )))) ; theorem :: BCIALG_2:41 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "A")) "," (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "IA")) "being" ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) (Bool "for" (Set (Var "II")) "being" ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) "st" (Bool (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "IA")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "II")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ))) "holds" (Bool (Set (Var "IA")) ($#r1_hidden :::"="::: ) (Set (Var "II"))))))) ; theorem :: BCIALG_2:42 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" "(" (Set (Var "y")) "," (Set (Var "u")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "k")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E"))))))) ; theorem :: BCIALG_2:43 (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")) (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set "(" (Set "(" "(" (Set (Var "x")) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" "(" (Set (Var "y")) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m")) ")" ) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")))))) ")" )) "holds" (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ))) "holds" (Bool (Set (Var "E")) "is" ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")))))) ; theorem :: BCIALG_2:44 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k3_bcialg_2 :::"IConSet"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_bcialg_2 :::"ConSet"::: ) (Set (Var "X"))))) ; theorem :: BCIALG_2:45 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_bcialg_2 :::"ConSet"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_bcialg_2 :::"LConSet"::: ) (Set (Var "X"))))) ; theorem :: BCIALG_2:46 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_bcialg_2 :::"ConSet"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_bcialg_2 :::"RConSet"::: ) (Set (Var "X"))))) ; theorem :: BCIALG_2:47 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool (Set ($#k4_bcialg_2 :::"ConSet"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_bcialg_2 :::"LConSet"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k6_bcialg_2 :::"RConSet"::: ) (Set (Var "X")) ")" )))) ; theorem :: BCIALG_2:48 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "RI")) "being" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "LC")) "being" ($#m2_bcialg_2 :::"L-congruence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "LC")) "is" ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I"))) ")" )) "holds" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set (Var "RI"))))))) ; theorem :: BCIALG_2:49 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "RI")) "being" ($#m4_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "RC")) "being" ($#m3_bcialg_2 :::"R-congruence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "RC")) "is" ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I"))) ")" )) "holds" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set (Var "RI"))))))) ; theorem :: BCIALG_2:50 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "LC")) "being" ($#m2_bcialg_2 :::"L-congruence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "LC")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" ) "is" ($#v12_bcialg_1 :::"closed"::: ) ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X"))))) ; registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "E" be ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Const "X")); cluster (Set ($#k7_eqrel_1 :::"Class"::: ) "E") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "E" be ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Const "X")); func :::"EqClaOp"::: "E" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) means :: BCIALG_2:def 17 (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "E") (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "E" "," (Set (Var "x")) ")" )) & (Bool (Set (Var "W2")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "E" "," (Set (Var "y")) ")" ))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "E" "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" )))); end; :: deftheorem defines :::"EqClaOp"::: BCIALG_2:def 17 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_bcialg_2 :::"EqClaOp"::: ) (Set (Var "E")))) "iff" (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E"))) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set (Var "x")) ")" )) & (Bool (Set (Var "W2")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set (Var "y")) ")" ))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" )))) ")" )))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "E" be ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Const "X")); func :::"zeroEqC"::: "E" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "E") equals :: BCIALG_2:def 18 (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "E" "," (Set "(" ($#k4_struct_0 :::"0."::: ) "X" ")" ) ")" ); end; :: deftheorem defines :::"zeroEqC"::: BCIALG_2:def 18 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k8_bcialg_2 :::"zeroEqC"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "E")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ")" )))); definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "E" be ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Const "X")); func "X" :::"./."::: "E" -> ($#l2_bcialg_1 :::"BCIStr_0"::: ) equals :: BCIALG_2:def 19 (Set ($#g2_bcialg_1 :::"BCIStr_0"::: ) "(#" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) "," (Set "(" ($#k7_bcialg_2 :::"EqClaOp"::: ) "E" ")" ) "," (Set "(" ($#k8_bcialg_2 :::"zeroEqC"::: ) "E" ")" ) "#)" ); end; :: deftheorem defines :::"./."::: BCIALG_2:def 19 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "X")) ($#k9_bcialg_2 :::"./."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set ($#g2_bcialg_1 :::"BCIStr_0"::: ) "(#" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E")) ")" ) "," (Set "(" ($#k7_bcialg_2 :::"EqClaOp"::: ) (Set (Var "E")) ")" ) "," (Set "(" ($#k8_bcialg_2 :::"zeroEqC"::: ) (Set (Var "E")) ")" ) "#)" )))); registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "E" be ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Const "X")); cluster (Set "X" ($#k9_bcialg_2 :::"./."::: ) "E") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "E" be ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Const "X")); let "W1", "W2" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Const "E"))); func "W1" :::"\"::: "W2" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "E") equals :: BCIALG_2:def 20 (Set (Set "(" ($#k7_bcialg_2 :::"EqClaOp"::: ) "E" ")" ) ($#k5_binop_1 :::"."::: ) "(" "W1" "," "W2" ")" ); end; :: deftheorem defines :::"\"::: BCIALG_2:def 20 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "E")) "being" ($#m1_bcialg_2 :::"Congruence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E"))) "holds" (Bool (Set (Set (Var "W1")) ($#k10_bcialg_2 :::"\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_bcialg_2 :::"EqClaOp"::: ) (Set (Var "E")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ))))); theorem :: BCIALG_2:51 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "RI")) "being" ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k9_bcialg_2 :::"./."::: ) (Set (Var "RI"))) "is" ($#l2_bcialg_1 :::"BCI-algebra":::))))) ; registrationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "I" be ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Const "X")); let "RI" be ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Const "X")) "," (Set (Const "I")); cluster (Set "X" ($#k9_bcialg_2 :::"./."::: ) "RI") -> ($#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"::: ) ; end; theorem :: BCIALG_2:52 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "I")) "being" ($#m2_bcialg_1 :::"Ideal"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "RI")) "being" ($#m5_bcialg_2 :::"I-congruence"::: ) "of" (Set (Var "X")) "," (Set (Var "I")) "holds" (Bool (Set (Set (Var "X")) ($#k9_bcialg_2 :::"./."::: ) (Set (Var "RI"))) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))))) ;