:: BVFUNC_1 semantic presentation begin definitionlet "k", "l" be ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) ; redefine pred "k" :::"<="::: "l" means :: BVFUNC_1:def 1 (Bool (Set "k" ($#k6_xboolean :::"=>"::: ) "l") ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )); end; :: deftheorem defines :::"<="::: BVFUNC_1:def 1 : (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) "iff" (Bool (Set (Set (Var "k")) ($#k6_xboolean :::"=>"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )); begin scheme :: BVFUNC_1:sch 1 BVFUniq1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'not'"::: redefine func :::"'not'"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "b" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'&'"::: redefine func "a" :::"'&'"::: "b" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; definitionlet "p", "q" be ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::); func "p" :::"'or'"::: "q" -> ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) means :: BVFUNC_1:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "p" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "q" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) ; idempotence (Bool "for" (Set (Var "p")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) ; func "p" :::"'xor'"::: "q" -> ($#m1_hidden :::"Function":::) means :: BVFUNC_1:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "p" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "q" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ))) ; end; :: deftheorem defines :::"'or'"::: BVFUNC_1:def 2 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b3")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_bvfunc_1 :::"'or'"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )); :: deftheorem defines :::"'xor'"::: BVFUNC_1:def 3 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k4_bvfunc_1 :::"'xor'"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))); registrationlet "p", "q" be ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "p" ($#k4_bvfunc_1 :::"'xor'"::: ) "q") -> ($#v1_margrel1 :::"boolean-valued"::: ) ; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'or'"::: redefine func "p" :::"'or'"::: "q" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" "q" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))); :: original: :::"'xor'"::: redefine func "p" :::"'xor'"::: "q" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" "q" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"'or'"::: BVFUNC_1:def 4 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))); :: deftheorem defines :::"'xor'"::: BVFUNC_1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_bvfunc_1 :::"'xor'"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))); definitionlet "p", "q" be ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::); func "p" :::"'imp'"::: "q" -> ($#m1_hidden :::"Function":::) means :: BVFUNC_1:def 6 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "p" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "q" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); func "p" :::"'eqv'"::: "q" -> ($#m1_hidden :::"Function":::) means :: BVFUNC_1:def 7 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "p" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "q" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xboolean :::"<=>"::: ) (Set "(" "q" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xboolean :::"<=>"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xboolean :::"<=>"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ))) ; end; :: deftheorem defines :::"'imp'"::: BVFUNC_1:def 6 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_bvfunc_1 :::"'imp'"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"'eqv'"::: BVFUNC_1:def 7 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_bvfunc_1 :::"'eqv'"::: ) (Set (Var "q")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xboolean :::"<=>"::: ) (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))); registrationlet "p", "q" be ($#v1_margrel1 :::"boolean-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "p" ($#k7_bvfunc_1 :::"'imp'"::: ) "q") -> ($#v1_margrel1 :::"boolean-valued"::: ) ; cluster (Set "p" ($#k8_bvfunc_1 :::"'eqv'"::: ) "q") -> ($#v1_margrel1 :::"boolean-valued"::: ) ; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'imp'"::: redefine func "p" :::"'imp'"::: "q" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" "q" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))); :: original: :::"'eqv'"::: redefine func "p" :::"'eqv'"::: "q" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set "(" "p" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" "q" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" )))); end; :: deftheorem defines :::"'imp'"::: BVFUNC_1:def 8 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))); :: deftheorem defines :::"'eqv'"::: BVFUNC_1:def 9 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "q")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_xboolean :::"'xor'"::: ) (Set "(" (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" )))) ")" ))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"O_el"::: "Y" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))); end; :: deftheorem defines :::"O_el"::: BVFUNC_1:def 10 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) ")" ))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"I_el"::: "Y" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))); end; :: deftheorem defines :::"I_el"::: BVFUNC_1:def 11 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ")" ))); theorem :: BVFUNC_1:1 canceled; theorem :: BVFUNC_1:2 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))) & (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) ")" )) ; theorem :: BVFUNC_1:3 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "a"))) ($#r2_funct_2 :::"="::: ) (Set (Var "a"))))) ; theorem :: BVFUNC_1:4 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "b")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: BVFUNC_1:5 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC_1:6 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "a"))))) ; theorem :: BVFUNC_1:7 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "a"))) ($#r2_funct_2 :::"="::: ) (Set (Var "a"))))) ; theorem :: BVFUNC_1:8 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "c"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set (Var "b")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: BVFUNC_1:9 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "a"))))) ; theorem :: BVFUNC_1:10 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC_1:11 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "c"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "c")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" (Set (Var "b")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: BVFUNC_1:12 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" (Set (Var "b")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "c")) ")" ))))) ; theorem :: BVFUNC_1:13 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BVFUNC_1:14 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))) ; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); pred "a" :::"'<'"::: "b" means :: BVFUNC_1:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "st" (Bool (Bool (Set "a" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set "b" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))); reflexivity (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "Y")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )))) ; end; :: deftheorem defines :::"'<'"::: BVFUNC_1:def 12 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set (Var "b")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ")" ))); theorem :: BVFUNC_1:15 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "c")))) "implies" (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "c"))) ")" ")" ))) ; theorem :: BVFUNC_1:16 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "b"))) ")" ))) ; theorem :: BVFUNC_1:17 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k10_bvfunc_1 :::"'eqv'"::: ) (Set (Var "b"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: BVFUNC_1:18 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y"))) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) ")" ))) ; begin definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"B_INF"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: BVFUNC_1:def 13 (Set ($#k12_bvfunc_1 :::"I_el"::: ) "Y") if (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool (Set "a" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) otherwise (Set ($#k11_bvfunc_1 :::"O_el"::: ) "Y"); func :::"B_SUP"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) equals :: BVFUNC_1:def 14 (Set ($#k11_bvfunc_1 :::"O_el"::: ) "Y") if (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool (Set "a" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) otherwise (Set ($#k12_bvfunc_1 :::"I_el"::: ) "Y"); end; :: deftheorem defines :::"B_INF"::: BVFUNC_1:def 13 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) "implies" (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) ")" & "(" (Bool (Bool "not" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))))) "implies" (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))) ")" ")" ))); :: deftheorem defines :::"B_SUP"::: BVFUNC_1:def 14 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" )) "implies" (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))) ")" & "(" (Bool (Bool "not" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))))) "implies" (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) ")" ")" ))); theorem :: BVFUNC_1:19 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ))) & (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ))) ")" ))) ; theorem :: BVFUNC_1:20 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set "(" ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))) & (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set "(" ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) & (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set "(" ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))) & (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set "(" ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) ")" )) ; registrationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_bvfunc_1 :::"O_el"::: ) "Y") -> ($#v3_funct_1 :::"constant"::: ) ; end; registrationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_bvfunc_1 :::"I_el"::: ) "Y") -> ($#v3_funct_1 :::"constant"::: ) ; end; registrationlet "Y" 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"::: ) "Y" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) bbbadV1_PARTFUN1("Y") ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_margrel1 :::"boolean-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: BVFUNC_1:21 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set ($#k11_bvfunc_1 :::"O_el"::: ) (Set (Var "Y")))) "or" (Bool (Set (Var "a")) ($#r2_funct_2 :::"="::: ) (Set ($#k12_bvfunc_1 :::"I_el"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: BVFUNC_1:22 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "d"))) ($#r2_funct_2 :::"="::: ) (Set (Var "d"))) & (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "d"))) ($#r2_funct_2 :::"="::: ) (Set (Var "d"))) ")" ))) ; theorem :: BVFUNC_1:23 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "b")) ")" ))) & (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a")) ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "b")) ")" ))) ")" ))) ; theorem :: BVFUNC_1:24 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set "(" (Set (Var "d")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "d")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set "(" ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a")) ")" ))) & (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set "(" (Set (Var "a")) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "d")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a")) ")" ) ($#k9_bvfunc_1 :::"'imp'"::: ) (Set (Var "d")))) ")" )))) ; theorem :: BVFUNC_1:25 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set "(" (Set (Var "d")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "d")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a")) ")" ))) & (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set "(" (Set (Var "d")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "d")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a")) ")" ))) & (Bool (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "d")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a")) ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "d")))) ")" )))) ; theorem :: BVFUNC_1:26 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; theorem :: BVFUNC_1:27 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))))) ; begin definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); pred "a" :::"is_dependent_of"::: "PA" means :: BVFUNC_1:def 15 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) "PA")) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set "a" ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k1_funct_1 :::"."::: ) (Set (Var "x2")))))); end; :: deftheorem defines :::"is_dependent_of"::: BVFUNC_1:def 15 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set (Var "PA"))) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set (Var "PA")))) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")))))) ")" )))); theorem :: BVFUNC_1:28 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Var "a")) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")))))) ; theorem :: BVFUNC_1:29 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Var "a")) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")))))) ; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "PA" -> ($#m1_subset_1 :::"Subset":::) "of" "Y"; end; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "Y")); let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); :: original: :::"EqClass"::: redefine func :::"EqClass"::: "(" "x" "," "PA" ")" -> ($#m1_bvfunc_1 :::"Element"::: ) "of" "PA"; end; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); func :::"B_INF"::: "(" "a" "," "PA" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 16 (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool "(" "(" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," "PA" ")" ))) "holds" (Bool (Set "a" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," "PA" ")" )) & (Bool (Bool "not" (Set "a" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ")" ))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )); end; :: deftheorem defines :::"B_INF"::: BVFUNC_1:def 16 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" "(" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "PA")) ")" ))) "holds" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) "implies" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "PA")) ")" )) & (Bool (Bool "not" (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ")" ))) "implies" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )) ")" ))))); definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); let "PA" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "Y")); func :::"B_SUP"::: "(" "a" "," "PA" ")" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) means :: BVFUNC_1:def 17 (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," "PA" ")" )) & (Bool (Set "a" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," "PA" ")" )) "or" "not" (Bool (Set "a" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) ")" )) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )); end; :: deftheorem defines :::"B_SUP"::: BVFUNC_1:def 17 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "PA")) ")" )) & (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ))) "implies" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" & "(" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k15_bvfunc_1 :::"EqClass"::: ) "(" (Set (Var "y")) "," (Set (Var "PA")) ")" )) "or" "not" (Bool (Set (Set (Var "a")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" ) ")" )) "implies" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" ")" )) ")" ))))); theorem :: BVFUNC_1:30 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" ) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set (Var "PA")))))) ; theorem :: BVFUNC_1:31 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" ) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set (Var "PA")))))) ; theorem :: BVFUNC_1:32 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" ) ($#r1_bvfunc_1 :::"'<'"::: ) (Set (Var "a")))))) ; theorem :: BVFUNC_1:33 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Var "a")) ($#r1_bvfunc_1 :::"'<'"::: ) (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" ))))) ; theorem :: BVFUNC_1:34 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k1_bvfunc_1 :::"'not'"::: ) (Set "(" ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set "(" ($#k1_bvfunc_1 :::"'not'"::: ) (Set (Var "a")) ")" ) "," (Set (Var "PA")) ")" ))))) ; theorem :: BVFUNC_1:35 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k13_bvfunc_1 :::"B_INF"::: ) (Set (Var "a")))))) ; theorem :: BVFUNC_1:36 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k6_partit1 :::"%O"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k14_bvfunc_1 :::"B_SUP"::: ) (Set (Var "a")))))) ; theorem :: BVFUNC_1:37 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "a"))))) ; theorem :: BVFUNC_1:38 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k10_eqrel_1 :::"%I"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "a"))))) ; theorem :: BVFUNC_1:39 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_bvfunc_1 :::"'&'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" ")" ) ($#k2_bvfunc_1 :::"'&'"::: ) (Set "(" ($#k16_bvfunc_1 :::"B_INF"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) ")" ")" )))))) ; theorem :: BVFUNC_1:40 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_bvfunc_1 :::"'or'"::: ) (Set (Var "b")) ")" ) "," (Set (Var "PA")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "a")) "," (Set (Var "PA")) ")" ")" ) ($#k5_bvfunc_1 :::"'or'"::: ) (Set "(" ($#k17_bvfunc_1 :::"B_SUP"::: ) "(" (Set (Var "b")) "," (Set (Var "PA")) ")" ")" )))))) ; definitionlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); func :::"GPart"::: "f" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "Y" equals :: BVFUNC_1:def 18 (Set (Set ($#k2_tarski :::"{"::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "Y" : (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "}" "," "{" (Set (Var "x9")) where x9 "is" ($#m1_subset_1 :::"Element"::: ) "of" "Y" : (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x9"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) "}" ($#k2_tarski :::"}"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"GPart"::: BVFUNC_1:def 18 : (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set ($#k18_bvfunc_1 :::"GPart"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) : (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) "}" "," "{" (Set (Var "x9")) where x9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) : (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x9"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) "}" ($#k2_tarski :::"}"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))); theorem :: BVFUNC_1:41 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "holds" (Bool (Set (Var "a")) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set ($#k18_bvfunc_1 :::"GPart"::: ) (Set (Var "a")))))) ; theorem :: BVFUNC_1:42 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) (Bool "for" (Set (Var "PA")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "a")) ($#r2_bvfunc_1 :::"is_dependent_of"::: ) (Set (Var "PA")))) "holds" (Bool (Set (Var "PA")) ($#r1_setfam_1 :::"is_finer_than"::: ) (Set ($#k18_bvfunc_1 :::"GPart"::: ) (Set (Var "a"))))))) ; begin definitionlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'nand'"::: redefine func "x" :::"'nand'"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; definitionlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"'nor'"::: redefine func "x" :::"'nor'"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; definitionlet "x", "y" be ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) ; redefine func "x" :::"<=>"::: "y" equals :: BVFUNC_1:def 19 (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" "x" ($#k10_xboolean :::"'xor'"::: ) "y" ")" )); end; :: deftheorem defines :::"<=>"::: BVFUNC_1:def 19 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k10_xboolean :::"'xor'"::: ) (Set (Var "y")) ")" )))); definitionlet "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); :: original: :::"<=>"::: redefine func "x" :::"<=>"::: "y" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; theorem :: BVFUNC_1:43 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k8_margrel1 :::"TRUE"::: ) ) ($#k8_xboolean :::"'nand'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "x"))))) ; theorem :: BVFUNC_1:44 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#k8_xboolean :::"'nand'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ; theorem :: BVFUNC_1:45 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k8_xboolean :::"'nand'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")))) & (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k8_xboolean :::"'nand'"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ; theorem :: BVFUNC_1:46 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k8_xboolean :::"'nand'"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "y"))))) ; theorem :: BVFUNC_1:47 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k8_xboolean :::"'nand'"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k8_xboolean :::"'nand'"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" )) ; theorem :: BVFUNC_1:48 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k8_xboolean :::"'nand'"::: ) (Set "(" (Set (Var "y")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set (Var "z")) ")" )))) ; theorem :: BVFUNC_1:49 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k8_xboolean :::"'nand'"::: ) (Set "(" (Set (Var "y")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "y")) ")" ) ($#k8_xboolean :::"'nand'"::: ) (Set (Var "z"))))) ; theorem :: BVFUNC_1:50 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k8_margrel1 :::"TRUE"::: ) ) ($#k9_xboolean :::"'nor'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) ))) ; theorem :: BVFUNC_1:51 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#k9_xboolean :::"'nor'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "x"))))) ; theorem :: BVFUNC_1:52 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k9_xboolean :::"'nor'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")))) & (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k9_xboolean :::"'nor'"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ; theorem :: BVFUNC_1:53 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k9_xboolean :::"'nor'"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_xboolean :::"'or'"::: ) (Set (Var "y"))))) ; theorem :: BVFUNC_1:54 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k9_xboolean :::"'nor'"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) & (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k9_xboolean :::"'nor'"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ; theorem :: BVFUNC_1:55 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k9_xboolean :::"'nor'"::: ) (Set "(" (Set (Var "y")) ($#k5_xboolean :::"'or'"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k5_xboolean :::"'or'"::: ) (Set (Var "y")) ")" ) ($#k5_xboolean :::"'or'"::: ) (Set (Var "z")) ")" )))) ; theorem :: BVFUNC_1:56 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k8_margrel1 :::"TRUE"::: ) ) ($#k7_xboolean :::"<=>"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: BVFUNC_1:57 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k7_margrel1 :::"FALSE"::: ) ) ($#k7_xboolean :::"<=>"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "x"))))) ; theorem :: BVFUNC_1:58 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) ")" )) ; theorem :: BVFUNC_1:59 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_xboolean :::"'xor'"::: ) (Set (Var "y"))))) ; theorem :: BVFUNC_1:60 (Bool "for" (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_margrel1 :::"FALSE"::: ) )) & (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) ")" )) ; theorem :: BVFUNC_1:61 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "y")) ($#k6_xboolean :::"=>"::: ) (Set (Var "z")))) "iff" (Bool (Set (Set (Var "x")) ($#k4_xboolean :::"'&'"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "z"))) ")" )) ; theorem :: BVFUNC_1:62 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_xboolean :::"=>"::: ) (Set (Var "y")) ")" ) ($#k4_xboolean :::"'&'"::: ) (Set "(" (Set (Var "y")) ($#k6_xboolean :::"=>"::: ) (Set (Var "x")) ")" )))) ; theorem :: BVFUNC_1:63 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k6_xboolean :::"=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "y")) ")" ) ($#k6_xboolean :::"=>"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" )))) ; theorem :: BVFUNC_1:64 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k7_xboolean :::"<=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "x")) ")" ) ($#k7_xboolean :::"<=>"::: ) (Set "(" ($#k3_xboolean :::"'not'"::: ) (Set (Var "y")) ")" )))) ; theorem :: BVFUNC_1:65 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set (Set (Var "x")) ($#k6_xboolean :::"=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ; theorem :: BVFUNC_1:66 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k6_xboolean :::"=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ; theorem :: BVFUNC_1:67 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_xboolean :::"'not'"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k6_xboolean :::"=>"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ; theorem :: BVFUNC_1:68 (Bool "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "y")) ($#k6_xboolean :::"=>"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set (Var "y")) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "z")) ($#k6_xboolean :::"=>"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ; theorem :: BVFUNC_1:69 (Bool "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "y")) ($#k6_xboolean :::"=>"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Set (Var "z")) ($#k6_xboolean :::"=>"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ; theorem :: BVFUNC_1:70 (Bool "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xboolean :::"boolean"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k6_xboolean :::"=>"::: ) (Set "(" (Set (Var "y")) ($#k6_xboolean :::"=>"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_margrel1 :::"TRUE"::: ) ))) ;