:: BCIALG_5 semantic presentation begin definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); let "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Polynom"::: "(" "m" "," "n" "," "x" "," "y" ")" -> ($#m1_subset_1 :::"Element":::) "of" "X" equals :: BCIALG_5:def 1 (Set "(" (Set "(" "(" "x" "," (Set "(" "x" ($#k1_bcialg_1 :::"\"::: ) "y" ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" "m" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "y" ($#k1_bcialg_1 :::"\"::: ) "x" ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) "n"); end; :: deftheorem defines :::"Polynom"::: BCIALG_5: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 "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" "(" (Set (Var "x")) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))); theorem :: BCIALG_5:1 (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"))) & (Bool (Set (Var "y")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "z")))) "holds" (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "z"))))) ; theorem :: BCIALG_5: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")) "st" (Bool (Bool (Set (Var "x")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: BCIALG_5:3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))) ($#r1_bcialg_1 :::"<="::: ) (Set (Var "x"))) & (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_bcialg_1 :::"<="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n")))) ")" )))) ; theorem :: BCIALG_5:4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set (Var "x")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; theorem :: BCIALG_5:5 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m"))) ($#r1_bcialg_1 :::"<="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_5:6 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCK-algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) & (Bool (Set "(" (Set (Var "x")) "," (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 "m"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool (Set "(" (Set (Var "x")) "," (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 "k")))))))) ; theorem :: BCIALG_5:7 (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 ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ))))) ; theorem :: BCIALG_5: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 "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" "(" (Set "(" ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "m")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" ) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BCIALG_5: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")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" )))))) ; theorem :: BCIALG_5: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 "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set "(" (Set (Var "y")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "x")) ")" )))))) ; theorem :: BCIALG_5:11 (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")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "y")) "," (Set (Var "x")) ")" ) ($#r1_bcialg_1 :::"<="::: ) (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "n")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ))))) ; theorem :: BCIALG_5:12 (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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "n")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_bcialg_1 :::"<="::: ) (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "n")) "," (Set (Var "n")) "," (Set (Var "y")) "," (Set (Var "x")) ")" ))))) ; definitionlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); attr "X" is :::"quasi-commutative"::: means :: BCIALG_5:def 2 (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "y")) "," (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"quasi-commutative"::: BCIALG_5:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_bcialg_5 :::"quasi-commutative"::: ) ) "iff" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "y")) "," (Set (Var "x")) ")" )))) ")" )); registration cluster (Set ($#k3_bcialg_1 :::"BCI-EXAMPLE"::: ) ) -> ($#v1_bcialg_5 :::"quasi-commutative"::: ) ; 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"::: ) ($#v1_bcialg_5 :::"quasi-commutative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; definitionlet "i", "j", "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"BCI-algebra"::: "of" "i" "," "j" "," "m" "," "n" -> ($#l2_bcialg_1 :::"BCI-algebra":::) means :: BCIALG_5:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" it "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" "i" "," "j" "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" "m" "," "n" "," (Set (Var "y")) "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"BCI-algebra"::: BCIALG_5:def 3 : (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n"))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b5")) "holds" (Bool (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_bcialg_5 :::"Polynom"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "y")) "," (Set (Var "x")) ")" ))) ")" ))); theorem :: BCIALG_5:13 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n"))) "iff" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j"))) ")" ))) ; theorem :: BCIALG_5:14 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))))))) ; theorem :: BCIALG_5:15 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "i")) "," (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) "," (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) "," (Set (Var "n")))))) ; 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"::: ) ($#v8_bcialg_1 :::"being_BCK-5"::: ) ($#v1_bcialg_5 :::"quasi-commutative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; registrationlet "i", "j", "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); 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"::: ) ($#v8_bcialg_1 :::"being_BCK-5"::: ) for ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" "i" "," "j" "," "m" "," "n"; end; definitionlet "i", "j", "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode BCK-algebra of "i" "," "j" "," "m" "," "n" is ($#v8_bcialg_1 :::"being_BCK-5"::: ) ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" "i" "," "j" "," "m" "," "n"; end; theorem :: BCIALG_5:16 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n"))) "iff" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j"))) ")" ))) ; theorem :: BCIALG_5:17 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))))))) ; theorem :: BCIALG_5:18 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) "," (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) "," (Set (Var "n")))))) ; theorem :: BCIALG_5:19 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) (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 "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: BCIALG_5:20 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) (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 "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: BCIALG_5:21 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "j")) "," (Set (Var "n"))))) ; theorem :: BCIALG_5:22 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "n")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n"))))) ; definitionlet "i", "j", "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"min"::: "(" "i" "," "j" "," "m" "," "n" ")" -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) equals :: BCIALG_5:def 4 (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k6_nat_1 :::"min"::: ) "(" "i" "," "j" ")" ")" ) "," (Set "(" ($#k6_nat_1 :::"min"::: ) "(" "m" "," "n" ")" ")" ) ")" ); func :::"max"::: "(" "i" "," "j" "," "m" "," "n" ")" -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) equals :: BCIALG_5:def 5 (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" ($#k7_nat_1 :::"max"::: ) "(" "i" "," "j" ")" ")" ) "," (Set "(" ($#k7_nat_1 :::"max"::: ) "(" "m" "," "n" ")" ")" ) ")" ); end; :: deftheorem defines :::"min"::: BCIALG_5:def 4 : (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k6_nat_1 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set "(" ($#k6_nat_1 :::"min"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ")" ))); :: deftheorem defines :::"max"::: BCIALG_5:def 5 : (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" ($#k7_nat_1 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) "," (Set "(" ($#k7_nat_1 :::"max"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ")" ))); theorem :: BCIALG_5:23 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "i"))) "or" (Bool (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "j"))) "or" (Bool (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))) "or" (Bool (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) ; theorem :: BCIALG_5:24 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "i"))) "or" (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "j"))) "or" (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))) "or" (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) ; theorem :: BCIALG_5:25 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) ; theorem :: BCIALG_5:26 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "i"))) & (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "j"))) & (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "m"))) & (Bool (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n"))) ")" )) ; theorem :: BCIALG_5:27 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "i")) "," (Set (Var "i")) "," (Set (Var "i"))))) ; theorem :: BCIALG_5:28 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "i")) "," (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: BCIALG_5:29 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k2_bcialg_5 :::"min"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "i")) "," (Set (Var "i")) "," (Set (Var "i"))))) ; theorem :: BCIALG_5:30 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "m")) "," (Set (Var "i"))))) ; theorem :: BCIALG_5:31 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "j")) "," (Set (Var "i"))))) ; theorem :: BCIALG_5:32 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "l")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "l")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "j"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "l")) "," (Set (Var "k"))))) ; theorem :: BCIALG_5:33 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_bcialg_5 :::"max"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "k")) "," (Set (Var "k")) "," (Set (Var "k")) "," (Set (Var "k"))))) ; theorem :: BCIALG_5:34 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "i")) "," (Set (Var "j"))))) ; theorem :: BCIALG_5:35 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "i")) "," (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: BCIALG_5:36 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))) "," (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))))) "holds" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::)))) ; theorem :: BCIALG_5:37 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: BCIALG_5:38 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_bcialg_3 :::"commutative"::: ) ($#l2_bcialg_1 :::"BCK-algebra":::)) "iff" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; notationlet "X" be ($#l2_bcialg_1 :::"BCI-algebra":::); synonym :::"p-Semisimple-part"::: "X" for :::"AtomSet"::: "X"; end; theorem :: BCIALG_5:39 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "B")) "," (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X")))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k5_bcialg_1 :::"p-Semisimple-part"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: BCIALG_5:40 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k5_bcialg_1 :::"p-Semisimple-part"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#l2_bcialg_1 :::"BCK-algebra":::)) "iff" (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" )))) ; theorem :: BCIALG_5:41 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k4_bcialg_1 :::"BCK-part"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)) "iff" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" )))) ; theorem :: BCIALG_5:42 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: BCIALG_5:43 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "n")) "," (Set (Var "j")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v19_bcialg_1 :::"p-Semisimple"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j"))) "," (Set (Var "n")) "," (Set (Var "m")) "," (Set (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: BCIALG_5:44 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v13_bcialg_1 :::"associative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: BCIALG_5:45 (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 (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) "," (Num 1))) ; theorem :: BCIALG_5:46 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v15_bcialg_1 :::"positive-implicative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 1) "," (Num 1))) ; theorem :: BCIALG_5:47 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v17_bcialg_1 :::"implicative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: BCIALG_5:48 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v20_bcialg_1 :::"alternative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: BCIALG_5:49 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v10_bcialg_3 :::"BCK-positive-implicative"::: ) ($#l2_bcialg_1 :::"BCK-algebra":::)) "iff" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1)) ")" )) ; theorem :: BCIALG_5:50 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v11_bcialg_3 :::"BCK-implicative"::: ) ($#l2_bcialg_1 :::"BCK-algebra":::)) "iff" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; 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"::: ) ($#v8_bcialg_1 :::"being_BCK-5"::: ) ($#v11_bcialg_3 :::"BCK-implicative"::: ) -> ($#v1_bcialg_3 :::"commutative"::: ) 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"::: ) ($#v8_bcialg_1 :::"being_BCK-5"::: ) ($#v11_bcialg_3 :::"BCK-implicative"::: ) -> ($#v10_bcialg_3 :::"BCK-positive-implicative"::: ) for ($#l2_bcialg_1 :::"BCIStr_0"::: ) ; end; theorem :: BCIALG_5:51 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1)) ")" ) ")" )) ; theorem :: BCIALG_5:52 (Bool "for" (Set (Var "X")) "being" ($#v1_bcialg_5 :::"quasi-commutative"::: ) ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1)) "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 (Var "x")) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y")) ")" ) ($#k1_bcialg_1 :::"\"::: ) (Set (Var "y"))))) ")" )) ; theorem :: BCIALG_5:53 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#v1_bcialg_5 :::"quasi-commutative"::: ) ($#l2_bcialg_1 :::"BCK-algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "n")) "," (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Var "n")) "," (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) "iff" (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k1_bcialg_2 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )))) ")" ))) ; theorem :: BCIALG_5:54 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#v4_bcialg_3 :::"BCI-commutative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::))) ; theorem :: BCIALG_5:55 (Bool "for" (Set (Var "X")) "being" ($#l2_bcialg_1 :::"BCI-algebra":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCI-algebra"::: ) "of" (Set (Var "n")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "m")) "," (Set (Var "m")))) "holds" (Bool (Set (Var "X")) "is" ($#v4_bcialg_3 :::"BCI-commutative"::: ) ($#l2_bcialg_1 :::"BCI-algebra":::)))) ; theorem :: BCIALG_5:56 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BCIALG_5:57 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1)))) ; theorem :: BCIALG_5:58 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: BCIALG_5:59 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "m")) "," (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#m1_bcialg_5 :::"BCK-algebra":::) "of" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1)))) ;