Loading theory "HOL-Eisbach.Eisbach" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect") Loading theory "LLL_Basis_Reduction.More_IArray" signature PARSE_TOOLS = sig val is_real_val: ('a, 'b) parse_val -> bool val name_term: (term, string) parse_val parser val parse_term_val: 'a parser -> (term, 'a) parse_val parser val parse_thm_val: 'a parser -> (thm, 'a) parse_val parser datatype ('a, 'b) parse_val = Parse_Val of 'b * ('a -> unit) | Real_Val of 'a val parse_val_cases: ('a -> 'b) -> ('b, 'a) parse_val -> 'b * ('b -> unit) val the_parse_fun: ('a, 'b) parse_val -> 'a -> unit val the_parse_val: ('a, 'b) parse_val -> 'b val the_real_val: ('a, 'b) parse_val -> 'a end structure Parse_Tools: PARSE_TOOLS signature METHOD_CLOSURE = sig val apply_method: Proof.context -> string -> term list -> thm list list -> (Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic val method: binding -> (binding * typ option * mixfix) list -> binding list -> binding list -> binding list -> Token.src -> local_theory -> string * local_theory val method_cmd: binding -> (binding * string option * mixfix) list -> binding list -> binding list -> binding list -> Token.src -> local_theory -> string * local_theory end structure Method_Closure: METHOD_CLOSURE Found termination order: "{}" ### theory "LLL_Basis_Reduction.More_IArray" ### 0.141s elapsed time, 0.276s cpu time, 0.000s GC time Loading theory "Perron_Frobenius.Bij_Nat" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect") structure Eisbach_Rule_Insts: sig end ### theory "Perron_Frobenius.Bij_Nat" ### 0.111s elapsed time, 0.220s cpu time, 0.000s GC time Loading theory "Perron_Frobenius.Cancel_Card_Constraint" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect") ### ML warning (line 55 of "$AFP/Perron_Frobenius/cancel_card_constraint.ML"): ### Pattern is not exhaustive. signature CARD_ELIMINATION = sig val cancel_card_constraint: thm -> thm val cancel_card_constraint_attr: attribute end structure Card_Elimination: CARD_ELIMINATION ### theory "Perron_Frobenius.Cancel_Card_Constraint" ### 0.308s elapsed time, 0.612s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Continuum_Not_Denumerable" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected") ### ML warning (line 170 of "~~/src/HOL/Eisbach/match_method.ML"): ### Pattern is not exhaustive. ### ML warning (line 187 of "~~/src/HOL/Eisbach/match_method.ML"): ### Pattern is not exhaustive. ### ML warning (line 309 of "~~/src/HOL/Eisbach/match_method.ML"): ### Pattern is not exhaustive. signature MATCH_METHOD = sig val focus_params: Proof.context -> term list val focus_schematics: Proof.context -> Envir.tenv end structure Match_Method: MATCH_METHOD val method_evaluate = fn: Method.text -> Proof.context -> thm list -> tactic ### theory "HOL-Eisbach.Eisbach" ### 0.689s elapsed time, 1.368s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Inner_Product" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Analysis.Euclidean_Space" via "HOL-Analysis.Product_Vector") ### theory "HOL-Analysis.Continuum_Not_Denumerable" ### 0.358s elapsed time, 0.836s cpu time, 0.000s GC time Loading theory "HOL-Analysis.L2_Norm" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Analysis.Euclidean_Space") ### theory "HOL-Analysis.L2_Norm" ### 0.155s elapsed time, 0.300s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Operator_Norm" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative") class real_inner = dist_norm + real_vector + sgn_div_norm + uniformity_dist + open_uniformity + fixes inner :: "'a \ 'a \ real" assumes "inner_commute": "\x y. inner x y = inner y x" and "inner_add_left": "\x y z. inner (x + y) z = inner x z + inner y z" and "inner_scaleR_left": "\r x y. inner (r *\<^sub>R x) y = r * inner x y" and "inner_ge_zero": "\x. 0 \ inner x x" and "inner_eq_zero_iff": "\x. (inner x x = 0) = (x = (0::'a))" and "norm_eq_sqrt_inner": "\x. norm x = sqrt (inner x x)" ### theory "HOL-Analysis.Operator_Norm" ### 0.172s elapsed time, 0.340s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Norm_Arith" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected" via "HOL-Analysis.Topology_Euclidean_Space") ### ML warning (line 103 of "~~/src/HOL/Analysis/normarith.ML"): ### Matches are not exhaustive. ### ML warning (line 347 of "~~/src/HOL/Analysis/normarith.ML"): ### Value identifier (instantiate_cterm') has not been referenced. signature NORM_ARITH = sig val norm_arith: Proof.context -> conv val norm_arith_tac: Proof.context -> int -> tactic end structure NormArith: NORM_ARITH instantiation real :: real_inner inner_real == inner :: real \ real \ real ### theory "HOL-Analysis.Norm_Arith" ### 0.459s elapsed time, 0.916s cpu time, 0.000s GC time Loading theory "LLL_Basis_Reduction.Cost" (required by "LLL_Basis_Reduction.LLL_GSO_Impl_Complexity") instantiation complex :: real_inner inner_complex == inner :: complex \ complex \ real ### theory "LLL_Basis_Reduction.Cost" ### 0.056s elapsed time, 0.112s cpu time, 0.000s GC time Loading theory "LLL_Basis_Reduction.List_Representation" ### theory "HOL-Analysis.Inner_Product" ### 1.214s elapsed time, 2.516s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Product_Vector" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product" via "HOL-Analysis.Euclidean_Space") ### theory "LLL_Basis_Reduction.List_Representation" ### 0.335s elapsed time, 0.608s cpu time, 0.264s GC time Loading theory "Algebraic_Numbers.Bivariate_Polynomials" (required by "LLL_Basis_Reduction.Norms" via "Algebraic_Numbers.Resultant") locale module_prod fixes s1 :: "'a \ 'b \ 'b" and s2 :: "'a \ 'c \ 'c" assumes "module_prod s1 s2" locale vector_space_prod fixes s1 :: "'a \ 'b \ 'b" (infixr "*a" 75) and s2 :: "'a \ 'c \ 'c" (infixr "*b" 75) assumes "vector_space_prod ( *a) ( *b)" instantiation prod :: (real_vector, real_vector) real_vector scaleR_prod == scaleR :: real \ 'a \ 'b \ 'a \ 'b instantiation prod :: (metric_space, metric_space) dist dist_prod == dist :: 'a \ 'b \ 'a \ 'b \ real instantiation prod :: (metric_space, metric_space) uniformity_dist uniformity_prod == uniformity :: (('a \ 'b) \ 'a \ 'b) filter instantiation prod :: (metric_space, metric_space) metric_space instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector sgn_prod == sgn :: 'a \ 'b \ 'a \ 'b norm_prod == norm :: 'a \ 'b \ real instantiation prod :: (real_inner, real_inner) real_inner inner_prod == inner :: 'a \ 'b \ 'a \ 'b \ real ### theory "Algebraic_Numbers.Bivariate_Polynomials" ### 0.898s elapsed time, 1.792s cpu time, 0.000s GC time Loading theory "Algebraic_Numbers.Resultant" (required by "LLL_Basis_Reduction.Norms") locale finite_dimensional_vector_space_prod fixes s1 :: "'a \ 'b \ 'b" (infixr "*a" 75) and s2 :: "'a \ 'c \ 'c" (infixr "*b" 75) and B1 :: "'b set" and B2 :: "'c set" assumes "finite_dimensional_vector_space_prod ( *a) ( *b) B1 B2" ### theory "HOL-Analysis.Product_Vector" ### 1.201s elapsed time, 2.340s cpu time, 0.264s GC time Loading theory "HOL-Analysis.Euclidean_Space" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Cartesian_Space" via "HOL-Analysis.Finite_Cartesian_Product") class euclidean_space = real_inner + fixes Basis :: "'a set" assumes "nonempty_Basis": "Basis \ {}" assumes "finite_Basis": "finite Basis" assumes "inner_Basis": "\u v. \u \ Basis; v \ Basis\ \ inner u v = (if u = v then 1 else 0)" assumes "euclidean_all_zero_iff": "\x. (\u\Basis. inner x u = 0) = (x = (0::'a))" instantiation real :: euclidean_space Basis_real == Basis :: real set instantiation complex :: euclidean_space Basis_complex == Basis :: complex set instantiation prod :: (euclidean_space, euclidean_space) euclidean_space Basis_prod == Basis :: ('a \ 'b) set ### theory "HOL-Analysis.Euclidean_Space" ### 1.573s elapsed time, 3.144s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Linear_Algebra" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Cartesian_Space") Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" class real_inner = real_normed_vector + fixes inner :: "'a \ 'a \ real" assumes "inner_commute": "\x y. x \ y = y \ x" and "inner_add_left": "\x y z. (x + y) \ z = x \ z + y \ z" and "inner_scaleR_left": "\r x y. r *\<^sub>R x \ y = r * (x \ y)" and "inner_ge_zero": "\x. 0 \ x \ x" and "inner_eq_zero_iff": "\x. (x \ x = 0) = (x = (0::'a))" and "norm_eq_sqrt_inner": "\x. norm x = sqrt (x \ x)" Found termination order: "(\p. size (snd (snd (snd (snd p))))) <*mlex*> {}" Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" ### theory "Algebraic_Numbers.Resultant" ### 3.116s elapsed time, 6.080s cpu time, 0.792s GC time Loading theory "HOL-Analysis.Finite_Cartesian_Product" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Cartesian_Space") ### theory "HOL-Analysis.Linear_Algebra" ### 1.462s elapsed time, 2.788s cpu time, 0.792s GC time Loading theory "HOL-Analysis.Topology_Euclidean_Space" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space" via "HOL-Analysis.Connected") bundle vec_syntax bundle no_vec_syntax instantiation vec :: (zero, finite) zero zero_vec == zero_class.zero :: ('a, 'b) vec instantiation vec :: (plus, finite) plus plus_vec == plus :: ('a, 'b) vec \ ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (minus, finite) minus minus_vec == minus :: ('a, 'b) vec \ ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (uminus, finite) uminus uminus_vec == uminus :: ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (times, finite) times times_vec == times :: ('a, 'b) vec \ ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (one, finite) one one_vec == one_class.one :: ('a, 'b) vec instantiation vec :: (ord, finite) ord less_eq_vec == less_eq :: ('a, 'b) vec \ ('a, 'b) vec \ bool less_vec == less :: ('a, 'b) vec \ ('a, 'b) vec \ bool ### Additional type variable(s) in locale specification "cart_one": 'a class cart_one = type + assumes "UNIV_one": "CARD('a) = Suc 0" class topological_space = open + assumes "open_UNIV": "open UNIV" assumes "open_Int": "\S T. \open S; open T\ \ open (S \ T)" assumes "open_Union": "\K. Ball K open \ open (\K)" instantiation vec :: (real_vector, finite) real_vector scaleR_vec == scaleR :: real \ ('a, 'b) vec \ ('a, 'b) vec instantiation vec :: (topological_space, finite) topological_space open_vec == open :: ('a, 'b) vec set \ bool locale countable_basis fixes B :: "'a set set" assumes "countable_basis B" instantiation vec :: (metric_space, finite) dist dist_vec == dist :: ('a, 'b) vec \ ('a, 'b) vec \ real instantiation vec :: (metric_space, finite) uniformity_dist uniformity_vec == uniformity :: (('a, 'b) vec \ ('a, 'b) vec) filter instantiation vec :: (metric_space, finite) metric_space instantiation vec :: (real_normed_vector, finite) real_normed_vector sgn_vec == sgn :: ('a, 'b) vec \ ('a, 'b) vec norm_vec == norm :: ('a, 'b) vec \ real class second_countable_topology = topological_space + assumes "ex_countable_subbasis": "\B. countable B \ open = generate_topology B" instantiation vec :: (real_inner, finite) real_inner inner_vec == inner :: ('a, 'b) vec \ ('a, 'b) vec \ real instantiation vec :: (euclidean_space, finite) euclidean_space Basis_vec == Basis :: ('a, 'b) vec set ### Ignoring duplicate rewrite rule: ### vec_lambda ?g1 $ ?i1 \ ?g1 ?i1 ### theory "HOL-Analysis.Finite_Cartesian_Product" ### 2.657s elapsed time, 5.276s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Cartesian_Space" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space") locale linear_first_finite_dimensional_vector_space fixes scaleB :: "'a \ 'b \ 'b" (infixr "*b" 75) and scaleC :: "'a \ 'c \ 'c" (infixr "*c" 75) and BasisB :: "'b set" and f :: "'b \ 'c" assumes "linear_first_finite_dimensional_vector_space ( *b) ( *c) BasisB f" ### theory "HOL-Analysis.Cartesian_Space" ### 1.283s elapsed time, 2.440s cpu time, 0.768s GC time Loading theory "LLL_Basis_Reduction.Missing_Lemmas" (required by "LLL_Basis_Reduction.Norms") class heine_borel = metric_space + assumes "bounded_imp_convergent_subsequence": "\f. bounded (range f) \ \l r. strict_mono r \ (f \ r) \ l" ### theory "HOL-Analysis.Topology_Euclidean_Space" ### 7.791s elapsed time, 15.012s cpu time, 1.416s GC time Loading theory "HOL-Analysis.Connected" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike" via "HOL-Analysis.Convex_Euclidean_Space") ### theory "HOL-Analysis.Connected" ### 3.648s elapsed time, 6.568s cpu time, 0.560s GC time Loading theory "HOL-Analysis.Convex_Euclidean_Space" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension" via "HOL-Analysis.Starlike") locale comp_fun_commute_on fixes f :: "'a \ 'a \ 'a" and A :: "'a set" assumes "comp_fun_commute_on f A" locale comp_fun_commute_on fixes f :: "'a \ 'a \ 'a" and A :: "'a set" assumes "comp_fun_commute_on f A" locale abelian_monoid fixes G :: "('a, 'b) ring_scheme" (structure) assumes "abelian_monoid G" ### Ignoring duplicate rewrite rule: ### interior (ball ?x1 ?e1) \ ball ?x1 ?e1 ### theory "HOL-Analysis.Convex_Euclidean_Space" ### 3.368s elapsed time, 6.680s cpu time, 0.656s GC time Loading theory "HOL-Analysis.Starlike" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected" via "HOL-Analysis.Continuous_Extension") Found termination order: "length <*mlex*> {}" consts rev_upt :: "nat \ nat \ nat list" instantiation vec :: (conjugate) conjugate conjugate_vec == conjugate :: 'a vec \ 'a vec ### theory "HOL-Analysis.Starlike" ### 3.674s elapsed time, 7.276s cpu time, 0.564s GC time Loading theory "HOL-Analysis.Continuous_Extension" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint" via "HOL-Analysis.Path_Connected") ### theory "HOL-Analysis.Continuous_Extension" ### 0.249s elapsed time, 0.496s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Path_Connected" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint") locale poly_mod fixes m :: "int" locale poly_mod_2 fixes m :: "int" assumes "poly_mod_2 m" locale poly_mod_prime fixes p :: "int" assumes "poly_mod_prime p" locale Module.module fixes R :: "('a, 'b) ring_scheme" (structure) and M :: "('a, 'c, 'd) module_scheme" (structure) assumes "Module.module R M" locale vec_module fixes f_ty :: "'a itself" and n :: "nat" locale idom_vec fixes n :: "nat" and f_ty :: "'a itself" locale Retracts fixes s :: "'a set" and h :: "'a \ 'b" and t :: "'b set" and k :: "'b \ 'a" assumes "Retracts s h t k" ### theory "HOL-Analysis.Path_Connected" ### 7.657s elapsed time, 15.860s cpu time, 5.828s GC time Loading theory "HOL-Analysis.Homeomorphism" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Brouwer_Fixpoint") locale vec_space fixes f_ty :: "'a itself" and n :: "nat" ### theory "LLL_Basis_Reduction.Missing_Lemmas" ### 24.852s elapsed time, 48.848s cpu time, 9.396s GC time Loading theory "HOL-Analysis.Extended_Real_Limits" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit" via "HOL-Analysis.Summation_Tests") ### theory "HOL-Analysis.Homeomorphism" ### 1.297s elapsed time, 2.512s cpu time, 0.448s GC time Loading theory "HOL-Analysis.Brouwer_Fixpoint" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative") locale kuhn_simplex fixes p :: "nat" and n :: "nat" and base :: "nat \ nat" and upd :: "nat \ nat" and s :: "(nat \ nat) set" assumes "kuhn_simplex p n base upd s" locale kuhn_simplex_pair fixes p :: "nat" and n :: "nat" and b_s :: "nat \ nat" and u_s :: "nat \ nat" and s :: "(nat \ nat) set" and b_t :: "nat \ nat" and u_t :: "nat \ nat" and t :: "(nat \ nat) set" assumes "kuhn_simplex_pair p n b_s u_s s b_t u_t t" Proofs for inductive predicate(s) "ksimplex" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "HOL-Analysis.Extended_Real_Limits" ### 1.327s elapsed time, 2.664s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Summation_Tests" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative" via "HOL-Analysis.Uniform_Limit") ### theory "HOL-Analysis.Summation_Tests" ### 1.229s elapsed time, 2.380s cpu time, 0.616s GC time Loading theory "HOL-Analysis.Uniform_Limit" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative") ### theory "HOL-Analysis.Brouwer_Fixpoint" ### 2.352s elapsed time, 4.632s cpu time, 0.616s GC time Loading theory "LLL_Basis_Reduction.Norms" ### theory "HOL-Analysis.Uniform_Limit" ### 1.318s elapsed time, 2.644s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Bounded_Linear_Function" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space" via "HOL-Analysis.Derivative") instantiation blinfun :: (real_normed_vector, real_normed_vector) real_normed_vector uminus_blinfun == uminus :: 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b zero_blinfun == zero_class.zero :: 'a \\<^sub>L 'b minus_blinfun == minus :: 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b plus_blinfun == plus :: 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b sgn_blinfun == sgn :: 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b norm_blinfun == norm :: 'a \\<^sub>L 'b \ real scaleR_blinfun == scaleR :: real \ 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b dist_blinfun == dist :: 'a \\<^sub>L 'b \ 'a \\<^sub>L 'b \ real uniformity_blinfun == uniformity :: ('a \\<^sub>L 'b \ 'a \\<^sub>L 'b) filter open_blinfun == open :: ('a \\<^sub>L 'b) set \ bool class semiring_real_line = ordered_semiring_strict + ordered_semiring_0 + assumes "add_pos_neg_is_real": "\a b. \(0::'a) < a; b < (0::'a)\ \ is_real (a + b)" and "mult_neg_neg": "\a b. \a < (0::'a); b < (0::'a)\ \ (0::'a) < a * b" and "pos_pos_linear": "\a b. \(0::'a) < a; (0::'a) < b\ \ a < b \ a = b \ b < a" and "neg_neg_linear": "\a b. \a < (0::'a); b < (0::'a)\ \ a < b \ a = b \ b < a" locale bounded_bilinear fixes prod :: "'a \ 'b \ 'c" (infixl "**" 70) assumes "bounded_bilinear ( ** )" locale bounded_bilinear fixes prod :: "'a \ 'b \ 'c" (infixl "**" 70) assumes "bounded_bilinear ( ** )" ### theory "HOL-Analysis.Bounded_Linear_Function" ### 2.156s elapsed time, 4.224s cpu time, 0.556s GC time Loading theory "HOL-Analysis.Derivative" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants" via "HOL-Analysis.Cartesian_Euclidean_Space") ### theory "HOL-Analysis.Derivative" ### 2.364s elapsed time, 4.692s cpu time, 0.476s GC time Loading theory "HOL-Analysis.Cartesian_Euclidean_Space" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect" via "HOL-Analysis.Determinants") ### Ignoring duplicate rewrite rule: ### ?x1 v* Finite_Cartesian_Product.transpose ?A1 \ ?A1 *v ?x1 ### Ignoring duplicate rewrite rule: ### Finite_Cartesian_Product.transpose ?A1 *v ?x1 \ ?x1 v* ?A1 ### Ignoring duplicate rewrite rule: ### 0 v* ?A1 \ 0 ### Ignoring duplicate rewrite rule: ### ?x1 v* 0 \ 0 ### Ignoring duplicate rewrite rule: ### ?y v* mat (1::?'a1) \ ?y instantiation 1 :: cart_one instantiation 1 :: linorder less_eq_num1 == less_eq :: 1 \ 1 \ bool less_num1 == less :: 1 \ 1 \ bool ### theory "HOL-Analysis.Cartesian_Euclidean_Space" ### 1.643s elapsed time, 3.296s cpu time, 0.000s GC time Loading theory "HOL-Analysis.Determinants" (required by "LLL_Basis_Reduction.Gram_Schmidt_2" via "Perron_Frobenius.HMA_Connect") ### theory "HOL-Analysis.Determinants" ### 4.324s elapsed time, 9.348s cpu time, 6.716s GC time Loading theory "Perron_Frobenius.HMA_Connect" (required by "LLL_Basis_Reduction.Gram_Schmidt_2") ### Ambiguous input (line 90 of "$AFP/Perron_Frobenius/HMA_Connect.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" vec_elements) ("_position" v)) ### ("_applC" ("_position" set) ### ("_listcompr" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" v) ### ("_position" i)) ### ("_lc_gen" ("_position" i) ### ("\<^const>List.upt" ("\<^const>Groups.zero_class.zero") ### ("_applC" ("_position" dim_vec) ("_position" v)))) ### ("_lc_end"))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" vec_elements) ("_position" v)) ### ("_applC" ("_position" set) ### ("_listcompr" ### ("\<^const>Matrix.vec_index" ("_position" v) ("_position" i)) ### ("_lc_gen" ("_position" i) ### ("\<^const>List.upt" ("\<^const>Groups.zero_class.zero") ### ("_applC" ("_position" dim_vec) ("_position" v)))) ### ("_lc_end"))))) ### 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 92 of "$AFP/Perron_Frobenius/HMA_Connect.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" vec_elements) ("_position" v)) ### ("_Setcompr" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" v) ### ("_position" i)) ### ("_position" i) ### ("\<^const>Orderings.ord_class.less" ("_position" i) ### ("_applC" ("_position" dim_vec) ("_position" v)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" vec_elements) ("_position" v)) ### ("_Setcompr" ### ("\<^const>Matrix.vec_index" ("_position" v) ("_position" i)) ### ("_position" i) ### ("\<^const>Orderings.ord_class.less" ("_position" i) ### ("_applC" ("_position" dim_vec) ("_position" v)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Ignoring duplicate rewrite rule: ### \i. ?y $h i \ ?y ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### rel_fun ?A ?B ?f ?g ### Rule already declared as introduction (intro) ### (\x y. ?A x y \ ?B (?f x) (?g y)) \ ### (?A ===> ?B) ?f ?g ### Ambiguous input (line 472 of "$AFP/Perron_Frobenius/HMA_Connect.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" mat2matofpoly) ("_position" A)) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_idts" ("_position" i) ("_position" j)) ### ("_poly" ### ("\<^const>Matrix.vec_index" ### ("\<^const>Matrix.vec_index" ("_position" A) ("_position" i)) ### ("_position" j)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" mat2matofpoly) ("_position" A)) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_idts" ("_position" i) ("_position" j)) ### ("_poly" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" A) ### ("\<^const>Matrix.vec_index" ("_position" i) ("_position" j))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" mat2matofpoly) ("_position" A)) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_idts" ("_position" i) ("_position" j)) ### ("_poly" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ### ("\<^const>Matrix.vec_index" ("_position" A) ("_position" i)) ### ("_position" j)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ("_applC" ("_position" mat2matofpoly) ("_position" A)) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_idts" ("_position" i) ("_position" j)) ### ("_poly" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" A) ### ("_position" i)) ### ("_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. ### Ambiguous input (line 477 of "$AFP/Perron_Frobenius/HMA_Connect.thy") produces 4 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" erase_mat) ### ("_cargs" ("_position" A) ("_cargs" ("_position" i) ("_position" j)))) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" i') ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" j') ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" i') ("_position" i)) ### ("\<^const>HOL.eq" ("_position" j') ("_position" j))) ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" A) ### ("_position" i')) ### ("_position" j'))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" erase_mat) ### ("_cargs" ("_position" A) ("_cargs" ("_position" i) ("_position" j)))) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" i') ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" j') ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" i') ("_position" i)) ### ("\<^const>HOL.eq" ("_position" j') ("_position" j))) ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ### ("\<^const>Matrix.vec_index" ("_position" A) ("_position" i')) ### ("_position" j'))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" erase_mat) ### ("_cargs" ("_position" A) ("_cargs" ("_position" i) ("_position" j)))) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" i') ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" j') ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" i') ("_position" i)) ### ("\<^const>HOL.eq" ("_position" j') ("_position" j))) ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" A) ### ("\<^const>Matrix.vec_index" ("_position" i') ### ("_position" j')))))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.eq" ### ("_applC" ("_position" erase_mat) ### ("_cargs" ("_position" A) ("_cargs" ("_position" i) ("_position" j)))) ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" i') ### ("\<^const>Finite_Cartesian_Product.vec.vec_lambda_binder" ### ("_position" j') ### ("\<^const>HOL.If" ### ("\<^const>HOL.disj" ### ("\<^const>HOL.eq" ("_position" i') ("_position" i)) ### ("\<^const>HOL.eq" ("_position" j') ("_position" j))) ### ("\<^const>Groups.zero_class.zero") ### ("\<^const>Matrix.vec_index" ### ("\<^const>Matrix.vec_index" ("_position" A) ("_position" i')) ### ("_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. ### theory "Perron_Frobenius.HMA_Connect" ### 4.314s elapsed time, 8.504s cpu time, 0.228s GC time class conjugatable_ring_1_abs_real_line = conjugatable_ring + ring_1_abs_real_line + assumes "sq_norm_as_sq_abs": "\a. a * conjugate a = \a\\<^sup>2" ### Ignoring duplicate rewrite rule: ### f (0::'a) \ 0::'b ### Ignoring duplicate rewrite rule: ### f (0::'a) \ 0::'b ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (\a. [:a:])) ?X1) ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (\a. [:a:])) ?X1) ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (\a. [:a:])) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (\a. [:a:])) [:?a1:] \ ### [:map_poly (\a. [:a:]) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'c1)) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (pCons (0::?'c1))) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (pCons (0::?'c1))) [:?a1:] \ ### [:map_poly (pCons (0::?'c1)) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?i1) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (\x. monom x ?i1)) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (\x. monom x ?i1)) [:?a1:] \ ### [:map_poly (\x. monom x ?i1) ?a1:] ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'b1)) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (pCons (0::?'b1))) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (pCons (0::?'b1))) [:?a1:] \ ### [:map_poly (pCons (0::?'b1)) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?i1) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (\x. monom x ?i1)) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (\x. monom x ?i1)) [:?a1:] \ ### [:map_poly (\x. monom x ?i1) ?a1:] ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### poly_y_x (sum_mset ?X1) \ sum_mset (image_mset poly_y_x ?X1) ### Ignoring duplicate rewrite rule: ### map_poly poly_y_x [:?a1:] \ [:poly_y_x ?a1:] ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### poly_y_x (sum_mset ?X1) \ sum_mset (image_mset poly_y_x ?X1) ### Ignoring duplicate rewrite rule: ### map_poly poly_y_x [:?a1:] \ [:poly_y_x ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?i1) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (\x. monom x ?i1)) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (\x. monom x ?i1)) [:?a1:] \ ### [:map_poly (\x. monom x ?i1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'d1)) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (pCons (0::?'d1))) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (pCons (0::?'d1))) [:?a1:] \ ### [:map_poly (pCons (0::?'d1)) ?a1:] ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### poly_y_x (sum_mset ?X1) \ sum_mset (image_mset poly_y_x ?X1) ### Ignoring duplicate rewrite rule: ### map_poly poly_y_x [:?a1:] \ [:poly_y_x ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) (sum_mset ?X1) \ ### sum_mset (image_mset (map_poly (( * ) ?c1)) ?X1) ### Ignoring duplicate rewrite rule: ### map_poly (map_poly (( * ) ?c1)) [:?a1:] \ ### [:map_poly (( * ) ?c1) ?a1:] ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### poly_y_x (sum_mset ?X1) \ sum_mset (image_mset poly_y_x ?X1) ### Ignoring duplicate rewrite rule: ### map_poly poly_y_x [:?a1:] \ [:poly_y_x ?a1:] ### Ignoring duplicate rewrite rule: ### of_int (sum_mset ?X1) \ sum_mset (image_mset of_int ?X1) ### Ignoring duplicate rewrite rule: ### of_rat (sum_mset ?X1) \ sum_mset (image_mset of_rat ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 + ?y1) \ of_real ?x1 + of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (sum_mset ?X1) \ sum_mset (image_mset of_real ?X1) ### Ignoring duplicate rewrite rule: ### of_real (?x1 * ?y1) \ of_real ?x1 * of_real ?y1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 ^ ?n1) \ of_real ?x1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### of_real (- ?x1) \ - of_real ?x1 ### Ignoring duplicate rewrite rule: ### of_real (?x1 - ?y1) \ of_real ?x1 - of_real ?y1 ### Ignoring duplicate rewrite rule: ### ?c1 * sum_mset ?X1 \ sum_mset (image_mset (( * ) ?c1) ?X1) ### Ignoring duplicate rewrite rule: ### poly (sum_mset ?X1) ?a1 \ \p\#?X1. poly p ?a1 ### Ignoring duplicate rewrite rule: ### sum_mset ?X1 \\<^sub>p ?p1 \ ### \q\#?X1. q \\<^sub>p ?p1 ### Ignoring duplicate rewrite rule: ### of_int_poly (sum_mset ?X1) \ sum_mset (image_mset of_int_poly ?X1) ### Ignoring duplicate rewrite rule: ### pCons (0::?'a1) (sum_mset ?X1) \ ### sum_mset (image_mset (pCons (0::?'a1)) ?X1) ### Ignoring duplicate rewrite rule: ### monom (sum_mset ?X1) ?d1 \ \x\#?X1. monom x ?d1 ### Ignoring duplicate rewrite rule: ### [:sum_mset ?X1:] \ \a\#?X1. [:a:] ### Ignoring duplicate rewrite rule: ### to_fract (?x1 + ?y1) \ to_fract ?x1 + to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (sum_mset ?X1) \ sum_mset (image_mset to_fract ?X1) ### Ignoring duplicate rewrite rule: ### map_poly to_fract (?p1 + ?q1) \ ### map_poly to_fract ?p1 + map_poly to_fract ?q1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 * ?y1) \ to_fract ?x1 * to_fract ?y1 ### Ignoring duplicate rewrite rule: ### to_fract (- ?x1) \ - to_fract ?x1 ### Ignoring duplicate rewrite rule: ### to_fract (?x1 - ?y1) \ to_fract ?x1 - to_fract ?y1 ### Ignoring duplicate rewrite rule: ### map_poly to_fract (smult ?c1 ?p1) \ ### smult (to_fract ?c1) (map_poly to_fract ?p1) ### Ignoring duplicate rewrite rule: ### poly2 (smult ?a1 ?p1) ?x1 ?y1 \ poly ?a1 ?x1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (sum_mset ?X1) ?x1 ?y1 \ \p\#?X1. poly2 p ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly2 (pCons ?a1 ?p1) ?x1 ?y1 \ ### poly ?a1 ?x1 + ?y1 * poly2 ?p1 ?x1 ?y1 ### Ignoring duplicate rewrite rule: ### poly_lift (sum_mset ?X1) \ sum_mset (image_mset poly_lift ?X1) ### Ignoring duplicate rewrite rule: ### map_poly of_int_poly [:?a1:] \ [:of_int_poly ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (pCons (0::?'a1)) [:?a1:] \ [:pCons (0::?'a1) ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly2 p ?x1 ?y1) [:?a1:] \ ### [:poly2 ?a1 ?x1 ?y1:] ### Ignoring duplicate rewrite rule: ### map_poly (\q. q \\<^sub>p ?p1) [:?a1:] \ ### [:?a1 \\<^sub>p ?p1:] ### Ignoring duplicate rewrite rule: ### map_poly (\x. monom x ?d1) [:?a1:] \ [:monom ?a1 ?d1:] ### Ignoring duplicate rewrite rule: ### map_poly (\p. poly p ?aa1) [:?a1:] \ [:poly ?a1 ?aa1:] ### Ignoring duplicate rewrite rule: ### map_poly (\a. [:a:]) [:?a1:] \ [:[:?a1:]:] ### Ignoring duplicate rewrite rule: ### map_poly (( * ) ?c1) [:?a1:] \ [:?c1 * ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly poly_lift [:?a1:] \ [:poly_lift ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_rat [:?a1:] \ [:of_rat ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly to_fract [:?a1:] \ [:to_fract ?a1:] ### Ignoring duplicate rewrite rule: ### map_poly of_real [:?a1:] \ [:of_real ?a1:] ### Ignoring duplicate rewrite rule: ### of_int_poly [:?a1:] \ [:of_int ?a1:] ### Ignoring duplicate rewrite rule: ### poly_y_x (sum_mset ?X1) \ sum_mset (image_mset poly_y_x ?X1) ### Ignoring duplicate rewrite rule: ### map_poly poly_y_x [:?a1:] \ [:poly_y_x ?a1:] class trivial_conjugatable_ordered_field = conjugatable_ordered_field + linordered_idom + assumes "conjugate_id": "\x. conjugate x = x" ### theory "LLL_Basis_Reduction.Norms" ### 22.541s elapsed time, 45.372s cpu time, 8.760s GC time Loading theory "LLL_Basis_Reduction.Int_Rat_Operations" (required by "LLL_Basis_Reduction.Gram_Schmidt_2") ### theory "LLL_Basis_Reduction.Int_Rat_Operations" ### 0.466s elapsed time, 0.852s cpu time, 0.352s GC time Loading theory "LLL_Basis_Reduction.Gram_Schmidt_2" ### Ignoring duplicate rewrite rule: ### p.dim UNIV \ card Basis_pair ### Ignoring duplicate rewrite rule: ### vs1.dim UNIV \ card B1 ### Ignoring duplicate rewrite rule: ### vs2.dim UNIV \ card B2 ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \ (1::?'a1) + of_nat ?m1 locale vec_module fixes f_ty :: "'a itself" and n :: "nat" ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 locale vec_space fixes f_ty :: "'a itself" and n :: "nat" locale cof_vec_space fixes n :: "nat" and f_ty :: "'a itself" ### Ignoring duplicate rewrite rule: ### \x\?A1. ?y1 \ ?y1 ^ card ?A1 locale gram_schmidt fixes n :: "nat" and f_ty :: "'a itself" Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" Found termination order: "(\p. length (snd p)) <*mlex*> {}" ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) locale gram_schmidt_fs fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" Found termination order: "case_sum size (\p. size (snd p)) <*mlex*> case_sum size (\p. size (fst p)) <*mlex*> {}" locale gram_schmidt_fs_Rn fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_Rn n fs" locale gram_schmidt_fs_lin_indpt fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_lin_indpt n fs" ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) locale gram_schmidt_fs_int fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_int n fs" locale gram_schmidt fixes n :: "nat" and f_ty :: "'a itself" Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" Found termination order: "(\p. length (snd (snd p))) <*mlex*> {}" locale gram_schmidt fixes n :: "nat" and f_ty :: "'a itself" Found termination order: "(\p. size_list size (fst (snd p))) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### ?y1 \ ball ?x1 ?e1 \ dist ?x1 ?y1 < ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ ball ?x1 ?e1 \ dist ?x1 ?y1 < ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ ball ?x1 ?e1 \ dist ?x1 ?y1 < ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ ball ?x1 ?e1 \ dist ?x1 ?y1 < ?e1 Found termination order: "(\p. length (fst p)) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### ?y1 \ cball ?x1 ?e1 \ dist ?x1 ?y1 \ ?e1 ### Ignoring duplicate rewrite rule: ### ?y1 \ ball ?x1 ?e1 \ dist ?x1 ?y1 < ?e1 ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True Found termination order: "(\p. size_list size (fst (snd p))) <*mlex*> {}" Found termination order: "(\p. length (fst (snd p))) <*mlex*> {}" locale gram_schmidt_fs_Rn fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_Rn n fs" ### Ignoring duplicate rewrite rule: ### 0 < dist ?x1 ?y1 \ ?x1 \ ?y1 locale fs_int fixes n :: "nat" and fs_init :: "int vec list" ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate rewrite rule: ### sup ?x1 (- ?x1) \ top locale fs_int_indpt fixes n :: "nat" and fs :: "int vec list" assumes "fs_int_indpt n fs" ### Rule already declared as introduction (intro) ### countable ?A \ countable (?f ` ?A) ### Rule already declared as introduction (intro) ### \countable ?I; ### \i. i \ ?I \ countable (?A i)\ ### \ countable (Sigma ?I ?A) ### Rule already declared as introduction (intro) ### \countable ?I; ### \i. i \ ?I \ countable (?A i)\ ### \ countable (\i\?I. ?A i) locale gram_schmidt_fs_lin_indpt fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_lin_indpt n fs" ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True locale gram_schmidt_fs_int fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_int n fs" ### Rule already declared as introduction (intro) ### ?P ?x \ \x. ?P x ### Ignoring duplicate rewrite rule: ### of_nat (Suc ?m1) \ (1::?'a1) + of_nat ?m1 ### theory "LLL_Basis_Reduction.Gram_Schmidt_2" ### 45.196s elapsed time, 89.384s cpu time, 5.452s GC time Loading theory "LLL_Basis_Reduction.Gram_Schmidt_Int" (required by "LLL_Basis_Reduction.LLL_Mu_Integer_Impl") Loading theory "LLL_Basis_Reduction.LLL" Found termination order: "(\p. size (snd (snd (snd (snd p))))) <*mlex*> {}" locale LLL fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" locale fs_int' fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" and upw :: "bool" and i :: "nat" and fs :: "int vec list" assumes "fs_int' n m fs_init \ upw i fs" locale gram_schmidt_fs_lin_indpt fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_lin_indpt n fs" locale gram_schmidt_fs_lin_indpt fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_lin_indpt n fs" Found termination order: "(\p. size (fst p)) <*mlex*> {}" locale LLL fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" locale gram_schmidt_fs_int fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_int n fs" locale fs_int_indpt fixes n :: "nat" and fs :: "int vec list" assumes "fs_int_indpt n fs" locale LLL_with_assms fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" assumes "LLL_with_assms n m fs_init \" Found termination order: "case_sum (\p. size (fst p)) (\p. size (snd p)) <*mlex*> case_sum (\x. Suc 0) (\x. 0) <*mlex*> {}" Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" ### theory "LLL_Basis_Reduction.LLL" ### 12.762s elapsed time, 25.296s cpu time, 1.744s GC time Loading theory "LLL_Basis_Reduction.LLL_GSO_Impl" locale gram_schmidt_fs_int fixes n :: "nat" and f_ty :: "'a itself" and fs :: "'a vec list" assumes "gram_schmidt_fs_int n fs" ### theory "LLL_Basis_Reduction.Gram_Schmidt_Int" ### 13.377s elapsed time, 26.528s cpu time, 1.744s GC time Loading theory "LLL_Basis_Reduction.LLL_Number_Bounds" (required by "LLL_Basis_Reduction.LLL_Mu_Integer_Impl" via "LLL_Basis_Reduction.LLL_Integer_Equations") Found termination order: "(\p. size_list (\p. size (snd p)) (snd p)) <*mlex*> {}" locale LLL fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" locale LLL fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" locale LLL_with_assms fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" assumes "LLL_with_assms n m fs_init \" Found termination order: "{}" locale LLL_with_assms fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" assumes "LLL_with_assms n m fs_init \" ### theory "LLL_Basis_Reduction.LLL_GSO_Impl" ### 8.132s elapsed time, 16.116s cpu time, 1.228s GC time Loading theory "LLL_Basis_Reduction.LLL_GSO_Impl_Complexity" ### theory "LLL_Basis_Reduction.LLL_Number_Bounds" ### 7.608s elapsed time, 15.064s cpu time, 1.228s GC time Loading theory "LLL_Basis_Reduction.LLL_Integer_Equations" (required by "LLL_Basis_Reduction.LLL_Mu_Integer_Impl") locale LLL fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" locale LLL_with_assms fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" assumes "LLL_with_assms n m fs_init \" Found termination order: "(\p. size_list (\p. size (snd p)) (snd p)) <*mlex*> {}" Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" Found termination order: "(\p. length (snd p)) <*mlex*> {}" locale LLL_with_assms fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" assumes "LLL_with_assms n m fs_init \" ### theory "LLL_Basis_Reduction.LLL_Integer_Equations" ### 6.609s elapsed time, 13.092s cpu time, 1.128s GC time Loading theory "LLL_Basis_Reduction.LLL_Mu_Integer_Impl" ### theory "LLL_Basis_Reduction.LLL_GSO_Impl_Complexity" ### 6.666s elapsed time, 13.208s cpu time, 1.128s GC time ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "{}" Found termination order: "(\p. length (snd (snd (snd (snd p))))) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True locale LLL fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" Found termination order: "{}" ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) locale LLL_with_assms fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" assumes "LLL_with_assms n m fs_init \" ### theory "LLL_Basis_Reduction.LLL_Mu_Integer_Impl" ### 18.948s elapsed time, 37.576s cpu time, 1.728s GC time Loading theory "LLL_Basis_Reduction.LLL_Mu_Integer_Impl_Complexity" ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### cbox ?a1 ?a1 \ {?a1} locale LLL_with_assms fixes n :: "nat" and m :: "nat" and fs_init :: "int vec list" and \ :: "rat" assumes "LLL_with_assms n m fs_init \" ### Ignoring duplicate rewrite rule: ### open {} \ True ### Ignoring duplicate rewrite rule: ### closed {} \ True ### Ignoring duplicate rewrite rule: ### closed UNIV \ True ### Ignoring duplicate rewrite rule: ### closed ?S1 \ closed (insert ?a1 ?S1) \ True ### Ignoring duplicate rewrite rule: ### open {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### open {.. True ### Ignoring duplicate rewrite rule: ### open {?a1<.. True ### Ignoring duplicate rewrite rule: ### closed {..?a1} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 id \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous bot ?f1 \ True ### Ignoring duplicate rewrite rule: ### continuous (at ?x1 within ?S1) (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; ?f1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. inverse (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. ?f1 x / ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \ 1; ### 0 < ?g1 ?a1\ ### \ isCont (\x. log (?f1 x) (?g1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \ 0\ ### \ isCont (\x. ?f1 x powr ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; cos (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. tan (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; sin (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. cot (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 ?g1 \ ### continuous ?F1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 ?g1 \ ### continuous_on ?s1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True Found termination order: "(\p. length (snd (snd (snd p)))) <*mlex*> {}" Found termination order: "(\p. size (snd (snd (snd (snd p))))) <*mlex*> {}" ### Ignoring duplicate rewrite rule: ### open {} \ True ### Ignoring duplicate rewrite rule: ### closed {} \ True ### Ignoring duplicate rewrite rule: ### closed UNIV \ True ### Ignoring duplicate rewrite rule: ### closed ?S1 \ closed (insert ?a1 ?S1) \ True ### Ignoring duplicate rewrite rule: ### open {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### open {.. True ### Ignoring duplicate rewrite rule: ### open {?a1<.. True ### Ignoring duplicate rewrite rule: ### closed {..?a1} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 id \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous bot ?f1 \ True ### Ignoring duplicate rewrite rule: ### continuous (at ?x1 within ?S1) (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; ?f1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. inverse (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. ?f1 x / ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \ 1; ### 0 < ?g1 ?a1\ ### \ isCont (\x. log (?f1 x) (?g1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \ 0\ ### \ isCont (\x. ?f1 x powr ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; cos (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. tan (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; sin (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. cot (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 ?g1 \ ### continuous ?F1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 ?g1 \ ### continuous_on ?s1 (\x. cnj (?g1 x)) \ True ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### theory "LLL_Basis_Reduction.LLL_Mu_Integer_Impl_Complexity" ### 7.046s elapsed time, 13.860s cpu time, 0.764s GC time ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### subspace (span ?S1) \ True ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g ### Ignoring duplicate rewrite rule: ### (\i. ### i \ Basis \ ### ?a1 \ i \ ?b1 \ i) \ ### clamp ?a1 ?b1 ?x1 \ cbox ?a1 ?b1 \ True ### Ignoring duplicate rewrite rule: ### dim UNIV \ DIM(?'a1) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate rewrite rule: ### convex {?a1..} \ True ### Ignoring duplicate rewrite rule: ### convex {..?b1} \ True ### Ignoring duplicate rewrite rule: ### convex {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### convex {.. True ### Ignoring duplicate rewrite rule: ### convex {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### convex {?a1<..?b1} \ True ### Ignoring duplicate rewrite rule: ### convex {?a1.. True ### Ignoring duplicate rewrite rule: ### convex {?a1<.. True ### Ignoring duplicate rewrite rule: ### convex (convex hull ?s1) \ True ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### interior (cbox ?a1 ?b1) \ box ?a1 ?b1 ### Rule already declared as introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Metis: Unused theorems: "Convex_Euclidean_Space.closest_point_exists_2" ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### \finite ?A1; ?A1 \ {}\ ### \ ?x1 < Min ?A1 \ \a\?A1. ?x1 < a ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### aff_dim UNIV \ int DIM(?'n1) ### Ignoring duplicate rewrite rule: ### rel_interior {} \ {} ### Ignoring duplicate rewrite rule: ### rel_interior {} \ {} ### Ignoring duplicate rewrite rule: ### affine hull (convex hull ?S1) \ affine hull ?S1 ### Ignoring duplicate rewrite rule: ### affine hull (convex hull ?S1) \ affine hull ?S1 ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Rewrite rule not in simpset: ### numeral ?w1 \ ?b1 / ?c1 \ ### if (0::?'a1) < ?c1 then numeral ?w1 * ?c1 \ ?b1 ### else if ?c1 < (0::?'a1) then ?b1 \ numeral ?w1 * ?c1 ### else numeral ?w1 \ (0::?'a1) ### Rewrite rule not in simpset: ### - numeral ?w1 \ ?b1 / ?c1 \ ### if (0::?'a1) < ?c1 then - numeral ?w1 * ?c1 \ ?b1 ### else if ?c1 < (0::?'a1) then ?b1 \ - numeral ?w1 * ?c1 ### else - numeral ?w1 \ (0::?'a1) ### Rewrite rule not in simpset: ### ?b1 / ?c1 \ numeral ?w1 \ ### if (0::?'a1) < ?c1 then ?b1 \ numeral ?w1 * ?c1 ### else if ?c1 < (0::?'a1) then numeral ?w1 * ?c1 \ ?b1 ### else (0::?'a1) \ numeral ?w1 ### Rewrite rule not in simpset: ### ?b1 / ?c1 \ - numeral ?w1 \ ### if (0::?'a1) < ?c1 then ?b1 \ - numeral ?w1 * ?c1 ### else if ?c1 < (0::?'a1) then - numeral ?w1 * ?c1 \ ?b1 ### else (0::?'a1) \ - numeral ?w1 ### Rewrite rule not in simpset: ### numeral ?w1 < ?b1 / ?c1 \ ### if (0::?'a1) < ?c1 then numeral ?w1 * ?c1 < ?b1 ### else if ?c1 < (0::?'a1) then ?b1 < numeral ?w1 * ?c1 ### else numeral ?w1 < (0::?'a1) ### Rewrite rule not in simpset: ### - numeral ?w1 < ?b1 / ?c1 \ ### if (0::?'a1) < ?c1 then - numeral ?w1 * ?c1 < ?b1 ### else if ?c1 < (0::?'a1) then ?b1 < - numeral ?w1 * ?c1 ### else - numeral ?w1 < (0::?'a1) ### Rewrite rule not in simpset: ### ?b1 / ?c1 < numeral ?w1 \ ### if (0::?'a1) < ?c1 then ?b1 < numeral ?w1 * ?c1 ### else if ?c1 < (0::?'a1) then numeral ?w1 * ?c1 < ?b1 ### else (0::?'a1) < numeral ?w1 ### Rewrite rule not in simpset: ### ?b1 / ?c1 < - numeral ?w1 \ ### if (0::?'a1) < ?c1 then ?b1 < - numeral ?w1 * ?c1 ### else if ?c1 < (0::?'a1) then - numeral ?w1 * ?c1 < ?b1 ### else (0::?'a1) < - numeral ?w1 ### Rewrite rule not in simpset: ### numeral ?w1 = ?b1 / ?c1 \ ### if ?c1 \ (0::?'a1) then numeral ?w1 * ?c1 = ?b1 ### else numeral ?w1 = (0::?'a1) ### Rewrite rule not in simpset: ### - numeral ?w1 = ?b1 / ?c1 \ ### if ?c1 \ (0::?'a1) then - numeral ?w1 * ?c1 = ?b1 ### else - numeral ?w1 = (0::?'a1) ### Rewrite rule not in simpset: ### ?b1 / ?c1 = numeral ?w1 \ ### if ?c1 \ (0::?'a1) then ?b1 = numeral ?w1 * ?c1 ### else numeral ?w1 = (0::?'a1) ### Rewrite rule not in simpset: ### ?b1 / ?c1 = - numeral ?w1 \ ### if ?c1 \ (0::?'a1) then ?b1 = - numeral ?w1 * ?c1 ### else - numeral ?w1 = (0::?'a1) ### Rewrite rule not in simpset: ### (1::?'a1) \ ?b1 / ?a1 \ ### (0::?'a1) < ?a1 \ ?a1 \ ?b1 \ ### ?a1 < (0::?'a1) \ ?b1 \ ?a1 ### Rewrite rule not in simpset: ### ?b1 / ?a1 \ (1::?'a1) \ ### (0::?'a1) < ?a1 \ ?b1 \ ?a1 \ ### ?a1 < (0::?'a1) \ ?a1 \ ?b1 \ ?a1 = (0::?'a1) ### Rewrite rule not in simpset: ### (1::?'a1) < ?b1 / ?a1 \ ### (0::?'a1) < ?a1 \ ?a1 < ?b1 \ ?a1 < (0::?'a1) \ ?b1 < ?a1 ### Rewrite rule not in simpset: ### ?b1 / ?a1 < (1::?'a1) \ ### (0::?'a1) < ?a1 \ ?b1 < ?a1 \ ### ?a1 < (0::?'a1) \ ?a1 < ?b1 \ ?a1 = (0::?'a1) ### Ignoring duplicate rewrite rule: ### ?x1 = (?u1 / ?v1) *\<^sub>R ?a1 \ ### if ?v1 = 0 then ?x1 = (0::?'a1) else ?v1 *\<^sub>R ?x1 = ?u1 *\<^sub>R ?a1 ### Ignoring duplicate rewrite rule: ### open {} \ True ### Ignoring duplicate rewrite rule: ### closed {} \ True ### Ignoring duplicate rewrite rule: ### closed UNIV \ True ### Ignoring duplicate rewrite rule: ### closed ?S1 \ closed (insert ?a1 ?S1) \ True ### Ignoring duplicate rewrite rule: ### open {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### open {.. True ### Ignoring duplicate rewrite rule: ### open {?a1<.. True ### Ignoring duplicate rewrite rule: ### closed {..?a1} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 id \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous bot ?f1 \ True ### Ignoring duplicate rewrite rule: ### continuous (at ?x1 within ?S1) (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; ?f1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. inverse (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. ?f1 x / ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \ 1; ### 0 < ?g1 ?a1\ ### \ isCont (\x. log (?f1 x) (?g1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \ 0\ ### \ isCont (\x. ?f1 x powr ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; cos (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. tan (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; sin (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. cot (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 ?g1 \ ### continuous ?F1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 ?g1 \ ### continuous_on ?s1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### closure ?S1 = {} \ ?S1 = {} ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### aff_dim UNIV \ int DIM(?'n1) ### Ignoring duplicate rewrite rule: ### aff_dim (affine hull ?S1) \ aff_dim ?S1 ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### subspace (span ?S1) \ True ### Ignoring duplicate rewrite rule: ### ?a1 \ (0::?'a1) \ ### aff_dim {x. ?a1 \ x = ?r1} \ int (DIM(?'a1) - 1) ### Ignoring duplicate rewrite rule: ### ?a1 \ (0::?'a1) \ ### aff_dim {x. ?a1 \ x = ?r1} \ int (DIM(?'a1) - 1) ### Ignoring duplicate rewrite rule: ### affine_dependent {?a1, ?b1} \ False ### Metis: Unused theorems: "local.sumSS'_2" ### Ignoring duplicate rewrite rule: ### aff_dim UNIV \ int DIM(?'n1) ### Metis: Unused theorems: "local.sumSS'_1" ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### span UNIV \ UNIV ### Ignoring duplicate rewrite rule: ### dim UNIV \ DIM(?'a1) ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### subspace (span ?S1) \ True ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### subspace (span ?S1) \ True ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### 0 \ setdist ?s1 ?t1 \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### 0 \ setdist ?s1 ?t1 \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Metis: Unused theorems: "Starlike.midpoint_eq_endpoint_2" ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate rewrite rule: ### pathfinish ?g1.1 = pathstart ?g2.1 \ ### path (?g1.1 +++ ?g2.1) \ path ?g1.1 \ path ?g2.1 ### Ignoring duplicate rewrite rule: ### pathfinish ?g1.1 = pathstart ?g2.1 \ ### path (?g1.1 +++ ?g2.1) \ path ?g1.1 \ path ?g2.1 ### Ignoring duplicate rewrite rule: ### pathfinish ?g1.1 = pathstart ?g2.1 \ ### path (?g1.1 +++ ?g2.1) \ path ?g1.1 \ path ?g2.1 ### Rule already declared as introduction (intro) ### \?a \ carrier R; ?x \ carrier M\ ### \ ?a \\<^bsub>M\<^esub> ?x \ carrier M ### Metis: Unused theorems: "Real.less_eq_real_def" ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate safe introduction (intro!) ### convex {?a..} ### Ignoring duplicate safe introduction (intro!) ### convex {..?b} ### Ignoring duplicate safe introduction (intro!) ### convex {?a<..} ### Ignoring duplicate safe introduction (intro!) ### convex {..x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### path_connected (path_component_set ?s1 ?x1) \ True ### Ignoring duplicate rewrite rule: ### path_connected (path_component_set ?s1 ?x1) \ True ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### path_connected {} \ True ### Ignoring duplicate rewrite rule: ### path_connected {?a1} \ True ### Ignoring duplicate rewrite rule: ### connected_component_set UNIV ?x1 \ UNIV ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Metis: Unused theorems: "Orderings.linorder_class.not_le" ### Metis: Unused theorems: "Path_Connected.path_image_reversepath" ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Metis: Unused theorems: "Path_Connected.homotopic_join_subpaths2", "Path_Connected.homotopic_join_subpaths3" ### Metis: Unused theorems: "Path_Connected.homotopic_join_subpaths3" ### Metis: Unused theorems: "Path_Connected.homotopic_join_subpaths2" ### Metis: Unused theorems: "Path_Connected.homotopic_join_subpaths2" ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### ws \ carrier_vec n \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### path_connected {} \ True ### Ignoring duplicate rewrite rule: ### open {} \ True ### Ignoring duplicate rewrite rule: ### closed {} \ True ### Ignoring duplicate rewrite rule: ### closed UNIV \ True ### Ignoring duplicate rewrite rule: ### closed ?S1 \ closed (insert ?a1 ?S1) \ True ### Ignoring duplicate rewrite rule: ### open {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### open {.. True ### Ignoring duplicate rewrite rule: ### open {?a1<.. True ### Ignoring duplicate rewrite rule: ### closed {..?a1} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 id \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous bot ?f1 \ True ### Ignoring duplicate rewrite rule: ### continuous (at ?x1 within ?S1) (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; ?f1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. inverse (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. ?f1 x / ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \ 1; ### 0 < ?g1 ?a1\ ### \ isCont (\x. log (?f1 x) (?g1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \ 0\ ### \ isCont (\x. ?f1 x powr ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; cos (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. tan (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; sin (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. cot (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 ?g1 \ ### continuous ?F1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 ?g1 \ ### continuous_on ?s1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### affine T \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate rewrite rule: ### closed (affine hull ?S1) \ True ### Ignoring duplicate rewrite rule: ### closed (affine hull ?S1) \ True ### Metis: Unused theorems: "local.b" ### Metis: Unused theorems: "local.a" ### Ignoring duplicate rewrite rule: ### open {} \ True ### Ignoring duplicate rewrite rule: ### closed {} \ True ### Ignoring duplicate rewrite rule: ### closed UNIV \ True ### Ignoring duplicate rewrite rule: ### closed ?S1 \ closed (insert ?a1 ?S1) \ True ### Ignoring duplicate rewrite rule: ### open {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### open {.. True ### Ignoring duplicate rewrite rule: ### open {?a1<.. True ### Ignoring duplicate rewrite rule: ### closed {..?a1} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 id \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous bot ?f1 \ True ### Ignoring duplicate rewrite rule: ### continuous (at ?x1 within ?S1) (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; ?f1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. inverse (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. ?f1 x / ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \ 1; ### 0 < ?g1 ?a1\ ### \ isCont (\x. log (?f1 x) (?g1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \ 0\ ### \ isCont (\x. ?f1 x powr ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; cos (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. tan (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; sin (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. cot (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 ?g1 \ ### continuous ?F1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 ?g1 \ ### continuous_on ?s1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### open {} \ True ### Ignoring duplicate rewrite rule: ### closed {} \ True ### Ignoring duplicate rewrite rule: ### closed UNIV \ True ### Ignoring duplicate rewrite rule: ### closed ?S1 \ closed (insert ?a1 ?S1) \ True ### Ignoring duplicate rewrite rule: ### open {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### open {.. True ### Ignoring duplicate rewrite rule: ### open {?a1<.. True ### Ignoring duplicate rewrite rule: ### closed {..?a1} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 id \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous bot ?f1 \ True ### Ignoring duplicate rewrite rule: ### continuous (at ?x1 within ?S1) (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; ?f1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. inverse (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \ (0::?'b1)\ ### \ isCont (\x. ?f1 x / ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \ 1; ### 0 < ?g1 ?a1\ ### \ isCont (\x. log (?f1 x) (?g1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \ 0\ ### \ isCont (\x. ?f1 x powr ?g1 x) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; cos (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. tan (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### \isCont ?f1 ?a1; sin (?f1 ?a1) \ (0::?'a1)\ ### \ isCont (\x. cot (?f1 x)) ?a1 \ True ### Ignoring duplicate rewrite rule: ### continuous ?F1 ?g1 \ ### continuous ?F1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 ?g1 \ ### continuous_on ?s1 (\x. cnj (?g1 x)) \ True ### Ignoring duplicate introduction (intro) ### open {} ### Ignoring duplicate introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### closed {} ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### closed UNIV ### Ignoring duplicate introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Ignoring duplicate introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Ignoring duplicate introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Ignoring duplicate introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Ignoring duplicate introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Ignoring duplicate introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Ignoring duplicate introduction (intro) ### closed ?S \ open (- ?S) ### Ignoring duplicate introduction (intro) ### open ?S \ closed (- ?S) ### Ignoring duplicate introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Metis: Unused theorems: "local.g_1", "local.g_2", "local.g_3", "local.g_4", "local.h_1", "local.h_2" ### Ignoring duplicate rewrite rule: ### 0 < dist ?x1 ?y1 \ ?x1 \ ?y1 ### Ignoring duplicate rewrite rule: ### 0 < dist ?x1 ?y1 \ ?x1 \ ?y1 ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### Fun.swap ?a1 ?b1 ?f1 ?a1 \ ?f1 ?b1 ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Metis: Unused theorems: "local.S_2" ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### of_nat (?m1 ^ ?n1) \ of_nat ?m1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### of_nat (?m1 ^ ?n1) \ of_nat ?m1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### closedin (subtopology ?U1 ?X1) ?X1 \ ?X1 \ topspace ?U1 ### Ignoring duplicate rewrite rule: ### closedin (subtopology ?U1 ?X1) ?X1 \ ?X1 \ topspace ?U1 ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Rule already declared as safe introduction (intro!) ### uniform_limit {} ?f ?g ?F ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Rule already declared as introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Rule already declared as introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Rule already declared as introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Rule already declared as introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Rule already declared as introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Rule already declared as introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ennreal (?f x)) \ ennreal ?x) ?F ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if ?a1 = k then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### 0 < DIM(?'a1) \ True ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?r1 *\<^sub>R ?x1 \ ?y1 \ ?r1 * (?x1 \ ?y1) ### Ignoring duplicate rewrite rule: ### ?x1 \ ?r1 *\<^sub>R ?y1 \ ?r1 * (?x1 \ ?y1) ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. open (?B x) \ ### open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. open T\ ### \ open (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. open (?B x)\ ### \ open (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### closed {} ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### closed UNIV ### Rule already declared as introduction (intro) ### \closed ?S; closed ?T\ ### \ closed (?S \ ?T) ### Rule already declared as introduction (intro) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \S\?K. closed S \ closed (\?K) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### Rule already declared as introduction (intro) ### \finite ?A; \x\?A. closed (?B x)\ ### \ closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \open ?S; closed ?T\ \ open (?S - ?T) ### Rule already declared as introduction (intro) ### \closed ?S; open ?T\ \ closed (?S - ?T) ### Rule already declared as introduction (intro) ### closed ?S \ open (- ?S) ### Rule already declared as introduction (intro) ### open ?S \ closed (- ?S) ### Rule already declared as introduction (intro) ### continuous_on ?s (linepath ?a ?b) ### Ignoring duplicate rewrite rule: ### convex (ball ?x1 ?e1) \ True ### Ignoring duplicate rewrite rule: ### finite ?S1 \ ### \k\?S1. if k = ?a1 then ?b1 k else (0::?'a1) \ ### if ?a1 \ ?S1 then ?b1 ?a1 else (0::?'a1) ### Ignoring duplicate rewrite rule: ### ?y1 \ ball ?x1 ?e1 \ dist ?x1 ?y1 < ?e1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 \ (1::?'a1) / ?a1 ### Ignoring duplicate rewrite rule: ### inverse ?a1 ^ ?n1 \ inverse (?a1 ^ ?n1) ### Ignoring duplicate rewrite rule: ### ((1::?'a1) / ?a1) ^ ?n1 \ (1::?'a1) / ?a1 ^ ?n1 ### Ignoring duplicate rewrite rule: ### (?a1 / ?b1) ^ ?n1 \ ?a1 ^ ?n1 / ?b1 ^ ?n1 ### Metis: Unused theorems: "Cartesian_Space.linear_matrix_vector_mul_eq", "Cartesian_Space.matrix_vector_mul_1", "Cartesian_Space.matrix_vector_mul_3" ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### \i. ?y $ i \ ?y ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. ?c1) \ True ### Ignoring duplicate rewrite rule: ### continuous_on ?s1 (\x. x) \ True ### Ignoring duplicate rewrite rule: ### dim (span ?S1) \ dim ?S1 ### Metis: Unused theorems: "Permutations.permutation_swap_id" ### Metis: Unused theorems: "Finite_Set.finite_class.finite_code" ### Ambiguous input (line 575 of "$AFP/Perron_Frobenius/HMA_Connect.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" from_hma\<^sub>v) ("_position" y)) ### ("_position" i)) ### ("_applC" ("_position" range) ### ("_applC" ("_position" vec_nth) ("_position" y))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>Set.member" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ### ("_applC" ("_position" from_hma\<^sub>v) ("_position" y)) ### ("_position" i)) ### ("_applC" ("_position" range) ### ("_applC" ("_position" vec_nth) ("_position" y))))) ### 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 581 of "$AFP/Perron_Frobenius/HMA_Connect.thy") produces 2 parse trees: ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" i) ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" y) ### ("_position" a)) ### ("\<^const>Matrix.vec_index" ### ("_applC" ("_position" from_hma\<^sub>v) ("_position" y)) ### ("_position" i))) ### ("\<^const>Orderings.ord_class.less" ("_position" i) ### ("_type_card" ("_position_sort" 'n)))))) ### ("\<^const>HOL.Trueprop" ### ("\<^const>HOL.Ex_binder" ("_position" i) ### ("\<^const>HOL.conj" ### ("\<^const>HOL.eq" ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ("_position" y) ### ("_position" a)) ### ("\<^const>Finite_Cartesian_Product.vec.vec_nth" ### ("_applC" ("_position" from_hma\<^sub>v) ("_position" y)) ### ("_position" i))) ### ("\<^const>Orderings.ord_class.less" ("_position" i) ### ("_type_card" ("_position_sort" 'n)))))) ### Fortunately, only one parse tree is well-formed and type-correct, ### but you may still want to disambiguate your grammar or your input. ### Rule already declared as introduction (intro) ### \\i j. ### \i < dim_row ?B; j < dim_col ?B\ ### \ ?A $$ (i, j) = ?B $$ (i, j); ### dim_row ?A = dim_row ?B; dim_col ?A = dim_col ?B\ ### \ ?A = ?B ### Rule already declared as introduction (intro) ### (\i. ### i \ ?j \ ### fs ! i \ carrier_vec n) \ ### gso ?j \ carrier_vec n ### Rule already declared as introduction (intro) ### \\i. i < dim_vec ?w \ ?v $v i = ?w $v i; ### dim_vec ?v = dim_vec ?w\ ### \ ?v = ?w ### Rule already declared as introduction (intro) ### \\i j. ### \i < dim_row ?B; j < dim_col ?B\ ### \ ?A $$ (i, j) = ?B $$ (i, j); ### dim_row ?A = dim_row ?B; dim_col ?A = dim_col ?B\ ### \ ?A = ?B linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) ### Ignoring duplicate rewrite rule: ### gs.\ 0 ?i1 ?j1 \ 0 ### Ignoring duplicate rewrite rule: ### gs.\ (Suc ?l1) ?i1 ?j1 \ ### (gs.d (Suc ?l1) * gs.\ ?l1 ?i1 ?j1 + ### gs.\' ?i1 ?l1 * gs.\' ?j1 ?l1) / ### gs.d ?l1 ### Introduced fixed type variable(s): 'a, 'b in "f__" or "x__" linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) ### Ignoring duplicate rewrite rule: ### fs.gs.\ ?i1 ?j1 \ ### if ?j1 < ?i1 ### then map of_int_hom.vec_hom fs ! ?i1 \ fs.gs.gso ?j1 / ### \fs.gs.gso ?j1\\<^sup>2 ### else if ?i1 = ?j1 then 1 else 0 linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) ### Introduced fixed type variable(s): 'a, 'b in "f__" or "x__" ### Rule already declared as introduction (intro) ### \(1::?'a) \ ?a; (1::?'a) \ ?b\ ### \ (1::?'a) \ ?a * ?b linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) "[vec_impl (Abs_vec_impl (3, IArray [0, 0, 1])), vec_impl (Abs_vec_impl (3, IArray [- 1, 1, 0])), vec_impl (Abs_vec_impl (3, IArray [2, 1, 0]))]" :: "int vec list" linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) linarith_split_limit exceeded (current value is 9) *** Failed to finish proof (line 483 of "$AFP/LLL_Basis_Reduction/LLL_Mu_Integer_Impl_Complexity.thy"): *** goal (1 subgoal): *** 1. \Suc k = m - i; i \ m\ *** \ \{Suc i..ii = Suc i..({i..ii\{i..?k \ length ?F; \i. i < length ?F \ dim_vec (?F ! i) = n\ \ gs.Gramian_determinant (map of_int_hom.vec_hom ?F) ?k = of_int (gs.Gramian_determinant ?F ?k) Gram_Schmidt_2.fs_int.of_int_Gramian_determinant: \?k \ length ?F; \i. i < length ?F \ dim_vec (?F ! i) = ?n\ \ gram_schmidt.Gramian_determinant ?n (map of_int_hom.vec_hom ?F) ?k = of_int (gram_schmidt.Gramian_determinant ?n ?F ?k) isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction/document -o pdf -n document isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LLL_Basis_Reduction/outline -o pdf -n outline -t /proof,/ML *** Failed to finish proof (line 483 of "$AFP/LLL_Basis_Reduction/LLL_Mu_Integer_Impl_Complexity.thy"): *** goal (1 subgoal): *** 1. \Suc k = m - i; i \ m\ *** \ \{Suc i..ii = Suc i..({i..ii\{i..