:: LFUZZY_1 semantic presentation begin registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"is_less_than"::: redefine pred "f" :::"is_less_than"::: "g" means :: LFUZZY_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool (Set "f" ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set "g" ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"is_less_than"::: LFUZZY_1:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "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 "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_lfuzzy_1 :::"is_less_than"::: ) (Set (Var "g"))) "iff" (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 (Set (Set (Var "f")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ")" ))); theorem :: LFUZZY_1:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "R")) ($#k7_lfuzzy_0 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k7_lfuzzy_0 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Var "S"))))) ; theorem :: LFUZZY_1:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (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 (Set (Set (Var "R")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" )) "holds" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Var "S"))))) ; theorem :: LFUZZY_1:3 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set (Var "S"))) "iff" (Bool "(" (Bool (Set (Var "S")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Var "R")) ($#r1_fuzzy_1 :::"c="::: ) ) ")" ) ")" ))) ; theorem :: LFUZZY_1:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "R")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: LFUZZY_1:5 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Var "T")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Var "T")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: LFUZZY_1:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "T")) "," (Set (Var "U")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "S")) ($#r1_fuzzy_1 :::"c="::: ) ) & (Bool (Set (Var "U")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Set (Var "S")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "U"))) ($#r1_fuzzy_1 :::"c="::: ) )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "X")); :: original: :::"min"::: redefine func :::"min"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); commutativity (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "X")) "holds" (Bool (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fuzzy_1 :::"min"::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ))) ; :: original: :::"max"::: redefine func :::"max"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); commutativity (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "X")) "holds" (Bool (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_fuzzy_1 :::"max"::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ))) ; end; theorem :: LFUZZY_1:7 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set (Var "f")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: LFUZZY_1:8 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_lfuzzy_1 :::"max"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); attr "R" is :::"reflexive"::: means :: LFUZZY_1:def 2 (Bool "R" ($#r1_fuzzy_1 :::"c="::: ) ); end; :: deftheorem defines :::"reflexive"::: LFUZZY_1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_lfuzzy_1 :::"reflexive"::: ) ) "iff" (Bool (Set (Var "R")) ($#r1_fuzzy_1 :::"c="::: ) ) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); redefine attr "R" is :::"reflexive"::: means :: LFUZZY_1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set "R" ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Num 1))); end; :: deftheorem defines :::"reflexive"::: LFUZZY_1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_lfuzzy_1 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "R")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); attr "R" is :::"symmetric"::: means :: LFUZZY_1:def 4 (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) "R") ($#r2_relset_1 :::"="::: ) "R"); end; :: deftheorem defines :::"symmetric"::: LFUZZY_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) "iff" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); redefine attr "R" is :::"symmetric"::: means :: LFUZZY_1:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set "R" ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "R" ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"symmetric"::: LFUZZY_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "R")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ))) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); attr "R" is :::"transitive"::: means :: LFUZZY_1:def 6 (Bool "R" ($#r1_fuzzy_1 :::"c="::: ) ); end; :: deftheorem defines :::"transitive"::: LFUZZY_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ) "iff" (Bool (Set (Var "R")) ($#r1_fuzzy_1 :::"c="::: ) ) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); redefine attr "R" is :::"transitive"::: means :: LFUZZY_1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set (Set "(" "R" ($#k7_lfuzzy_0 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" "R" ($#k7_lfuzzy_0 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ")" )) ($#r1_orders_2 :::"<<="::: ) (Set "R" ($#k7_lfuzzy_0 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) )))); end; :: deftheorem defines :::"transitive"::: LFUZZY_1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "R")) ($#k7_lfuzzy_0 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "R")) ($#k7_lfuzzy_0 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ")" )) ($#r1_orders_2 :::"<<="::: ) (Set (Set (Var "R")) ($#k7_lfuzzy_0 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) )))) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); attr "R" is :::"antisymmetric"::: means :: LFUZZY_1:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set "R" ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "R" ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); end; :: deftheorem defines :::"antisymmetric"::: LFUZZY_1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_lfuzzy_1 :::"antisymmetric"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "R")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "R")) ($#k8_lfuzzy_0 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" ))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_fuzzy_4 :::"Imf"::: ) "(" "X" "," "X" ")" ) -> ($#v1_lfuzzy_1 :::"reflexive"::: ) ($#v2_lfuzzy_1 :::"symmetric"::: ) ($#v3_lfuzzy_1 :::"transitive"::: ) ($#v4_lfuzzy_1 :::"antisymmetric"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v1_lfuzzy_1 :::"reflexive"::: ) ($#v2_lfuzzy_1 :::"symmetric"::: ) ($#v3_lfuzzy_1 :::"transitive"::: ) ($#v4_lfuzzy_1 :::"antisymmetric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: LFUZZY_1:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) & (Bool (Set (Var "S")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) )) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" ($#k1_lfuzzy_1 :::"min"::: ) "(" (Set (Var "R")) "," (Set (Var "S")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k1_lfuzzy_1 :::"min"::: ) "(" (Set (Var "R")) "," (Set (Var "S")) ")" )))) ; theorem :: LFUZZY_1:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) & (Bool (Set (Var "S")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) )) "holds" (Bool (Set ($#k2_fuzzy_4 :::"converse"::: ) (Set "(" ($#k2_lfuzzy_1 :::"max"::: ) "(" (Set (Var "R")) "," (Set (Var "S")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k2_lfuzzy_1 :::"max"::: ) "(" (Set (Var "R")) "," (Set (Var "S")) ")" )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R", "S" be ($#v2_lfuzzy_1 :::"symmetric"::: ) ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set ($#k1_fuzzy_1 :::"min"::: ) "(" "R" "," "S" ")" ) -> ($#v2_lfuzzy_1 :::"symmetric"::: ) ; cluster (Set ($#k2_fuzzy_1 :::"max"::: ) "(" "R" "," "S" ")" ) -> ($#v2_lfuzzy_1 :::"symmetric"::: ) ; end; theorem :: LFUZZY_1:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ) & (Bool (Set (Var "S")) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) )) "holds" (Bool (Set ($#k1_lfuzzy_1 :::"min"::: ) "(" (Set (Var "R")) "," (Set (Var "S")) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R", "S" be ($#v3_lfuzzy_1 :::"transitive"::: ) ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set ($#k1_fuzzy_1 :::"min"::: ) "(" "R" "," "S" ")" ) -> ($#v3_lfuzzy_1 :::"transitive"::: ) ; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"chi"::: redefine func :::"chi"::: "(" "A" "," "X" ")" -> ($#m1_subset_1 :::"Membership_Func":::) "of" "X"; end; theorem :: LFUZZY_1:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "r")) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_lfuzzy_1 :::"chi"::: ) "(" (Set (Var "r")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "is" ($#v1_lfuzzy_1 :::"reflexive"::: ) ))) ; theorem :: LFUZZY_1:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "r")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) )) "holds" (Bool (Set ($#k3_lfuzzy_1 :::"chi"::: ) "(" (Set (Var "r")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "is" ($#v4_lfuzzy_1 :::"antisymmetric"::: ) ))) ; theorem :: LFUZZY_1:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "r")) "is" ($#v3_relat_2 :::"symmetric"::: ) )) "holds" (Bool (Set ($#k3_lfuzzy_1 :::"chi"::: ) "(" (Set (Var "r")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ))) ; theorem :: LFUZZY_1:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "r")) "is" ($#v8_relat_2 :::"transitive"::: ) )) "holds" (Bool (Set ($#k3_lfuzzy_1 :::"chi"::: ) "(" (Set (Var "r")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ))) ; theorem :: LFUZZY_1:16 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) & (Bool (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "is" ($#v4_lfuzzy_1 :::"antisymmetric"::: ) ) & (Bool (Set ($#k4_fuzzy_2 :::"Zmf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ) ")" )) ; theorem :: LFUZZY_1:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) & (Bool (Set ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ) & (Bool (Set ($#k5_fuzzy_2 :::"Umf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "is" ($#v1_lfuzzy_1 :::"reflexive"::: ) ) ")" )) ; theorem :: LFUZZY_1:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k2_lfuzzy_1 :::"max"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ))) ; theorem :: LFUZZY_1:19 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k1_lfuzzy_1 :::"min"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "R")) ")" ) ")" ) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ))) ; theorem :: LFUZZY_1:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "R9")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "R9")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) & (Bool (Set (Var "R9")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Var "R9")) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: LFUZZY_1:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "R9")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "R9")) "is" ($#v2_lfuzzy_1 :::"symmetric"::: ) ) & (Bool (Set (Var "R")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set ($#k1_lfuzzy_1 :::"min"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k2_fuzzy_4 :::"converse"::: ) (Set (Var "R")) ")" ) ")" ) ($#r1_fuzzy_1 :::"c="::: ) ))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); func "n" :::"iter"::: "R" -> ($#m1_subset_1 :::"RMembership_Func":::) "of" "X" "," "X" means :: LFUZZY_1:def 9 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) "n")) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_fuzzy_4 :::"Imf"::: ) "(" "X" "," "X" ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" "X" "," "X" "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k4_fuzzy_4 :::"(#)"::: ) "R")) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"iter"::: LFUZZY_1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_fuzzy_4 :::"Imf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "Q"))) & (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "R")))) ")" )) ")" ) ")" )) ")" ))))); theorem :: LFUZZY_1:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k5_fuzzy_4 :::"Imf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))))) ; theorem :: LFUZZY_1:23 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set (Var "R")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k5_fuzzy_4 :::"Imf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))))) ; theorem :: LFUZZY_1:24 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set ($#k5_fuzzy_4 :::"Imf"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" )))) ; theorem :: LFUZZY_1:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Num 1) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Var "R"))))) ; theorem :: LFUZZY_1:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "R"))))))) ; theorem :: LFUZZY_1:27 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" )))))) ; theorem :: LFUZZY_1:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "m")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set "(" (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" )))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); func :::"TrCl"::: "R" -> ($#m1_subset_1 :::"RMembership_Func":::) "of" "X" "," "X" equals :: LFUZZY_1:def 10 (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) "R" ")" ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"TrCl"::: LFUZZY_1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k5_lfuzzy_1 :::"TrCl"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" )))); theorem :: LFUZZY_1:29 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k5_lfuzzy_1 :::"TrCl"::: ) (Set (Var "R")) ")" ) ($#k7_lfuzzy_0 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set "(" ($#k5_card_3 :::"pi"::: ) "(" "{" (Set "(" (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ")" ")" ) "," (Set "(" ($#k1_lfuzzy_0 :::"RealPoset"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ))))) ; theorem :: LFUZZY_1:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k5_lfuzzy_1 :::"TrCl"::: ) (Set (Var "R"))) ($#r1_fuzzy_1 :::"c="::: ) ))) ; theorem :: LFUZZY_1:31 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k5_lfuzzy_1 :::"TrCl"::: ) (Set (Var "R"))) ($#r1_fuzzy_1 :::"c="::: ) )))) ; theorem :: LFUZZY_1:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Q")) "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set (Var "X")) ")" ) ")" ")" ) ($#k9_lfuzzy_0 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set "(" ($#k5_card_3 :::"pi"::: ) "(" (Set (Var "Q")) "," (Set (Var "x")) ")" ")" ) "," (Set "(" ($#k1_lfuzzy_0 :::"RealPoset"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ))))) ; theorem :: LFUZZY_1:33 (Bool "for" (Set (Var "R")) "being" ($#v3_lattice3 :::"complete"::: ) ($#v9_waybel_1 :::"Heyting"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "y")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "R")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "y")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" "," (Set (Var "R")) ")" ))))) ; theorem :: LFUZZY_1:34 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "R")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k5_lfuzzy_0 :::"@"::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Q")) "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set (Var "R")) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k5_lfuzzy_0 :::"@"::: ) (Set (Var "r")) ")" ) ")" ) where r "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) : (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) "}" "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" ))))) ; theorem :: LFUZZY_1:35 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_lfuzzy_0 :::"@"::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Q")) "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" ")" ) ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set "(" ($#k5_lfuzzy_0 :::"@"::: ) (Set (Var "r")) ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set (Var "R")) ")" ) where r "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) : (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) "}" "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" ))))) ; theorem :: LFUZZY_1:36 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k5_lfuzzy_1 :::"TrCl"::: ) (Set (Var "R")) ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" ($#k5_lfuzzy_1 :::"TrCl"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" (Set "(" (Set (Var "i")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" ) ($#k4_fuzzy_4 :::"(#)"::: ) (Set "(" (Set (Var "j")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "R")) ")" ) ")" ) where i, j "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "}" "," (Set "(" ($#k4_lfuzzy_0 :::"FuzzyLattice"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set ($#k5_lfuzzy_1 :::"TrCl"::: ) "R") -> ($#v3_lfuzzy_1 :::"transitive"::: ) ; end; theorem :: LFUZZY_1:37 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "R")) ($#r1_fuzzy_1 :::"c="::: ) )))) ; theorem :: LFUZZY_1:38 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) )) "holds" (Bool (Set (Var "R")) ($#r2_relset_1 :::"="::: ) (Set ($#k5_lfuzzy_1 :::"TrCl"::: ) (Set (Var "R")))))) ; theorem :: LFUZZY_1:39 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "S")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Set (Var "n")) ($#k4_lfuzzy_1 :::"iter"::: ) (Set (Var "S"))) ($#r1_fuzzy_1 :::"c="::: ) )))) ; theorem :: LFUZZY_1:40 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_lfuzzy_1 :::"transitive"::: ) ) & (Bool (Set (Var "S")) ($#r1_fuzzy_1 :::"c="::: ) )) "holds" (Bool (Set (Var "S")) ($#r1_fuzzy_1 :::"c="::: ) ))) ;