Loading theory "Green.General_Utils" (required by "Green.CircExample" via "Green.Green" via "Green.Paths" via "Green.Derivs")
### theory "Green.General_Utils"
### 0.120s elapsed time, 0.368s cpu time, 0.000s GC time
Loading theory "Green.Derivs" (required by "Green.CircExample" via "Green.Green" via "Green.Paths")
Loading theory "Green.Integrals" (required by "Green.CircExample" via "Green.Green" via "Green.Paths")
### theory "Green.Derivs"
### 0.508s elapsed time, 2.004s cpu time, 0.000s GC time
### Ignoring duplicate introduction (intro)
### open {}
### Ignoring duplicate introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Ignoring duplicate introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### closed {}
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Ignoring duplicate introduction (intro)
### closed UNIV
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Ignoring duplicate introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Ignoring duplicate introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Ignoring duplicate introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Ignoring duplicate introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### theory "Green.Integrals"
### 0.605s elapsed time, 2.388s cpu time, 0.000s GC time
Loading theory "Green.Paths" (required by "Green.CircExample" via "Green.Green")
### Ignoring duplicate rewrite rule:
### (\<lambda>x. ?c1) piecewise_C1_differentiable_on ?s1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?f1 piecewise_C1_differentiable_on ?S1;
###  ?g1 piecewise_C1_differentiable_on ?S1\<rbrakk>
### \<Longrightarrow> (\<lambda>x. ?f1 x * ?g1 x) piecewise_C1_differentiable_on
###                   ?S1 \<equiv>
###                   True
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate introduction (intro)
### open {}
### Ignoring duplicate introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Ignoring duplicate introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### closed {}
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Ignoring duplicate introduction (intro)
### closed UNIV
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Ignoring duplicate introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Ignoring duplicate introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Ignoring duplicate introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Ignoring duplicate introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Ignoring duplicate introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Ignoring duplicate introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Ignoring duplicate introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Undeclared classical rule
### continuous_on ?A ?f
Found termination order: "{}"
Found termination order:
  "size_list (\<lambda>p. (nat \<circ> abs) (fst p)) <*mlex*> {}"
Found termination order:
  "size_list (\<lambda>p. (nat \<circ> 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.654s elapsed time, 10.028s cpu time, 0.224s GC time
Loading theory "Green.Green" (required by "Green.CircExample")
locale R2
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
  assumes "R2 i j"
locale green_typeII_cube
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
    and twoC :: "real \<times> real \<Rightarrow> real \<times> real"
    and F :: "real \<times> real \<Rightarrow> real \<times> real"
  assumes "green_typeII_cube i j twoC F"
locale green_typeII_chain
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
    and F :: "real \<times> real \<Rightarrow> real \<times> real"
    and
    two_chain :: "(real \<times> real \<Rightarrow> real \<times> real) set"
    and s :: "(real \<times> real) set"
  assumes "green_typeII_chain i j F two_chain s"
locale green_typeI_cube
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
    and twoC :: "real \<times> real \<Rightarrow> real \<times> real"
    and F :: "real \<times> real \<Rightarrow> real \<times> real"
  assumes "green_typeI_cube i j twoC F"
locale green_typeI_chain
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
    and F :: "real \<times> real \<Rightarrow> real \<times> real"
    and
    two_chain :: "(real \<times> real \<Rightarrow> real \<times> real) set"
    and s :: "(real \<times> real) set"
  assumes "green_typeI_chain i j F two_chain s"
locale green_typeI_typeII_chain
  fixes s :: "(real \<times> real) set"
    and i :: "real \<times> real"
    and j :: "real \<times> real"
    and F :: "real \<times> real \<Rightarrow> real \<times> real"
    and
    two_chain_typeI ::
      "(real \<times> real \<Rightarrow> real \<times> real) set"
    and
    two_chain_typeII ::
      "(real \<times> real \<Rightarrow> real \<times> real) set"
  assumes
    "green_typeI_typeII_chain s i j F two_chain_typeI two_chain_typeII"
### theory "Green.Green"
### 1.792s elapsed time, 6.792s cpu time, 0.300s GC time
Loading theory "Green.SymmetricR2Shapes" (required by "Green.CircExample")
locale R2
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
  assumes "R2 i j"
### theory "Green.SymmetricR2Shapes"
### 0.157s elapsed time, 0.628s cpu time, 0.000s GC time
Loading theory "Green.CircExample"
locale circle
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
    and d :: "real"
  assumes "circle i j d"
Loading theory "Green.DiamExample"
### theory "Green.CircExample"
### 0.846s elapsed time, 3.344s cpu time, 0.260s GC time
locale diamond
  fixes i :: "real \<times> real"
    and j :: "real \<times> real"
    and d :: "real"
  assumes "diamond i j d"
### theory "Green.DiamExample"
### 0.605s elapsed time, 2.404s cpu time, 0.000s GC time
### Ignoring duplicate rewrite rule:
### open {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed UNIV \<equiv> True
### Ignoring duplicate rewrite rule:
### closed ?S1 \<Longrightarrow> closed (insert ?a1 ?S1) \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {..<?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### open {?a1<..<?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {..?a1} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..} \<equiv> True
### Ignoring duplicate rewrite rule:
### closed {?a1..?b1} \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous bot ?f1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous (at ?x1 within ?S1) id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 (\<lambda>x. ?c1) \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?g1 ?a1 \<noteq> (0::?'b1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x / ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; 0 < ?f1 ?a1; ?f1 ?a1 \<noteq> 1;
###  0 < ?g1 ?a1\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. log (?f1 x) (?g1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; isCont ?g1 ?a1; ?f1 ?a1 \<noteq> 0\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. ?f1 x powr ?g1 x) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; cos (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. tan (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?a1; sin (?f1 ?a1) \<noteq> (0::?'a1)\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. cot (?f1 x)) ?a1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous ?F1 ?g1 \<Longrightarrow>
### continuous ?F1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 ?g1 \<Longrightarrow>
### continuous_on ?s1 (\<lambda>x. cnj (?g1 x)) \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 id \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_map ?X1 ?X1 (\<lambda>x. x) \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>isCont ?f1 ?z1;
###  ?f1 ?z1 \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk>
### \<Longrightarrow> isCont (\<lambda>x. Ln (?f1 x)) ?z1 \<equiv> True
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. ?c1) \<equiv> True
### Metis: Unused theorems: "local.Cons.prems_4"
### Ignoring duplicate rewrite rule:
### continuous_on ?s1 (\<lambda>x. x) \<equiv> True
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### [] = ?x21.1 # ?x22.1 \<equiv> False
### Ignoring duplicate rewrite rule:
### ?x21.1 # ?x22.1 = ?y21.1 # ?y22.1 \<equiv>
### ?x21.1 = ?y21.1 \<and> ?x22.1 = ?y22.1
### Metis: Unused theorems: "Product_Type.case_prodI2"
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
*** Undefined fact: "sum_not_0" (line 2004 of "$AFP/Green/Green.thy")
*** At command "using" (line 2004 of "$AFP/Green/Green.thy")
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Rule already declared as introduction (intro)
### open {}
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; open ?T\<rbrakk> \<Longrightarrow> open (?S \<union> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. open (?B x) \<Longrightarrow> open (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. open T\<rbrakk>
### \<Longrightarrow> open (\<Inter> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. open (?B x)\<rbrakk>
### \<Longrightarrow> open (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### closed {}
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<union> ?T)
### Rule already declared as introduction (intro)
### closed UNIV
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; closed ?T\<rbrakk>
### \<Longrightarrow> closed (?S \<inter> ?T)
### Rule already declared as introduction (intro)
### \<forall>x\<in>?A. closed (?B x) \<Longrightarrow>
### closed (\<Inter> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
### \<Longrightarrow> closed (\<Union> ?S)
### Rule already declared as introduction (intro)
### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
### \<Longrightarrow> closed (\<Union> (?B ` ?A))
### Rule already declared as introduction (intro)
### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
### Rule already declared as introduction (intro)
### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
### Rule already declared as introduction (intro)
### closed ?S \<Longrightarrow> open (- ?S)
### Rule already declared as introduction (intro)
### open ?S \<Longrightarrow> closed (- ?S)
### Rule already declared as introduction (intro)
### continuous_on ?s (linepath ?a ?b)
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Metis: Unused theorems: "local.neqs2_1"
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
### Ignoring duplicate rewrite rule:
### (?a1 * ?b1) ^ ?n1 \<equiv> ?a1 ^ ?n1 * ?b1 ^ ?n1
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/outline -o pdf -n outline -t /proof,/ML
*** Undefined fact: "sum_not_0" (line 2004 of "$AFP/Green/Green.thy")
*** At command "using" (line 2004 of "$AFP/Green/Green.thy")