:: FUZZY_4 semantic presentation begin registrationlet "C1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C1")); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: FUZZY_4:1 (Bool "for" (Set (Var "C1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C1")) "holds" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) ")" ) ")" ))) ; theorem :: FUZZY_4:2 (Bool "for" (Set (Var "C1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C1")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C1")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "G")) ")" ))))) ; theorem :: FUZZY_4:3 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" )))) ; definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "C1")) "," (Set (Const "C2")); let "x", "y" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "f" :::"."::: "(" "x" "," "y" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: FUZZY_4:4 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Set (Var "f")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" )))) ; begin notationlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "h" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "C2")) "," (Set (Const "C1")); synonym :::"converse"::: "h" for :::"~"::: "C1"; end; definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "h" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "C2")) "," (Set (Const "C1")); :: original: :::"converse"::: redefine func :::"converse"::: "h" -> ($#m1_subset_1 :::"RMembership_Func":::) "of" "C1" "," "C2" means :: FUZZY_4:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C2" ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set it ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "h" ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"converse"::: FUZZY_4:def 1 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C1")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "h")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))) ")" )))); theorem :: FUZZY_4:5 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))))) ; theorem :: FUZZY_4:6 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "f")) ")" ))))) ; theorem :: FUZZY_4:7 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "g")) ")" ) ")" )))) ; theorem :: FUZZY_4:8 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "g")) ")" ) ")" )))) ; theorem :: FUZZY_4:9 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "C2"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool (Set (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "g")) ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: FUZZY_4:10 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "g"))) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_4:11 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" ) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "g")) ")" ))))) ; theorem :: FUZZY_4:12 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" (Set (Var "f")) ($#k6_fuzzy_1 :::"\+\"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" ) ($#k6_fuzzy_1 :::"\+\"::: ) (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "g")) ")" ))))) ; begin definitionlet "C1", "C2", "C3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "h" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "C1")) "," (Set (Const "C2")); let "g" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "C2")) "," (Set (Const "C3")); let "x", "z" be ($#m1_hidden :::"set"::: ) ; assume that (Bool (Set (Const "x")) ($#r2_hidden :::"in"::: ) (Set (Const "C1"))) and (Bool (Set (Const "z")) ($#r2_hidden :::"in"::: ) (Set (Const "C3"))) ; func :::"min"::: "(" "h" "," "g" "," "x" "," "z" ")" -> ($#m1_subset_1 :::"Membership_Func":::) "of" "C2" means :: FUZZY_4:def 2 (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C2" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set "(" "h" ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) "x" "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ")" ) "," (Set "(" "g" ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," "z" ($#k4_tarski :::"]"::: ) ) ")" ) ")" ))); end; :: deftheorem defines :::"min"::: FUZZY_4:def 2 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "C3")))) "holds" (Bool "for" (Set (Var "b8")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set ($#k3_fuzzy_4 :::"min"::: ) "(" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "x")) "," (Set (Var "z")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C2")) "holds" (Bool (Set (Set (Var "b8")) ($#k1_seq_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ")" ) ")" ))) ")" )))))); definitionlet "C1", "C2", "C3" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "h" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "C1")) "," (Set (Const "C2")); let "g" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "C2")) "," (Set (Const "C3")); func "h" :::"(#)"::: "g" -> ($#m1_subset_1 :::"RMembership_Func":::) "of" "C1" "," "C3" means :: FUZZY_4:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C3" ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set it ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k3_fuzzy_4 :::"min"::: ) "(" "h" "," "g" "," (Set (Var "x")) "," (Set (Var "z")) ")" ")" ) ")" )))); end; :: deftheorem defines :::"(#)"::: FUZZY_4:def 3 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C3")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C3")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k3_fuzzy_4 :::"min"::: ) "(" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "x")) "," (Set (Var "z")) ")" ")" ) ")" )))) ")" ))))); theorem :: FUZZY_4:13 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) "holds" (Bool (Set (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: FUZZY_4:14 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) "holds" (Bool (Set (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h"))) ($#r2_relset_1 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: FUZZY_4:15 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) "holds" (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h")) ")" ) ")" ) ($#r1_fuzzy_1 :::"c="::: ) )))) ; theorem :: FUZZY_4:16 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) "holds" (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h")) ")" ) ")" ) ($#r1_fuzzy_1 :::"c="::: ) )))) ; theorem :: FUZZY_4:17 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "g")) ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" )))))) ; theorem :: FUZZY_4:18 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "h")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C1"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "C3"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "C2")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "g")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "k")) ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))))))) ; theorem :: FUZZY_4:19 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "h")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) "st" (Bool (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Var "k")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "k"))) ($#r1_fuzzy_1 :::"c="::: ) )))) ; begin definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Imf"::: "(" "C1" "," "C2" ")" -> ($#m1_subset_1 :::"RMembership_Func":::) "of" "C1" "," "C2" means :: FUZZY_4:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C2" ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "implies" (Bool (Set it ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "implies" (Bool (Set it ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )); end; :: deftheorem defines :::"Imf"::: FUZZY_4:def 4 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_fuzzy_4 :::"Imf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )) ")" ))); theorem :: FUZZY_4:20 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))) ; theorem :: FUZZY_4:21 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))) ; theorem :: FUZZY_4:22 (Bool "for" (Set (Var "C2")) "," (Set (Var "C3")) "," (Set (Var "C1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C2")) "," (Set (Var "C3")) "holds" (Bool (Set (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C3")) ")" )))) ; theorem :: FUZZY_4:23 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool (Set (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C2")) "," (Set (Var "C3")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C3")) ")" )))) ; theorem :: FUZZY_4:24 (Bool "for" (Set (Var "C1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C1")) "holds" (Bool (Set (Set (Var "f")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C1")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C1")) ")" ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "f")))))) ; begin theorem :: FUZZY_4:25 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "implies" (Bool (Set (Set "(" ($#k5_fuzzy_4 :::"Imf"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "implies" (Bool (Set (Set "(" ($#k5_fuzzy_4 :::"Imf"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))) ; theorem :: FUZZY_4:26 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "f")) ")" ) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_fuzzy_4 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))))) ;