:: MATRIXJ1 semantic presentation begin theorem :: MATRIXJ1:1 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "g1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "g2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g1")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g2")) ")" ))))) ; theorem :: MATRIXJ1:2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k4_wsierp_1 :::"Del"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_wsierp_1 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))))))) ; theorem :: MATRIXJ1:3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k4_wsierp_1 :::"Del"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k4_wsierp_1 :::"Del"::: ) "(" (Set (Var "g")) "," (Set (Var "i")) ")" ")" )))))) ; theorem :: MATRIXJ1:4 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set ($#k4_wsierp_1 :::"Del"::: ) "(" (Set "(" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d"))))))) ; theorem :: MATRIXJ1:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"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")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "K")) ")" ) ($#k1_laplace :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "n")) ")" ))))) ; definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m1_hidden :::"Nat":::); assume (Bool (Set (Const "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Const "f")) ")" ))) ; func :::"min"::: "(" "f" "," "i" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: MATRIXJ1:def 1 (Bool "(" (Bool "i" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" "f" ($#k17_finseq_1 :::"|"::: ) it ")" ))) & (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "i" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" "f" ($#k17_finseq_1 :::"|"::: ) (Set (Var "j")) ")" )))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) ")" ) ")" ); end; :: deftheorem defines :::"min"::: MATRIXJ1:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "b3")) ")" ))) & (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "j")) ")" )))) "holds" (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) ")" ) ")" ) ")" )))); theorem :: MATRIXJ1:6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "i"))))) ; theorem :: MATRIXJ1:7 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) ")" ))) ; theorem :: MATRIXJ1:8 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" )))) ; theorem :: MATRIXJ1:9 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "g")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" ) ")" ) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: MATRIXJ1:10 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ")" ))) & (Bool (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "i"))) ")" ))) ; theorem :: MATRIXJ1:11 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "j")) ")" ))) & "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ")" ) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j"))))) ; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); attr "F" is :::"Matrix-yielding"::: means :: MATRIXJ1:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F"))) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m2_finseq_1 :::"Matrix":::) "of" "D")); end; :: deftheorem defines :::"Matrix-yielding"::: MATRIXJ1:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_matrixj1 :::"Matrix-yielding"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")))) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#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_matrixj1 :::"Matrix-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode FinSequence_of_Matrix of "D" is ($#v1_matrixj1 :::"Matrix-yielding"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); mode FinSequence_of_Matrix of "K" is ($#v1_matrixj1 :::"Matrix-yielding"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); end; theorem :: MATRIXJ1:12 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "D")); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "F" :::"."::: "x" -> ($#m2_finseq_1 :::"Matrix":::) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F1", "F2" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "D")); :: original: :::"^"::: redefine func "F1" :::"^"::: "F2" -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M1" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"M1":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "D"; let "M2" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"M1" "," "M2":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "F" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "D")); :: original: :::"|"::: redefine func "F" :::"|"::: "n" -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "D"; :: original: :::"/^"::: redefine func "F" :::"/^"::: "n" -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "D"; end; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "D")); func :::"Len"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: MATRIXJ1:def 3 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" "F" ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); func :::"Width"::: "F" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: MATRIXJ1:def 4 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" "F" ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Len"::: MATRIXJ1:def 3 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_matrixj1 :::"Len"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))); :: deftheorem defines :::"Width"::: MATRIXJ1:def 4 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_matrixj1 :::"Width"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "D")); :: original: :::"Len"::: redefine func :::"Len"::: "F" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "F" ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); :: original: :::"Width"::: redefine func :::"Width"::: "F" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "F" ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; theorem :: MATRIXJ1:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))) "holds" (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )))) ; theorem :: MATRIXJ1:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F1")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F2")) ")" ))))) ; theorem :: MATRIXJ1:15 (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 ($#k10_matrixj1 :::"Len"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "M")) ($#k4_matrixj1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: MATRIXJ1:16 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2")) ")" ))))) ; theorem :: MATRIXJ1:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set "(" (Set (Var "F1")) ($#k6_matrixj1 :::"|"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F1")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))))))) ; theorem :: MATRIXJ1:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F1")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F2")) ")" ))))) ; theorem :: MATRIXJ1:19 (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 ($#k11_matrixj1 :::"Width"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "M")) ($#k4_matrixj1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: MATRIXJ1:20 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2")) ")" ))))) ; theorem :: MATRIXJ1:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set "(" (Set (Var "F1")) ($#k6_matrixj1 :::"|"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F1")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))))))) ; begin definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "F" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "D")); func :::"block_diagonal"::: "(" "F" "," "d" ")" -> ($#m2_finseq_1 :::"Matrix":::) "of" "D" means :: MATRIXJ1:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) "F" ")" ))) & (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"::: ) it))) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) "F" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) "or" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) "F" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" )) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) "d") ")" & "(" (Bool (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) "F" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) "F" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) "," (Set (Var "i")) ")" ")" ) ")" )))) "implies" (Bool (Set it ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k2_matrixj1 :::"."::: ) (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) "F" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" )) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"block_diagonal"::: MATRIXJ1:def 5 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ))) & (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 "b4"))))) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) "or" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" )) "implies" (Bool (Set (Set (Var "b4")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" & "(" (Bool (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" )))) "implies" (Bool (Set (Set (Var "b4")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" )) ")" ")" ) ")" ) ")" ) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "F" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "D")); :: original: :::"block_diagonal"::: redefine func :::"block_diagonal"::: "(" "F" "," "d" ")" -> ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) "F" ")" )) "," (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) "F" ")" )) "," "D"; end; theorem :: MATRIXJ1:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: MATRIXJ1:23 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" )) "," (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" )) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set (Var "d")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M1"))))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "M2"))))) "implies" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set (Var "M2")) "," (Set (Var "i")) ")" ")" ))) ")" ")" )) ")" ))))) ; theorem :: MATRIXJ1:24 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix"::: ) "of" (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" )) "," (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" )) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set (Var "d")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")) ")" )))) "implies" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M1")) "," (Set (Var "i")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2")) ")" )))) "implies" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set (Var "M2")) "," (Set (Var "i")) ")" ")" ))) ")" ")" )) ")" ))))) ; theorem :: MATRIXJ1:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F1")) "," (Set (Var "d1")) ")" ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d2")) ")" ")" ) ")" ))))) ; theorem :: MATRIXJ1:26 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F1")) "," (Set (Var "d")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F1")) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" )))))) ; theorem :: MATRIXJ1:27 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F2")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F2")) "," (Set (Var "d1")) ")" ")" ))) "iff" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F1")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F1")) ")" ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d2")) ")" ")" ))) ")" ) ")" ))))) ; theorem :: MATRIXJ1:28 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F2")) "," (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F2")) "," (Set (Var "d")) ")" ")" )))) "holds" (Bool (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F2")) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F1")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F1")) ")" ) ")" ) ")" ) ")" )))))) ; theorem :: MATRIXJ1:29 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d")) ")" ")" ))) & (Bool "(" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F1")) ")" ))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F1")) ")" ))) ")" ) "or" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F1")) ")" ))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F1")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: MATRIXJ1:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "j")) "," (Set (Var "k")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" ")" ))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "j")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" ")" ) ($#k3_matrix_1 :::"*"::: ) "(" (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" )) ")" ))))) ; theorem :: MATRIXJ1:31 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ) ")" )))))) ; theorem :: MATRIXJ1:32 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "M")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F")) ")" ) "," (Set (Var "d")) ")" ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ")" ) ")" )))))) ; theorem :: MATRIXJ1:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k6_matrix13 :::"Segm"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "M")) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "d")) ")" ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ")" ) ")" )))))) ; theorem :: MATRIXJ1:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "M")) ($#k4_matrixj1 :::"*>"::: ) ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "M")))))) ; theorem :: MATRIXJ1:35 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F1")) "," (Set (Var "d")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d")) ")" ))))) ; theorem :: MATRIXJ1:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F2")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F1")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F2")) "," (Set (Var "d")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "d")) ")" ))))) ; theorem :: MATRIXJ1:37 (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ")" ))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set "(" (Set (Var "F")) ($#k6_matrixj1 :::"|"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k8_matrix_1 :::"Line"::: ) "(" (Set "(" (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set "(" (Set (Var "F")) ($#k6_matrixj1 :::"|"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set "(" (Set (Var "F")) ($#k6_matrixj1 :::"|"::: ) (Set (Var "m")) ")" ) ")" ) ")" ) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ))))))) ; theorem :: MATRIXJ1:38 (Bool "for" (Set (Var "i")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) ")" ))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrixj1 :::"min"::: ) "(" (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "F")) ")" ) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set "(" (Set (Var "F")) ($#k6_matrixj1 :::"|"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k9_matrix_1 :::"Col"::: ) "(" (Set "(" (Set (Var "F")) ($#k2_matrixj1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set "(" (Set (Var "F")) ($#k6_matrixj1 :::"|"::: ) (Set "(" (Set (Var "m")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "F")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set "(" (Set (Var "F")) ($#k6_matrixj1 :::"|"::: ) (Set (Var "m")) ")" ) ")" ) ")" ) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ))))))) ; theorem :: MATRIXJ1:39 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "," (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "N1")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "N1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "N2")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "N2")))) & (Bool (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "M1")) "," (Set (Var "M2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "N1")) "," (Set (Var "N2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set (Var "d2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Var "N1"))) & (Bool (Set (Var "M2")) ($#r1_hidden :::"="::: ) (Set (Var "N2"))) ")" )))) ; theorem :: MATRIXJ1:40 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "F")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "M")) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" )) & (Bool (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "M")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "F")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" )) ")" ))))) ; theorem :: MATRIXJ1:41 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G")) ")" ) "," (Set (Var "a")) ")" ))))))) ; theorem :: MATRIXJ1:42 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "G")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set "(" (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "G")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "G")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k8_matrix_2 :::"DelLine"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "a")) ")" ))))))) ; theorem :: MATRIXJ1:43 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set ($#k7_matrix_2 :::"DelCol"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k7_matrix_2 :::"DelCol"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G")) ")" ) "," (Set (Var "a")) ")" ))))))) ; theorem :: MATRIXJ1:44 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k1_matrix_1 :::"width"::: ) (Set (Var "A")) ")" )))) "holds" (Bool (Set ($#k7_matrix_2 :::"DelCol"::: ) "(" (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "G")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k11_matrixj1 :::"Width"::: ) (Set (Var "G")) ")" ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "G")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k7_matrix_2 :::"DelCol"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "a")) ")" ))))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); attr "F" is :::"Square-Matrix-yielding"::: means :: MATRIXJ1:def 6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F"))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," "D"))); end; :: deftheorem defines :::"Square-Matrix-yielding"::: MATRIXJ1:def 6 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_matrixj1 :::"Square-Matrix-yielding"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D"))))) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#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"::: ) ($#v2_matrixj1 :::"Square-Matrix-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v2_matrixj1 :::"Square-Matrix-yielding"::: ) -> ($#v1_matrixj1 :::"Matrix-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode FinSequence_of_Square-Matrix of "D" is ($#v2_matrixj1 :::"Square-Matrix-yielding"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); mode FinSequence_of_Square-Matrix of "K" is ($#v2_matrixj1 :::"Square-Matrix-yielding"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ); end; theorem :: MATRIXJ1:45 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "D")))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "D")); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "S" :::"."::: "x" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" "S" ($#k2_matrixj1 :::"."::: ) "x" ")" )) "," "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S1", "S2" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "D")); :: original: :::"^"::: redefine func "S1" :::"^"::: "S2" -> ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"M1":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n", "m" be ($#m1_hidden :::"Nat":::); let "M1" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "D")); let "M2" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "m")) "," (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"M1" "," "M2":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" "D"; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "S" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "D")); :: original: :::"|"::: redefine func "S" :::"|"::: "n" -> ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" "D"; :: original: :::"/^"::: redefine func "S" :::"/^"::: "n" -> ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" "D"; end; theorem :: MATRIXJ1:46 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "D")) "holds" (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "S")))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "S" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "D")); :: original: :::"block_diagonal"::: redefine func :::"block_diagonal"::: "(" "S" "," "d" ")" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) "S" ")" )) "," "D"; end; theorem :: MATRIXJ1:47 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 "R")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k9_matrix_2 :::"Deleting"::: ) "(" (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k16_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k16_matrixj1 :::"*>"::: ) ) ($#k15_matrixj1 :::"^"::: ) (Set (Var "R")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k9_matrix_2 :::"Deleting"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ($#k3_matrixj1 :::"^"::: ) (Set (Var "R")) ")" ) "," (Set (Var "a")) ")" ))))))) ; theorem :: MATRIXJ1:48 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"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 "R")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k9_matrix_2 :::"Deleting"::: ) "(" (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "R")) ($#k15_matrixj1 :::"^"::: ) (Set ($#k16_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k16_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) "," (Set "(" (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_matrixj1 :::"Len"::: ) (Set (Var "R")) ")" ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "R")) ($#k3_matrixj1 :::"^"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" ($#k9_matrix_2 :::"Deleting"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) "," (Set (Var "a")) ")" ))))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "R" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "K")); func :::"Det"::: "R" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "K" means :: MATRIXJ1:def 7 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "R")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" "R" ($#k14_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Det"::: MATRIXJ1:def 7 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k21_matrixj1 :::"Det"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "R")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" (Set (Var "R")) ($#k14_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "R" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "K")); :: original: :::"Det"::: redefine func :::"Det"::: "R" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "R" ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; theorem :: MATRIXJ1:49 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "N")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool (Set ($#k22_matrixj1 :::"Det"::: ) (Set ($#k16_matrixj1 :::"<*"::: ) (Set (Var "N")) ($#k16_matrixj1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "N")) ")" ) ($#k4_matrix_2 :::"*>"::: ) ))))) ; theorem :: MATRIXJ1:50 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k22_matrixj1 :::"Det"::: ) (Set "(" (Set (Var "R1")) ($#k15_matrixj1 :::"^"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k22_matrixj1 :::"Det"::: ) (Set (Var "R1")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k22_matrixj1 :::"Det"::: ) (Set (Var "R2")) ")" ))))) ; theorem :: MATRIXJ1:51 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k22_matrixj1 :::"Det"::: ) (Set "(" (Set (Var "R")) ($#k18_matrixj1 :::"|"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k22_matrixj1 :::"Det"::: ) (Set (Var "R")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n"))))))) ; theorem :: MATRIXJ1:52 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "N")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) (Bool "for" (Set (Var "N1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "m")) "," (Set (Var "K")) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k17_matrixj1 :::"<*"::: ) (Set (Var "N")) "," (Set (Var "N1")) ($#k17_matrixj1 :::"*>"::: ) ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "N")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k12_matrix_3 :::"Det"::: ) (Set (Var "N1")) ")" ))))))) ; theorem :: MATRIXJ1:53 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "R")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" ($#k22_matrixj1 :::"Det"::: ) (Set (Var "R")) ")" ))))) ; theorem :: MATRIXJ1:54 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "N")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A1")))) & (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A1")) "," (Set (Var "A2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: MATRIXJ1:55 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "G"))) ($#r1_hidden :::"<>"::: ) (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "G"))))) "holds" (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "G")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ))) "holds" (Bool (Set ($#k12_matrix_3 :::"Det"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"1."::: "(" "K" "," "f" ")" -> ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" "K" means :: MATRIXJ1:def 8 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k14_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" "K" "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"1."::: MATRIXJ1:def 8 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "f")) ")" )) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k14_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) ")" ) ")" )))); theorem :: MATRIXJ1:56 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set "(" ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set "(" ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: MATRIXJ1:57 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "i")) ($#k4_matrix_2 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k16_matrixj1 :::"<*"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "i")) ")" ")" ) ($#k16_matrixj1 :::"*>"::: ) )))) ; theorem :: MATRIXJ1:58 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "f")) ")" ")" ) ($#k15_matrixj1 :::"^"::: ) (Set "(" ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "g")) ")" ")" ))))) ; theorem :: MATRIXJ1:59 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "f")) ")" ")" ) ($#k18_matrixj1 :::"|"::: ) (Set (Var "n"))))))) ; theorem :: MATRIXJ1:60 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k17_matrixj1 :::"<*"::: ) (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "j")) ")" ")" ) ($#k17_matrixj1 :::"*>"::: ) ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ")" )))) ; theorem :: MATRIXJ1:61 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" ($#k23_matrixj1 :::"1."::: ) "(" (Set (Var "K")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_matrix_1 :::"1."::: ) "(" (Set (Var "K")) "," (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")) ")" ) ")" )))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "G" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "K")); let "p" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); func :::"mlt"::: "(" "p" "," "G" ")" -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "K" means :: MATRIXJ1:def 9 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "G")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k2_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_matrix_3 :::"*"::: ) (Set "(" "G" ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"mlt"::: MATRIXJ1:def 9 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k24_matrixj1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "G")) ")" )) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_matrix_3 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))))); registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "R" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "K")); let "p" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "K")); cluster (Set ($#k24_matrixj1 :::"mlt"::: ) "(" "p" "," "R" ")" ) -> ($#v2_matrixj1 :::"Square-Matrix-yielding"::: ) ; end; theorem :: MATRIXJ1:62 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set "(" ($#k24_matrixj1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "G")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "G")))) & (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set "(" ($#k24_matrixj1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "G")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "G")))) ")" )))) ; theorem :: MATRIXJ1:63 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "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 (Set ($#k24_matrixj1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k4_matrixj1 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k6_matrix_3 :::"*"::: ) (Set (Var "A")) ")" ) ($#k4_matrixj1 :::"*>"::: ) ))))) ; theorem :: MATRIXJ1:64 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G")) "," (Set (Var "G1")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k24_matrixj1 :::"mlt"::: ) "(" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "G")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k24_matrixj1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "G")) ")" ")" ) ($#k3_matrixj1 :::"^"::: ) (Set "(" ($#k24_matrixj1 :::"mlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "G1")) ")" ")" )))))) ; theorem :: MATRIXJ1:65 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "G")) "," (Set (Var "a1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" ($#k24_matrixj1 :::"mlt"::: ) "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) "," (Set (Var "G")) ")" ")" ) "," (Set "(" (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "a1")) ")" ) ")" ))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "G1", "G2" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "K")); func "G1" :::"(+)"::: "G2" -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "K" means :: MATRIXJ1:def 10 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "G1")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k2_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "G1" ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" "G2" ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(+)"::: MATRIXJ1:def 10 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k25_matrixj1 :::"(+)"::: ) (Set (Var "G2")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G1")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "G2")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))); registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "R" be ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Const "K")); let "G" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "K")); cluster (Set "R" ($#k25_matrixj1 :::"(+)"::: ) "G") -> ($#v2_matrixj1 :::"Square-Matrix-yielding"::: ) ; end; theorem :: MATRIXJ1:66 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set "(" (Set (Var "G1")) ($#k25_matrixj1 :::"(+)"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "G1")))) & (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set "(" (Set (Var "G1")) ($#k25_matrixj1 :::"(+)"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "G1")))) ")" ))) ; theorem :: MATRIXJ1:67 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G")) "," (Set (Var "G9")) "," (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G9"))))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G1")) ")" ) ($#k25_matrixj1 :::"(+)"::: ) (Set "(" (Set (Var "G9")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k25_matrixj1 :::"(+)"::: ) (Set (Var "G9")) ")" ) ($#k3_matrixj1 :::"^"::: ) (Set "(" (Set (Var "G1")) ($#k25_matrixj1 :::"(+)"::: ) (Set (Var "G2")) ")" ))))) ; theorem :: MATRIXJ1:68 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k25_matrixj1 :::"(+)"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" (Set (Var "A")) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k2_matrixj1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k4_matrixj1 :::"*>"::: ) ))))) ; theorem :: MATRIXJ1:69 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A1")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k25_matrixj1 :::"(+)"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A2")) ($#k4_matrixj1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" (Set (Var "A1")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "A2")) ")" ) ($#k4_matrixj1 :::"*>"::: ) )))) ; theorem :: MATRIXJ1:70 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A1")) "," (Set (Var "B1")) ($#k5_matrixj1 :::"*>"::: ) ) ($#k25_matrixj1 :::"(+)"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A2")) "," (Set (Var "B2")) ($#k5_matrixj1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set "(" (Set (Var "A1")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "A2")) ")" ) "," (Set "(" (Set (Var "B1")) ($#k3_matrix_3 :::"+"::: ) (Set (Var "B2")) ")" ) ($#k5_matrixj1 :::"*>"::: ) )))) ; theorem :: MATRIXJ1:71 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B1")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B2")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B1")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "B2"))))) "holds" (Bool (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A1")) "," (Set (Var "A2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set (Var "a1")) ")" ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "B1")) "," (Set (Var "B2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set (Var "a2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A1")) "," (Set (Var "A2")) ($#k5_matrixj1 :::"*>"::: ) ) ($#k25_matrixj1 :::"(+)"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "B1")) "," (Set (Var "B2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ")" ))))) ; theorem :: MATRIXJ1:72 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "R2")))) & (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "R2"))))) "holds" (Bool (Set (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "R1")) "," (Set (Var "a1")) ")" ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "R2")) "," (Set (Var "a2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "R1")) ($#k25_matrixj1 :::"(+)"::: ) (Set (Var "R2")) ")" ) "," (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ")" ))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "G1", "G2" be ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Const "K")); func "G1" :::"(#)"::: "G2" -> ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" "K" means :: MATRIXJ1:def 11 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "G1")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k2_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "G1" ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" "G2" ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: MATRIXJ1:def 11 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k26_matrixj1 :::"(#)"::: ) (Set (Var "G2")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G1")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G1")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" (Set (Var "G2")) ($#k2_matrixj1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" ))); theorem :: MATRIXJ1:73 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "G2"))))) "holds" (Bool "(" (Bool (Set ($#k10_matrixj1 :::"Len"::: ) (Set "(" (Set (Var "G1")) ($#k26_matrixj1 :::"(#)"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "G1")))) & (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set "(" (Set (Var "G1")) ($#k26_matrixj1 :::"(#)"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "G2")))) ")" ))) ; theorem :: MATRIXJ1:74 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "G")) "," (Set (Var "G9")) "," (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G9"))))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G1")) ")" ) ($#k26_matrixj1 :::"(#)"::: ) (Set "(" (Set (Var "G9")) ($#k3_matrixj1 :::"^"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k26_matrixj1 :::"(#)"::: ) (Set (Var "G9")) ")" ) ($#k3_matrixj1 :::"^"::: ) (Set "(" (Set (Var "G1")) ($#k26_matrixj1 :::"(#)"::: ) (Set (Var "G2")) ")" ))))) ; theorem :: MATRIXJ1:75 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence_of_Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k26_matrixj1 :::"(#)"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" (Set (Var "A")) ($#k4_matrix_3 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k2_matrixj1 :::"."::: ) (Num 1) ")" ) ")" ) ($#k4_matrixj1 :::"*>"::: ) ))))) ; theorem :: MATRIXJ1:76 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A1")) ($#k4_matrixj1 :::"*>"::: ) ) ($#k26_matrixj1 :::"(#)"::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set (Var "A2")) ($#k4_matrixj1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrixj1 :::"<*"::: ) (Set "(" (Set (Var "A1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "A2")) ")" ) ($#k4_matrixj1 :::"*>"::: ) )))) ; theorem :: MATRIXJ1:77 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A1")) "," (Set (Var "B1")) ($#k5_matrixj1 :::"*>"::: ) ) ($#k26_matrixj1 :::"(#)"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A2")) "," (Set (Var "B2")) ($#k5_matrixj1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set "(" (Set (Var "A1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "A2")) ")" ) "," (Set "(" (Set (Var "B1")) ($#k4_matrix_3 :::"*"::: ) (Set (Var "B2")) ")" ) ($#k5_matrixj1 :::"*>"::: ) )))) ; theorem :: MATRIXJ1:78 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B1")))) & (Bool (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "B2"))))) "holds" (Bool (Set (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A1")) "," (Set (Var "A2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "B1")) "," (Set (Var "B2")) ($#k5_matrixj1 :::"*>"::: ) ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "A1")) "," (Set (Var "A2")) ($#k5_matrixj1 :::"*>"::: ) ) ($#k26_matrixj1 :::"(#)"::: ) (Set ($#k5_matrixj1 :::"<*"::: ) (Set (Var "B1")) "," (Set (Var "B2")) ($#k5_matrixj1 :::"*>"::: ) ) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" )))) ; theorem :: MATRIXJ1:79 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_1 :::"FinSequence_of_Square-Matrix":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k11_matrixj1 :::"Width"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k10_matrixj1 :::"Len"::: ) (Set (Var "R2"))))) "holds" (Bool (Set (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "R1")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ")" ) ($#k4_matrix_3 :::"*"::: ) (Set "(" ($#k20_matrixj1 :::"block_diagonal"::: ) "(" (Set (Var "R2")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_matrixj1 :::"block_diagonal"::: ) "(" (Set "(" (Set (Var "R1")) ($#k26_matrixj1 :::"(#)"::: ) (Set (Var "R2")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" )))) ;