Loading theory "Green.General_Utils" (required by "Green.CircExample" via "Green.Green" via "Green.Paths" via "Green.Derivs") Loading theory "Green.PairToEuclidIntegral" ### theory "Green.General_Utils" ### 0.162s elapsed time, 0.432s cpu time, 0.000s GC time Loading theory "Green.Derivs" (required by "Green.CircExample" via "Green.Green" via "Green.Paths") locale twoD_Space fixes i :: "'a" and j :: "'a" and F_b' :: "'a \ real" and Dy :: "'a set" and pair_to_euclid :: "real \ real \ 'a" and euclid_to_pair :: "'a \ real \ real" assumes "twoD_Space i j Dy pair_to_euclid euclid_to_pair" ### theory "Green.PairToEuclidIntegral" ### 0.382s elapsed time, 0.776s cpu time, 0.000s GC time Loading theory "Green.Integrals" (required by "Green.CircExample" via "Green.Green" via "Green.Paths") ### theory "Green.Derivs" ### 0.447s elapsed time, 0.896s cpu time, 0.000s GC time ### theory "Green.Integrals" ### 0.548s elapsed time, 1.092s cpu time, 0.000s GC time Loading theory "Green.Paths" (required by "Green.CircExample" via "Green.Green") Found termination order: "{}" Found termination order: "size_list (\p. (nat \ abs) (fst p)) <*mlex*> {}" Found termination order: "size_list (\p. (nat \ abs) (fst p)) <*mlex*> {}" Proofs for inductive predicate(s) "chain_subdiv_path" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Green.Paths" ### 2.005s elapsed time, 3.968s cpu time, 0.000s GC time Loading theory "Green.Green" (required by "Green.CircExample") ### 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 rewrite rule: ### (\x. ?c1) piecewise_C1_differentiable_on ?s1 \ True ### Ignoring duplicate rewrite rule: ### \?f1 piecewise_C1_differentiable_on ?S1; ### ?g1 piecewise_C1_differentiable_on ?S1\ ### \ (\x. ?f1 x * ?g1 x) piecewise_C1_differentiable_on ### ?S1 \ ### True locale R2 fixes i :: "real \ real" and j :: "real \ real" assumes "R2 i j" locale green_typeII_cube fixes i :: "real \ real" and j :: "real \ real" and twoC :: "real \ real \ real \ real" and F :: "real \ real \ real \ real" assumes "green_typeII_cube i j twoC F" locale green_typeII_chain fixes i :: "real \ real" and j :: "real \ real" and F :: "real \ real \ real \ real" and two_chain :: "(real \ real \ real \ real) set" and s :: "(real \ real) set" assumes "green_typeII_chain i j F two_chain s" locale green_typeI_cube fixes i :: "real \ real" and j :: "real \ real" and twoC :: "real \ real \ real \ real" and F :: "real \ real \ real \ real" assumes "green_typeI_cube i j twoC F" ### Rule already declared as introduction (intro) ### open {} ### Rule already declared as introduction (intro) ### \open ?S; open ?T\ \ open (?S \ ?T) locale green_typeI_chain fixes i :: "real \ real" and j :: "real \ real" and F :: "real \ real \ real \ real" and two_chain :: "(real \ real \ real \ real) set" and s :: "(real \ real) set" assumes "green_typeI_chain i j F two_chain 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) ### \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 locale green_typeI_typeII_chain fixes s :: "(real \ real) set" and i :: "real \ real" and j :: "real \ real" and F :: "real \ real \ real \ real" and two_chain_typeI :: "(real \ real \ real \ real) set" and two_chain_typeII :: "(real \ real \ real \ real) set" assumes "green_typeI_typeII_chain s i j F two_chain_typeI two_chain_typeII" ### 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 ### theory "Green.Green" ### 1.516s elapsed time, 2.976s cpu time, 0.308s GC time Loading theory "Green.SymmetricR2Shapes" (required by "Green.CircExample") locale R2 fixes i :: "real \ real" and j :: "real \ real" assumes "R2 i j" ### theory "Green.SymmetricR2Shapes" ### 0.144s elapsed time, 0.288s cpu time, 0.000s GC time Loading theory "Green.CircExample" locale circle fixes i :: "real \ real" and j :: "real \ real" and d :: "real" assumes "circle i j d" Loading theory "Green.DiamExample" locale diamond fixes i :: "real \ real" and j :: "real \ real" and d :: "real" assumes "diamond i j d" ### theory "Green.CircExample" ### 0.550s elapsed time, 1.104s cpu time, 0.000s GC time ### theory "Green.DiamExample" ### 0.484s elapsed time, 0.972s 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 ### 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 *** SMT: Solver "z3": Timed out (setting the configuration option "smt_timeout" might help) *** At command "by" (line 986 of "~~/afp/thys/Green/PairToEuclidIntegral.thy") ### Ignoring duplicate rewrite rule: ### integral ?S1 (\x. 0::?'m1) \ 0::?'m1 ### Ignoring duplicate rewrite rule: ### integral ?S1 (\x. 0::?'m1) \ 0::?'m1 ### Ignoring duplicate rewrite rule: ### open {} \ True ### Ignoring duplicate rewrite rule: ### closed {} \ True ### Ignoring duplicate rewrite rule: ### closed UNIV \ True ### Ignoring duplicate rewrite rule: ### closed ?S1 \ closed (insert ?a1 ?S1) \ True ### Ignoring duplicate rewrite rule: ### open {?a1<..} \ True ### Ignoring duplicate rewrite rule: ### open {.. True ### Ignoring duplicate rewrite rule: ### open {?a1<.. True ### Ignoring duplicate rewrite rule: ### closed {..?a1} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..} \ True ### Ignoring duplicate rewrite rule: ### closed {?a1..?b1} \ True ### Ignoring duplicate rewrite rule: ### continuous bot ?f1 \ True ### Ignoring duplicate rewrite rule: ### continuous (at ?x1 within ?S1) (\x. x) \