:: MATRIX16 semantic presentation begin theorem :: MATRIX16:1 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: MATRIX16:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ) ")" ) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")))))) ; definitionlet "K" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "p" be ($#m1_hidden :::"FinSequence":::); pred "M" :::"is_line_circulant_about"::: "p" means :: MATRIX16:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_line_circulant_about"::: MATRIX16:def 1 : (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_matrix16 :::"is_line_circulant_about"::: ) (Set (Var "p"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" )))); definitionlet "K" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); attr "M" is :::"line_circulant"::: means :: MATRIX16:def 2 (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "K" "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "M" ($#r1_matrix16 :::"is_line_circulant_about"::: ) (Set (Var "p"))) ")" )); end; :: deftheorem defines :::"line_circulant"::: MATRIX16:def 2 : (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set (Var "M")) ($#r1_matrix16 :::"is_line_circulant_about"::: ) (Set (Var "p"))) ")" )) ")" ))); definitionlet "K" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "K")); attr "p" is :::"first-line-of-circulant"::: means :: MATRIX16:def 3 (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" "st" (Bool (Set (Var "M")) ($#r1_matrix16 :::"is_line_circulant_about"::: ) "p")); end; :: deftheorem defines :::"first-line-of-circulant"::: MATRIX16:def 3 : (Bool "for" (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) "iff" (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "st" (Bool (Set (Var "M")) ($#r1_matrix16 :::"is_line_circulant_about"::: ) (Set (Var "p")))) ")" ))); definitionlet "K" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "p" be ($#m1_hidden :::"FinSequence":::); pred "M" :::"is_col_circulant_about"::: "p" means :: MATRIX16:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M"))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_col_circulant_about"::: MATRIX16:def 4 : (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r2_matrix16 :::"is_col_circulant_about"::: ) (Set (Var "p"))) "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 "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" )))); definitionlet "K" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); attr "M" is :::"col_circulant"::: means :: MATRIX16:def 5 (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "K" "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "M")) & (Bool "M" ($#r2_matrix16 :::"is_col_circulant_about"::: ) (Set (Var "p"))) ")" )); end; :: deftheorem defines :::"col_circulant"::: MATRIX16:def 5 : (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")))) & (Bool (Set (Var "M")) ($#r2_matrix16 :::"is_col_circulant_about"::: ) (Set (Var "p"))) ")" )) ")" ))); definitionlet "K" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "K")); attr "p" is :::"first-col-of-circulant"::: means :: MATRIX16:def 6 (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" "st" (Bool (Set (Var "M")) ($#r2_matrix16 :::"is_col_circulant_about"::: ) "p")); end; :: deftheorem defines :::"first-col-of-circulant"::: MATRIX16:def 6 : (Bool "for" (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) "iff" (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "st" (Bool (Set (Var "M")) ($#r2_matrix16 :::"is_col_circulant_about"::: ) (Set (Var "p")))) ")" ))); definitionlet "K" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "K")); assume (Bool (Set (Const "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) ; func :::"LCirc"::: "p" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" means :: MATRIX16:def 7 (Bool it ($#r1_matrix16 :::"is_line_circulant_about"::: ) "p"); end; :: deftheorem defines :::"LCirc"::: MATRIX16:def 7 : (Bool "for" (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "b3")) ($#r1_matrix16 :::"is_line_circulant_about"::: ) (Set (Var "p"))) ")" )))); definitionlet "K" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "K")); assume (Bool (Set (Const "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) ; func :::"CCirc"::: "p" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" means :: MATRIX16:def 8 (Bool it ($#r2_matrix16 :::"is_col_circulant_about"::: ) "p"); end; :: deftheorem defines :::"CCirc"::: MATRIX16:def 8 : (Bool "for" (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "b3")) ($#r2_matrix16 :::"is_col_circulant_about"::: ) (Set (Var "p"))) ")" )))); registrationlet "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_matrix16 :::"first-line-of-circulant"::: ) ($#v4_matrix16 :::"first-col-of-circulant"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k11_matrix_1 :::"0."::: ) "(" "K" "," "n" ")" ) -> ($#v1_matrix16 :::"line_circulant"::: ) ($#v3_matrix16 :::"col_circulant"::: ) ; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) "a") -> ($#v1_matrix16 :::"line_circulant"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) "a") -> ($#v3_matrix16 :::"col_circulant"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_matrix_1 :::"tabular"::: ) ($#v1_matrix16 :::"line_circulant"::: ) ($#v3_matrix16 :::"col_circulant"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ); end; theorem :: MATRIX16:3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ) "is" ($#v3_matrix16 :::"col_circulant"::: ) )))) ; theorem :: MATRIX16:4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "A")) ($#r1_matrix16 :::"is_line_circulant_about"::: ) (Set (Var "t"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "A")) "," (Num 1) ")" )))))) ; theorem :: MATRIX16:5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))))) ; theorem :: MATRIX16:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1"))) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))))) ; theorem :: MATRIX16:7 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v1_matrix16 :::"line_circulant"::: ) )))) ; theorem :: MATRIX16:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M3"))) "is" ($#v1_matrix16 :::"line_circulant"::: ) )))) ; theorem :: MATRIX16:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" )) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))))) ; theorem :: MATRIX16:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))))) ; theorem :: MATRIX16:11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1"))) "is" ($#v1_matrix16 :::"line_circulant"::: ) )))) ; theorem :: MATRIX16:12 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2"))) "is" ($#v1_matrix16 :::"line_circulant"::: ) )))) ; theorem :: MATRIX16:13 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" )) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))))) ; theorem :: MATRIX16:14 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))))) ; theorem :: MATRIX16:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))))) ; theorem :: MATRIX16:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v1_matrix16 :::"line_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v1_matrix16 :::"line_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))))) ; theorem :: MATRIX16:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ) "is" ($#v1_matrix16 :::"line_circulant"::: ) )))) ; theorem :: MATRIX16:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "A")) ($#r2_matrix16 :::"is_col_circulant_about"::: ) (Set (Var "t"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "A")) "," (Num 1) ")" )))))) ; theorem :: MATRIX16:19 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))))) ; theorem :: MATRIX16:20 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1"))) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))))) ; theorem :: MATRIX16:21 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v3_matrix16 :::"col_circulant"::: ) )))) ; theorem :: MATRIX16:22 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M3"))) "is" ($#v3_matrix16 :::"col_circulant"::: ) )))) ; theorem :: MATRIX16:23 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" )) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))))) ; theorem :: MATRIX16:24 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))))) ; theorem :: MATRIX16:25 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1"))) "is" ($#v3_matrix16 :::"col_circulant"::: ) )))) ; theorem :: MATRIX16:26 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2"))) "is" ($#v3_matrix16 :::"col_circulant"::: ) )))) ; theorem :: MATRIX16:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" )) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))))) ; theorem :: MATRIX16:28 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))))) ; theorem :: MATRIX16:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))))) ; theorem :: MATRIX16:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "M3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v3_matrix16 :::"col_circulant"::: ) ) & (Bool (Set (Var "M3")) "is" ($#v3_matrix16 :::"col_circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1")) ")" ) ($#k3_matrix_6 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M2")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M3")) ")" )) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))))) ; theorem :: MATRIX16:31 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )) "holds" (Bool (Set ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p"))) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ))) ; theorem :: MATRIX16:32 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix16 :::"LCirc"::: ) (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")) ")" ))))) ; theorem :: MATRIX16:33 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q"))) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ))) ; theorem :: MATRIX16:34 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "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")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix16 :::"LCirc"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "q")) ")" ))))) ; theorem :: MATRIX16:35 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )) "holds" (Bool (Set ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p"))) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ))) ; theorem :: MATRIX16:36 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )) "holds" (Bool (Set ($#k2_matrix16 :::"CCirc"::: ) (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")) ")" ))))) ; theorem :: MATRIX16:37 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q"))) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ))) ; theorem :: MATRIX16:38 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "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")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )) "holds" (Bool (Set ($#k2_matrix16 :::"CCirc"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "q")) ")" ))))) ; theorem :: MATRIX16:39 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v3_matrix16 :::"col_circulant"::: ) ))) ; theorem :: MATRIX16:40 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "n")) ")" ) "is" ($#v1_matrix16 :::"line_circulant"::: ) ))) ; theorem :: MATRIX16:41 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )))) ; theorem :: MATRIX16:42 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix16 :::"LCirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX16:43 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix16 :::"LCirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX16:44 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix16 :::"LCirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: MATRIX16:45 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v2_matrix16 :::"first-line-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix16 :::"LCirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix16 :::"LCirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: MATRIX16:46 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )))) ; theorem :: MATRIX16:47 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )) "holds" (Bool (Set ($#k2_matrix16 :::"CCirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX16:48 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix16 :::"CCirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX16:49 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) & (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 "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix16 :::"CCirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: MATRIX16:50 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v4_matrix16 :::"first-col-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k2_matrix16 :::"CCirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_matrix16 :::"CCirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" )))))) ; notationlet "K" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); synonym :::"circulant"::: "M" for :::"line_circulant"::: ; end; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "p" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); pred "M1" :::"is_anti-circular_about"::: "p" means :: MATRIX16:def 9 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M1")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M1")) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set "M1" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M1")) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set "M1" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fvsum_1 :::"-"::: ) "p" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_anti-circular_about"::: MATRIX16:def 9 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r3_matrix16 :::"is_anti-circular_about"::: ) (Set (Var "p"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); attr "M" is :::"anti-circular"::: means :: MATRIX16:def 10 (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "K" "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "M" ($#r3_matrix16 :::"is_anti-circular_about"::: ) (Set (Var "p"))) ")" )); end; :: deftheorem defines :::"anti-circular"::: MATRIX16:def 10 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v5_matrix16 :::"anti-circular"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set (Var "M")) ($#r3_matrix16 :::"is_anti-circular_about"::: ) (Set (Var "p"))) ")" )) ")" ))); definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "p" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); attr "p" is :::"first-line-of-anti-circular"::: means :: MATRIX16:def 11 (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" "st" (Bool (Set (Var "M")) ($#r3_matrix16 :::"is_anti-circular_about"::: ) "p")); end; :: deftheorem defines :::"first-line-of-anti-circular"::: MATRIX16:def 11 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) "iff" (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "st" (Bool (Set (Var "M")) ($#r3_matrix16 :::"is_anti-circular_about"::: ) (Set (Var "p")))) ")" ))); definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "p" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); assume (Bool (Set (Const "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) ; func :::"ACirc"::: "p" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" means :: MATRIX16:def 12 (Bool it ($#r3_matrix16 :::"is_anti-circular_about"::: ) "p"); end; :: deftheorem defines :::"ACirc"::: MATRIX16:def 12 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "b3")) ($#r3_matrix16 :::"is_anti-circular_about"::: ) (Set (Var "p"))) ")" )))); theorem :: MATRIX16:51 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v5_matrix16 :::"anti-circular"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1"))) "is" ($#v5_matrix16 :::"anti-circular"::: ) ))))) ; theorem :: MATRIX16:52 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v5_matrix16 :::"anti-circular"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v5_matrix16 :::"anti-circular"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) "is" ($#v5_matrix16 :::"anti-circular"::: ) )))) ; theorem :: MATRIX16:53 (Bool "for" (Set (Var "K")) "being" ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "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")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Var "M1")) "is" ($#v5_matrix16 :::"anti-circular"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; theorem :: MATRIX16:54 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v5_matrix16 :::"anti-circular"::: ) ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))))) ; theorem :: MATRIX16:55 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v5_matrix16 :::"anti-circular"::: ) )) "holds" (Bool (Set ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1"))) "is" ($#v5_matrix16 :::"anti-circular"::: ) )))) ; theorem :: MATRIX16:56 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v5_matrix16 :::"anti-circular"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v5_matrix16 :::"anti-circular"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_6 :::"-"::: ) (Set (Var "M2"))) "is" ($#v5_matrix16 :::"anti-circular"::: ) )))) ; theorem :: MATRIX16:57 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r3_matrix16 :::"is_anti-circular_about"::: ) (Set (Var "p"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Num 1) ")" )))))) ; theorem :: MATRIX16:58 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) )) "holds" (Bool (Set ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p"))) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ))) ; theorem :: MATRIX16:59 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) )) "holds" (Bool (Set ($#k3_matrix16 :::"ACirc"::: ) (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")) ")" ))))) ; theorem :: MATRIX16:60 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q"))) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ))) ; theorem :: MATRIX16:61 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k3_matrix16 :::"ACirc"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "q")) ")" ))))) ; theorem :: MATRIX16:62 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) )))) ; theorem :: MATRIX16:63 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) )) "holds" (Bool (Set ($#k3_matrix16 :::"ACirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX16:64 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix16 :::"ACirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX16:65 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix16 :::"ACirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: MATRIX16:66 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_matrix16 :::"first-line-of-anti-circular"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k3_matrix16 :::"ACirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_matrix16 :::"ACirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" )))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k11_matrix_1 :::"0."::: ) "(" "K" "," "n" ")" ) -> ($#v5_matrix16 :::"anti-circular"::: ) ; end;