Loading theory "HOL-Eisbach.Eisbach" (required by "HOL-Eisbach.Eisbach_Tools") Loading theory "Sturm_Tarski.PolyMisc" (required by "Sturm_Tarski.Sturm_Tarski") 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 ### theory "Sturm_Tarski.PolyMisc" ### 0.161s elapsed time, 0.320s cpu time, 0.000s GC time Loading theory "Sturm_Tarski.Sturm_Tarski" structure Eisbach_Rule_Insts: sig end ### 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 ### theory "HOL-Eisbach.Eisbach" ### 0.584s elapsed time, 1.168s cpu time, 0.000s GC time Loading theory "HOL-Eisbach.Eisbach_Tools" val try_map = fn: 'a Seq.seq -> 'a Seq.seq -> 'a Seq.seq val uncurry_rule = fn: thm -> thm val curry_rule = fn: thm -> thm ### theory "HOL-Eisbach.Eisbach_Tools" ### 0.052s elapsed time, 0.108s cpu time, 0.000s GC time Found termination order: "length <*mlex*> {}" ### theory "Sturm_Tarski.Sturm_Tarski" ### 1.731s elapsed time, 3.536s cpu time, 0.188s GC time ### Metis: Unused theorems: "List.list.inject" Loading theory "Winding_Number_Eval.Missing_Analysis" (required by "Winding_Number_Eval.Winding_Number_Eval" via "Winding_Number_Eval.Cauchy_Index_Theorem") Loading theory "Winding_Number_Eval.Missing_Topology" (required by "Winding_Number_Eval.Winding_Number_Eval" via "Winding_Number_Eval.Cauchy_Index_Theorem" via "Winding_Number_Eval.Missing_Transcendental") ### theory "Winding_Number_Eval.Missing_Analysis" ### 0.207s elapsed time, 0.528s cpu time, 0.000s GC time ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### theory "Winding_Number_Eval.Missing_Topology" ### 0.639s elapsed time, 1.324s cpu time, 0.108s GC time Loading theory "Winding_Number_Eval.Missing_Algebraic" (required by "Winding_Number_Eval.Winding_Number_Eval" via "Winding_Number_Eval.Cauchy_Index_Theorem" via "Winding_Number_Eval.Missing_Transcendental") ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Ignoring duplicate introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Ignoring duplicate introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### theory "Winding_Number_Eval.Missing_Algebraic" ### 2.015s elapsed time, 4.040s cpu time, 0.000s GC time Loading theory "Winding_Number_Eval.Missing_Transcendental" (required by "Winding_Number_Eval.Winding_Number_Eval" via "Winding_Number_Eval.Cauchy_Index_Theorem") ### theory "Winding_Number_Eval.Missing_Transcendental" ### 0.239s elapsed time, 0.476s cpu time, 0.000s GC time Loading theory "Winding_Number_Eval.Cauchy_Index_Theorem" (required by "Winding_Number_Eval.Winding_Number_Eval") ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Ignoring duplicate introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Ignoring duplicate introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F Proofs for inductive predicate(s) "finite_Psegments" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### 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 ### 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 ### theory "Winding_Number_Eval.Cauchy_Index_Theorem" ### 3.797s elapsed time, 7.564s cpu time, 0.316s GC time Loading theory "Winding_Number_Eval.Winding_Number_Eval" ### theory "Winding_Number_Eval.Winding_Number_Eval" ### 1.480s elapsed time, 2.928s cpu time, 0.264s GC time Loading theory "Winding_Number_Eval.Winding_Number_Eval_Examples" ### theory "Winding_Number_Eval.Winding_Number_Eval_Examples" ### 0.116s elapsed time, 0.232s cpu time, 0.000s GC time ### Metis: Unused theorems: "local.assms_3" ### 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 ### 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 ### 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 ### Ignoring duplicate rewrite rule: ### sgn (?a1 / ?b1) \ sgn ?a1 / sgn ?b1 ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Ignoring duplicate introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Ignoring duplicate introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Ignoring duplicate introduction (intro) ### ((\x. x) \ ?a) (at ?a within ?s) ### Ignoring duplicate introduction (intro) ### ((\x. ?k) \ ?k) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. ereal (?f x)) \ ereal ?x) ?F ### Ignoring duplicate introduction (intro) ### (?f \ ?x) ?F \ ### ((\x. - ?f x) \ - ?x) ?F ### Ignoring duplicate introduction (intro) ### \\?c\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?x \ 0; (?f \ ?x) ?F\ ### \ ((\x. ?c * ?f x) \ ?c * ?x) ?F ### Ignoring duplicate introduction (intro) ### \?y \ - \; ?x \ - \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Ignoring duplicate introduction (intro) ### \\?y\ \ \; ### (?f \ ?x) ?F\ ### \ ((\x. ?f x + ?y) \ ?x + ?y) ?F ### Metis: Unused theorems: "Cauchy_Index_Theorem.sgnx_able_poly_3", "Cauchy_Index_Theorem.sgnx_able_poly_4" ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f *** Undefined fact: "isCont_inverse" (line 2371 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy") *** At command "by" (line 2371 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy") ### Ignoring duplicate elimination (elim) ### \filterlim ?f at_top ?F; filterlim ?f at_bot ?F; ### ?F \ bot\ ### \ False ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f *** Undefined fact: "at_within_closed_interval" (line 2646 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy") *** At command "by" (line 2646 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy") ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Rewrite rule not in simpset: ### Complex ?a1 ?b1 \ complex_of_real ?a1 + \ * complex_of_real ?b1 ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Ignoring duplicate rewrite rule: ### path (\t. ?g1 t - ?z1) \ path ?g1 ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Ignoring duplicate rewrite rule: ### path (\t. ?g1 t - ?z1) \ path ?g1 ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### 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) ### \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) ### \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) ### \x\?A. closed (?B x) \ ### closed (\x\?A. ?B x) ### Rule already declared as introduction (intro) ### \finite ?S; \T\?S. closed T\ ### \ closed (\?S) ### 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) ### \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) ### continuous_on ?s (linepath ?a ?b) ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### Rule already declared as introduction (intro) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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) ### (\i. continuous_on UNIV (\x. ?f x i)) \ ### continuous_on UNIV ?f ### 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 isabelle document -o 'pdf' -n 'document' -t '' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Winding_Number_Eval/document 2>&1 isabelle document -o 'pdf' -n 'outline' -t '/proof,/ML' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Winding_Number_Eval/outline 2>&1 This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode LaTeX2e <2016/02/01> Babel <3.9q> and hyphenation patterns for 81 language(s) loaded. (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2014/09/29 v1.4h Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory' Including comment 'isatagtheory' Including comment 'isadelimproof' Including comment 'isatagproof' Including comment 'isadelimML' Including comment 'isatagML' Including comment 'isadelimvisible' Including comment 'isatagvisible' Excluding comment 'isadeliminvisible' Excluding comment 'isataginvisible') (./isabelletags.sty Including comment 'isadelimproof' Excluding comment 'isatagproof' Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) Package hyperref Message: Driver (autodetected): hpdftex. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) No file root.aux. (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) LaTeX Warning: Citation `eisermann2012fundamental' on page 1 undefined on input line 21. LaTeX Warning: Citation `rahman2002analytic' on page 1 undefined on input line 21. (./session.tex (./Missing_Topology.tex [1{/var/lib/texmf/fonts/map/pdftex/updma p/pdftex.map}] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. [2] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. [3] [4] [5] Overfull \hbox (30.33867pt too wide) in paragraph at lines 1775--1777 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 uniform[]discrete[]subset$\OT1/cmr/ m/n/10 [$\OT1/cmr/m/it/10 elim$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 uniform[] discrete S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 T $\OMS/cms y/m/n/10 ^^R$ \OT1/cmr/m/it/10 S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/c mr/m/it/10 uniform[]discrete [6]) (./Missing_Algebraic.tex [7] Overfull \hbox (5.7285pt too wide) in paragraph at lines 204--206 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 continuous[]on[]poly $\OT1/cmr/m/n/ 10 [$\OT1/cmr/m/it/10 continuous[]intros$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 continuous[]on s f $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 co ntinuous[]on [8] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. [9] [10] [11] [12]) (./Missing_Transcendental.tex [13] [14]) (./Missing_Analysis.tex [15] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. [16]) (./Cauchy_Index_Theorem.tex) (./Winding_Number_Eval.tex Overfull \hbox (5.34778pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Evaluate wind-ing num-bers by cal-cu-lat-ing Cauchy [17] Overfull \hbox (59.50618pt too wide) in paragraph at lines 723--723 []\OT1/cmr/bx/n/12 More lem-mas re-lated \OT1/cmr/m/it/12 cindex[]pathE \OT1/cm r/bx/n/12 / \OT1/cmr/m/it/12 jumpF[]pathstart \OT1/cmr/bx/n/12 / \OT1/cmr/m/it/ 12 jumpF[]pathfinish Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Overfull \hbox (5.14441pt too wide) in paragraph at lines 2156--2157 [][] \OT1/cmr/m/it/10 c3 $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 Im$\OT1/cm r/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/ m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$+$\OT1/cmr/m /it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n /10 ^^C$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/1 0 )$$+$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^ @$ \OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$ \OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\ OT1/cmr/m/n/10 )$ [18] [19] [20] Overfull \hbox (33.49898pt too wide) in paragraph at lines 5661--5664 []\OT1/cmr/m/n/10.95 The method "eval[]winding" \OT1/cmr/m/it/10.95 1$\OT1/cmr/ m/n/10.95 :$$:$$ [] $\OT1/cmr/m/it/10.95 a \OT1/cmr/m/n/10.95 will try to sim-p lify of the form \OT1/cmr/m/it/10.95 winding[]number ) (./Winding_Number_Eval_Examples.tex Overfull \hbox (5.94653pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Some ex-am-ples of ap-ply the method wind-ing[]eval [21])) No file root.bbl. [22] (./root.aux) Package rerunfilecheck Warning: File `root.out' has changed. (rerunfilecheck) Rerun to get outlines right (rerunfilecheck) or use package `bookmark'. LaTeX Warning: There were undefined references. ) (see the transcript file for additional information) Output written on root.pdf (22 pages, 199147 bytes). Transcript written on root.log. This is BibTeX, Version 0.99d (TeX Live 2015/Debian) The top-level auxiliary file: root.aux The style file: abbrv.bst Database file #1: root.bib Warning--there's a number but no series in rahman2002analytic (There was 1 warning) This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode LaTeX2e <2016/02/01> Babel <3.9q> and hyphenation patterns for 81 language(s) loaded. (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2014/09/29 v1.4h Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory' Including comment 'isatagtheory' Including comment 'isadelimproof' Including comment 'isatagproof' Including comment 'isadelimML' Including comment 'isatagML' Including comment 'isadelimvisible' Including comment 'isatagvisible' Excluding comment 'isadeliminvisible' Excluding comment 'isataginvisible') (./isabelletags.sty Including comment 'isadelimproof' Excluding comment 'isatagproof' Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) Package hyperref Message: Driver (autodetected): hpdftex. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./root.out) (./root.out) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) LaTeX Warning: Citation `eisermann2012fundamental' on page 1 undefined on input line 21. LaTeX Warning: Citation `rahman2002analytic' on page 1 undefined on input line 21. (./session.tex (./Missing_Topology.tex [1{/var/lib/texmf/fonts/map/pdftex/updma p/pdftex.map}] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. [2] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. [3] [4] [5] Overfull \hbox (30.33867pt too wide) in paragraph at lines 1775--1777 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 uniform[]discrete[]subset$\OT1/cmr/ m/n/10 [$\OT1/cmr/m/it/10 elim$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 uniform[] discrete S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 T $\OMS/cms y/m/n/10 ^^R$ \OT1/cmr/m/it/10 S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/c mr/m/it/10 uniform[]discrete [6]) (./Missing_Algebraic.tex [7] Overfull \hbox (5.7285pt too wide) in paragraph at lines 204--206 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 continuous[]on[]poly $\OT1/cmr/m/n/ 10 [$\OT1/cmr/m/it/10 continuous[]intros$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 continuous[]on s f $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 co ntinuous[]on [8] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. [9] [10] [11] [12]) (./Missing_Transcendental.tex [13] [14]) (./Missing_Analysis.tex [15] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. [16]) (./Cauchy_Index_Theorem.tex) (./Winding_Number_Eval.tex Overfull \hbox (5.34778pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Evaluate wind-ing num-bers by cal-cu-lat-ing Cauchy [17] Overfull \hbox (59.50618pt too wide) in paragraph at lines 723--723 []\OT1/cmr/bx/n/12 More lem-mas re-lated \OT1/cmr/m/it/12 cindex[]pathE \OT1/cm r/bx/n/12 / \OT1/cmr/m/it/12 jumpF[]pathstart \OT1/cmr/bx/n/12 / \OT1/cmr/m/it/ 12 jumpF[]pathfinish Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Overfull \hbox (5.14441pt too wide) in paragraph at lines 2156--2157 [][] \OT1/cmr/m/it/10 c3 $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 Im$\OT1/cm r/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/ m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$+$\OT1/cmr/m /it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n /10 ^^C$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/1 0 )$$+$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^ @$ \OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$ \OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\ OT1/cmr/m/n/10 )$ [18] [19] [20] Overfull \hbox (33.49898pt too wide) in paragraph at lines 5661--5664 []\OT1/cmr/m/n/10.95 The method "eval[]winding" \OT1/cmr/m/it/10.95 1$\OT1/cmr/ m/n/10.95 :$$:$$ [] $\OT1/cmr/m/it/10.95 a \OT1/cmr/m/n/10.95 will try to sim-p lify of the form \OT1/cmr/m/it/10.95 winding[]number ) (./Winding_Number_Eval_Examples.tex Overfull \hbox (5.94653pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Some ex-am-ples of ap-ply the method wind-ing[]eval [21])) (./root.bbl) [22] (./root.aux) LaTeX Warning: There were undefined references. LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. ) (see the transcript file for additional information) Output written on root.pdf (22 pages, 203962 bytes). Transcript written on root.log. This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode LaTeX2e <2016/02/01> Babel <3.9q> and hyphenation patterns for 81 language(s) loaded. (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2014/09/29 v1.4h Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory' Including comment 'isatagtheory' Including comment 'isadelimproof' Including comment 'isatagproof' Including comment 'isadelimML' Including comment 'isatagML' Including comment 'isadelimvisible' Including comment 'isatagvisible' Excluding comment 'isadeliminvisible' Excluding comment 'isataginvisible') (./isabelletags.sty Including comment 'isadelimproof' Excluding comment 'isatagproof' Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty ) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) Package hyperref Message: Driver (autodetected): hpdftex. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./root.out) (./root.out) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (./session.tex (./Missing_Topology.tex [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. [2] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. [3] [4] [5] Overfull \hbox (30.33867pt too wide) in paragraph at lines 1775--1777 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 uniform[]discrete[]subset$\OT1/cmr/ m/n/10 [$\OT1/cmr/m/it/10 elim$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 uniform[] discrete S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 T $\OMS/cms y/m/n/10 ^^R$ \OT1/cmr/m/it/10 S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/c mr/m/it/10 uniform[]discrete [6]) (./Missing_Algebraic.tex [7] Overfull \hbox (5.7285pt too wide) in paragraph at lines 204--206 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 continuous[]on[]poly $\OT1/cmr/m/n/ 10 [$\OT1/cmr/m/it/10 continuous[]intros$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 continuous[]on s f $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 co ntinuous[]on [8] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. [9] [10] [11] [12]) (./Missing_Transcendental.tex [13] [14]) (./Missing_Analysis.tex [15] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. [16]) (./Cauchy_Index_Theorem.tex) (./Winding_Number_Eval.tex Overfull \hbox (5.34778pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Evaluate wind-ing num-bers by cal-cu-lat-ing Cauchy [17] Overfull \hbox (59.50618pt too wide) in paragraph at lines 723--723 []\OT1/cmr/bx/n/12 More lem-mas re-lated \OT1/cmr/m/it/12 cindex[]pathE \OT1/cm r/bx/n/12 / \OT1/cmr/m/it/12 jumpF[]pathstart \OT1/cmr/bx/n/12 / \OT1/cmr/m/it/ 12 jumpF[]pathfinish Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Overfull \hbox (5.14441pt too wide) in paragraph at lines 2156--2157 [][] \OT1/cmr/m/it/10 c3 $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 Im$\OT1/cm r/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/ m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$+$\OT1/cmr/m /it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n /10 ^^C$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/1 0 )$$+$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^ @$ \OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$ \OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\ OT1/cmr/m/n/10 )$ [18] [19] [20] Overfull \hbox (33.49898pt too wide) in paragraph at lines 5661--5664 []\OT1/cmr/m/n/10.95 The method "eval[]winding" \OT1/cmr/m/it/10.95 1$\OT1/cmr/ m/n/10.95 :$$:$$ [] $\OT1/cmr/m/it/10.95 a \OT1/cmr/m/n/10.95 will try to sim-p lify of the form \OT1/cmr/m/it/10.95 winding[]number ) (./Winding_Number_Eval_Examples.tex Overfull \hbox (5.94653pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Some ex-am-ples of ap-ply the method wind-ing[]eval [21])) (./root.bbl) [22] (./root.aux) ) (see the transcript file for additional information) Output written on root.pdf (22 pages, 203866 bytes). Transcript written on root.log. This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode LaTeX2e <2016/02/01> Babel <3.9q> and hyphenation patterns for 81 language(s) loaded. (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2014/09/29 v1.4h Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory' Including comment 'isatagtheory' Including comment 'isadelimproof' Including comment 'isatagproof' Including comment 'isadelimML' Including comment 'isatagML' Including comment 'isadelimvisible' Including comment 'isatagvisible' Excluding comment 'isadeliminvisible' Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) Package hyperref Message: Driver (autodetected): hpdftex. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) No file root.aux. (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) LaTeX Warning: Citation `eisermann2012fundamental' on page 1 undefined on input line 21. LaTeX Warning: Citation `rahman2002analytic' on page 1 undefined on input line 21. (./session.tex (./Missing_Topology.tex [1{/var/lib/texmf/fonts/map/pdftex/updma p/pdftex.map}] [2] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [3] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. [4] [5] [6] [7] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Overfull \hbox (21.3087pt too wide) in paragraph at lines 979--981 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro tendsto[] mult tendsto[]inverse assms filterlim[]compose$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/ 10 OF tendsto[]inverse[]0$\OT1/cmr/m/n/10 ]$$)$[] [8] [9] [10] [11] [12] Overfull \hbox (30.33867pt too wide) in paragraph at lines 1775--1777 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 uniform[]discrete[]subset$\OT1/cmr/ m/n/10 [$\OT1/cmr/m/it/10 elim$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 uniform[] discrete S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 T $\OMS/cms y/m/n/10 ^^R$ \OT1/cmr/m/it/10 S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/c mr/m/it/10 uniform[]discrete Overfull \hbox (19.55737pt too wide) in paragraph at lines 1795--1809 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 continuous[]on[]topological \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis discrete[]def is -limptI isolate[]islimpt[]iff$\OT1/cmr/m/n/10 )$[] Overfull \hbox (34.29984pt too wide) in paragraph at lines 1833--1838 [][] \OT1/cmr/bx/n/10 more-over have \OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/1 0 when \OT1/cmr/m/it/10 S$\OT1/cmr/m/n/10 =$$\OMS/cmsy/m/n/10 f$$g$ \OT1/cmr/bx /n/10 us-ing \OT1/cmr/m/it/10 that asm \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\ OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 uniform[]discrete[ ]def$\OT1/cmr/m/n/10 )$[] [13] Overfull \hbox (46.90544pt too wide) in paragraph at lines 1986--1988 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 uniform[]discrete[]imp[]discre te uniform[]discrete[]imp[]closed compact[]eq[]bounded[]closed[] [14] [15]) (./Missing_Algebraic.tex [16] Overfull \hbox (5.7285pt too wide) in paragraph at lines 204--206 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 continuous[]on[]poly $\OT1/cmr/m/n/ 10 [$\OT1/cmr/m/it/10 continuous[]intros$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 continuous[]on s f $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 co ntinuous[]on Overfull \hbox (31.95682pt too wide) in paragraph at lines 275--277 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 zorder[]exist$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of UNIV z poly p$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 folded n[]def h[]def$\OT1/cmr/m/n/10 ]$ []\OT1/cmr/m/it/10 poly p z$\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0[] poly[]holomorphic[]on[] [17] [18] Overfull \hbox (2.61458pt too wide) in paragraph at lines 587--589 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr /m/n/10 ($\OT1/cmr/m/it/10 mono[]tags$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lift -ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 an-ti-sym assms$\OT1/cmr/m/n/10 ($\OT1 /cmr/m/it/10 1$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 assms$\OT1/cmr/m/n/10 ($\OT1 /cmr/m/it/10 2$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 coeff[]0[]degree[]minus[]1 [19] Overfull \hbox (34.18707pt too wide) in paragraph at lines 668--670 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\ OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 tendsto[]add[]filterlim[]at[]infinity filt erlim[]at[]infinity[]times filterlim[]ident$\OT1/cmr/m/n/10 )$[] [20] Overfull \hbox (0.65536pt too wide) in paragraph at lines 752--754 [][] \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in -tro$\OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 tendsto[]intros tendsto[]divide[]0 s imp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 degree[]monom[]eq$\OT1/cmr/m/n/10 ) $[] [21] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. [22] Overfull \hbox (46.5098pt too wide) in paragraph at lines 1101--1103 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr/m /n/10 ($\OT1/cmr/m/it/10 full[]types$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 last[] conv[]nth[]default length[]map no[]trailing[]unfold nth[]default[]coeffs[]eq Overfull \hbox (5.57529pt too wide) in paragraph at lines 1134--1135 [][] \OT1/cmr/m/it/10 degree[]eq[]length[]coeffs length[]greater[]0[]con v list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 size$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 3$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it /10 size$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 4$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/ 10 not[]less[]zero[] [23] [24] [25] Overfull \hbox (52.22517pt too wide) in paragraph at lines 1523--1528 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 u n-fold-ing \OT1/cmr/m/it/10 proots[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($ \OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 comm[]monoid []add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sum$\OML/cmm/m/it/10 :$\OT1/cm r/m/it/10 cong$\OT1/cmr/m/n/10 )$[] [26] [27] Overfull \hbox (31.40704pt too wide) in paragraph at lines 1816--1823 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases a$\OMS/cmsy /m/n/10 2$\OT1/cmr/m/it/10 s$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 auto simp add$ \OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 proots[]within[]pCons[]1[]iff order[]power[] n[]n$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] 1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/i t/10 simplified$\OT1/cmr/m/n/10 ]$$)$[] [28] Overfull \hbox (20.29214pt too wide) in paragraph at lines 1954--1956 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr /m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 hide[ ]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/ 10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]neutral mi nus[]pCons Overfull \hbox (9.36722pt too wide) in paragraph at lines 2017--2019 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/c mr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lif t-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/ 10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]neutral mi nus[]pCons ) (./Missing_Transcendental.tex [29] Overfull \hbox (47.2507pt too wide) in paragraph at lines 53--54 [][] \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]inve rse divide[]minus[]left less[]eq[]real[]def linorder[]not[]le minus[]pi[]half[] less[]zero$\OT1/cmr/m/n/10 )$[] Overfull \hbox (16.37035pt too wide) in paragraph at lines 61--63 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis []Im z $\OML/cmm/m/it/10 <$ \OT1/cmr/m/it/10 0[] []Re z $\OT1/cmr/m/n/10 =$ \OT1/cmr/m /it/10 0[] add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 commute add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 ri ght[]neutral [30] Overfull \hbox (19.25873pt too wide) in paragraph at lines 150--152 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp a dd$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 sin[]arctan divide[]simps complex[]neq[]0 cmod[]def real[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] Overfull \hbox (19.7698pt too wide) in paragraph at lines 169--171 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp a dd$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 cos[]arctan divide[]simps complex[]neq[]0 cmod[]def real[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] [31] [32] [33] Overfull \hbox (11.6628pt too wide) in paragraph at lines 620--622 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis arctan[]u nique cos[]pi[]half division[]ring[]divide[]zero tan[]def tan[]periodic[]int [34] [35] [36] [37] [38] [39] [40] [41] [42]) (./Missing_Analysis.tex Overfull \hbox (38.10612pt too wide) in paragraph at lines 29--37 [][] \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1 /cmr/m/n/10 :$ \OT1/cmr/m/it/10 closed[]segment[]real[]eq image[]affinity[]atLe astAtMost path[]image[]subpath$\OT1/cmr/m/n/10 )$[] Overfull \hbox (14.29695pt too wide) in paragraph at lines 63--65 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 imp$\OT1/cmr/m/n/10 :$\OT1/cmr/m/i t/10 valid[]path g $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 val id[]path $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 uminus $\OMS/cmsy/m/n/10 ^^N$ \OT1 /cmr/m/it/10 g$\OT1/cmr/m/n/10 )$ \OT1/cmr/bx/n/10 for \OT1/cmr/m/it/10 g$\OT1/ cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real $\OMS/cmsy/m/n/10 )$ $ [] $\OT1/cmr/m/it/ 10 a $\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]field[] Overfull \hbox (40.12338pt too wide) in paragraph at lines 67--69 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT 1/cmr/m/n/10 :$\OT1/cmr/m/it/10 derivative[]intros continuous[]intros simp add$ \OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 deriv[]linear$\OT1/cmr/m/n/10 [$\OT1/cmr/m/i t/10 of $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/ it/10 simplified$\OT1/cmr/m/n/10 ]$$)$ [43] [44] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. [45] Overfull \hbox (1.82657pt too wide) in paragraph at lines 428--430 [][] \OT1/cmr/bx/n/10 show \OT1/cmr/m/it/10 open UNIV umi-nus holomorphic[]o n UNIV path[]image $\OML/cmm/m/it/10 ^^M$ $\OMS/cmsy/m/n/10 ^^R$ \OT1/cmr/m/it/ 10 UNIV valid[]path [46]) (./Cauchy_Index_Theorem.tex) (./Winding_Number_Eval.tex Overfull \hbox (5.34778pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Evaluate wind-ing num-bers by cal-cu-lat-ing Cauchy [47] [48] [49] Overfull \hbox (14.73059pt too wide) in paragraph at lines 313--317 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 finite[]axes[]cross $\OT1/cmr/m/ n/10 ($\OT1/cmr/m/it/10 g1$\OT1/cmr/m/n/10 +$$+$$+$\OT1/cmr/m/it/10 g2$\OT1/cmr /m/n/10 )$ \OT1/cmr/m/it/10 z \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \O T1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/ 10 :$\OT1/cmr/m/it/10 finite[]cross[]intros$\OT1/cmr/m/n/10 )$[] [50] Overfull \hbox (7.23737pt too wide) in paragraph at lines 436--439 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 path[]def \OT1/cm r/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 !$ $:$\OT1/cmr/m/it/10 continuous[]intros continuous[]on[]interior$\OT1/cmr/m/n/10 )$[] [51] [52] [53] Overfull \hbox (59.50618pt too wide) in paragraph at lines 723--723 []\OT1/cmr/bx/n/12 More lem-mas re-lated \OT1/cmr/m/it/12 cindex[]pathE \OT1/cm r/bx/n/12 / \OT1/cmr/m/it/12 jumpF[]pathstart \OT1/cmr/bx/n/12 / \OT1/cmr/m/it/ 12 jumpF[]pathfinish Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. [54] [55] Overfull \hbox (0.52429pt too wide) in paragraph at lines 973--975 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 cindex[]ends$\OT1/cmr/m/n/10 : $\OT1/cmr/m/it/10 cindex[]pathE ?g z $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 jumpF []pathstart ?g z $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 jumpF[]pathfinish [56] [57] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1227--1231 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [58] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1304--1308 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [59] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1467--1471 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1545--1549 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [60] [61] [62] [63] [64] Overfull \hbox (5.14441pt too wide) in paragraph at lines 2156--2157 [][] \OT1/cmr/m/it/10 c3 $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 Im$\OT1/cm r/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/ m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$+$\OT1/cmr/m /it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n /10 ^^C$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/1 0 )$$+$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^ @$ \OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$ \OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\ OT1/cmr/m/n/10 )$ [65] [66] [67] [68] [69] [70] Overfull \hbox (3.1392pt too wide) in paragraph at lines 2765--2767 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathstart[]def p art[]circlepath[]def exp[]Euler f[]def g[]def comp[]def Overfull \hbox (6.58923pt too wide) in paragraph at lines 2795--2797 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathfinish[]def part[]circlepath[]def exp[]Euler f[]def g[]def comp[]def [71] [72] [73] Overfull \hbox (36.32861pt too wide) in paragraph at lines 3119--3124 [][] \OT1/cmr/bx/n/10 sub-goal us-ing \OT1/cmr/m/it/10 finite[]jFs \OT1/ cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 finite[]jumpFs[]def \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it /10 rev[]finite[]subset$\OT1/cmr/m/n/10 )$[] Overfull \hbox (36.32861pt too wide) in paragraph at lines 3139--3144 [][] \OT1/cmr/bx/n/10 sub-goal us-ing \OT1/cmr/m/it/10 finite[]jFs \OT1/ cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 finite[]jumpFs[]def \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it /10 rev[]finite[]subset$\OT1/cmr/m/n/10 )$[] [74] [75] [76] [77] [78] [79] [80] [81] Overfull \hbox (3.1392pt too wide) in paragraph at lines 4108--4110 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathstart[]def p art[]circlepath[]def exp[]Euler f[]def g[]def comp[]def[] [82] [83] Overfull \hbox (3.80205pt too wide) in paragraph at lines 4372--4374 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 g st $\OT1/cmr/m/n/10 =$ \OT1/cm r/m/it/10 0 f st$\OMS/cmsy/m/n/10 6\OT1/cmr/m/n/10 =$\OT1/cmr/m/it/10 0 \OT1/cm r/bx/n/10 and \OT1/cmr/m/it/10 g[]cont$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 con- tin-u-ous $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 at[]right st$\OT1/cmr/m/n/10 )$ \ OT1/cmr/m/it/10 g \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 f[]cont$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 continuous Overfull \hbox (7.21634pt too wide) in paragraph at lines 4460--4465 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/10 us -ing []\OT1/cmr/m/it/10 cmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OMS/cmsy/m/ n/10 ^^@$\OT1/cmr/m/it/10 z0$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 6\OT1/cmr/m/n /10 =$\OT1/cmr/m/it/10 r[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 norm[]minus[]commute$\OT1/cmr/ m/n/10 )$[] Overfull \hbox (57.64598pt too wide) in paragraph at lines 4473--4475 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1 /cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 h ide[]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m /it/10 right[]neutral cancel[]comm[]monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/ cmr/m/it/10 diff[]cancel [84] Overfull \hbox (5.23206pt too wide) in paragraph at lines 4475--4476 [][] \OT1/cmr/m/it/10 cos[]diff cos[]zero mult[]eq[]0[]iff power2[]e q[]1[]iff power2[]eq[]square sin[]squared[]eq$\OT1/cmr/m/n/10 )$[] Overfull \hbox (6.58923pt too wide) in paragraph at lines 4563--4565 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathfinish[]def part[]circlepath[]def exp[]Euler f[]def g[]def comp[]def[] [85] [86] [87] Overfull \hbox (7.21634pt too wide) in paragraph at lines 4914--4919 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/10 us -ing []\OT1/cmr/m/it/10 cmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OMS/cmsy/m/ n/10 ^^@$\OT1/cmr/m/it/10 z0$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 6\OT1/cmr/m/n /10 =$\OT1/cmr/m/it/10 r[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 norm[]minus[]commute$\OT1/cmr/ m/n/10 )$[] Overfull \hbox (57.64598pt too wide) in paragraph at lines 4927--4929 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1 /cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 h ide[]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m /it/10 right[]neutral cancel[]comm[]monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/ cmr/m/it/10 diff[]cancel Overfull \hbox (5.23206pt too wide) in paragraph at lines 4929--4930 [][] \OT1/cmr/m/it/10 cos[]diff cos[]zero mult[]eq[]0[]iff power2[]e q[]1[]iff power2[]eq[]square sin[]squared[]eq$\OT1/cmr/m/n/10 )$[] [88] Overfull \hbox (13.45331pt too wide) in paragraph at lines 5003--5006 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis assms complex[]Re[]le[]cmod le[]less[]trans minus[]complex$\OML/cmm/m/it/10 :$\ OT1/cmr/m/it/10 simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$ Overfull \hbox (10.4239pt too wide) in paragraph at lines 5038--5040 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis cmod[]p ower2 dvd[]refl linorder[]not[]le norm[]complex[]def power2[]le[]imp[]le[] Overfull \hbox (8.69661pt too wide) in paragraph at lines 5061--5065 [][] \OT1/cmr/bx/n/10 sub-goal us-ing []\OT1/cmr/m/it/10 r$\OML/cmm/m/it/1 0 >$\OT1/cmr/m/it/10 0[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/1 0 auto simp add$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 field[]simps divide[]simps r eal[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] [89] [90] [91] [92] Overfull \hbox (15.84285pt too wide) in paragraph at lines 5580--5583 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp$\OM L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 subst sin$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 minus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/ cmm/m/it/10 ;$\OT1/cmr/m/it/10 subst cos$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 mi nus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/cmm /m/it/10 ;$\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n/10 )$[] [93] Overfull \hbox (15.84285pt too wide) in paragraph at lines 5589--5592 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp$\OM L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 subst sin$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 minus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/ cmm/m/it/10 ;$\OT1/cmr/m/it/10 subst cos$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 mi nus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/cmm /m/it/10 ;$\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n/10 )$[] Overfull \hbox (33.49898pt too wide) in paragraph at lines 5661--5664 []\OT1/cmr/m/n/10.95 The method "eval[]winding" \OT1/cmr/m/it/10.95 1$\OT1/cmr/ m/n/10.95 :$$:$$ [] $\OT1/cmr/m/it/10.95 a \OT1/cmr/m/n/10.95 will try to sim-p lify of the form \OT1/cmr/m/it/10.95 winding[]number [94]) (./Winding_Number_Eval_Examples.tex Overfull \hbox (5.94653pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Some ex-am-ples of ap-ply the method wind-ing[]eval Overfull \hbox (7.50224pt too wide) in paragraph at lines 66--68 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\ OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 jumpF[]pathstart[]part[]circlepath jumpF[]pat hfinish[]part[]circlepath$\OT1/cmr/m/n/10 )$[] [95] Overfull \hbox (7.50224pt too wide) in paragraph at lines 126--128 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\ OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 jumpF[]pathstart[]part[]circlepath jumpF[]pat hfinish[]part[]circlepath$\OT1/cmr/m/n/10 )$[] Overfull \hbox (31.35716pt too wide) in paragraph at lines 170--173 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]gt[]0[]iff[]gt mult[]pos[]pos or-der$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 asym zero[]less[]mult[]pos2$\OT1/cm r/m/n/10 )$[] Overfull \hbox (8.33937pt too wide) in paragraph at lines 184--187 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]less[]0[]iff[]less linordered []field[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sign[]simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 44$\OT1/cmr/m/n/10 )$ Overfull \hbox (8.33937pt too wide) in paragraph at lines 191--194 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]less[]0[]iff[]less linordered []field[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sign[]simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 44$\OT1/cmr/m/n/10 )$ Overfull \hbox (3.7772pt too wide) in paragraph at lines 194--196 [][] \OT1/cmr/bx/n/10 show $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 complex[]of []real $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cindex[]pathE ?l1 z $\OT1/cmr/m/n/10 +$ $($\OT1/cmr/m/it/10 cindex[]pathE ?l2 z $\OT1/cmr/m/n/10 +$ $($\OT1/cmr/m/i t/10 cindex[]pathE [96])) No file root.bbl. [97] (./root.aux) Package rerunfilecheck Warning: File `root.out' has changed. (rerunfilecheck) Rerun to get outlines right (rerunfilecheck) or use package `bookmark'. LaTeX Warning: There were undefined references. ) (see the transcript file for additional information) Output written on root.pdf (97 pages, 403045 bytes). Transcript written on root.log. This is BibTeX, Version 0.99d (TeX Live 2015/Debian) The top-level auxiliary file: root.aux The style file: abbrv.bst Database file #1: root.bib Warning--there's a number but no series in rahman2002analytic (There was 1 warning) This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode LaTeX2e <2016/02/01> Babel <3.9q> and hyphenation patterns for 81 language(s) loaded. (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2014/09/29 v1.4h Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory' Including comment 'isatagtheory' Including comment 'isadelimproof' Including comment 'isatagproof' Including comment 'isadelimML' Including comment 'isatagML' Including comment 'isadelimvisible' Including comment 'isatagvisible' Excluding comment 'isadeliminvisible' Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) Package hyperref Message: Driver (autodetected): hpdftex. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./root.out) (./root.out) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) LaTeX Warning: Citation `eisermann2012fundamental' on page 1 undefined on input line 21. LaTeX Warning: Citation `rahman2002analytic' on page 1 undefined on input line 21. (./session.tex (./Missing_Topology.tex [1{/var/lib/texmf/fonts/map/pdftex/updma p/pdftex.map}] [2] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [3] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. [4] [5] [6] [7] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Overfull \hbox (21.3087pt too wide) in paragraph at lines 979--981 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro tendsto[] mult tendsto[]inverse assms filterlim[]compose$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/ 10 OF tendsto[]inverse[]0$\OT1/cmr/m/n/10 ]$$)$[] [8] [9] [10] [11] [12] Overfull \hbox (30.33867pt too wide) in paragraph at lines 1775--1777 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 uniform[]discrete[]subset$\OT1/cmr/ m/n/10 [$\OT1/cmr/m/it/10 elim$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 uniform[] discrete S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 T $\OMS/cms y/m/n/10 ^^R$ \OT1/cmr/m/it/10 S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/c mr/m/it/10 uniform[]discrete Overfull \hbox (19.55737pt too wide) in paragraph at lines 1795--1809 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 continuous[]on[]topological \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis discrete[]def is -limptI isolate[]islimpt[]iff$\OT1/cmr/m/n/10 )$[] Overfull \hbox (34.29984pt too wide) in paragraph at lines 1833--1838 [][] \OT1/cmr/bx/n/10 more-over have \OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/1 0 when \OT1/cmr/m/it/10 S$\OT1/cmr/m/n/10 =$$\OMS/cmsy/m/n/10 f$$g$ \OT1/cmr/bx /n/10 us-ing \OT1/cmr/m/it/10 that asm \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\ OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 uniform[]discrete[ ]def$\OT1/cmr/m/n/10 )$[] [13] Overfull \hbox (46.90544pt too wide) in paragraph at lines 1986--1988 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 uniform[]discrete[]imp[]discre te uniform[]discrete[]imp[]closed compact[]eq[]bounded[]closed[] [14] [15]) (./Missing_Algebraic.tex [16] Overfull \hbox (5.7285pt too wide) in paragraph at lines 204--206 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 continuous[]on[]poly $\OT1/cmr/m/n/ 10 [$\OT1/cmr/m/it/10 continuous[]intros$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 continuous[]on s f $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 co ntinuous[]on Overfull \hbox (31.95682pt too wide) in paragraph at lines 275--277 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 zorder[]exist$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of UNIV z poly p$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 folded n[]def h[]def$\OT1/cmr/m/n/10 ]$ []\OT1/cmr/m/it/10 poly p z$\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0[] poly[]holomorphic[]on[] [17] [18] Overfull \hbox (2.61458pt too wide) in paragraph at lines 587--589 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr /m/n/10 ($\OT1/cmr/m/it/10 mono[]tags$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lift -ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 an-ti-sym assms$\OT1/cmr/m/n/10 ($\OT1 /cmr/m/it/10 1$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 assms$\OT1/cmr/m/n/10 ($\OT1 /cmr/m/it/10 2$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 coeff[]0[]degree[]minus[]1 [19] Overfull \hbox (34.18707pt too wide) in paragraph at lines 668--670 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\ OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 tendsto[]add[]filterlim[]at[]infinity filt erlim[]at[]infinity[]times filterlim[]ident$\OT1/cmr/m/n/10 )$[] [20] Overfull \hbox (0.65536pt too wide) in paragraph at lines 752--754 [][] \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in -tro$\OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 tendsto[]intros tendsto[]divide[]0 s imp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 degree[]monom[]eq$\OT1/cmr/m/n/10 ) $[] [21] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. [22] Overfull \hbox (46.5098pt too wide) in paragraph at lines 1101--1103 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr/m /n/10 ($\OT1/cmr/m/it/10 full[]types$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 last[] conv[]nth[]default length[]map no[]trailing[]unfold nth[]default[]coeffs[]eq Overfull \hbox (5.57529pt too wide) in paragraph at lines 1134--1135 [][] \OT1/cmr/m/it/10 degree[]eq[]length[]coeffs length[]greater[]0[]con v list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 size$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 3$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it /10 size$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 4$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/ 10 not[]less[]zero[] [23] [24] [25] Overfull \hbox (52.22517pt too wide) in paragraph at lines 1523--1528 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 u n-fold-ing \OT1/cmr/m/it/10 proots[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($ \OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 comm[]monoid []add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sum$\OML/cmm/m/it/10 :$\OT1/cm r/m/it/10 cong$\OT1/cmr/m/n/10 )$[] [26] [27] Overfull \hbox (31.40704pt too wide) in paragraph at lines 1816--1823 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases a$\OMS/cmsy /m/n/10 2$\OT1/cmr/m/it/10 s$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 auto simp add$ \OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 proots[]within[]pCons[]1[]iff order[]power[] n[]n$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] 1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/i t/10 simplified$\OT1/cmr/m/n/10 ]$$)$[] [28] Overfull \hbox (20.29214pt too wide) in paragraph at lines 1954--1956 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr /m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 hide[ ]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/ 10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]neutral mi nus[]pCons Overfull \hbox (9.36722pt too wide) in paragraph at lines 2017--2019 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/c mr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lif t-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/ 10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]neutral mi nus[]pCons ) (./Missing_Transcendental.tex [29] Overfull \hbox (47.2507pt too wide) in paragraph at lines 53--54 [][] \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]inve rse divide[]minus[]left less[]eq[]real[]def linorder[]not[]le minus[]pi[]half[] less[]zero$\OT1/cmr/m/n/10 )$[] Overfull \hbox (16.37035pt too wide) in paragraph at lines 61--63 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis []Im z $\OML/cmm/m/it/10 <$ \OT1/cmr/m/it/10 0[] []Re z $\OT1/cmr/m/n/10 =$ \OT1/cmr/m /it/10 0[] add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 commute add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 ri ght[]neutral [30] Overfull \hbox (19.25873pt too wide) in paragraph at lines 150--152 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp a dd$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 sin[]arctan divide[]simps complex[]neq[]0 cmod[]def real[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] Overfull \hbox (19.7698pt too wide) in paragraph at lines 169--171 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp a dd$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 cos[]arctan divide[]simps complex[]neq[]0 cmod[]def real[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] [31] [32] [33] Overfull \hbox (11.6628pt too wide) in paragraph at lines 620--622 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis arctan[]u nique cos[]pi[]half division[]ring[]divide[]zero tan[]def tan[]periodic[]int [34] [35] [36] [37] [38] [39] [40] [41] [42]) (./Missing_Analysis.tex Overfull \hbox (38.10612pt too wide) in paragraph at lines 29--37 [][] \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1 /cmr/m/n/10 :$ \OT1/cmr/m/it/10 closed[]segment[]real[]eq image[]affinity[]atLe astAtMost path[]image[]subpath$\OT1/cmr/m/n/10 )$[] Overfull \hbox (14.29695pt too wide) in paragraph at lines 63--65 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 imp$\OT1/cmr/m/n/10 :$\OT1/cmr/m/i t/10 valid[]path g $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 val id[]path $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 uminus $\OMS/cmsy/m/n/10 ^^N$ \OT1 /cmr/m/it/10 g$\OT1/cmr/m/n/10 )$ \OT1/cmr/bx/n/10 for \OT1/cmr/m/it/10 g$\OT1/ cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real $\OMS/cmsy/m/n/10 )$ $ [] $\OT1/cmr/m/it/ 10 a $\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]field[] Overfull \hbox (40.12338pt too wide) in paragraph at lines 67--69 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT 1/cmr/m/n/10 :$\OT1/cmr/m/it/10 derivative[]intros continuous[]intros simp add$ \OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 deriv[]linear$\OT1/cmr/m/n/10 [$\OT1/cmr/m/i t/10 of $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/ it/10 simplified$\OT1/cmr/m/n/10 ]$$)$ [43] [44] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. [45] Overfull \hbox (1.82657pt too wide) in paragraph at lines 428--430 [][] \OT1/cmr/bx/n/10 show \OT1/cmr/m/it/10 open UNIV umi-nus holomorphic[]o n UNIV path[]image $\OML/cmm/m/it/10 ^^M$ $\OMS/cmsy/m/n/10 ^^R$ \OT1/cmr/m/it/ 10 UNIV valid[]path [46]) (./Cauchy_Index_Theorem.tex) (./Winding_Number_Eval.tex Overfull \hbox (5.34778pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Evaluate wind-ing num-bers by cal-cu-lat-ing Cauchy [47] [48] [49] Overfull \hbox (14.73059pt too wide) in paragraph at lines 313--317 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 finite[]axes[]cross $\OT1/cmr/m/ n/10 ($\OT1/cmr/m/it/10 g1$\OT1/cmr/m/n/10 +$$+$$+$\OT1/cmr/m/it/10 g2$\OT1/cmr /m/n/10 )$ \OT1/cmr/m/it/10 z \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \O T1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/ 10 :$\OT1/cmr/m/it/10 finite[]cross[]intros$\OT1/cmr/m/n/10 )$[] [50] Overfull \hbox (7.23737pt too wide) in paragraph at lines 436--439 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 path[]def \OT1/cm r/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 !$ $:$\OT1/cmr/m/it/10 continuous[]intros continuous[]on[]interior$\OT1/cmr/m/n/10 )$[] [51] [52] [53] Overfull \hbox (59.50618pt too wide) in paragraph at lines 723--723 []\OT1/cmr/bx/n/12 More lem-mas re-lated \OT1/cmr/m/it/12 cindex[]pathE \OT1/cm r/bx/n/12 / \OT1/cmr/m/it/12 jumpF[]pathstart \OT1/cmr/bx/n/12 / \OT1/cmr/m/it/ 12 jumpF[]pathfinish Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. [54] [55] Overfull \hbox (0.52429pt too wide) in paragraph at lines 973--975 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 cindex[]ends$\OT1/cmr/m/n/10 : $\OT1/cmr/m/it/10 cindex[]pathE ?g z $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 jumpF []pathstart ?g z $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 jumpF[]pathfinish [56] [57] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1227--1231 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [58] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1304--1308 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [59] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1467--1471 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1545--1549 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [60] [61] [62] [63] [64] Overfull \hbox (5.14441pt too wide) in paragraph at lines 2156--2157 [][] \OT1/cmr/m/it/10 c3 $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 Im$\OT1/cm r/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/ m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$+$\OT1/cmr/m /it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n /10 ^^C$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/1 0 )$$+$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^ @$ \OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$ \OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\ OT1/cmr/m/n/10 )$ [65] [66] [67] [68] [69] [70] Overfull \hbox (3.1392pt too wide) in paragraph at lines 2765--2767 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathstart[]def p art[]circlepath[]def exp[]Euler f[]def g[]def comp[]def Overfull \hbox (6.58923pt too wide) in paragraph at lines 2795--2797 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathfinish[]def part[]circlepath[]def exp[]Euler f[]def g[]def comp[]def [71] [72] [73] Overfull \hbox (36.32861pt too wide) in paragraph at lines 3119--3124 [][] \OT1/cmr/bx/n/10 sub-goal us-ing \OT1/cmr/m/it/10 finite[]jFs \OT1/ cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 finite[]jumpFs[]def \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it /10 rev[]finite[]subset$\OT1/cmr/m/n/10 )$[] Overfull \hbox (36.32861pt too wide) in paragraph at lines 3139--3144 [][] \OT1/cmr/bx/n/10 sub-goal us-ing \OT1/cmr/m/it/10 finite[]jFs \OT1/ cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 finite[]jumpFs[]def \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it /10 rev[]finite[]subset$\OT1/cmr/m/n/10 )$[] [74] [75] [76] [77] [78] [79] [80] [81] Overfull \hbox (3.1392pt too wide) in paragraph at lines 4108--4110 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathstart[]def p art[]circlepath[]def exp[]Euler f[]def g[]def comp[]def[] [82] [83] Overfull \hbox (3.80205pt too wide) in paragraph at lines 4372--4374 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 g st $\OT1/cmr/m/n/10 =$ \OT1/cm r/m/it/10 0 f st$\OMS/cmsy/m/n/10 6\OT1/cmr/m/n/10 =$\OT1/cmr/m/it/10 0 \OT1/cm r/bx/n/10 and \OT1/cmr/m/it/10 g[]cont$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 con- tin-u-ous $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 at[]right st$\OT1/cmr/m/n/10 )$ \ OT1/cmr/m/it/10 g \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 f[]cont$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 continuous Overfull \hbox (7.21634pt too wide) in paragraph at lines 4460--4465 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/10 us -ing []\OT1/cmr/m/it/10 cmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OMS/cmsy/m/ n/10 ^^@$\OT1/cmr/m/it/10 z0$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 6\OT1/cmr/m/n /10 =$\OT1/cmr/m/it/10 r[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 norm[]minus[]commute$\OT1/cmr/ m/n/10 )$[] Overfull \hbox (57.64598pt too wide) in paragraph at lines 4473--4475 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1 /cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 h ide[]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m /it/10 right[]neutral cancel[]comm[]monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/ cmr/m/it/10 diff[]cancel [84] Overfull \hbox (5.23206pt too wide) in paragraph at lines 4475--4476 [][] \OT1/cmr/m/it/10 cos[]diff cos[]zero mult[]eq[]0[]iff power2[]e q[]1[]iff power2[]eq[]square sin[]squared[]eq$\OT1/cmr/m/n/10 )$[] Overfull \hbox (6.58923pt too wide) in paragraph at lines 4563--4565 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathfinish[]def part[]circlepath[]def exp[]Euler f[]def g[]def comp[]def[] [85] [86] [87] Overfull \hbox (7.21634pt too wide) in paragraph at lines 4914--4919 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/10 us -ing []\OT1/cmr/m/it/10 cmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OMS/cmsy/m/ n/10 ^^@$\OT1/cmr/m/it/10 z0$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 6\OT1/cmr/m/n /10 =$\OT1/cmr/m/it/10 r[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 norm[]minus[]commute$\OT1/cmr/ m/n/10 )$[] Overfull \hbox (57.64598pt too wide) in paragraph at lines 4927--4929 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1 /cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 h ide[]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m /it/10 right[]neutral cancel[]comm[]monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/ cmr/m/it/10 diff[]cancel Overfull \hbox (5.23206pt too wide) in paragraph at lines 4929--4930 [][] \OT1/cmr/m/it/10 cos[]diff cos[]zero mult[]eq[]0[]iff power2[]e q[]1[]iff power2[]eq[]square sin[]squared[]eq$\OT1/cmr/m/n/10 )$[] [88] Overfull \hbox (13.45331pt too wide) in paragraph at lines 5003--5006 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis assms complex[]Re[]le[]cmod le[]less[]trans minus[]complex$\OML/cmm/m/it/10 :$\ OT1/cmr/m/it/10 simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$ Overfull \hbox (10.4239pt too wide) in paragraph at lines 5038--5040 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis cmod[]p ower2 dvd[]refl linorder[]not[]le norm[]complex[]def power2[]le[]imp[]le[] Overfull \hbox (8.69661pt too wide) in paragraph at lines 5061--5065 [][] \OT1/cmr/bx/n/10 sub-goal us-ing []\OT1/cmr/m/it/10 r$\OML/cmm/m/it/1 0 >$\OT1/cmr/m/it/10 0[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/1 0 auto simp add$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 field[]simps divide[]simps r eal[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] [89] [90] [91] [92] Overfull \hbox (15.84285pt too wide) in paragraph at lines 5580--5583 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp$\OM L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 subst sin$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 minus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/ cmm/m/it/10 ;$\OT1/cmr/m/it/10 subst cos$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 mi nus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/cmm /m/it/10 ;$\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n/10 )$[] [93] Overfull \hbox (15.84285pt too wide) in paragraph at lines 5589--5592 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp$\OM L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 subst sin$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 minus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/ cmm/m/it/10 ;$\OT1/cmr/m/it/10 subst cos$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 mi nus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/cmm /m/it/10 ;$\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n/10 )$[] Overfull \hbox (33.49898pt too wide) in paragraph at lines 5661--5664 []\OT1/cmr/m/n/10.95 The method "eval[]winding" \OT1/cmr/m/it/10.95 1$\OT1/cmr/ m/n/10.95 :$$:$$ [] $\OT1/cmr/m/it/10.95 a \OT1/cmr/m/n/10.95 will try to sim-p lify of the form \OT1/cmr/m/it/10.95 winding[]number [94]) (./Winding_Number_Eval_Examples.tex Overfull \hbox (5.94653pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Some ex-am-ples of ap-ply the method wind-ing[]eval Overfull \hbox (7.50224pt too wide) in paragraph at lines 66--68 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\ OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 jumpF[]pathstart[]part[]circlepath jumpF[]pat hfinish[]part[]circlepath$\OT1/cmr/m/n/10 )$[] [95] Overfull \hbox (7.50224pt too wide) in paragraph at lines 126--128 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\ OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 jumpF[]pathstart[]part[]circlepath jumpF[]pat hfinish[]part[]circlepath$\OT1/cmr/m/n/10 )$[] Overfull \hbox (31.35716pt too wide) in paragraph at lines 170--173 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]gt[]0[]iff[]gt mult[]pos[]pos or-der$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 asym zero[]less[]mult[]pos2$\OT1/cm r/m/n/10 )$[] Overfull \hbox (8.33937pt too wide) in paragraph at lines 184--187 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]less[]0[]iff[]less linordered []field[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sign[]simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 44$\OT1/cmr/m/n/10 )$ Overfull \hbox (8.33937pt too wide) in paragraph at lines 191--194 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]less[]0[]iff[]less linordered []field[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sign[]simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 44$\OT1/cmr/m/n/10 )$ Overfull \hbox (3.7772pt too wide) in paragraph at lines 194--196 [][] \OT1/cmr/bx/n/10 show $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 complex[]of []real $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cindex[]pathE ?l1 z $\OT1/cmr/m/n/10 +$ $($\OT1/cmr/m/it/10 cindex[]pathE ?l2 z $\OT1/cmr/m/n/10 +$ $($\OT1/cmr/m/i t/10 cindex[]pathE [96])) (./root.bbl) [97] (./root.aux) LaTeX Warning: There were undefined references. LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. ) (see the transcript file for additional information) Output written on root.pdf (97 pages, 407819 bytes). Transcript written on root.log. This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode LaTeX2e <2016/02/01> Babel <3.9q> and hyphenation patterns for 81 language(s) loaded. (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2014/09/29 v1.4h Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory' Including comment 'isatagtheory' Including comment 'isadelimproof' Including comment 'isatagproof' Including comment 'isadelimML' Including comment 'isatagML' Including comment 'isadelimvisible' Including comment 'isatagvisible' Excluding comment 'isadeliminvisible' Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty)))) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty)) (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)) Package hyperref Message: Driver (autodetected): hpdftex. (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty)) (./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty)) (./root.out) (./root.out) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (./session.tex (./Missing_Topology.tex [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [3] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 429. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 555. [4] [5] [6] [7] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 963. Overfull \hbox (21.3087pt too wide) in paragraph at lines 979--981 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro tendsto[] mult tendsto[]inverse assms filterlim[]compose$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/ 10 OF tendsto[]inverse[]0$\OT1/cmr/m/n/10 ]$$)$[] [8] [9] [10] [11] [12] Overfull \hbox (30.33867pt too wide) in paragraph at lines 1775--1777 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 uniform[]discrete[]subset$\OT1/cmr/ m/n/10 [$\OT1/cmr/m/it/10 elim$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 uniform[] discrete S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 T $\OMS/cms y/m/n/10 ^^R$ \OT1/cmr/m/it/10 S $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/c mr/m/it/10 uniform[]discrete Overfull \hbox (19.55737pt too wide) in paragraph at lines 1795--1809 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 continuous[]on[]topological \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis discrete[]def is -limptI isolate[]islimpt[]iff$\OT1/cmr/m/n/10 )$[] Overfull \hbox (34.29984pt too wide) in paragraph at lines 1833--1838 [][] \OT1/cmr/bx/n/10 more-over have \OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/1 0 when \OT1/cmr/m/it/10 S$\OT1/cmr/m/n/10 =$$\OMS/cmsy/m/n/10 f$$g$ \OT1/cmr/bx /n/10 us-ing \OT1/cmr/m/it/10 that asm \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\ OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 uniform[]discrete[ ]def$\OT1/cmr/m/n/10 )$[] [13] Overfull \hbox (46.90544pt too wide) in paragraph at lines 1986--1988 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 uniform[]discrete[]imp[]discre te uniform[]discrete[]imp[]closed compact[]eq[]bounded[]closed[] [14] [15]) (./Missing_Algebraic.tex [16] Overfull \hbox (5.7285pt too wide) in paragraph at lines 204--206 [][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 continuous[]on[]poly $\OT1/cmr/m/n/ 10 [$\OT1/cmr/m/it/10 continuous[]intros$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 continuous[]on s f $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 co ntinuous[]on Overfull \hbox (31.95682pt too wide) in paragraph at lines 275--277 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 zorder[]exist$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of UNIV z poly p$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 folded n[]def h[]def$\OT1/cmr/m/n/10 ]$ []\OT1/cmr/m/it/10 poly p z$\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0[] poly[]holomorphic[]on[] [17] [18] Overfull \hbox (2.61458pt too wide) in paragraph at lines 587--589 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr /m/n/10 ($\OT1/cmr/m/it/10 mono[]tags$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lift -ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 an-ti-sym assms$\OT1/cmr/m/n/10 ($\OT1 /cmr/m/it/10 1$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 assms$\OT1/cmr/m/n/10 ($\OT1 /cmr/m/it/10 2$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 coeff[]0[]degree[]minus[]1 [19] Overfull \hbox (34.18707pt too wide) in paragraph at lines 668--670 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\ OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 tendsto[]add[]filterlim[]at[]infinity filt erlim[]at[]infinity[]times filterlim[]ident$\OT1/cmr/m/n/10 )$[] [20] Overfull \hbox (0.65536pt too wide) in paragraph at lines 752--754 [][] \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in -tro$\OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 tendsto[]intros tendsto[]divide[]0 s imp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 degree[]monom[]eq$\OT1/cmr/m/n/10 ) $[] [21] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 958. [22] Overfull \hbox (46.5098pt too wide) in paragraph at lines 1101--1103 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr/m /n/10 ($\OT1/cmr/m/it/10 full[]types$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 last[] conv[]nth[]default length[]map no[]trailing[]unfold nth[]default[]coeffs[]eq Overfull \hbox (5.57529pt too wide) in paragraph at lines 1134--1135 [][] \OT1/cmr/m/it/10 degree[]eq[]length[]coeffs length[]greater[]0[]con v list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 size$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 3$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it /10 size$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 4$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/ 10 not[]less[]zero[] [23] [24] [25] Overfull \hbox (52.22517pt too wide) in paragraph at lines 1523--1528 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 u n-fold-ing \OT1/cmr/m/it/10 proots[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($ \OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 !$$:$\OT1/cmr/m/it/10 comm[]monoid []add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sum$\OML/cmm/m/it/10 :$\OT1/cm r/m/it/10 cong$\OT1/cmr/m/n/10 )$[] [26] [27] Overfull \hbox (31.40704pt too wide) in paragraph at lines 1816--1823 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases a$\OMS/cmsy /m/n/10 2$\OT1/cmr/m/it/10 s$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 auto simp add$ \OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 proots[]within[]pCons[]1[]iff order[]power[] n[]n$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] 1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/i t/10 simplified$\OT1/cmr/m/n/10 ]$$)$[] [28] Overfull \hbox (20.29214pt too wide) in paragraph at lines 1954--1956 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/cmr /m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 hide[ ]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/ 10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]neutral mi nus[]pCons Overfull \hbox (9.36722pt too wide) in paragraph at lines 2017--2019 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1/c mr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lif t-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/ 10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]neutral mi nus[]pCons ) (./Missing_Transcendental.tex [29] Overfull \hbox (47.2507pt too wide) in paragraph at lines 53--54 [][] \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]inve rse divide[]minus[]left less[]eq[]real[]def linorder[]not[]le minus[]pi[]half[] less[]zero$\OT1/cmr/m/n/10 )$[] Overfull \hbox (16.37035pt too wide) in paragraph at lines 61--63 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis []Im z $\OML/cmm/m/it/10 <$ \OT1/cmr/m/it/10 0[] []Re z $\OT1/cmr/m/n/10 =$ \OT1/cmr/m /it/10 0[] add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 commute add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 inverse[]inverse add$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 ri ght[]neutral [30] Overfull \hbox (19.25873pt too wide) in paragraph at lines 150--152 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp a dd$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 sin[]arctan divide[]simps complex[]neq[]0 cmod[]def real[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] Overfull \hbox (19.7698pt too wide) in paragraph at lines 169--171 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp a dd$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 cos[]arctan divide[]simps complex[]neq[]0 cmod[]def real[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] [31] [32] [33] Overfull \hbox (11.6628pt too wide) in paragraph at lines 620--622 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis arctan[]u nique cos[]pi[]half division[]ring[]divide[]zero tan[]def tan[]periodic[]int [34] [35] [36] [37] [38] [39] [40] [41] [42]) (./Missing_Analysis.tex Overfull \hbox (38.10612pt too wide) in paragraph at lines 29--37 [][] \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1 /cmr/m/n/10 :$ \OT1/cmr/m/it/10 closed[]segment[]real[]eq image[]affinity[]atLe astAtMost path[]image[]subpath$\OT1/cmr/m/n/10 )$[] Overfull \hbox (14.29695pt too wide) in paragraph at lines 63--65 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 imp$\OT1/cmr/m/n/10 :$\OT1/cmr/m/i t/10 valid[]path g $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 val id[]path $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 uminus $\OMS/cmsy/m/n/10 ^^N$ \OT1 /cmr/m/it/10 g$\OT1/cmr/m/n/10 )$ \OT1/cmr/bx/n/10 for \OT1/cmr/m/it/10 g$\OT1/ cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real $\OMS/cmsy/m/n/10 )$ $ [] $\OT1/cmr/m/it/ 10 a $\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]field[] Overfull \hbox (40.12338pt too wide) in paragraph at lines 67--69 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT 1/cmr/m/n/10 :$\OT1/cmr/m/it/10 derivative[]intros continuous[]intros simp add$ \OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 deriv[]linear$\OT1/cmr/m/n/10 [$\OT1/cmr/m/i t/10 of $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/ it/10 simplified$\OT1/cmr/m/n/10 ]$$)$ [43] [44] Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 319. [45] Overfull \hbox (1.82657pt too wide) in paragraph at lines 428--430 [][] \OT1/cmr/bx/n/10 show \OT1/cmr/m/it/10 open UNIV umi-nus holomorphic[]o n UNIV path[]image $\OML/cmm/m/it/10 ^^M$ $\OMS/cmsy/m/n/10 ^^R$ \OT1/cmr/m/it/ 10 UNIV valid[]path [46]) (./Cauchy_Index_Theorem.tex) (./Winding_Number_Eval.tex Overfull \hbox (5.34778pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Evaluate wind-ing num-bers by cal-cu-lat-ing Cauchy [47] [48] [49] Overfull \hbox (14.73059pt too wide) in paragraph at lines 313--317 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 finite[]axes[]cross $\OT1/cmr/m/ n/10 ($\OT1/cmr/m/it/10 g1$\OT1/cmr/m/n/10 +$$+$$+$\OT1/cmr/m/it/10 g2$\OT1/cmr /m/n/10 )$ \OT1/cmr/m/it/10 z \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \O T1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/ 10 :$\OT1/cmr/m/it/10 finite[]cross[]intros$\OT1/cmr/m/n/10 )$[] [50] Overfull \hbox (7.23737pt too wide) in paragraph at lines 436--439 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 path[]def \OT1/cm r/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 !$ $:$\OT1/cmr/m/it/10 continuous[]intros continuous[]on[]interior$\OT1/cmr/m/n/10 )$[] [51] [52] [53] Overfull \hbox (59.50618pt too wide) in paragraph at lines 723--723 []\OT1/cmr/bx/n/12 More lem-mas re-lated \OT1/cmr/m/it/12 cindex[]pathE \OT1/cm r/bx/n/12 / \OT1/cmr/m/it/12 jumpF[]pathstart \OT1/cmr/bx/n/12 / \OT1/cmr/m/it/ 12 jumpF[]pathfinish Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding): (hyperref) removing `\sfcode' on input line 723. [54] [55] Overfull \hbox (0.52429pt too wide) in paragraph at lines 973--975 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 cindex[]ends$\OT1/cmr/m/n/10 : $\OT1/cmr/m/it/10 cindex[]pathE ?g z $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 jumpF []pathstart ?g z $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 jumpF[]pathfinish [56] [57] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1227--1231 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [58] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1304--1308 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [59] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1467--1471 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] Overfull \hbox (16.59697pt too wide) in paragraph at lines 1545--1549 [][] \OT1/cmr/bx/n/10 sub-goal un-fold-ing \OT1/cmr/m/it/10 c2[] def c1[]def d1[]def \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 aut o in-tro$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/it/10 derivative[]eq[]intros$\OT1/cmr /m/n/10 )$[] [60] [61] [62] [63] [64] Overfull \hbox (5.14441pt too wide) in paragraph at lines 2156--2157 [][] \OT1/cmr/m/it/10 c3 $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 Im$\OT1/cm r/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/ m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$+$\OT1/cmr/m /it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n /10 ^^C$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/1 0 )$$+$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^@$\OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OT1/cmr/m/n/10 )$$\OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 ^^ @$ \OT1/cmr/m/it/10 Im$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 b$\OT1/cmr/m/n/10 )$$ \OMS/cmsy/m/n/10 ^^C$\OT1/cmr/m/it/10 Re$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 a$\ OT1/cmr/m/n/10 )$ [65] [66] [67] [68] [69] [70] Overfull \hbox (3.1392pt too wide) in paragraph at lines 2765--2767 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathstart[]def p art[]circlepath[]def exp[]Euler f[]def g[]def comp[]def Overfull \hbox (6.58923pt too wide) in paragraph at lines 2795--2797 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathfinish[]def part[]circlepath[]def exp[]Euler f[]def g[]def comp[]def [71] [72] [73] Overfull \hbox (36.32861pt too wide) in paragraph at lines 3119--3124 [][] \OT1/cmr/bx/n/10 sub-goal us-ing \OT1/cmr/m/it/10 finite[]jFs \OT1/ cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 finite[]jumpFs[]def \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it /10 rev[]finite[]subset$\OT1/cmr/m/n/10 )$[] Overfull \hbox (36.32861pt too wide) in paragraph at lines 3139--3144 [][] \OT1/cmr/bx/n/10 sub-goal us-ing \OT1/cmr/m/it/10 finite[]jFs \OT1/ cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 finite[]jumpFs[]def \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it /10 rev[]finite[]subset$\OT1/cmr/m/n/10 )$[] [74] [75] [76] [77] [78] [79] [80] [81] Overfull \hbox (3.1392pt too wide) in paragraph at lines 4108--4110 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathstart[]def p art[]circlepath[]def exp[]Euler f[]def g[]def comp[]def[] [82] [83] Overfull \hbox (3.80205pt too wide) in paragraph at lines 4372--4374 [][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 g st $\OT1/cmr/m/n/10 =$ \OT1/cm r/m/it/10 0 f st$\OMS/cmsy/m/n/10 6\OT1/cmr/m/n/10 =$\OT1/cmr/m/it/10 0 \OT1/cm r/bx/n/10 and \OT1/cmr/m/it/10 g[]cont$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 con- tin-u-ous $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 at[]right st$\OT1/cmr/m/n/10 )$ \ OT1/cmr/m/it/10 g \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 f[]cont$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 continuous Overfull \hbox (7.21634pt too wide) in paragraph at lines 4460--4465 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/10 us -ing []\OT1/cmr/m/it/10 cmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OMS/cmsy/m/ n/10 ^^@$\OT1/cmr/m/it/10 z0$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 6\OT1/cmr/m/n /10 =$\OT1/cmr/m/it/10 r[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 norm[]minus[]commute$\OT1/cmr/ m/n/10 )$[] Overfull \hbox (57.64598pt too wide) in paragraph at lines 4473--4475 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1 /cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 h ide[]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m /it/10 right[]neutral cancel[]comm[]monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/ cmr/m/it/10 diff[]cancel [84] Overfull \hbox (5.23206pt too wide) in paragraph at lines 4475--4476 [][] \OT1/cmr/m/it/10 cos[]diff cos[]zero mult[]eq[]0[]iff power2[]e q[]1[]iff power2[]eq[]square sin[]squared[]eq$\OT1/cmr/m/n/10 )$[] Overfull \hbox (6.58923pt too wide) in paragraph at lines 4563--4565 [][] \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 jumpF[]pathfinish[]def part[]circlepath[]def exp[]Euler f[]def g[]def comp[]def[] [85] [86] [87] Overfull \hbox (7.21634pt too wide) in paragraph at lines 4914--4919 [][] \OT1/cmr/bx/n/10 then show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/10 us -ing []\OT1/cmr/m/it/10 cmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 z$\OMS/cmsy/m/ n/10 ^^@$\OT1/cmr/m/it/10 z0$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 6\OT1/cmr/m/n /10 =$\OT1/cmr/m/it/10 r[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it /10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 norm[]minus[]commute$\OT1/cmr/ m/n/10 )$[] Overfull \hbox (57.64598pt too wide) in paragraph at lines 4927--4929 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\OT1 /cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 h ide[]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr/m /it/10 right[]neutral cancel[]comm[]monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/ cmr/m/it/10 diff[]cancel Overfull \hbox (5.23206pt too wide) in paragraph at lines 4929--4930 [][] \OT1/cmr/m/it/10 cos[]diff cos[]zero mult[]eq[]0[]iff power2[]e q[]1[]iff power2[]eq[]square sin[]squared[]eq$\OT1/cmr/m/n/10 )$[] [88] Overfull \hbox (13.45331pt too wide) in paragraph at lines 5003--5006 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis assms complex[]Re[]le[]cmod le[]less[]trans minus[]complex$\OML/cmm/m/it/10 :$\ OT1/cmr/m/it/10 simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$ Overfull \hbox (10.4239pt too wide) in paragraph at lines 5038--5040 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis cmod[]p ower2 dvd[]refl linorder[]not[]le norm[]complex[]def power2[]le[]imp[]le[] Overfull \hbox (8.69661pt too wide) in paragraph at lines 5061--5065 [][] \OT1/cmr/bx/n/10 sub-goal us-ing []\OT1/cmr/m/it/10 r$\OML/cmm/m/it/1 0 >$\OT1/cmr/m/it/10 0[] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/1 0 auto simp add$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 field[]simps divide[]simps r eal[]sqrt[]divide$\OT1/cmr/m/n/10 )$[] [89] [90] [91] [92] Overfull \hbox (15.84285pt too wide) in paragraph at lines 5580--5583 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp$\OM L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 subst sin$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 minus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/ cmm/m/it/10 ;$\OT1/cmr/m/it/10 subst cos$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 mi nus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/cmm /m/it/10 ;$\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n/10 )$[] [93] Overfull \hbox (15.84285pt too wide) in paragraph at lines 5589--5592 [][] \OT1/cmr/bx/n/10 sub-goal by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp$\OM L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 subst sin$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 minus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/ cmm/m/it/10 ;$\OT1/cmr/m/it/10 subst cos$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 mi nus[]1$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$$\OML/cmm /m/it/10 ;$\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n/10 )$[] Overfull \hbox (33.49898pt too wide) in paragraph at lines 5661--5664 []\OT1/cmr/m/n/10.95 The method "eval[]winding" \OT1/cmr/m/it/10.95 1$\OT1/cmr/ m/n/10.95 :$$:$$ [] $\OT1/cmr/m/it/10.95 a \OT1/cmr/m/n/10.95 will try to sim-p lify of the form \OT1/cmr/m/it/10.95 winding[]number [94]) (./Winding_Number_Eval_Examples.tex Overfull \hbox (5.94653pt too wide) in paragraph at lines 6--6 []\OT1/cmr/bx/n/14.4 Some ex-am-ples of ap-ply the method wind-ing[]eval Overfull \hbox (7.50224pt too wide) in paragraph at lines 66--68 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\ OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 jumpF[]pathstart[]part[]circlepath jumpF[]pat hfinish[]part[]circlepath$\OT1/cmr/m/n/10 )$[] [95] Overfull \hbox (7.50224pt too wide) in paragraph at lines 126--128 [][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\ OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 jumpF[]pathstart[]part[]circlepath jumpF[]pat hfinish[]part[]circlepath$\OT1/cmr/m/n/10 )$[] Overfull \hbox (31.35716pt too wide) in paragraph at lines 170--173 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]gt[]0[]iff[]gt mult[]pos[]pos or-der$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 asym zero[]less[]mult[]pos2$\OT1/cm r/m/n/10 )$[] Overfull \hbox (8.33937pt too wide) in paragraph at lines 184--187 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]less[]0[]iff[]less linordered []field[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sign[]simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 44$\OT1/cmr/m/n/10 )$ Overfull \hbox (8.33937pt too wide) in paragraph at lines 191--194 [][] \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 order[]asms \OT1/cmr/bx/n/10 b y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis diff[]less[]0[]iff[]less linordered []field[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 sign[]simps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 44$\OT1/cmr/m/n/10 )$ Overfull \hbox (3.7772pt too wide) in paragraph at lines 194--196 [][] \OT1/cmr/bx/n/10 show $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 complex[]of []real $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cindex[]pathE ?l1 z $\OT1/cmr/m/n/10 +$ $($\OT1/cmr/m/it/10 cindex[]pathE ?l2 z $\OT1/cmr/m/n/10 +$ $($\OT1/cmr/m/i t/10 cindex[]pathE [96])) (./root.bbl) [97] (./root.aux) ) (see the transcript file for additional information) Output written on root.pdf (97 pages, 407750 bytes). Transcript written on root.log. *** Undefined fact: "at_within_closed_interval" (line 2646 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy") *** At command "by" (line 2646 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy") *** Undefined fact: "isCont_inverse" (line 2371 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy") *** At command "by" (line 2371 of "~~/afp/thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy")