:: HILBERT3 semantic presentation begin registrationlet "m", "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," "n" ")" ($#k4_funct_4 :::"-->"::: ) "(" "m" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set "(" "n" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," "m" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: HILBERT3:1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "i")) "is" ($#v1_abian :::"even"::: ) ) "iff" (Bool (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) "is" ($#v1_abian :::"odd"::: ) ) ")" )) ; theorem :: HILBERT3:2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "i")) "is" ($#v1_abian :::"odd"::: ) ) "iff" (Bool (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) "is" ($#v1_abian :::"even"::: ) ) ")" )) ; theorem :: HILBERT3:3 (Bool "for" (Set (Var "X")) "being" ($#v1_zfmisc_1 :::"trivial"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set (Var "f")))))) ; theorem :: HILBERT3:4 (Bool "for" (Set (Var "f")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) ; theorem :: HILBERT3:5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "B"))))) ; theorem :: HILBERT3:6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "B")))))) ; theorem :: HILBERT3:7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: HILBERT3:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_funct_3 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "X")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "X")) ")" )))) ; theorem :: HILBERT3:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_funct_3 :::"chi"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "X")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "X")) ")" )))) ; theorem :: HILBERT3:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "x9")) "," (Set (Var "y9")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) ")" )) ; theorem :: HILBERT3:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )))) ; theorem :: HILBERT3:12 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 2) "," (Set (Var "D")) (Bool "ex" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ))))) ; theorem :: HILBERT3:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" ))) ; theorem :: HILBERT3:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")) ")" ) ")" )))) ; theorem :: HILBERT3:15 (Bool (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Num 2)) ; begin registrationlet "f", "g" be ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k15_funct_3 :::"[:"::: ) "f" "," "g" ($#k15_funct_3 :::":]"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: HILBERT3:16 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k16_funct_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Set (Var "C")) "," (Set (Var "D")) ")" ")" ))))))) ; theorem :: HILBERT3:17 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k16_funct_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set (Var "C")) "," (Set (Var "D")) ")" ")" ))))))) ; theorem :: HILBERT3:18 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k15_pralg_1 :::".."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: HILBERT3:19 (Bool "for" (Set (Var "f")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k15_pralg_1 :::".."::: ) (Set (Var "g")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k15_pralg_1 :::".."::: ) (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "h")) ")" ))))) ; theorem :: HILBERT3:20 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "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 "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k15_pralg_1 :::".."::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: HILBERT3:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k15_pralg_1 :::".."::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "C")))))) ; theorem :: HILBERT3:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; theorem :: HILBERT3:23 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" )))) ; theorem :: HILBERT3:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set ($#k2_pralg_2 :::"Frege"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" )))) ; begin registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "A")); let "Q" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "B")); cluster (Set ($#k15_funct_3 :::"[:"::: ) "P" "," "Q" ($#k15_funct_3 :::":]"::: ) ) -> ($#v3_funct_2 :::"bijective"::: ) for ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ); end; theorem :: HILBERT3:25 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "B")) "holds" (Bool (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k16_funct_3 :::":]"::: ) ) "is" ($#v3_funct_2 :::"bijective"::: ) )))) ; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "A")); let "Q" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set (Const "B")); func "P" :::"=>"::: "Q" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," "B" ")" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," "B" ")" ")" ) means :: HILBERT3:def 1 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "A" "," "B" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "Q" ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" "P" ($#k2_funct_2 :::"""::: ) ")" )))); end; :: deftheorem defines :::"=>"::: HILBERT3:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "B")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_hilbert3 :::"=>"::: ) (Set (Var "Q")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Q")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k2_funct_2 :::"""::: ) ")" )))) ")" ))))); registrationlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "A")); let "Q" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "B")); cluster (Set "P" ($#k1_hilbert3 :::"=>"::: ) "Q") -> ($#v3_funct_2 :::"bijective"::: ) ; end; theorem :: HILBERT3:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "P")) ($#k1_hilbert3 :::"=>"::: ) (Set (Var "Q")) ")" ) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Q")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "P")))))))) ; theorem :: HILBERT3:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_hilbert3 :::"=>"::: ) (Set (Var "Q")) ")" ) ($#k2_funct_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_hilbert3 :::"=>"::: ) (Set "(" (Set (Var "Q")) ($#k2_funct_2 :::"""::: ) ")" )))))) ; theorem :: HILBERT3:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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 "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "P")) ($#k1_hilbert3 :::"=>"::: ) (Set (Var "Q")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k16_pralg_1 :::".."::: ) (Set "(" (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k16_pralg_1 :::".."::: ) (Set (Var "g")) ")" )))))))) ; begin definitionmode SetValuation is bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "V" be ($#m1_hidden :::"SetValuation":::); func :::"SetVal"::: "V" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) means :: HILBERT3:def 2 (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k2_hilbert1 :::"VERUM"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set "V" ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) "," (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) "," (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "q")) ")" ) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SetVal"::: HILBERT3:def 2 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_hilbert3 :::"SetVal"::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_hilbert1 :::"VERUM"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")) ")" ) ")" )) ")" ) ")" ) ")" ) ")" ))); definitionlet "V" be ($#m1_hidden :::"SetValuation":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); func :::"SetVal"::: "(" "V" "," "p" ")" -> ($#m1_hidden :::"set"::: ) equals :: HILBERT3:def 3 (Set (Set "(" ($#k2_hilbert3 :::"SetVal"::: ) "V" ")" ) ($#k1_funct_1 :::"."::: ) "p"); end; :: deftheorem defines :::"SetVal"::: HILBERT3:def 3 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_hilbert3 :::"SetVal"::: ) (Set (Var "V")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))))); registrationlet "V" be ($#m1_hidden :::"SetValuation":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," "p" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: HILBERT3:29 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) "holds" (Bool (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set ($#k2_hilbert1 :::"VERUM"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: HILBERT3:30 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) "holds" (Bool (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))) ; theorem :: HILBERT3:31 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) "holds" (Bool (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "q")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: HILBERT3:32 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) "holds" (Bool (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "q")) ")" ")" ) ")" )))) ; registrationlet "V" be ($#m1_hidden :::"SetValuation":::); let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) "q" ")" ) ")" ) -> ($#v4_funct_1 :::"functional"::: ) ; end; registrationlet "V" be ($#m1_hidden :::"SetValuation":::); let "p", "q", "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) (Set "(" "q" ($#k3_hilbert1 :::"=>"::: ) "r" ")" ) ")" ) ")" ); end; registrationlet "V" be ($#m1_hidden :::"SetValuation":::); let "p", "q", "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) "q" ")" ) ")" ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) "r" ")" ) ")" ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) "q" ")" ) ")" ")" ) "," (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) "r" ")" ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) (Set "(" "q" ($#k3_hilbert1 :::"=>"::: ) "r" ")" ) ")" ) ")" ); end; begin definitionlet "V" be ($#m1_hidden :::"SetValuation":::); mode :::"Permutation"::: "of" "V" -> ($#m1_hidden :::"Function":::) means :: HILBERT3:def 4 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" "V" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Permutation"::: HILBERT3:def 4 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ")" ) ")" ) ")" ))); definitionlet "V" be ($#m1_hidden :::"SetValuation":::); let "P" be ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Const "V")); func :::"Perm"::: "P" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k2_hilbert3 :::"SetVal"::: ) "V") "," (Set ($#k2_hilbert3 :::"SetVal"::: ) "V") means :: HILBERT3:def 5 (Bool "(" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set ($#k2_hilbert1 :::"VERUM"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set "P" ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "ex" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set (Var "p")) ")" ")" )(Bool "ex" (Set (Var "q9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," (Set (Var "q")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "q")))) & (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "p9")) "," (Set (Var "q9")) ($#k16_funct_3 :::":]"::: ) )) & (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p9")) ($#k1_hilbert3 :::"=>"::: ) (Set (Var "q9")))) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Perm"::: HILBERT3:def 5 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b3")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k2_hilbert3 :::"SetVal"::: ) (Set (Var "V"))) "," (Set ($#k2_hilbert3 :::"SetVal"::: ) (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_hilbert3 :::"Perm"::: ) (Set (Var "P")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set ($#k2_hilbert1 :::"VERUM"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "ex" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ")" )(Bool "ex" (Set (Var "q9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "q")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "p9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Var "q9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "p9")) "," (Set (Var "q9")) ($#k16_funct_3 :::":]"::: ) )) & (Bool (Set (Set (Var "b3")) ($#k1_msualg_3 :::"."::: ) (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p9")) ($#k1_hilbert3 :::"=>"::: ) (Set (Var "q9")))) ")" ))) ")" ) ")" ) ")" )))); definitionlet "V" be ($#m1_hidden :::"SetValuation":::); let "P" be ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Const "V")); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); func :::"Perm"::: "(" "P" "," "p" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," "p" ")" ")" ) "," (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" "V" "," "p" ")" ")" ) equals :: HILBERT3:def 6 (Set (Set "(" ($#k4_hilbert3 :::"Perm"::: ) "P" ")" ) ($#k1_msualg_3 :::"."::: ) "p"); end; :: deftheorem defines :::"Perm"::: HILBERT3:def 6 : (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_hilbert3 :::"Perm"::: ) (Set (Var "P")) ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "p"))))))); theorem :: HILBERT3:33 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set ($#k2_hilbert1 :::"VERUM"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set ($#k2_hilbert1 :::"VERUM"::: ) ) ")" ")" ))))) ; theorem :: HILBERT3:34 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: HILBERT3:35 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set "(" (Set (Var "p")) ($#k4_hilbert1 :::"'&'"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "q")) ")" ")" ) ($#k16_funct_3 :::":]"::: ) ))))) ; theorem :: HILBERT3:36 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ")" ) (Bool "for" (Set (Var "q9")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "q")) ")" ")" ) "st" (Bool (Bool (Set (Var "p9")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" )) & (Bool (Set (Var "q9")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "q")) ")" ))) "holds" (Bool (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "p9")) ($#k1_hilbert3 :::"=>"::: ) (Set (Var "q9"))))))))) ; registrationlet "V" be ($#m1_hidden :::"SetValuation":::); let "P" be ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Const "V")); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster (Set ($#k5_hilbert3 :::"Perm"::: ) "(" "P" "," "p" ")" ) -> ($#v3_funct_2 :::"bijective"::: ) ; end; theorem :: HILBERT3:37 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "q")) ")" ")" ) "holds" (Bool (Set (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "q")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ")" ) ($#k2_funct_2 :::"""::: ) ")" ))))))) ; theorem :: HILBERT3:38 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "q")) ")" ")" ) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "q")) ")" ")" ) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ")" ))))))) ; theorem :: HILBERT3:39 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k3_hilbert3 :::"SetVal"::: ) "(" (Set (Var "V")) "," (Set (Var "q")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "q")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ")" ))))))) ; theorem :: HILBERT3:40 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set "(" (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q")) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "q")) ")" ))))))) ; begin definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); attr "p" is :::"canonical"::: means :: HILBERT3:def 7 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," "p" ")" ))))); end; :: deftheorem defines :::"canonical"::: HILBERT3:def 7 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_hilbert3 :::"canonical"::: ) ) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ))))) ")" )); registration cluster (Set ($#k2_hilbert1 :::"VERUM"::: ) ) -> ($#v1_hilbert3 :::"canonical"::: ) ; end; registrationlet "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster (Set "p" ($#k3_hilbert1 :::"=>"::: ) (Set "(" "q" ($#k3_hilbert1 :::"=>"::: ) "p" ")" )) -> ($#v1_hilbert3 :::"canonical"::: ) ; cluster (Set (Set "(" "p" ($#k4_hilbert1 :::"'&'"::: ) "q" ")" ) ($#k3_hilbert1 :::"=>"::: ) "p") -> ($#v1_hilbert3 :::"canonical"::: ) ; cluster (Set (Set "(" "p" ($#k4_hilbert1 :::"'&'"::: ) "q" ")" ) ($#k3_hilbert1 :::"=>"::: ) "q") -> ($#v1_hilbert3 :::"canonical"::: ) ; cluster (Set "p" ($#k3_hilbert1 :::"=>"::: ) (Set "(" "q" ($#k3_hilbert1 :::"=>"::: ) (Set "(" "p" ($#k4_hilbert1 :::"'&'"::: ) "q" ")" ) ")" )) -> ($#v1_hilbert3 :::"canonical"::: ) ; end; registrationlet "p", "q", "r" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); cluster (Set (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) (Set "(" "q" ($#k3_hilbert1 :::"=>"::: ) "r" ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) "q" ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" "p" ($#k3_hilbert1 :::"=>"::: ) "r" ")" ) ")" )) -> ($#v1_hilbert3 :::"canonical"::: ) ; end; theorem :: HILBERT3:41 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_hilbert3 :::"canonical"::: ) ) & (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) "is" ($#v1_hilbert3 :::"canonical"::: ) )) "holds" (Bool (Set (Var "q")) "is" ($#v1_hilbert3 :::"canonical"::: ) )) ; theorem :: HILBERT3:42 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k6_hilbert1 :::"HP_TAUT"::: ) ))) "holds" (Bool (Set (Var "p")) "is" ($#v1_hilbert3 :::"canonical"::: ) )) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSEQ_1() ($#v1_hilbert3 :::"canonical"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); end; begin definitionlet "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); attr "p" is :::"pseudo-canonical"::: means :: HILBERT3:def 8 (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," "p" ")" ))))); end; :: deftheorem defines :::"pseudo-canonical"::: HILBERT3:def 8 : (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v2_hilbert3 :::"pseudo-canonical"::: ) ) "iff" (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ))))) ")" )); registration cluster ($#v1_hilbert3 :::"canonical"::: ) -> ($#v2_hilbert3 :::"pseudo-canonical"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ); end; theorem :: HILBERT3:43 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_hilbert3 :::"pseudo-canonical"::: ) ) & (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_hilbert3 :::"pseudo-canonical"::: ) )) "holds" (Bool (Set (Var "q")) "is" ($#v2_hilbert3 :::"pseudo-canonical"::: ) )) ; theorem :: HILBERT3:44 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_hilbert1 :::"HP-WFF"::: ) ) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"SetValuation":::) (Bool "for" (Set (Var "P")) "being" ($#m1_hilbert3 :::"Permutation"::: ) "of" (Set (Var "V")) "st" (Bool (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "f")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "p")) ")" ))) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set (Var "f")) ($#r1_abian :::"is_a_fixpoint_of"::: ) (Set ($#k5_hilbert3 :::"Perm"::: ) "(" (Set (Var "P")) "," (Set (Var "q")) ")" ))) ")" )) "holds" (Bool "not" (Bool (Set (Set (Var "p")) ($#k3_hilbert1 :::"=>"::: ) (Set (Var "q"))) "is" ($#v2_hilbert3 :::"pseudo-canonical"::: ) ))))) ; theorem :: HILBERT3:45 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "not" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "a")) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "b")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "a")) ")" ) ")" ) ($#k3_hilbert1 :::"=>"::: ) (Set "(" ($#k1_hilbert2 :::"prop"::: ) (Set (Var "a")) ")" )) "is" ($#v2_hilbert3 :::"pseudo-canonical"::: ) ))) ;