Loading theory "DL_Missing_List" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "DL_Rank") Loading theory "DL_Missing_Finite_Set" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "DL_Deep_Model") ### theory "DL_Missing_Finite_Set" ### 0.148s elapsed time, 0.348s cpu time, 0.000s GC time Loading theory "DL_Missing_Sublist" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "Tensor_Matricization") Found termination order: "(\p. length (snd p)) <*mlex*> {}" ### theory "DL_Missing_List" ### 0.264s elapsed time, 0.580s cpu time, 0.000s GC time Loading theory "PP_More_List2" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "PP_More_MPoly" via "PP_MPoly" via "PP_Poly_Mapping") Found termination order: "(\p. size (snd p)) <*mlex*> {}" ### theory "PP_More_List2" ### 0.318s elapsed time, 0.632s cpu time, 0.000s GC time Loading theory "PP_Poly_Mapping" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "PP_More_MPoly" via "PP_MPoly") ### theory "DL_Missing_Sublist" ### 0.428s elapsed time, 0.856s cpu time, 0.000s GC time Loading theory "Tensor" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "Tensor_Rank" via "Tensor_Unit_Vec" via "Tensor_Product" via "Tensor_Scalar_Mult" via "Tensor_Plus") Proofs for inductive predicate(s) "valid_index" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Missing patterns in function definition: ### \v va b. lookup_base (v # va) b [] = undefined ### \b v va. lookup_base [] b (v # va) = undefined class zero = type + fixes zero :: "'a" Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" class monoid_add = semigroup_add + zero + assumes "add_0_left": "\a. (0::'a) + a = a" and "add_0_right": "\a. a + (0::'a) = a" Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" class comm_monoid_add = ab_semigroup_add + monoid_add + assumes "add_0": "\a. (0::'a) + a = a" ### theory "Tensor" ### 0.647s elapsed time, 1.292s cpu time, 0.000s GC time Loading theory "Tensor_Subtensor" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "Tensor_Rank" via "Tensor_Unit_Vec" via "Tensor_Product" via "Tensor_Scalar_Mult" via "Tensor_Plus") class group_add = cancel_semigroup_add + minus + monoid_add + uminus + assumes "left_minus": "\a. - a + a = (0::'a)" assumes "add_uminus_conv_diff": "\a b. a + - b = a - b" class mult_zero = times + zero + assumes "mult_zero_left": "\a. (0::'a) * a = (0::'a)" assumes "mult_zero_right": "\a. a * (0::'a) = (0::'a)" ### theory "Tensor_Subtensor" ### 0.199s elapsed time, 0.392s cpu time, 0.000s GC time Loading theory "Tensor_Plus" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "Tensor_Rank" via "Tensor_Unit_Vec" via "Tensor_Product" via "Tensor_Scalar_Mult") instantiation poly_mapping :: (type, zero) zero zero_poly_mapping == zero_class.zero :: 'a \\<^sub>0 'b instantiation poly_mapping :: (type, monoid_add) monoid_add plus_poly_mapping == plus :: ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b instantiation poly_mapping :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add minus_poly_mapping == minus :: ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b instantiation poly_mapping :: (type, ab_group_add) ab_group_add uminus_poly_mapping == uminus :: ('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b instantiation tensor :: (semigroup_add) plus plus_tensor == plus :: 'a tensor \ 'a tensor \ 'a tensor instantiation poly_mapping :: (zero, zero_neq_one) zero_neq_one one_poly_mapping == one_class.one :: 'a \\<^sub>0 'b instantiation poly_mapping :: (monoid_add, semiring_0) semiring_0 times_poly_mapping == times :: ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b ### theory "Tensor_Plus" ### 0.282s elapsed time, 0.564s cpu time, 0.000s GC time Loading theory "Tensor_Scalar_Mult" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "Tensor_Rank" via "Tensor_Unit_Vec" via "Tensor_Product") instantiation poly_mapping :: (linorder, {zero,linorder}) linorder less_eq_poly_mapping == less_eq :: ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ bool less_poly_mapping == less :: ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ bool ### theory "Tensor_Scalar_Mult" ### 0.307s elapsed time, 0.588s cpu time, 0.284s GC time Loading theory "Tensor_Product" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "Tensor_Rank" via "Tensor_Unit_Vec") instantiation tensor :: (ring) semigroup_mult times_tensor == times :: 'a tensor \ 'a tensor \ 'a tensor instantiation tensor :: (ring_1) monoid_mult one_tensor == one_class.one :: 'a tensor ### theory "Tensor_Product" ### 0.185s elapsed time, 0.368s cpu time, 0.000s GC time Loading theory "Tensor_Unit_Vec" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "Tensor_Rank") ### theory "Tensor_Unit_Vec" ### 0.112s elapsed time, 0.224s cpu time, 0.000s GC time Loading theory "Tensor_Rank" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank") instantiation poly_mapping :: (type, zero) size size_poly_mapping == size :: ('a \\<^sub>0 'b) \ nat ### theory "PP_Poly_Mapping" ### 1.802s elapsed time, 3.572s cpu time, 0.284s GC time Loading theory "PP_MPoly" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "PP_More_MPoly") Proofs for inductive predicate(s) "cprank_max1" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Proofs for inductive predicate(s) "cprank_max" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Tensor_Rank" ### 0.196s elapsed time, 0.392s cpu time, 0.000s GC time Loading theory "Lebesgue_Functional" (required by "DL_Fundamental_Theorem_Network_Capacity" via "Lebesgue_Zero_Set") ### Generation of a parametrized correspondence relation failed. ### Reason: No relator for the type "PP_Poly_Mapping.poly_mapping" found. instantiation mpoly :: (zero) zero zero_mpoly == zero_class.zero :: 'a mpoly instantiation mpoly :: (monoid_add) monoid_add plus_mpoly == plus :: 'a mpoly \ 'a mpoly \ 'a mpoly ### theory "Lebesgue_Functional" ### 0.277s elapsed time, 0.552s cpu time, 0.000s GC time Loading theory "DL_Missing_Vector_Space" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "DL_Rank" via "DL_Missing_VS_Connect") instantiation mpoly :: (cancel_comm_monoid_add) cancel_comm_monoid_add minus_mpoly == minus :: 'a mpoly \ 'a mpoly \ 'a mpoly instantiation mpoly :: (ab_group_add) ab_group_add uminus_mpoly == uminus :: 'a mpoly \ 'a mpoly instantiation mpoly :: (zero_neq_one) zero_neq_one one_mpoly == one_class.one :: 'a mpoly instantiation mpoly :: (semiring_0) semiring_0 times_mpoly == times :: 'a mpoly \ 'a mpoly \ 'a mpoly ### Ambiguous input (line 468 of "~~/afp/thys/Deep_Learning/PP_MPoly.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("\<^fixed>div" ("_position" x) ("_position" y)) ### ("_The" ("_position" q') ### ("\<^const>HOL.Ex_binder" ### ("_idts" ("_position" a) ("_idts" ("_position" q) ("_position" r))) ### ("\<^const>HOL.conj" ### ("_applC" ("_position" pseudo_divmod_rel) ### ("_cargs" ("_position" a) ### ("_cargs" ("_position" x) ### ("_cargs" ("_position" y) ### ("_cargs" ("_position" q) ("_position" r)))))) ### ("\<^const>HOL.eq" ("_position" q') ### ("_applC" ("_position" smult) ### ("_cargs" ("_applC" ("_position" inverse) ("_position" a)) ### ("_position" q))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Rings.divide_class.divide" ("_position" x) ("_position" y)) ### ("_The" ("_position" q') ### ("\<^const>HOL.Ex_binder" ### ("_idts" ("_position" a) ("_idts" ("_position" q) ("_position" r))) ### ("\<^const>HOL.conj" ### ("_applC" ("_position" pseudo_divmod_rel) ### ("_cargs" ("_position" a) ### ("_cargs" ("_position" x) ### ("_cargs" ("_position" y) ### ("_cargs" ("_position" q) ("_position" r)))))) ### ("\<^const>HOL.eq" ("_position" q') ### ("_applC" ("_position" smult) ### ("_cargs" ("_applC" ("_position" inverse) ("_position" a)) ### ("_position" q))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 472 of "~~/afp/thys/Deep_Learning/PP_MPoly.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("\<^fixed>mod" ("_position" x) ("_position" y)) ### ("_The" ("_position" r') ### ("\<^const>HOL.Ex_binder" ### ("_idts" ("_position" a) ("_idts" ("_position" q) ("_position" r))) ### ("\<^const>HOL.conj" ### ("_applC" ("_position" pseudo_divmod_rel) ### ("_cargs" ("_position" a) ### ("_cargs" ("_position" x) ### ("_cargs" ("_position" y) ### ("_cargs" ("_position" q) ("_position" r)))))) ### ("\<^const>HOL.eq" ("_position" r') ### ("_applC" ("_position" smult) ### ("_cargs" ("_applC" ("_position" inverse) ("_position" a)) ### ("_position" r))))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Rings.modulo_class.modulo" ("_position" x) ("_position" y)) ### ("_The" ("_position" r') ### ("\<^const>HOL.Ex_binder" ### ("_idts" ("_position" a) ("_idts" ("_position" q) ("_position" r))) ### ("\<^const>HOL.conj" ### ("_applC" ("_position" pseudo_divmod_rel) ### ("_cargs" ("_position" a) ### ("_cargs" ("_position" x) ### ("_cargs" ("_position" y) ### ("_cargs" ("_position" q) ("_position" r)))))) ### ("\<^const>HOL.eq" ("_position" r') ### ("_applC" ("_position" smult) ### ("_cargs" ("_applC" ("_position" inverse) ("_position" a)) ### ("_position" r))))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 476 of "~~/afp/thys/Deep_Learning/PP_MPoly.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q))) ### ("_tuple" ### ("\<^const>Rings.divide_class.divide" ("_position" p) ("_position" q)) ### ("_tuple_arg" ### ("\<^const>PP_MPoly.mod" ("_position" p) ("_position" q)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q))) ### ("_tuple" ("\<^const>PP_MPoly.div" ("_position" p) ("_position" q)) ### ("_tuple_arg" ### ("\<^const>PP_MPoly.mod" ("_position" p) ("_position" q)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q))) ### ("_tuple" ### ("\<^const>Rings.divide_class.divide" ("_position" p) ("_position" q)) ### ("_tuple_arg" ### ("\<^const>Rings.modulo_class.modulo" ("_position" p) ### ("_position" q)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q))) ### ("_tuple" ("\<^const>PP_MPoly.div" ("_position" p) ("_position" q)) ### ("_tuple_arg" ### ("\<^const>Rings.modulo_class.modulo" ("_position" p) ### ("_position" q)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 479 of "~~/afp/thys/Deep_Learning/PP_MPoly.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>PP_MPoly.div" ("_position" p) ("_position" q)) ### ("_applC" ("_position" fst) ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Rings.divide_class.divide" ("_position" p) ("_position" q)) ### ("_applC" ("_position" fst) ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 483 of "~~/afp/thys/Deep_Learning/PP_MPoly.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>PP_MPoly.mod" ("_position" p) ("_position" q)) ### ("_applC" ("_position" snd) ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Rings.modulo_class.modulo" ("_position" p) ("_position" q)) ### ("_applC" ("_position" snd) ### ("_applC" ("_position" divmod) ### ("_cargs" ("_position" p) ("_position" q)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### theory "PP_MPoly" ### 0.853s elapsed time, 1.704s cpu time, 0.000s GC time Loading theory "PP_More_MPoly" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly") ### theory "DL_Missing_Vector_Space" ### 0.600s elapsed time, 1.200s cpu time, 0.000s GC time Loading theory "DL_Flatten_Matrix" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "DL_Deep_Model" via "DL_Network") ### theory "PP_More_MPoly" ### 0.500s elapsed time, 1.000s cpu time, 0.000s GC time Loading theory "PP_Univariate" (required by "DL_Fundamental_Theorem_Network_Capacity" via "Lebesgue_Zero_Set") ### theory "DL_Flatten_Matrix" ### 0.593s elapsed time, 1.188s cpu time, 0.000s GC time Loading theory "DL_Missing_Matrix" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "DL_Deep_Model" via "DL_Network") ### theory "DL_Missing_Matrix" ### 0.166s elapsed time, 0.332s cpu time, 0.000s GC time Loading theory "DL_Concrete_Matrices" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "DL_Deep_Model") ### theory "PP_Univariate" ### 0.768s elapsed time, 1.528s cpu time, 0.000s GC time Loading theory "Lebesgue_Zero_Set" (required by "DL_Fundamental_Theorem_Network_Capacity") ### theory "DL_Concrete_Matrices" ### 0.655s elapsed time, 1.300s cpu time, 0.000s GC time Loading theory "DL_Network" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly" via "DL_Deep_Model") ### theory "Lebesgue_Zero_Set" ### 0.852s elapsed time, 1.696s cpu time, 0.000s GC time Loading theory "DL_Submatrix" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank") ### theory "DL_Submatrix" ### 0.314s elapsed time, 0.628s cpu time, 0.000s GC time Loading theory "Tensor_Matricization" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank") ### Missing patterns in function definition: ### \v va. digit_decode (v # va) [] = undefined ### \v va. digit_decode [] (v # va) = undefined Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" ### theory "Tensor_Matricization" ### 1.313s elapsed time, 2.584s cpu time, 0.652s GC time Loading theory "DL_Missing_VS_Connect" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank" via "DL_Rank") Found termination order: "size <*mlex*> {}" Found termination order: "size <*mlex*> {}" Found termination order: "size <*mlex*> {}" Proofs for inductive predicate(s) "valid_net" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "(\p. size (fst p)) <*mlex*> {}" Found termination order: "size <*mlex*> {}" ### theory "DL_Missing_VS_Connect" ### 1.232s elapsed time, 2.460s cpu time, 0.000s GC time Loading theory "DL_Rank" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Rank_CP_Rank") Found termination order: "(\p. size (fst p)) <*mlex*> {}" Found termination order: "size <*mlex*> {}" ### theory "DL_Network" ### 3.709s elapsed time, 7.364s cpu time, 0.652s GC time Loading theory "DL_Shallow_Model" (required by "DL_Fundamental_Theorem_Network_Capacity") Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" ### theory "DL_Shallow_Model" ### 0.467s elapsed time, 0.932s cpu time, 0.000s GC time Loading theory "DL_Deep_Model" (required by "DL_Fundamental_Theorem_Network_Capacity" via "DL_Deep_Model_Poly") Found termination order: "case_sum (\p. size_list size (snd (snd p))) (\p. size_list size (snd p)) <*mlex*> case_sum (\x. Suc 0) (\x. 0) <*mlex*> {}" Found termination order: "case_sum (\p. size_list size (snd (snd p))) (\p. size_list size (snd p)) <*mlex*> case_sum (\x. Suc 0) (\x. 0) <*mlex*> {}" ### Ambiguous input (line 275 of "~~/afp/thys/Deep_Learning/DL_Deep_Model.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Tensor_Product.tensor_prod_otimes" ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))) ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j)))) ### ("_applC" ("_position" tensor_from_lookup) ### ("_cargs" ("_list" ("_args" ("_position" M) ("_position" M))) ### ("_lambda" ("_position" is) ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" is) ### ("_list" ("_args" ("_position" j) ("_position" j)))) ### ("\<^const>Groups.one_class.one") ### ("\<^const>Groups.zero_class.zero"))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Group.monoid.mult_indexed" ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))) ### ("_indexdefault") ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j)))) ### ("_applC" ("_position" tensor_from_lookup) ### ("_cargs" ("_list" ("_args" ("_position" M) ("_position" M))) ### ("_lambda" ("_position" is) ### ("\<^const>HOL.If" ### ("\<^const>HOL.eq" ("_position" is) ### ("_list" ("_args" ("_position" j) ("_position" j)))) ### ("\<^const>Groups.one_class.one") ### ("\<^const>Groups.zero_class.zero"))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 294 of "~~/afp/thys/Deep_Learning/DL_Deep_Model.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness') ### ("_cargs" ("_position" r0) ("_list" ("_position" M))))) ### ("_position" j)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" j) ("_position" M)) ### ("\<^const>Tensor_Product.tensor_prod_otimes" ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))) ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j)))) ### ("_applC" ("_position" tensor0) ### ("_list" ("_args" ("_position" M) ("_position" M))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness') ### ("_cargs" ("_position" r0) ("_list" ("_position" M))))) ### ("_position" j)) ### ("\<^const>HOL.If" ### ("\<^const>Orderings.ord_class.less" ("_position" j) ("_position" M)) ### ("\<^const>Group.monoid.mult_indexed" ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))) ### ("_indexdefault") ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j)))) ### ("_applC" ("_position" tensor0) ### ("_list" ("_args" ("_position" M) ("_position" M))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. locale deep_model_correct_params = fixes rs :: "nat list" assumes "deep_model_correct_params rs" locale deep_model_correct_params_y = fixes rs :: "nat list" and y :: "nat" assumes "deep_model_correct_params_y rs y" ### theory "DL_Deep_Model" ### 3.783s elapsed time, 7.484s cpu time, 0.936s GC time Loading theory "DL_Deep_Model_Poly" (required by "DL_Fundamental_Theorem_Network_Capacity") locale deep_model_correct_params_y = fixes rs :: "nat list" and y :: "nat" assumes "deep_model_correct_params_y rs y" ### theory "DL_Deep_Model_Poly" ### 0.862s elapsed time, 1.724s cpu time, 0.000s GC time ### Legacy feature! Old 'def' command -- use 'define' instead ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### theory "DL_Rank" ### 12.708s elapsed time, 25.164s cpu time, 1.800s GC time Loading theory "DL_Rank_CP_Rank" (required by "DL_Fundamental_Theorem_Network_Capacity") ### theory "DL_Rank_CP_Rank" ### 2.166s elapsed time, 4.292s cpu time, 0.276s GC time Loading theory "DL_Rank_Submatrix" (required by "DL_Fundamental_Theorem_Network_Capacity") ### theory "DL_Rank_Submatrix" ### 1.841s elapsed time, 3.668s cpu time, 0.080s GC time Loading theory "DL_Fundamental_Theorem_Network_Capacity" ### Legacy feature! Old 'def' command -- use 'define' instead MPoly (mapping_of ?x) = ?x ?y \ UNIV \ mapping_of (MPoly ?y) = ?y (mapping_of ?x = mapping_of ?y) = (?x = ?y) \?x \ UNIV; ?y \ UNIV\ \ (MPoly ?x = MPoly ?y) = (?x = ?y) \?y \ UNIV; \x. ?P (mapping_of x)\ \ ?P ?y (\y. y \ UNIV \ ?P (MPoly y)) \ ?P ?x \?y \ UNIV; \x. ?y = mapping_of x \ ?P\ \ ?P (\y. \?x = MPoly y; y \ UNIV\ \ ?P) \ ?P locale deep_model_correct_params_y = fixes rs :: "nat list" and y :: "nat" assumes "deep_model_correct_params_y rs y" ### theory "DL_Fundamental_Theorem_Network_Capacity" ### 3.371s elapsed time, 6.712s cpu time, 0.196s GC time ### Legacy feature! Old 'def' command -- use 'define' instead ### Metis: Unused theorems: "List.drop_map" ### Metis: Unused theorems: "List.take_map" ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ambiguous input (line 654 of "~~/afp/thys/Deep_Learning/DL_Deep_Model.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Tensor.lookup) ### ("_cargs" ### ("\<^const>Group.monoid.mult_indexed" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero")) ### ("_indexdefault") ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" is))) ### ("\<^const>HOL.If" ### ("_applC" ("_position" ?cond) ### ("_cargs" ("_position" is) ("_position" rs))) ### ("\<^const>Groups.one_class.one") ### ("\<^const>Groups.zero_class.zero")))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" Tensor.lookup) ### ("_cargs" ### ("\<^const>Tensor_Product.tensor_prod_otimes" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero"))) ### ("_position" is))) ### ("\<^const>HOL.If" ### ("_applC" ("_position" ?cond) ### ("_cargs" ("_position" is) ("_position" rs))) ### ("\<^const>Groups.one_class.one") ### ("\<^const>Groups.zero_class.zero")))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ambiguous input (line 677 of "~~/afp/thys/Deep_Learning/DL_Deep_Model.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness') ### ("_cargs" ### ("\<^const>List.nth" ("_position" rs) ### ("\<^const>Groups.one_class.one")) ### ("\<^const>List.list.Cons" ### ("\<^const>List.nth" ("_position" rs) ### ("_Numeral" ("_constify" ("_position" 2)))) ### ("_applC" ("_position" tl) ### ("_applC" ("_position" tl) ### ("_applC" ("_position" tl) ("_position" rs)))))))) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Group.monoid.mult_indexed" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero")) ### ("_indexdefault") ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness') ### ("_cargs" ### ("\<^const>List.nth" ("_position" rs) ### ("\<^const>Groups.one_class.one")) ### ("\<^const>List.list.Cons" ### ("\<^const>List.nth" ("_position" rs) ### ("_Numeral" ("_constify" ("_position" 2)))) ### ("_applC" ("_position" tl) ### ("_applC" ("_position" tl) ### ("_applC" ("_position" tl) ("_position" rs)))))))) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Tensor_Product.tensor_prod_otimes" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero")) ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" tensors_from_net) ### ("_applC" ("_position" witness_l) ### ("_applC" ("_position" tl) ("_position" rs)))) ### ("\<^const>Groups.zero_class.zero"))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Metis: Unused theorems: "Groups.ab_semigroup_mult_class.mult.commute" ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Ambiguous input (line 279 of "~~/afp/thys/Deep_Learning/DL_Deep_Model.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Tensor.valid_index" ("_position" is) ### ("_applC" ("_position" Tensor.dims) ### ("\<^const>Tensor_Product.tensor_prod_otimes" ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))) ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Tensor.valid_index" ("_position" is) ### ("_applC" ("_position" Tensor.dims) ### ("\<^const>Group.monoid.mult_indexed" ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))) ### ("_indexdefault") ### ("_applC" ("_position" unit_vec) ### ("_cargs" ("_position" M) ("_position" j))))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Metis: Unused theorems: "??.unknown", "??.unknown", "local.assms_3", "DL_Network.base_input_length", "DL_Network.dims_tensors_from_net", "DL_Missing_Matrix.vec_setI", "local.assms_4" ### Metis: Unused theorems: "??.unknown", "??.unknown", "DL_Network.base_input_length", "local.assms_4" ### Metis: Unused theorems: "??.unknown" ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Legacy feature! Old 'def' command -- use 'define' instead ### Metis: Unused theorems: "??.unknown", "Tensor.lookup_tensor_from_lookup", "Tensor.valid_index.Nil", "Groups.monoid_mult_class.mult.left_neutral" ### Metis: Unused theorems: "??.unknown", "Tensor.lookup_tensor_from_lookup", "Tensor.valid_index.Nil", "Groups.monoid_mult_class.mult.right_neutral" find_theorems "vectorspace.basis" found 10 theorem(s): VectorSpace.vectorspace.finite_basis_exists: \vectorspace ?K ?V; vectorspace.fin_dim ?K ?V\ \ \\. finite \ \ vectorspace.basis ?K ?V \ VectorSpace.vectorspace.dim_basis: \vectorspace ?K ?V; finite ?A; vectorspace.basis ?K ?V ?A\ \ vectorspace.dim ?K ?V = card ?A VectorSpace.vectorspace.max_li_is_basis: \vectorspace ?K ?V; maximal ?A (\S. S \ carrier ?V \ \ module.lin_dep ?K ?V S)\ \ vectorspace.basis ?K ?V ?A VectorSpace.vectorspace.min_gen_is_basis: \vectorspace ?K ?V; minimal ?A (\S. S \ carrier ?V \ module.span ?K ?V S = carrier ?V)\ \ vectorspace.basis ?K ?V ?A VectorSpace.vectorspace.basis_def: vectorspace ?K ?V \ vectorspace.basis ?K ?V ?A = (\ module.lin_dep ?K ?V ?A \ module.span ?K ?V ?A = carrier ?V \ ?A \ carrier ?V) VectorSpace.vectorspace.dim_gen_is_basis: \vectorspace ?K ?V; finite ?A; ?A \ carrier ?V; module.span ?K ?V ?A = carrier ?V; card ?A \ vectorspace.dim ?K ?V\ \ vectorspace.basis ?K ?V ?A Missing_VectorSpace.linear_map.linear_inj_image_is_basis: \linear_map ?K ?V ?W ?T; inj_on ?T (carrier ?V); ?T ` carrier ?V = carrier ?W; vectorspace.basis ?K ?V ?B; vectorspace.fin_dim ?K ?V\ \ vectorspace.basis ?K ?W (?T ` ?B) VectorSpace.vectorspace.dim_li_is_basis: \vectorspace ?K ?V; vectorspace.fin_dim ?K ?V; finite ?A; ?A \ carrier ?V; \ module.lin_dep ?K ?V ?A; vectorspace.dim ?K ?V \ card ?A\ \ vectorspace.basis ?K ?V ?A VectorSpace.vectorspace.basis_criterion: \vectorspace ?K ?V; finite ?A; ?A \ carrier ?V\ \ vectorspace.basis ?K ?V ?A = (\v. v \ carrier ?V \ (\!a. a \ ?A \\<^sub>E carrier ?K \ module.lincomb ?V a ?A = v)) Missing_VectorSpace.vectorspace.basis_swap: \vectorspace ?K ?V; finite ?E; ?u \ carrier ?V; ?u \ ?E; vectorspace.basis ?K ?V (insert ?u ?E); ?v \ carrier ?V; ?u \ module.span ?K ?V (insert ?v ?E)\ \ vectorspace.basis ?K ?V (insert ?v ?E) "(Gcd (coeffs (M [1::'b, (1::'b) + (1::'b), (1::'b) + (1::'b) + (1::'b)] 4 + M [(1::'b) + (1::'b), 0::'b, (1::'b) + (1::'b) + ((1::'b) + (1::'b))] 6 + M [(1::'b) + (1::'b), 0::'b, (1::'b) + (1::'b) + ((1::'b) + (1::'b)) + (1::'b)] 8)), sdiv (Gcd (coeffs (M [1::'b, (1::'b) + (1::'b), (1::'b) + (1::'b) + (1::'b)] 4 + M [(1::'b) + (1::'b), 0::'b, (1::'b) + (1::'b) + ((1::'b) + (1::'b))] 6 + M [(1::'b) + (1::'b), 0::'b, (1::'b) + (1::'b) + ((1::'b) + (1::'b)) + (1::'b)] 8))) (M [1::'b, (1::'b) + (1::'b), (1::'b) + (1::'b) + (1::'b)] 4 + M [(1::'b) + (1::'b), 0::'b, (1::'b) + (1::'b) + ((1::'b) + (1::'b))] 6 + M [(1::'b) + (1::'b), 0::'b, (1::'b) + (1::'b) + ((1::'b) + (1::'b)) + (1::'b)] 8))" :: "'a \ 'a mpoly" ### Ignoring duplicate rewrite rule: ### ?a1 + - ?b1 \ ?a1 - ?b1 isabelle document -c -o 'pdf' -n 'document' -t '' /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/document 2>&1 isabelle document -c -o 'pdf' -n 'outline' -t '/proof,/ML' /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/outline 2>&1 *** This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex) *** restricted \write18 enabled. *** entering extended mode *** LaTeX2e <2016/02/01> *** Babel <3.9q> and hyphenation patterns for 81 language(s) loaded. *** *** (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls *** Document Class: article 2014/09/29 v1.4h Standard LaTeX document class *** (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) *** (/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty) (./isabelle.sty *** (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory' *** Including comment 'isatagtheory' Including comment 'isadelimproof' *** Including comment 'isatagproof' Including comment 'isadelimML' *** Including comment 'isatagML' Including comment 'isadelimvisible' *** Including comment 'isatagvisible' Excluding comment 'isadeliminvisible' *** Excluding comment 'isataginvisible') (./isabelletags.sty *** Including comment 'isadelimproof' Excluding comment 'isatagproof' *** Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty *** ) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty *** (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg) *** (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def *** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty) *** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) *** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty *** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty *** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) *** (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) *** (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) *** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) *** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) *** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) *** (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) *** (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) *** *** Package hyperref Message: Driver (autodetected): hpdftex. *** *** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def *** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) *** No file root.aux. *** (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii *** [Loading MPS to PDF converter (version 2006.09.02).] *** ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty *** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) *** (/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd) *** *** LaTeX Warning: Citation `cohen2015' on page 1 undefined on input line 22. *** *** *** LaTeX Warning: Citation `bentkamp2016' on page 1 undefined on input line 22. *** *** *** Package hyperref Warning: old toc file detected, not used; run LaTeX again. *** *** (./session.tex (./Tensor.tex [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.m *** ap}] [2] [3]) (./Tensor_Subtensor.tex *** Overfull \hbox (3.79184pt too wide) in paragraph at lines 27--28 *** [][] \OT1/cmr/m/it/10 sub-ten-sor A i $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 ten *** sor[]from[]vec $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 tl $\OT1/cmr/m/n/10 ($\OT1/c *** mr/m/it/10 dims A$\OT1/cmr/m/n/10 )$$)$ $($\OT1/cmr/m/it/10 fixed[]length[]subl *** ist $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 vec A$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/ *** it/10 prod[]list *** [4] [5]) (./Tensor_Plus.tex [6] [7] [8]) (./Tensor_Scalar_Mult.tex [9]) *** (./Tensor_Product.tex [10] [11]) (./Tensor_Unit_Vec.tex [12]) *** (./Tensor_Rank.tex [13] [14]) (./DL_Missing_Vector_Space.tex) *** (./DL_Missing_VS_Connect.tex [15]) (./DL_Missing_List.tex [16]) (./DL_Rank.tex *** [17] [18] *** Overfull \hbox (98.24303pt too wide) in paragraph at lines 791--793 *** []\OT1/cmr/m/n/10.95 The the-o-rem "det non-zero $\OMS/cmsy/m/n/10.95 []!$ \OT *** 1/cmr/m/n/10.95 full rank" is prac-ti-cally proven in det[]0[]iff[]vec[]prod[]z *** ero[]field, *** [19] [20]) (./DL_Missing_Sublist.tex [21] [22] [23] [24]) *** (./Tensor_Matricization.tex [25] [26]) (./DL_Submatrix.tex) *** (./DL_Rank_CP_Rank.tex [27] *** Overfull \hbox (50.87773pt too wide) in paragraph at lines 15--16 *** [][]\OT1/cmr/bx/n/10 imports \OT1/cmr/m/it/10 Tensor[]Rank DL[]Rank Tensor[]Mat *** ricization DL[]Submatrix DL[]Missing[]Vector[]Space[] *** ) (./DL_Missing_Matrix.tex [28]) (./DL_Flatten_Matrix.tex [29]) *** (./DL_Network.tex *** Overfull \hbox (10.82027pt too wide) in paragraph at lines 16--17 *** [][]$\OML/cmm/m/it/10 :$$:$$=$\OT1/cmr/m/it/10 Jordan[]Normal[]Form$\OML/cmm/m/ *** it/10 =$\OT1/cmr/m/it/10 Matrix Tensor[]Unit[]Vec DL[]Flatten[]Matrix DL[]Missi *** ng[]List[] *** [30] [31] *** Overfull \hbox (19.21951pt too wide) in paragraph at lines 194--195 *** [][]\OT1/cmr/m/it/10 tensors[]from[]net $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Con *** v A m$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 mat[]tensorlist[]mult A $\OT1/cmr *** /m/n/10 ($\OT1/cmr/m/it/10 tensors[]from[]net m$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/ *** m/it/10 input[]sizes *** *** Overfull \hbox (35.87817pt too wide) in paragraph at lines 195--196 *** [][]\OT1/cmr/m/it/10 tensors[]from[]net $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Poo *** l m1 m2$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 component[]mult $\OT1/cmr/m/n/1 *** 0 ($\OT1/cmr/m/it/10 tensors[]from[]net m1$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/ *** 10 tensors[]from[]net *** [32] [33]) (./DL_Concrete_Matrices.tex [34] *** Overfull \hbox (28.67195pt too wide) in paragraph at lines 267--269 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 copy[]first[]matrix[]dim$\OT1/cmr/m *** /n/10 :$ \OT1/cmr/m/it/10 dim$[][]$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 copy[]f *** irst[]matrix nr nc$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 nr dim$[][]$ $\OT1/c *** mr/m/n/10 ($\OT1/cmr/m/it/10 copy[]first[]matrix *** ) (./DL_Missing_Finite_Set.tex [35]) (./DL_Deep_Model.tex [36] [37] [38] *** [39] [40] *** Overfull \hbox (5.51314pt too wide) in paragraph at lines 1414--1416 *** [][]\OT1/cmr/bx/n/10 definition \OT1/cmr/m/it/10 witness[]weights $\OT1/cmr/m/n *** /10 =$ $($\OT1/cmr/m/it/10 SOME ws$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 witness *** []l rs $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 insert[]weights $\OT1/cmr/m/n/10 ($ *** \OT1/cmr/m/it/10 deep[]model[]l *** *** Overfull \hbox (13.38652pt too wide) in paragraph at lines 1417--1419 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 witness[]weights$\OT1/cmr/m/n/10 :$ *** \OT1/cmr/m/it/10 witness[]l rs $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 insert[]wei *** ghts $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 deep[]model[]l rs$\OT1/cmr/m/n/10 )$ \ *** OT1/cmr/m/it/10 witness[]weights[] *** [41] *** Overfull \hbox (4.02184pt too wide) in paragraph at lines 2461--2463 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 witness[]submatrix$\OT1/cmr/m/n/10 *** :$ \OT1/cmr/m/it/10 sub-ma-trix Aw$ [] $ rows[]with[]1 rows[]with[]1 $\OT1/cmr/ *** m/n/10 =$ $\OT1/cmr/bx/n/10 1$$[][]$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 r^N[]h *** alf$\OT1/cmr/m/n/10 )$[] *** ) (./PP_More_List2.tex [42] [43] [44] [45] [46]) (./PP_Poly_Mapping.tex *** Overfull \hbox (2.79784pt too wide) in paragraph at lines 6--6 *** []\OT1/cmr/bx/n/14.4 Polynomial map-ping: com-bi-na-tion of al-most ev- *** *** Overfull \hbox (5.24034pt too wide) in paragraph at lines 29--29 *** []\OT1/cmr/bx/n/12 Preliminary: aux-il-iary op-er-a-tions for `al-most ev-ery-w *** here *** [47] [48] [49] [50] *** *** LaTeX Warning: Citation `Haftmann-Nipkow:2010:code' on page 51 undefined on inp *** ut line 828. *** *** [51] [52] *** Overfull \hbox (29.52538pt too wide) in paragraph at lines 1027--1029 *** [][]\OT1/cmr/bx/n/10 instantiation \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n *** /10 :$$:$ $($\OT1/cmr/m/it/10 type$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 cancel[ *** ]comm[]monoid[]add$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 cancel[]comm[]monoid[]ad *** d[] *** [53] [54] *** Overfull \hbox (1.37982pt too wide) in paragraph at lines 1683--1685 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 comm[]monoid[]add$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 *** comm[]semiring[]0$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 comm[]semiring[]0[] *** *** Overfull \hbox (60.346pt too wide) in paragraph at lines 1808--1810 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 comm[]monoid[]add$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 *** comm[]semiring[]0[]cancel$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 comm[]semiring[] *** 0[]cancel[] *** *** Overfull \hbox (1.37982pt too wide) in paragraph at lines 1864--1866 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 comm[]monoid[]add$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 *** comm[]semiring[]1$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 comm[]semiring[]1[] *** [55] [56] *** Overfull \hbox (52.64885pt too wide) in paragraph at lines 2447--2448 *** \OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 :$$:$ *** $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 ordered[]cancel[]comm[]monoid[]add$\OM *** L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 linorder$\OMS/cmsy/m/n/10 g$$\OML/cmm/m/it/10 *** ;$ \OT1/cmr/m/it/10 ring[]no[]zero[]divisors$\OT1/cmr/m/n/10 )$ *** *** Overfull \hbox (61.33768pt too wide) in paragraph at lines 2600--2602 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 ordered[]cancel[]comm[]monoid[]add *** $\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 linorder$\OMS/cmsy/m/n/10 g$$\OML/cmm/m/i *** t/10 ;$ \OT1/cmr/m/it/10 ring[]1[]no[]zero[]divisors$\OT1/cmr/m/n/10 )$ *** *** Overfull \hbox (8.25667pt too wide) in paragraph at lines 2618--2620 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 ordered[]cancel[]comm[]monoid[]add *** $\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 linorder$\OMS/cmsy/m/n/10 g$$\OML/cmm/m/i *** t/10 ;$ \OT1/cmr/m/it/10 idom$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 idom[] *** *** Overfull \hbox (68.70148pt too wide) in paragraph at lines 2763--2765 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 linorder$\OML/cmm/m/it/10 ;$ $\OMS/cmsy/m/n/10 f$\OT1/ *** cmr/m/it/10 ordered[]comm[]monoid[]add$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 ord *** ered[]ab[]semigroup[]add[]imp[]le$\OML/cmm/m/it/10 ;$ *** [57] *** Overfull \hbox (68.70148pt too wide) in paragraph at lines 2812--2814 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 linorder$\OML/cmm/m/it/10 ;$ $\OMS/cmsy/m/n/10 f$\OT1/ *** cmr/m/it/10 ordered[]comm[]monoid[]add$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 ord *** ered[]ab[]semigroup[]add[]imp[]le$\OML/cmm/m/it/10 ;$ *** *** Overfull \hbox (68.70148pt too wide) in paragraph at lines 2830--2832 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 linorder$\OML/cmm/m/it/10 ;$ $\OMS/cmsy/m/n/10 f$\OT1/ *** cmr/m/it/10 ordered[]comm[]monoid[]add$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 ord *** ered[]ab[]semigroup[]add[]imp[]le$\OML/cmm/m/it/10 ;$ *** *** Overfull \hbox (68.70148pt too wide) in paragraph at lines 2848--2850 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 linorder$\OML/cmm/m/it/10 ;$ $\OMS/cmsy/m/n/10 f$\OT1/ *** cmr/m/it/10 ordered[]comm[]monoid[]add$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 ord *** ered[]ab[]semigroup[]add[]imp[]le$\OML/cmm/m/it/10 ;$ *** *** Overfull \hbox (9.0226pt too wide) in paragraph at lines 2866--2868 *** [][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly[]mapping $\OT1/cmr/m/n/10 : *** $$:$ $($\OT1/cmr/m/it/10 linorder$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 linorder *** ed[]ab[]group[]add$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 linordered[]ab[]group[]a *** dd[] *** *** Overfull \hbox (29.55527pt too wide) in paragraph at lines 2885--2889 *** []\OT1/cmr/m/n/10.95 For prag-ma-tism we leave out the fi-nal el-e-ments in the *** hi-er-ar-chy: \OT1/cmr/m/it/10.95 linordered[]ring\OT1/cmr/m/n/10.95 , *** [58] [59] [60] [61] *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\Rightarrow' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\-command' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\isamath' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\-command' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\isatext' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `subscript' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\mskip' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\mskip' on input line 4080. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4080. *** *** [62] *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\sfcode' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\mskip' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\mskip' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\Rightarrow' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\-command' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\isamath' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\-command' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\isatext' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `subscript' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\mskip' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `\mskip' on input line 4507. *** *** *** Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): *** (hyperref) removing `math shift' on input line 4507. *** *** [63] [64] [65] *** Overfull \hbox (6.6393pt too wide) in paragraph at lines 5111--5113 *** [][]\OT1/cmr/bx/n/10 hide[]const $\OT1/cmr/m/n/10 ($\OT1/cmr/bx/n/10 open$\OT1/ *** cmr/m/n/10 )$ \OT1/cmr/m/it/10 lookup sin-gle up-date keys range map map[]key d *** e-gree nth the[]value *** ) (./PP_MPoly.tex [66] [67] [68] [69] *** Overfull \hbox (43.18304pt too wide) in paragraph at lines 926--927 *** \OT1/cmr/bx/n/10 definition \OT1/cmr/m/it/10 insertion[]fun[]natural $\OT1/cmr/ *** m/n/10 :$$:$ $($\OT1/cmr/m/it/10 nat $\OMS/cmsy/m/n/10 )$ $ [] $\OT1/cmr/m/it/1 *** 0 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 )$ $\OT1/cmr/m/n/10 ($$($\OT1/cmr/m/it *** /10 nat $\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 nat$\OT1/cmr/m/n/10 )$ $\OMS/cmsy *** /m/n/10 )$ $ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 )$ $ [ *** ] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 comm[]semiring[]1[] *** *** [70] *** Overfull \hbox (13.03099pt too wide) in paragraph at lines 930--932 *** [][]\OT1/cmr/bx/n/10 definition \OT1/cmr/m/it/10 insertion[]fun $\OT1/cmr/m/n/1 *** 0 :$$:$ $($\OT1/cmr/m/it/10 nat $\OMS/cmsy/m/n/10 )$ $ [] $\OT1/cmr/m/it/10 a$\ *** OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 )$ $\OT1/cmr/m/n/10 ($$($\OT1/cmr/m/it/10 n *** at $\OMS/cmsy/m/n/10 )$$[][]$ \OT1/cmr/m/it/10 nat$\OT1/cmr/m/n/10 )$ $\OMS/cms *** y/m/n/10 )$ $ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 )$ $ *** [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 comm[]semiring[]1[ *** ] *** *** Overfull \hbox (37.2235pt too wide) in paragraph at lines 938--939 *** []\OT1/cmr/bx/n/10 lift[]definition \OT1/cmr/m/it/10 insertion[]aux $\OT1/cmr/m *** /n/10 :$$:$ $($\OT1/cmr/m/it/10 nat $\OMS/cmsy/m/n/10 )$ $ [] $\OT1/cmr/m/it/10 *** a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 )$ $\OT1/cmr/m/n/10 ($$($\OT1/cmr/m/it/ *** 10 nat $\OMS/cmsy/m/n/10 )$$[][]$ \OT1/cmr/m/it/10 nat$\OT1/cmr/m/n/10 )$ $\OMS *** /cmsy/m/n/10 )$$[][]$ $ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/ *** n/10 )$ $ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 comm[]se *** miring[]1[] *** [71] *** Overfull \hbox (4.62216pt too wide) in paragraph at lines 1304--1319 *** [][]\OT1/cmr/bx/n/10 is $\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 p v$\OML/cmm/m/i *** t/10 :$ \OT1/cmr/m/it/10 Max $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 insert 0 $\OT1 *** /cmr/m/n/10 ($$($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 m$\OML/cmm/m/it/10 :$ \ *** OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 lookup m *** v$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 ` PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\O *** T1/cmr/m/it/10 keys *** *** Overfull \hbox (12.6683pt too wide) in paragraph at lines 1323--1338 *** [][]\OT1/cmr/bx/n/10 is $\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 p$\OML/cmm/m/it/ *** 10 :$ \OT1/cmr/m/it/10 Max $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 insert 0 $\OT1/c *** mr/m/n/10 ($$($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 m$\OML/cmm/m/it/10 :$ \OT *** 1/cmr/m/it/10 sum $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/cm *** m/m/it/10 :$\OT1/cmr/m/it/10 lookup m$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 PP *** []Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 keys *** [72] *** ! Missing $ inserted. *** *** $ *** l.1520 ...ion below generalises HOL/Computational_ *** Algebra/Polynomial.thy. *** ! Missing $ inserted. *** *** $ *** l.1525 \end{isamarkuptext} *** \isamarkuptrue% *** *** Overfull \hbox (1371.46657pt too wide) in paragraph at lines 1520--1525 *** []\OT1/cmr/m/n/10.95 The in-tro-duc-tion of pseudo-division be-low gen-er-alise *** s HOL/Computational$[]\OML/cmm/m/it/10.95 lgebra=Polynomial:thy:\OT1/cmr/m/n/10 *** .95 [1]\OML/cmm/m/it/10.95 Winkler; PolynomialAlgorithms; \OT1/cmr/m/n/10.95 19 *** 96\OML/cmm/m/it/10.95 :ThegeneralisationraisesissuesaddressedbyWendaLiandcommen *** tedbelow:Florianrepliedtotheissuesconjecturing; thattheabstractmpolyneedsnotbea *** wareoftheissues; incasetheseareonlyconcernedwithexecutability:$ *** [73]) (./PP_More_MPoly.tex [74] [75] [76] *** Overfull \hbox (85.06708pt too wide) in paragraph at lines 1118--1120 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 monom[]pow$\OT1/cmr/m/n/10 :$\OT1/c *** mr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/cmm *** /m/it/10 :$\OT1/cmr/m/it/10 single v n0$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 a ^ *** n $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/ *** 10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 single *** *** Overfull \hbox (3.52673pt too wide) in paragraph at lines 1140--1142 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 insertion[]fun[]single$\OT1/cmr/m/n *** /10 :$ \OT1/cmr/m/it/10 insertion[]fun f $\OT1/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^ *** ^U$\OT1/cmr/m/it/10 m$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a *** when $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$ *** \OT1/cmr/m/it/10 single *** *** Overfull \hbox (10.76723pt too wide) in paragraph at lines 1206--1208 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 insertion[]single$\OT1/cmr/m/n/10 [ *** $\OT1/cmr/m/it/10 simp$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 in-ser-tion f $\O *** T1/cmr/m/n/10 ($\OT1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 PP[] *** Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 single $\OT1/cmr/m/n/10 ($\OT *** 1/cmr/m/it/10 v$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 nat$\OT1/cmr/m/n/10 )$ *** [77] *** Overfull \hbox (17.67397pt too wide) in paragraph at lines 1348--1349 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 reduce[]nested[]mpoly $\OT1/cmr/m/n *** /10 ($\OT1/cmr/m/it/10 p1 $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 p2$\OT1/cmr/m/n/ *** 10 )$ $=$ \OT1/cmr/m/it/10 reduce[]nested[]mpoly p1 $\OT1/cmr/m/n/10 +$ \OT1/cm *** r/m/it/10 reduce[]nested[]mpoly *** *** Overfull \hbox (12.1184pt too wide) in paragraph at lines 1368--1369 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 reduce[]nested[]mpoly $\OT1/cmr/m/n *** /10 ($\OT1/cmr/m/it/10 p1 $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 p2$\OT1/cmr/m *** /n/10 )$ $=$ \OT1/cmr/m/it/10 reduce[]nested[]mpoly p1 $\OMS/cmsy/m/n/10 ^^C$ \ *** OT1/cmr/m/it/10 reduce[]nested[]mpoly *** *** Overfull \hbox (23.5074pt too wide) in paragraph at lines 1406--1407 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 in-ser-tion f $\OT1/cmr/m/n/10 ($\O *** T1/cmr/m/it/10 insertion $\OT1/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it *** /10 v$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 monom 0 $\OT1/cmr/m/n/10 ($\OT1/cmr/ *** m/it/10 f v$\OT1/cmr/m/n/10 )$$)$ \OT1/cmr/m/it/10 pp$\OT1/cmr/m/n/10 )$ $=$ \O *** T1/cmr/m/it/10 in-ser-tion f $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 reduce[]nested *** []mpoly *** *** Overfull \hbox (8.03319pt too wide) in paragraph at lines 1472--1473 *** [][]\OT1/cmr/m/it/10 extract[]var p v $\OT1/cmr/m/n/10 =$ $($$[] $\OT1/cmr/m/it *** /10 m$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/ *** it/10 remove[]key v m$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 monom $\OT1/cmr/m/ *** n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 s *** ingle *** [78] *** Overfull \hbox (53.27187pt too wide) in paragraph at lines 1478--1479 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 extract[]var p v $\OT1/cmr/m/n/10 = *** $ $($$[] $\OT1/cmr/m/it/10 m$\OMS/cmsy/m/n/10 2$\OT1/cmr/m/it/10 S$\OML/cmm/m/i *** t/10 :$ \OT1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 remove[]key *** v m$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/ *** it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 single *** *** Overfull \hbox (64.50641pt too wide) in paragraph at lines 1587--1588 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 extract[]var $\OT1/cmr/m/n/10 ($\OT *** 1/cmr/m/it/10 monom m a$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 v $\OT1/cmr/m/n/10 *** =$ \OT1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 remove[]key v m$\ *** OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 *** PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 single *** *** Overfull \hbox (72.76335pt too wide) in paragraph at lines 1683--1684 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 extract[]var $\OT1/cmr/m/n/10 ($\OT *** 1/cmr/m/it/10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/ *** cmm/m/it/10 :$\OT1/cmr/m/it/10 single v n$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 a *** $\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 v$ [] $ $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/ *** 10 monom $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 *** :$\OT1/cmr/m/it/10 single *** [79] *** Overfull \hbox (5.67621pt too wide) in paragraph at lines 2011--2012 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 in-ser-tion f $\OT1/cmr/m/n/10 ($\O *** T1/cmr/m/it/10 replace[]coeff $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 insertion f$\ *** OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 pp$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 i *** n-ser-tion f $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 reduce[]nested[]mpoly *** ) (./DL_Deep_Model_Poly.tex *** Overfull \hbox (27.40462pt too wide) in paragraph at lines 6--6 *** []\OT1/cmr/bx/n/14.4 Polynomials rep-re-sent-ing the Deep Net-work Model *** [80] [81] *** Overfull \hbox (29.83835pt too wide) in paragraph at lines 669--670 *** [][]\OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 poly-fun $\OMS/cmsy/m/n/10 f$$\OML/ *** cmm/m/it/10 :$$:$$<$\OT1/cmr/m/it/10 count[]weights m$\OMS/cmsy/m/n/10 g$ $\OT1 *** /cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 f$\OML/cmm/m/it/10 :$ \OT1 *** /cmr/m/it/10 Ten-sor$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 lookup $\OT1/cmr/m/n/1 *** 0 ($\OT1/cmr/m/it/10 tensors[]from[]net $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 ins *** ert[]weights *** [82] *** Overfull \hbox (7.4437pt too wide) in paragraph at lines 891--893 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 input[]sizes[]deep[]model$\OT1/cmr/ *** m/n/10 :$ \OT1/cmr/m/it/10 input[]sizes $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 dee *** p[]model[]l rs$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 repli-cate $\OT1/cmr/m/n *** /10 ($\OT1/cmr/m/it/10 2 $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 N[]half$\OT1/c *** mr/m/n/10 )$ *** ) (./Lebesgue_Functional.tex [83] *** Overfull \hbox (9.5813pt too wide) in paragraph at lines 15--16 *** [][]\OT1/cmr/bx/n/10 imports $[][]$$[][]$$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/10 s *** rc$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/10 HOL$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/10 *** Analysis$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/10 Lebesgue[]Measure $[][]$$[][]$$\OM *** L/cmm/m/it/10 =$\OT1/cmr/m/it/10 src$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/10 HOL$\O *** ML/cmm/m/it/10 =$\OT1/cmr/m/it/10 Topological[]Spaces[] *** *** Overfull \hbox (7.64981pt too wide) in paragraph at lines 26--32 *** []\OT1/cmr/m/n/10.95 Lebesgue[]Measure.lborel is de-fined on the type-class eu- *** clidean[]space, which *** *** Overfull \hbox (8.36926pt too wide) in paragraph at lines 36--38 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 product[]sigma[]finite[]interval$\O *** T1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 product[]sigma[]finite $\OT1/cmr/m/n/10 ($$\O *** ML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 b$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 inte *** rval[]measure $\OT1/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 x$\OML/ *** cmm/m/it/10 :$ *** [84]) (./PP_Univariate.tex *** Overfull \hbox (21.94554pt too wide) in paragraph at lines 12--13 *** [][]\OT1/cmr/bx/n/10 imports \OT1/cmr/m/it/10 PP[]MPoly PP[]More[]MPoly $[][]$$ *** [][]$$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/10 src$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/ *** 10 HOL$\OML/cmm/m/it/10 =$\OT1/cmr/m/it/10 Computational[]Algebra$\OML/cmm/m/it *** /10 =$\OT1/cmr/m/it/10 Polynomial[] *** ! Missing $ inserted. *** *** $ *** l.23 ...ariate polynomials from HOL/Computational_ *** Algebra/Polynomial.% *** ! Missing $ inserted. *** *** $ *** l.24 \end{isamarkuptext} *** \isamarkuptrue% *** *** Overfull \hbox (45.54262pt too wide) in paragraph at lines 26--27 *** [][]\OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 poly[]to[]mpoly v p $\OT1/cmr/m/n/1 *** 0 =$ \OT1/cmr/m/it/10 MPoly $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Abs[]poly[]mapp *** ing $\OT1/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 m$\OML/cmm/m/it/1 *** 0 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeff p $\OT1/cmr/m/n/10 ($\OT1/cmr/m/ *** it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 lookup *** *** Overfull \hbox (12.33939pt too wide) in paragraph at lines 28--30 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 poly[]to[]mpoly[]finite$\OT1/cmr/m/ *** n/10 :$ \OT1/cmr/m/it/10 fi-nite $\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 m$\OT1/cm *** r/m/n/10 :$$:$\OT1/cmr/m/it/10 nat $\OMS/cmsy/m/n/10 )$$[][]$ \OT1/cmr/m/it/10 *** nat$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeff p $\OT1/cmr/m *** /n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 *** lookup *** *** Overfull \hbox (29.68018pt too wide) in paragraph at lines 77--79 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 coeff[]poly[]to[]mpoly$\OT1/cmr/m/n *** /10 :$ \OT1/cmr/m/it/10 PP[]MPoly$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 coeff $\O *** T1/cmr/m/n/10 ($\OT1/cmr/m/it/10 poly[]to[]mpoly v p$\OT1/cmr/m/n/10 )$ $($\OT1 *** /cmr/m/it/10 PP[]Poly[]Mapping$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 single *** *** Overfull \hbox (8.67422pt too wide) in paragraph at lines 100--101 *** [][]\OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 mpoly[]to[]poly v p $\OT1/cmr/m/n/1 *** 0 =$ \OT1/cmr/m/it/10 Abs[]poly $\OT1/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/c *** mr/m/it/10 k$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 PP[]MPoly$\OML/cmm/m/it/10 :$ *** \OT1/cmr/m/it/10 coeff p $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 PP[]Poly[]Mapping$ *** \OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 single *** *** Overfull \hbox (37.35866pt too wide) in paragraph at lines 102--104 *** [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 coeff[]mpoly[]to[]poly$\OT1/cmr/m/n *** /10 [$\OT1/cmr/m/it/10 simp$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 Poly-no-mial *** $\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 coeff $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 *** mpoly[]to[]poly v p$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 k $\OT1/cmr/m/n/10 =$ \ *** OT1/cmr/m/it/10 PP[]MPoly$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 coeff *** [85]) (./Lebesgue_Zero_Set.tex *** Overfull \hbox (14.1863pt too wide) in paragraph at lines 148--150 *** \OT1/cmr/m/n/10.95 poly-no-mial" http://www1.uwindsor.ca/math/sites/uwindsor.ca *** .math/files/05- *** [86]) (./DL_Rank_Submatrix.tex) (./DL_Shallow_Model.tex [87]) *** (./DL_Fundamental_Theorem_Network_Capacity.tex *** Overfull \hbox (28.14441pt too wide) in paragraph at lines 15--16 *** [][]\OT1/cmr/bx/n/10 imports \OT1/cmr/m/it/10 DL[]Rank[]CP[]Rank DL[]Deep[]Mode *** l[]Poly Lebesgue[]Zero[]Set DL[]Rank[]Submatrix *** *** Overfull \hbox (15.32675pt too wide) in paragraph at lines 29--31 *** [][]\OT1/cmr/bx/n/10 definition \OT1/cmr/m/it/10 polynomial[]f w $\OT1/cmr/m/n/ *** 10 =$ \OT1/cmr/m/it/10 det $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 submatrix $\OT1/ *** cmr/m/n/10 ($\OT1/cmr/m/it/10 matricize $\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 n$ *** \OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 even n$\OMS/cmsy/m/n/10 g$ $\OT1/cmr/m/n/1 *** 0 ($\OT1/cmr/m/it/10 A w$\OT1/cmr/m/n/10 )$$)$ \OT1/cmr/m/it/10 rows[]with[]1 *** [88] *** Overfull \hbox (4.73578pt too wide) in paragraph at lines 140--141 *** [][]\OT1/cmr/bx/n/10 assumes $\OMS/cmsy/m/n/10 8 $\OT1/cmr/m/it/10 inputs$\OML/ *** cmm/m/it/10 :$ \OT1/cmr/m/it/10 input[]sizes $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/1 *** 0 deep[]model[]l rs$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 map dim$[][]$ in-pu *** ts $[][]\OMS/cmsy/m/n/10 !$ \OT1/cmr/m/it/10 evaluate[]net *** [89])) *** No file root.bbl. *** [90] (./root.aux) *** *** Package rerunfilecheck Warning: File `root.out' has changed. *** (rerunfilecheck) Rerun to get outlines right *** (rerunfilecheck) or use package `bookmark'. *** *** *** LaTeX Warning: There were undefined references. *** *** ) *** (see the transcript file for additional information) *** Output written on root.pdf (90 pages, 368656 bytes). *** Transcript written on root.log. *** Document preparation failure in directory '/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/outline' *** *** Failed to build document "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Deep_Learning/outline.pdf"