:: ENTROPY1 semantic presentation begin theorem :: ENTROPY1:1 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "l")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "k")) ($#r1_nat_d :::"divides"::: ) (Set (Var "l")))) "holds" (Bool (Set (Set (Var "i")) ($#k3_nat_d :::"div"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "j")) ($#k3_nat_d :::"div"::: ) (Set (Var "k"))))) ; theorem :: ENTROPY1:2 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1))) & "(" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1)))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Num 1))) "implies" (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1)))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Num 1)) ")" ")" )) ; theorem :: ENTROPY1:3 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1))) & "(" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1)))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Num 1))) "implies" (Bool (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "r")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Num 1)))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Num 1)) ")" ")" )) ; theorem :: ENTROPY1:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ENTROPY1:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "b")) ")" ) ")" ))) ; theorem :: ENTROPY1:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "b")) ($#k8_real_1 :::"*"::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k8_real_1 :::"*"::: ) (Set (Var "c")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b")) ($#k8_real_1 :::"*"::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k8_real_1 :::"*"::: ) (Set (Var "c")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" )))) ; theorem :: ENTROPY1:7 (Bool "for" (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q2")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q1"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q1")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "q2")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q2")) ")" )))) ; theorem :: ENTROPY1:8 (Bool "for" (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q2")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q1"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q1")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "q2")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q2")) ")" )))) ; theorem :: ENTROPY1:9 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) & (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" ))) ; notationlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); synonym :::"nonnegative"::: "p" for :::"nonnegative-yielding"::: ; end; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); redefine attr "p" is :::"nonnegative-yielding"::: means :: ENTROPY1:def 1 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set "p" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"nonnegative"::: ENTROPY1:def 1 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_partfun3 :::"nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_valued_0 :::"complex-yielding"::: ) bbbadV2_VALUED_0() bbbadV3_VALUED_0() ($#v4_partfun3 :::"nonnegative"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: ENTROPY1:10 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_partfun3 :::"nonnegative"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "p"))) "is" ($#v4_partfun3 :::"nonnegative"::: ) ))) ; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "p" :::"has_onlyone_value_in"::: "k" means :: ENTROPY1:def 2 (Bool "(" (Bool "k" ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p")) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) "k")) "holds" (Bool (Set "p" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"has_onlyone_value_in"::: ENTROPY1:def 2 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "k"))) "iff" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ))); theorem :: ENTROPY1:11 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "k"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: ENTROPY1:12 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool (Set (Var "p")) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "k")))) "holds" (Bool "(" (Bool (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "k"))) & (Bool (Set (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" ))) ; theorem :: ENTROPY1:13 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))))) ; theorem :: ENTROPY1:14 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_partfun3 :::"nonnegative"::: ) )) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "p")) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "k"))))) ; registration cluster ($#v1_matrprob :::"ProbFinS"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_partfun3 :::"nonnegative"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: ENTROPY1:15 (Bool "for" (Set (Var "p")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "p")) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "k"))))) ; theorem :: ENTROPY1:16 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "i")) ")" )) "is" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ))) ; registration cluster ($#v1_matrix_1 :::"tabular"::: ) ($#v3_matrprob :::"with_sum=1"::: ) -> ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); cluster ($#v1_matrix_1 :::"tabular"::: ) ($#v4_matrprob :::"Joint_Probability"::: ) -> ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); end; theorem :: ENTROPY1:17 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_matrprob :::"SumAll"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ENTROPY1:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))))) ; theorem :: ENTROPY1:19 (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "MR")) "is" ($#v2_matrprob :::"m-nonnegative"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "MR"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "i")) ")" ) "is" ($#v4_partfun3 :::"nonnegative"::: ) )) ")" )) ; begin theorem :: ENTROPY1:20 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" ($#k10_matrixr1 :::"LineVec2Mx"::: ) (Set (Var "p")) ")" ) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_matrprob :::"<*"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k2_matrprob :::"*>"::: ) )))) ; theorem :: ENTROPY1:21 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_matrixr1 :::"ColVec2Mx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set "(" ($#k10_matrixr1 :::"LineVec2Mx"::: ) (Set (Var "q")) ")" ))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")) ")" ))) ")" ) ")" ) ")" )))) ; theorem :: ENTROPY1:22 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_matrixr1 :::"ColVec2Mx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set "(" ($#k10_matrixr1 :::"LineVec2Mx"::: ) (Set (Var "q")) ")" ))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "q")))) ")" ) ")" ) ")" )))) ; theorem :: ENTROPY1:23 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k9_matrixr1 :::"ColVec2Mx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set "(" ($#k10_matrixr1 :::"LineVec2Mx"::: ) (Set (Var "q")) ")" )) "is" ($#v4_matrprob :::"Joint_Probability"::: ) )) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "MR" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "MR" is :::"diagonal"::: means :: ENTROPY1:def 3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "MR")) & (Bool (Set "MR" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))); end; :: deftheorem defines :::"diagonal"::: ENTROPY1:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "MR")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "MR")) "is" ($#v1_entropy1 :::"diagonal"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "MR")))) & (Bool (Set (Set (Var "MR")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_matrix_1 :::"tabular"::: ) ($#v1_entropy1 :::"diagonal"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: ENTROPY1:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "MR")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "MR")) "is" ($#v1_entropy1 :::"diagonal"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "MR"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "i")) ")" ) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "i")))) ")" ))) ; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Vec2DiagMx"::: "p" -> ($#v1_entropy1 :::"diagonal"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: ENTROPY1:def 4 (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "j")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_seq_1 :::"."::: ) (Set (Var "j"))))); end; :: deftheorem defines :::"Vec2DiagMx"::: ENTROPY1:def 4 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#v1_entropy1 :::"diagonal"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "j")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))))) ")" ))); theorem :: ENTROPY1:25 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "MR")) ($#r1_hidden :::"="::: ) (Set ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MR"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "MR"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "MR"))))) "holds" (Bool "(" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "i")) ")" ) ($#r1_entropy1 :::"has_onlyone_value_in"::: ) (Set (Var "i"))) & (Bool (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "i")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ) ")" ))) ; theorem :: ENTROPY1:26 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "MR")) "," (Set (Var "MR1")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MR"))))) "holds" (Bool "(" (Bool (Set (Var "MR1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set (Var "MR")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MR1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "MR1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "MR")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "MR1"))))) "holds" (Bool (Set (Set (Var "MR1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "MR")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ))) ")" ) ")" ) ")" ))) ; theorem :: ENTROPY1:27 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "MR")) "," (Set (Var "MR1")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MR"))))) "holds" (Bool "(" (Bool (Set (Var "MR1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set (Var "MR")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MR1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "MR1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "MR")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "MR1"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR1")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k11_rvsum_1 :::"*"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "i")) ")" ")" ))) ")" ) ")" ) ")" ))) ; theorem :: ENTROPY1:28 (Bool "for" (Set (Var "p")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v6_matrprob :::"Conditional_Probability"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set "(" ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set (Var "M"))) "is" ($#v4_matrprob :::"Joint_Probability"::: ) ))) ; theorem :: ENTROPY1:29 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))))))) ; theorem :: ENTROPY1:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "i")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "j")) ")" ))))))) ; theorem :: ENTROPY1:31 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Num 1) "," (Set (Var "j")) ")" )) ")" ) ")" ) ")" )))) ; theorem :: ENTROPY1:32 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "j")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "j")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))))))))) ; theorem :: ENTROPY1:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "j")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))))))))) ; theorem :: ENTROPY1:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "j")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "l"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "j")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" )))))) ; theorem :: ENTROPY1:35 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "j")) ")" ))) ")" ))))) ; theorem :: ENTROPY1:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ))) & (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "j")) ")" ))) ")" ))))) ; theorem :: ENTROPY1:37 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))))) ; theorem :: ENTROPY1:38 (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "holds" (Bool (Set ($#k5_matrprob :::"SumAll"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); func :::"Mx2FinS"::: "M" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D" means :: ENTROPY1:def 5 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) if (Bool (Set ($#k3_finseq_1 :::"len"::: ) "M") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "M" ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set "M" ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M"))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "M" ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"Mx2FinS"::: ENTROPY1:def 5 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "M")) ($#k1_matrprob :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" )) ")" ) ")" ")" )))); theorem :: ENTROPY1:39 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ))))) ; theorem :: ENTROPY1:40 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "j")) ")" ))) ")" )))) ; theorem :: ENTROPY1:41 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k9_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k3_nat_d :::"div"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set (Var "l")) ($#k4_nat_d :::"mod"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set "(" (Set (Var "l")) ($#k3_nat_d :::"div"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set (Var "l")) ($#k4_nat_d :::"mod"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ")" )))) ; theorem :: ENTROPY1:42 (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_matrprob :::"SumAll"::: ) (Set (Var "MR"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "MR")) ")" )))) ; theorem :: ENTROPY1:43 (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "MR")) "is" ($#v2_matrprob :::"m-nonnegative"::: ) ) "iff" (Bool (Set ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "MR"))) "is" ($#v4_partfun3 :::"nonnegative"::: ) ) ")" )) ; theorem :: ENTROPY1:44 (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "MR")) "is" ($#v4_matrprob :::"Joint_Probability"::: ) ) "iff" (Bool (Set ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "MR"))) "is" ($#v1_matrprob :::"ProbFinS"::: ) ) ")" )) ; theorem :: ENTROPY1:45 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_entropy1 :::"Mx2FinS"::: ) (Set "(" (Set "(" ($#k9_matrixr1 :::"ColVec2Mx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set "(" ($#k10_matrixr1 :::"LineVec2Mx"::: ) (Set (Var "q")) ")" ) ")" )) "is" ($#v1_matrprob :::"ProbFinS"::: ) )) ; theorem :: ENTROPY1:46 (Bool "for" (Set (Var "p")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v6_matrprob :::"Conditional_Probability"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k2_entropy1 :::"Mx2FinS"::: ) (Set "(" (Set "(" ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set (Var "M")) ")" )) "is" ($#v1_matrprob :::"ProbFinS"::: ) ))) ; begin definitionlet "a" be ($#m1_subset_1 :::"Real":::); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); assume (Bool (Set (Const "p")) "is" ($#v4_partfun3 :::"nonnegative"::: ) ) ; func :::"FinSeq_log"::: "(" "a" "," "p" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: ENTROPY1:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool "(" "(" (Bool (Bool (Set "p" ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" "a" "," (Set "(" "p" ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set "p" ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"FinSeq_log"::: ENTROPY1:def 6 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_partfun3 :::"nonnegative"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_entropy1 :::"FinSeq_log"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) ")" ) ")" )))); definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Infor_FinSeq_of"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: ENTROPY1:def 7 (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" "p" "," (Set "(" ($#k3_entropy1 :::"FinSeq_log"::: ) "(" (Num 2) "," "p" ")" ")" ) ")" ); end; :: deftheorem defines :::"Infor_FinSeq_of"::: ENTROPY1:def 7 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k3_entropy1 :::"FinSeq_log"::: ) "(" (Num 2) "," (Set (Var "p")) ")" ")" ) ")" ))); theorem :: ENTROPY1:47 (Bool "for" (Set (Var "p")) "being" ($#v4_partfun3 :::"nonnegative"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ")" ))) ")" ) ")" ) ")" ))) ; theorem :: ENTROPY1:48 (Bool "for" (Set (Var "p")) "being" ($#v4_partfun3 :::"nonnegative"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ")" ))) ")" ")" ))) ; theorem :: ENTROPY1:49 (Bool "for" (Set (Var "p")) "being" ($#v4_partfun3 :::"nonnegative"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ) ")" ")" ))) ")" ) ")" ) ")" ))) ; theorem :: ENTROPY1:50 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#v4_partfun3 :::"nonnegative"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "r2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "r2"))))) "holds" (Bool (Set (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "r2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set (Var "r1")) ")" ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set (Var "r2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set (Var "r2")) ")" ")" ) ")" )))))) ; theorem :: ENTROPY1:51 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#v4_partfun3 :::"nonnegative"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set (Var "r")) ")" ")" ) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k3_entropy1 :::"FinSeq_log"::: ) "(" (Num 2) "," (Set (Var "p")) ")" ")" ) ")" ")" ) ")" ))))) ; theorem :: ENTROPY1:52 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; definitionlet "MR" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); assume (Bool (Set (Const "MR")) "is" ($#v2_matrprob :::"m-nonnegative"::: ) ) ; func :::"Infor_FinSeq_of"::: "MR" -> ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: ENTROPY1:def 8 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "MR")) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "MR")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_matrprob :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" "MR" "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k3_entropy1 :::"FinSeq_log"::: ) "(" (Num 2) "," (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" "MR" "," (Set (Var "k")) ")" ")" ) ")" ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Infor_FinSeq_of"::: ENTROPY1:def 8 : (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "MR")) "is" ($#v2_matrprob :::"m-nonnegative"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "MR")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MR")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "MR")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_matrprob :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "k")) ")" ")" ) "," (Set "(" ($#k3_entropy1 :::"FinSeq_log"::: ) "(" (Num 2) "," (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "k")) ")" ")" ) ")" ")" ) ")" )) ")" ) ")" ) ")" ))); theorem :: ENTROPY1:53 (Bool "for" (Set (Var "M")) "being" ($#v2_matrprob :::"m-nonnegative"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M")) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: ENTROPY1:54 (Bool "for" (Set (Var "M")) "being" ($#v2_matrprob :::"m-nonnegative"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M1")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M1"))))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ")" ))) ")" ) ")" ) ")" ))) ; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Entropy"::: "p" -> ($#m1_subset_1 :::"Real":::) equals :: ENTROPY1:def 9 (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) "p" ")" ) ")" )); end; :: deftheorem defines :::"Entropy"::: ENTROPY1:def 9 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ) ")" )))); theorem :: ENTROPY1:55 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ENTROPY1:56 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))) "holds" (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: ENTROPY1:57 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "pp")) "," (Set (Var "qq")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pp"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qq"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "pp")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ")" ) ")" ))) & (Bool (Set (Set (Var "qq")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ")" ) ")" ))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "pp"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "qq")))) & "(" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" )) "implies" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "pp"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "qq")))) ")" & "(" (Bool (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "pp"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "qq"))))) "implies" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))))) ")" & "(" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ))) "implies" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "pp"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "qq")))) ")" & "(" (Bool (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "pp"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "qq"))))) "implies" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" )) ")" ")" ))) ; theorem :: ENTROPY1:58 (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) & "(" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" )) "implies" (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))) "implies" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )))) ")" & "(" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" ))) "implies" (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_power :::"log"::: ) "(" (Num 2) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))) "implies" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" )) ")" ")" )) ; theorem :: ENTROPY1:59 (Bool "for" (Set (Var "M")) "being" ($#v2_matrprob :::"m-nonnegative"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k2_entropy1 :::"Mx2FinS"::: ) (Set "(" ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "M")) ")" )))) ; theorem :: ENTROPY1:60 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_matrixr1 :::"ColVec2Mx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set "(" ($#k10_matrixr1 :::"LineVec2Mx"::: ) (Set (Var "q")) ")" )))) "holds" (Bool (Set ($#k5_matrprob :::"SumAll"::: ) (Set "(" ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "q")) ")" ) ")" ))))) ; definitionlet "MR" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Entropy_of_Joint_Prob"::: "MR" -> ($#m1_subset_1 :::"Real":::) equals :: ENTROPY1:def 10 (Set ($#k6_entropy1 :::"Entropy"::: ) (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) "MR" ")" )); end; :: deftheorem defines :::"Entropy_of_Joint_Prob"::: ENTROPY1:def 10 : (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k7_entropy1 :::"Entropy_of_Joint_Prob"::: ) (Set (Var "MR"))) ($#r1_hidden :::"="::: ) (Set ($#k6_entropy1 :::"Entropy"::: ) (Set "(" ($#k2_entropy1 :::"Mx2FinS"::: ) (Set (Var "MR")) ")" )))); theorem :: ENTROPY1:61 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k7_entropy1 :::"Entropy_of_Joint_Prob"::: ) (Set "(" (Set "(" ($#k9_matrixr1 :::"ColVec2Mx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set "(" ($#k10_matrixr1 :::"LineVec2Mx"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "q")) ")" )))) ; definitionlet "MR" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Entropy_of_Cond_Prob"::: "MR" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: ENTROPY1:def 11 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "MR")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_entropy1 :::"Entropy"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" "MR" "," (Set (Var "k")) ")" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Entropy_of_Cond_Prob"::: ENTROPY1:def 11 : (Bool "for" (Set (Var "MR")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_entropy1 :::"Entropy_of_Cond_Prob"::: ) (Set (Var "MR")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "MR")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_entropy1 :::"Entropy"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "MR")) "," (Set (Var "k")) ")" ")" ))) ")" ) ")" ) ")" ))); theorem :: ENTROPY1:62 (Bool "for" (Set (Var "M")) "being" ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v6_matrprob :::"Conditional_Probability"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k8_entropy1 :::"Entropy_of_Cond_Prob"::: ) (Set (Var "M")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M")) ")" ) ($#k1_matrprob :::"."::: ) (Set (Var "k")) ")" ) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: ENTROPY1:63 (Bool "for" (Set (Var "M")) "being" ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v6_matrprob :::"Conditional_Probability"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k8_entropy1 :::"Entropy_of_Cond_Prob"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" ($#k3_matrprob :::"LineSum"::: ) (Set "(" ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M")) ")" ) ")" )))) ; theorem :: ENTROPY1:64 (Bool "for" (Set (Var "p")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v6_matrprob :::"Conditional_Probability"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool "for" (Set (Var "M1")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k5_matrprob :::"SumAll"::: ) (Set "(" ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k3_matrprob :::"LineSum"::: ) (Set "(" ($#k5_entropy1 :::"Infor_FinSeq_of"::: ) (Set (Var "M")) ")" ) ")" ) ")" ")" ) ")" )))))) ; theorem :: ENTROPY1:65 (Bool "for" (Set (Var "p")) "being" ($#v1_matrprob :::"ProbFinS"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "M")) "being" ($#~v3_relat_1 "non" ($#v3_relat_1 :::"empty-yielding"::: ) ) ($#v6_matrprob :::"Conditional_Probability"::: ) ($#m2_finseq_1 :::"Matrix":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#k7_entropy1 :::"Entropy_of_Joint_Prob"::: ) (Set "(" (Set "(" ($#k1_entropy1 :::"Vec2DiagMx"::: ) (Set (Var "p")) ")" ) ($#k6_matrixr1 :::"*"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_entropy1 :::"Entropy"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k14_rvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k8_entropy1 :::"Entropy_of_Cond_Prob"::: ) (Set (Var "M")) ")" ) ")" ")" ) ")" ))))) ;