:: FUZZY_2 semantic presentation begin theorem :: FUZZY_2:1 (Bool "for" (Set (Var "C")) "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 "C")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" )))) ; theorem :: FUZZY_2:2 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "h")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" )))) ; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func "f" :::"\"::: "g" -> ($#m1_subset_1 :::"Membership_Func":::) "of" "C" equals :: FUZZY_2:def 1 (Set ($#k1_fuzzy_1 :::"min"::: ) "(" "f" "," (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) "g" ")" ) ")" ); end; :: deftheorem defines :::"\"::: FUZZY_2:def 1 : (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "g")) ")" ) ")" )))); theorem :: FUZZY_2:3 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "f")) ")" ) "," (Set (Var "g")) ")" )))) ; theorem :: FUZZY_2:4 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "h"))) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:5 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "f"))) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:6 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "h1")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Var "h1")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "h"))) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:7 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k4_fuzzy_1 :::"EMF"::: ) (Set (Var "C")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: FUZZY_2:8 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:9 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Var "f")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:10 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:11 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" (Set (Var "g")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "h")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g")) ")" ) "," (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ")" )))) ; theorem :: FUZZY_2:12 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g")) ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:13 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g"))) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:14 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: FUZZY_2:15 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: FUZZY_2:16 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g")) ")" ) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "h"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ))))) ; theorem :: FUZZY_2:17 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:18 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "h")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Var "h")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Var "h")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:19 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:20 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:21 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" (Set (Var "f")) ($#k6_fuzzy_1 :::"\+\"::: ) (Set (Var "g")) ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:22 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k6_fuzzy_1 :::"\+\"::: ) (Set (Var "g")) ")" ) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "h"))) ($#r2_funct_2 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ")" ) ")" )))) ; theorem :: FUZZY_2:23 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set "(" (Set (Var "g")) ($#k6_fuzzy_1 :::"\+\"::: ) (Set (Var "h")) ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:24 (Bool "for" (Set (Var "C")) "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 "C")) "st" (Bool (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:25 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:26 (Bool "for" (Set (Var "C")) "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 "C")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set ($#k4_fuzzy_1 :::"EMF"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:27 (Bool "for" (Set (Var "C")) "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 "C")) "st" (Bool (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_fuzzy_1 :::"EMF"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; begin definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "h", "g" be ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func "h" :::"*"::: "g" -> ($#m1_subset_1 :::"Membership_Func":::) "of" "C" means :: FUZZY_2:def 2 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "h" ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "g" ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ))))) ; end; :: deftheorem defines :::"*"::: FUZZY_2:def 2 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" )))) ")" ))); definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "h", "g" be ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func "h" :::"++"::: "g" -> ($#m1_subset_1 :::"Membership_Func":::) "of" "C" means :: FUZZY_2:def 3 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "h" ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "g" ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" "h" ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "g" ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ))))) ; end; :: deftheorem defines :::"++"::: FUZZY_2:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" )))) ")" ))); theorem :: FUZZY_2:28 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "f"))) ($#r1_fuzzy_1 :::"c="::: ) ) ")" ))) ; theorem :: FUZZY_2:29 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h")) ")" ))))) ; theorem :: FUZZY_2:30 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g")) ")" ) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "h"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" (Set (Var "g")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "h")) ")" ))))) ; theorem :: FUZZY_2:31 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "g")) ")" )) ($#r1_fuzzy_1 :::"c="::: ) ) ")" ))) ; theorem :: FUZZY_2:32 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h")) ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:33 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" (Set (Var "g")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h")) ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:34 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "g")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "f")) ")" ) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "g")) ")" ))))) ; theorem :: FUZZY_2:35 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "f")) ")" ) ($#k2_fuzzy_2 :::"*"::: ) (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "g")) ")" ))))) ; theorem :: FUZZY_2:36 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "f")) ")" ) ($#k2_fuzzy_2 :::"*"::: ) (Set "(" ($#k3_fuzzy_1 :::"1_minus"::: ) (Set (Var "g")) ")" ) ")" ))))) ; theorem :: FUZZY_2:37 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set "(" ($#k4_fuzzy_1 :::"EMF"::: ) (Set (Var "C")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k4_fuzzy_1 :::"EMF"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set "(" ($#k5_fuzzy_1 :::"UMF"::: ) (Set (Var "C")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: FUZZY_2:38 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" ($#k4_fuzzy_1 :::"EMF"::: ) (Set (Var "C")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" ($#k5_fuzzy_1 :::"UMF"::: ) (Set (Var "C")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k5_fuzzy_1 :::"UMF"::: ) (Set (Var "C")))) ")" ))) ; theorem :: FUZZY_2:39 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:40 (Bool "for" (Set (Var "C")) "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 "C")) "holds" (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g"))) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:41 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c")))) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_square_1 :::"max"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" (Set (Var "c")) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "c")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ")" )) & (Bool (Set (Set (Var "c")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_square_1 :::"min"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set "(" (Set (Var "c")) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "c")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ")" )) ")" )) ; theorem :: FUZZY_2:42 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_square_1 :::"max"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_square_1 :::"max"::: ) "(" (Set "(" (Set (Var "c")) ($#k7_real_1 :::"+"::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "c")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" )) & (Bool (Set (Set (Var "c")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_square_1 :::"min"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_square_1 :::"min"::: ) "(" (Set "(" (Set (Var "c")) ($#k7_real_1 :::"+"::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "c")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" )) ")" )) ; theorem :: FUZZY_2:43 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: FUZZY_2:44 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: FUZZY_2:45 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: FUZZY_2:46 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: FUZZY_2:47 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "g")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:48 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "g")) ($#k2_fuzzy_2 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:49 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_fuzzy_2 :::"++"::: ) (Set (Var "g")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ) ")" )))))) ; theorem :: FUZZY_2:50 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:51 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k3_fuzzy_2 :::"++"::: ) (Set "(" ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" )) ($#r1_fuzzy_1 :::"c="::: ) ))) ; begin registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster bbbadV5_RELAT_1((Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) bbbadV1_FUNCT_1() ($#v1_funct_2 :::"quasi_total"::: ) -> for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "C" "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode RMembership_Func of "C1" "," "C2" is ($#m1_subset_1 :::"Membership_Func":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C2" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "C1", "C2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Zmf"::: "(" "C1" "," "C2" ")" -> ($#m1_subset_1 :::"RMembership_Func":::) "of" "C1" "," "C2" equals :: FUZZY_2:def 4 (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C2" ($#k2_zfmisc_1 :::":]"::: ) ) ")" ); func :::"Umf"::: "(" "C1" "," "C2" ")" -> ($#m1_subset_1 :::"RMembership_Func":::) "of" "C1" "," "C2" equals :: FUZZY_2:def 5 (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C2" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "C1" "," "C2" ($#k2_zfmisc_1 :::":]"::: ) ) ")" ); end; :: deftheorem defines :::"Zmf"::: FUZZY_2:def 4 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))); :: deftheorem defines :::"Umf"::: FUZZY_2:def 5 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))); theorem :: FUZZY_2:52 (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")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )))) ; theorem :: FUZZY_2:53 (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 "(" (Bool (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" )) & (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" )) ")" ))) ; theorem :: FUZZY_2:54 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" )) & (Bool (Set ($#k3_fuzzy_1 :::"1_minus"::: ) (Set "(" ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" )) ")" )) ; theorem :: FUZZY_2:55 (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 (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ))) "holds" (Bool (Set (Var "g")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: FUZZY_2:56 (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 ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "C1")) "," (Set (Var "C2")) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_fuzzy_2 :::"\"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ;