:: QMAX_1 semantic presentation begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); func :::"Probabilities"::: "S" -> ($#m1_hidden :::"set"::: ) means :: QMAX_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m2_prob_1 :::"Probability"::: ) "of" "S") ")" )); end; :: deftheorem defines :::"Probabilities"::: QMAX_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_qmax_1 :::"Probabilities"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "S"))) ")" )) ")" )))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); cluster (Set ($#k1_qmax_1 :::"Probabilities"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"QM_Str"::: -> ; aggr :::"QM_Str":::(# :::"Observables":::, :::"FStates":::, :::"Quantum_Probability"::: #) -> ($#l1_qmax_1 :::"QM_Str"::: ) ; sel :::"Observables"::: "c1" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; sel :::"FStates"::: "c1" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; sel :::"Quantum_Probability"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_qmax_1 :::"Observables"::: ) "of" "c1") "," (Set "the" ($#u2_qmax_1 :::"FStates"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_qmax_1 :::"Probabilities"::: ) (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) ")" ); end; definitionlet "Q" be ($#l1_qmax_1 :::"QM_Str"::: ) ; func :::"Obs"::: "Q" -> ($#m1_hidden :::"set"::: ) equals :: QMAX_1:def 2 (Set "the" ($#u1_qmax_1 :::"Observables"::: ) "of" "Q"); func :::"Sts"::: "Q" -> ($#m1_hidden :::"set"::: ) equals :: QMAX_1:def 3 (Set "the" ($#u2_qmax_1 :::"FStates"::: ) "of" "Q"); end; :: deftheorem defines :::"Obs"::: QMAX_1:def 2 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"QM_Str"::: ) "holds" (Bool (Set ($#k2_qmax_1 :::"Obs"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_qmax_1 :::"Observables"::: ) "of" (Set (Var "Q"))))); :: deftheorem defines :::"Sts"::: QMAX_1:def 3 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"QM_Str"::: ) "holds" (Bool (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_qmax_1 :::"FStates"::: ) "of" (Set (Var "Q"))))); registrationlet "Q" be ($#l1_qmax_1 :::"QM_Str"::: ) ; cluster (Set ($#k2_qmax_1 :::"Obs"::: ) "Q") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k3_qmax_1 :::"Sts"::: ) "Q") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "Q" be ($#l1_qmax_1 :::"QM_Str"::: ) ; let "A1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) (Set (Const "Q"))); let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Const "Q"))); func :::"Meas"::: "(" "A1" "," "s" ")" -> ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) equals :: QMAX_1:def 4 (Set (Set "the" ($#u3_qmax_1 :::"Quantum_Probability"::: ) "of" "Q") ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) "A1" "," "s" ($#k1_domain_1 :::"]"::: ) )); end; :: deftheorem defines :::"Meas"::: QMAX_1:def 4 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"QM_Str"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) (Set (Var "Q"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "Q"))) "holds" (Bool (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A1")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_qmax_1 :::"Quantum_Probability"::: ) "of" (Set (Var "Q"))) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "A1")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )))))); definitionlet "IT" be ($#l1_qmax_1 :::"QM_Str"::: ) ; attr "IT" is :::"Quantum_Mechanics-like"::: means :: QMAX_1:def 5 (Bool "(" (Bool "(" "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) "IT") "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) "IT") "holds" (Bool (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A1")) "," (Set (Var "s")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A2")) "," (Set (Var "s")) ")" )) ")" )) "holds" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "A2"))) ")" ) & (Bool "(" "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) "IT") "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) "IT") "holds" (Bool (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s1")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s2")) ")" )) ")" )) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) ")" ) & (Bool "(" "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) "IT") (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) "IT") "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) "IT") (Bool "for" (Set (Var "E")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s1")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "E")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "E")) ")" ) ")" ))))))) ")" ) ")" ); end; :: deftheorem defines :::"Quantum_Mechanics-like"::: QMAX_1:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#l1_qmax_1 :::"QM_Str"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_qmax_1 :::"Quantum_Mechanics-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) (Set (Var "IT"))) "st" (Bool (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "IT"))) "holds" (Bool (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A1")) "," (Set (Var "s")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A2")) "," (Set (Var "s")) ")" )) ")" )) "holds" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "A2"))) ")" ) & (Bool "(" "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "IT"))) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) (Set (Var "IT"))) "holds" (Bool (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s1")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s2")) ")" )) ")" )) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) ")" ) & (Bool "(" "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "IT"))) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "IT"))) "st" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) (Set (Var "IT"))) (Bool "for" (Set (Var "E")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s1")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "E")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set (Var "A")) "," (Set (Var "s2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "E")) ")" ) ")" ))))))) ")" ) ")" ) ")" )); registration cluster ($#v1_qmax_1 :::"strict"::: ) ($#v2_qmax_1 :::"Quantum_Mechanics-like"::: ) for ($#l1_qmax_1 :::"QM_Str"::: ) ; end; definitionmode Quantum_Mechanics is ($#v2_qmax_1 :::"Quantum_Mechanics-like"::: ) ($#l1_qmax_1 :::"QM_Str"::: ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"OrthoRelStr"::: -> ($#l1_orders_2 :::"RelStr"::: ) "," ($#l1_robbins1 :::"ComplStr"::: ) ; aggr :::"OrthoRelStr":::(# :::"carrier":::, :::"InternalRel":::, :::"Compl"::: #) -> ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "X1" be ($#m1_hidden :::"set"::: ) ; let "Inv" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X1")) "," (Set (Const "X1")); pred "Inv" :::"is_an_involution"::: means :: QMAX_1:def 6 (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X1" "holds" (Bool (Set "Inv" ($#k1_funct_1 :::"."::: ) (Set "(" "Inv" ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x1")))); end; :: deftheorem defines :::"is_an_involution"::: QMAX_1:def 6 : (Bool "for" (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Inv")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "X1")) "holds" (Bool "(" (Bool (Set (Var "Inv")) ($#r1_qmax_1 :::"is_an_involution"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) "holds" (Bool (Set (Set (Var "Inv")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "Inv")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) ")" ))); definitionlet "W" be ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; pred "W" :::"is_a_Quantum_Logic"::: means :: QMAX_1:def 7 (Bool "(" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "W") ($#r2_orders_1 :::"partially_orders"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W")) & (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "W") ($#r1_qmax_1 :::"is_an_involution"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "W" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "W"))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "W") ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "W") ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "W")) ")" ) ")" ); end; :: deftheorem defines :::"is_a_Quantum_Logic"::: QMAX_1:def 7 : (Bool "for" (Set (Var "W")) "being" ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r2_qmax_1 :::"is_a_Quantum_Logic"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "W"))) ($#r2_orders_1 :::"partially_orders"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) & (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "W"))) ($#r1_qmax_1 :::"is_an_involution"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "W"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "W"))) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "W"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "W")))) ")" ) ")" ) ")" )); definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); func :::"Prop"::: "Q" -> ($#m1_hidden :::"set"::: ) equals :: QMAX_1:def 8 (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_qmax_1 :::"Obs"::: ) "Q" ")" ) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); end; :: deftheorem defines :::"Prop"::: QMAX_1:def 8 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) "holds" (Bool (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_qmax_1 :::"Obs"::: ) (Set (Var "Q")) ")" ) "," (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))); registrationlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); cluster (Set ($#k5_qmax_1 :::"Prop"::: ) "Q") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))); :: original: :::"`1"::: redefine func "p" :::"`1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_qmax_1 :::"Obs"::: ) "Q"); :: original: :::"`2"::: redefine func "p" :::"`2"::: -> ($#m1_prob_1 :::"Event"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ); end; theorem :: QMAX_1:1 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "Q"))) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) (Bool "for" (Set (Var "E")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set ($#k12_prob_1 :::"Borel_Sets"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_qmax_1 :::"`2"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_qmax_1 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "E")) ")" ))))))) ; definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); let "p" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))); func :::"'not'"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) "Q") equals :: QMAX_1:def 9 (Set ($#k1_domain_1 :::"["::: ) (Set "(" "p" ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" "p" ($#k7_qmax_1 :::"`2"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "b2")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "b2")) ($#k7_qmax_1 :::"`2"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "b1")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "b1")) ($#k7_qmax_1 :::"`2"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ))) ; end; :: deftheorem defines :::"'not'"::: QMAX_1:def 9 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool (Set ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "p")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k7_qmax_1 :::"`2"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) )))); definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))); pred "p" :::"|-"::: "q" means :: QMAX_1:def 10 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) "Q") "holds" (Bool (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" "p" ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" "p" ($#k7_qmax_1 :::"`2"::: ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" "q" ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" "q" ($#k7_qmax_1 :::"`2"::: ) ")" )))); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Const "Q"))) "holds" (Bool (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_qmax_1 :::"`2"::: ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_qmax_1 :::"`2"::: ) ")" ))))) ; end; :: deftheorem defines :::"|-"::: QMAX_1:def 10 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "Q"))) "holds" (Bool (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_qmax_1 :::"`2"::: ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "q")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "q")) ($#k7_qmax_1 :::"`2"::: ) ")" )))) ")" ))); definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); let "p", "q" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))); pred "p" :::"<==>"::: "q" means :: QMAX_1:def 11 (Bool "(" (Bool "p" ($#r3_qmax_1 :::"|-"::: ) "q") & (Bool "q" ($#r3_qmax_1 :::"|-"::: ) "p") ")" ); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "p"))) ")" )) ; symmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Const "Q"))) "st" (Bool (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "p")))) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) ")" )) ; end; :: deftheorem defines :::"<==>"::: QMAX_1:def 11 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "p"))) ")" ) ")" ))); theorem :: QMAX_1:2 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "q"))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_qmax_1 :::"Sts"::: ) (Set (Var "Q"))) "holds" (Bool (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "p")) ($#k7_qmax_1 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_qmax_1 :::"Meas"::: ) "(" (Set "(" (Set (Var "q")) ($#k6_qmax_1 :::"`1"::: ) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "q")) ($#k7_qmax_1 :::"`2"::: ) ")" )))) ")" ))) ; theorem :: QMAX_1:3 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "p"))))) ; theorem :: QMAX_1:4 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "r"))))) ; theorem :: QMAX_1:5 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "p"))))) ; theorem :: QMAX_1:6 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "q")))) "holds" (Bool (Set (Var "q")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "p"))))) ; theorem :: QMAX_1:7 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "r"))))) ; theorem :: QMAX_1:8 canceled; theorem :: QMAX_1:9 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "q"))) ($#r3_qmax_1 :::"|-"::: ) (Set ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "p")))))) ; definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); func :::"PropRel"::: "Q" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k5_qmax_1 :::"Prop"::: ) "Q" ")" ) means :: QMAX_1:def 12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) "Q") "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "q"))) ")" )); end; :: deftheorem defines :::"PropRel"::: QMAX_1:def 12 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")))) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "p")) ($#r4_qmax_1 :::"<==>"::: ) (Set (Var "q"))) ")" )) ")" ))); theorem :: QMAX_1:10 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ))) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" )))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "b")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "d")))))) ; definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); func :::"OrdRel"::: "Q" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) "Q" ")" ) ")" ) means :: QMAX_1:def 13 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_qmax_1 :::"Prop"::: ) "Q" ")" ) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) "Q" ")" ))) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) "Q" ")" ))) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) "Q") "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"OrdRel"::: QMAX_1:def 13 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_qmax_1 :::"OrdRel"::: ) (Set (Var "Q")))) "iff" (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q")) ")" ) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ))) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ))) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) ")" ) ")" ) ")" )) ")" ))); theorem :: QMAX_1:11 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_qmax_1 :::"|-"::: ) (Set (Var "q"))) "iff" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) "," (Set (Var "p")) ")" ")" ) "," (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) "," (Set (Var "q")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_qmax_1 :::"OrdRel"::: ) (Set (Var "Q")))) ")" ))) ; theorem :: QMAX_1:12 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ))) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" )))) "holds" (Bool "for" (Set (Var "p1")) "," (Set (Var "q1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "q1")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "p1"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "q1"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))))) ; theorem :: QMAX_1:13 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ))) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" )))) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "st" (Bool (Bool (Set ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))))) ; definitionlet "Q" be ($#l1_qmax_1 :::"Quantum_Mechanics":::); func :::"InvRel"::: "Q" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) "Q" ")" ) ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) "Q" ")" ) ")" ) means :: QMAX_1:def 14 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) "Q") "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) "Q" ")" ) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) "Q" ")" ) "," (Set "(" ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ))); end; :: deftheorem defines :::"InvRel"::: QMAX_1:def 14 : (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_qmax_1 :::"InvRel"::: ) (Set (Var "Q")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_qmax_1 :::"Prop"::: ) (Set (Var "Q"))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) "," (Set (Var "p")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) "," (Set "(" ($#k8_qmax_1 :::"'not'"::: ) (Set (Var "p")) ")" ) ")" ))) ")" ))); theorem :: QMAX_1:14 (Bool "for" (Set (Var "Q")) "being" ($#l1_qmax_1 :::"Quantum_Mechanics":::) "holds" (Bool (Set ($#g2_qmax_1 :::"OrthoRelStr"::: ) "(#" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k9_qmax_1 :::"PropRel"::: ) (Set (Var "Q")) ")" ) ")" ) "," (Set "(" ($#k10_qmax_1 :::"OrdRel"::: ) (Set (Var "Q")) ")" ) "," (Set "(" ($#k11_qmax_1 :::"InvRel"::: ) (Set (Var "Q")) ")" ) "#)" ) ($#r2_qmax_1 :::"is_a_Quantum_Logic"::: ) )) ;