Loading theory "Akra_Bazzi.Dense_Linear_Order" (required by "Akra_Bazzi.Approximation")
### ML warning (line 99 of "~~/src/HOL/Decision_Procs/langford_data.ML"):
### Pattern is not exhaustive.
### ML warning (line 100 of "~~/src/HOL/Decision_Procs/langford_data.ML"):
### Pattern is not exhaustive.
signature LANGFORD_DATA =
  sig
    val add: entry -> attribute
    val del: attribute
    type entry
    val get: Proof.context -> simpset * (thm * entry) list
    val match: Proof.context -> cterm -> entry option
  end
structure Langford_Data: LANGFORD_DATA
signature FERRANTE_RACKOF_DATA =
  sig
    val add: entry -> attribute
    val del: attribute
    type entry
    val funs:
       thm ->
         {isolate_conv:
          morphism -> Proof.context -> cterm list -> cterm -> thm,
          simpset: morphism -> Proof.context -> simpset,
          whatis: morphism -> cterm -> cterm -> ord}
           -> declaration
    val get: Proof.context -> (thm * entry) list
    val match: Proof.context -> cterm -> entry option
    datatype ord = Eq | Ge | Gt | Le | Lt | NEq | Nox
  end
structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
### ML warning (line 19 of "~~/src/HOL/Decision_Procs/langford.ML"):
### Value identifier (t) has not been referenced.
### ML warning (line 18 of "~~/src/HOL/Decision_Procs/langford.ML"):
### Matches are not exhaustive.
### ML warning (line 24 of "~~/src/HOL/Decision_Procs/langford.ML"):
### Pattern is not exhaustive.
### ML warning (line 92 of "~~/src/HOL/Decision_Procs/langford.ML"):
### Value identifier (q) has not been referenced.
### ML warning (line 92 of "~~/src/HOL/Decision_Procs/langford.ML"):
### Value identifier (p) has not been referenced.
### ML warning (line 92 of "~~/src/HOL/Decision_Procs/langford.ML"):
### Matches are not exhaustive.
### ML warning (line 102 of "~~/src/HOL/Decision_Procs/langford.ML"):
### Matches are not exhaustive.
signature LANGFORD =
  sig
    val dlo_conv: Proof.context -> cterm -> thm
    val dlo_tac: Proof.context -> int -> tactic
  end
structure Langford: LANGFORD
locale linorder_stupid_syntax =
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
  assumes "linorder_stupid_syntax less_eq less"
locale linorder_no_ub =
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
  assumes "linorder_no_ub op \<sqsubseteq> op \<sqsubset>"
locale linorder_no_lb =
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
  assumes "linorder_no_lb op \<sqsubseteq> op \<sqsubset>"
locale constr_dense_linorder =
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
    and between :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
  assumes "constr_dense_linorder op \<sqsubseteq> op \<sqsubset> between"
### ML warning (line 33 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Value identifier (simpset) has not been referenced.
### ML warning (line 32 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Value identifier (atoms) has not been referenced.
### ML warning (line 31 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Value identifier (entr) has not been referenced.
### ML warning (line 35 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Value identifier (vs) has not been referenced.
### ML warning (line 35 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Matches are not exhaustive.
### ML warning (line 63 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Matches are not exhaustive.
### ML warning (line 81 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Value identifier (xT) has not been referenced.
### ML warning (line 90 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 102 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Matches are not exhaustive.
### ML warning (line 113 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 115 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 117 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 119 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 121 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 149 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Matches are not exhaustive.
### ML warning (line 147 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 143 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 149 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Matches are not exhaustive.
### ML warning (line 147 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
### ML warning (line 143 of "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"):
### Pattern is not exhaustive.
signature FERRANTE_RACKOFF =
  sig
    val dlo_conv: Proof.context -> conv
    val dlo_tac: Proof.context -> int -> tactic
  end
structure FerranteRackoff: FERRANTE_RACKOFF
### Partially applied constant "Orderings.ord_class.less_eq" on left hand side of equation, in theorem:
### linorder.Min op \<le> (set (?x # ?xs)) \<equiv>
### fold (ord.min op \<le>) ?xs ?x
### Partially applied constant "Orderings.ord_class.less_eq" on left hand side of equation, in theorem:
### linorder.Max op \<le> (set (?x # ?xs)) \<equiv>
### fold (ord.max op \<le>) ?xs ?x
### theory "Akra_Bazzi.Dense_Linear_Order"
### 2.331s elapsed time, 3.396s cpu time, 0.148s GC time
Loading theory "Akra_Bazzi.Approximation"
consts
  horner ::
    "(nat \<Rightarrow> nat)
     \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> nat)
                   \<Rightarrow> nat
                                 \<Rightarrow> nat
         \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> real"
Found termination order: "(\<lambda>p. size (fst (snd p))) <*mlex*> {}"
Found termination order:
  "case_sum (\<lambda>p. size (fst (snd p)))
    (\<lambda>p. size (fst (snd p))) <*mlex*>
   {}"
Found termination order:
  "case_sum (\<lambda>p. size (fst (snd p)))
    (\<lambda>p. size (fst (snd p))) <*mlex*>
   {}"
Found termination order:
  "case_sum (\<lambda>p. size (fst (snd p)))
    (\<lambda>p. size (fst (snd p))) <*mlex*>
   {}"
Found termination order:
  "case_sum (\<lambda>p. size (fst (snd p)))
    (\<lambda>p. size (fst (snd p))) <*mlex*>
   {}"
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 < ?x1; 0 < ?y1\<rbrakk>
### \<Longrightarrow> ln (?x1 * ?y1) \<equiv> ln ?x1 + ln ?y1
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 < ?x1; 0 < ?y1\<rbrakk>
### \<Longrightarrow> ln (?x1 * ?y1) \<equiv> ln ?x1 + ln ?y1
### Ignoring duplicate rewrite rule:
### 0 < ?x1 \<Longrightarrow> ln (inverse ?x1) \<equiv> - ln ?x1
### Ignoring duplicate rewrite rule:
### 0 < ?x1 \<Longrightarrow> ln (inverse ?x1) \<equiv> - ln ?x1
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order:
  "case_sum (\<lambda>p. size (fst (snd p)))
    (\<lambda>p. size (fst (snd p))) <*mlex*>
   case_sum (\<lambda>x. 0) (\<lambda>x. Suc 0) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order:
  "case_sum (\<lambda>p. size (fst (snd p)))
    (\<lambda>p. size (fst (snd p))) <*mlex*>
   case_sum (\<lambda>x. Suc 0) (\<lambda>x. 0) <*mlex*>
   case_sum (\<lambda>p. size (fst (snd (snd p))))
    (\<lambda>p. size_list size (snd (snd (snd p)))) <*mlex*>
   {}"
Found termination order: "(\<lambda>p. size (fst (snd p))) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (fst (snd (snd p)))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (fst (snd (snd p)))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (fst (snd (snd (snd p))))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (fst (snd (snd p)))) <*mlex*> {}"
### Rule already declared as introduction (intro)
### ?P ?x \<Longrightarrow> \<exists>x. ?P x
### Rule already declared as introduction (intro)
### ?P ?x \<Longrightarrow> \<exists>x. ?P x
Found termination order: "(\<lambda>p. size (fst (snd p))) <*mlex*> {}"
signature APPROXIMATION =
  sig
    val approx: int -> Proof.context -> term -> term
    val approximate: Proof.context -> term -> term
    val approximation_tac:
       int ->
         (string * int) list -> int option -> Proof.context -> int -> tactic
    val reify_form: Proof.context -> term -> term
  end
structure Approximation: APPROXIMATION
### ML warning (line 200 of "~~/src/HOL/Decision_Procs/approximation_generator.ML"):
### Matches are not exhaustive.
signature APPROXIMATION_GENERATOR =
  sig
    val approximation_generator:
       Proof.context ->
         (term * term list) list ->
           bool ->
             int list ->
               (bool * term list) option * Quickcheck.report option
    val custom_seed: int Config.T
    val epsilon: real Config.T
    val precision: int Config.T
    val setup: theory -> theory
  end
structure Approximation_Generator: APPROXIMATION_GENERATOR
### theory "Akra_Bazzi.Approximation"
### 51.600s elapsed time, 85.872s cpu time, 3.884s GC time
Loading theory "Akra_Bazzi.Eval_Numeral" (required by "Akra_Bazzi.Akra_Bazzi_Method")
Loading theory "Akra_Bazzi.Akra_Bazzi_Library" (required by "Akra_Bazzi.Akra_Bazzi" via "Akra_Bazzi.Akra_Bazzi_Real" via "Akra_Bazzi.Akra_Bazzi_Asymptotics")
signature EVAL_NUMERAL =
  sig val eval_numeral_tac: Proof.context -> int -> tactic end
structure Eval_Numeral: EVAL_NUMERAL
### theory "Akra_Bazzi.Eval_Numeral"
### 0.323s elapsed time, 0.708s cpu time, 0.000s GC time
### theory "Akra_Bazzi.Akra_Bazzi_Library"
### 0.357s elapsed time, 0.776s cpu time, 0.000s GC time
Loading theory "Akra_Bazzi.Akra_Bazzi_Asymptotics" (required by "Akra_Bazzi.Akra_Bazzi" via "Akra_Bazzi.Akra_Bazzi_Real")
### Ignoring duplicate rewrite rule:
### 0 < ?x1 \<Longrightarrow> ?x1 powr numeral ?n1 \<equiv> ?x1 ^ numeral ?n1
locale akra_bazzi_asymptotics_bep =
  fixes b :: "real" 
    and e :: "real" 
    and p :: "real" 
    and hb :: "real" 
  assumes "akra_bazzi_asymptotics_bep b e hb"
### theory "Akra_Bazzi.Akra_Bazzi_Asymptotics"
### 0.580s elapsed time, 1.164s cpu time, 0.000s GC time
Loading theory "Akra_Bazzi.Akra_Bazzi_Real" (required by "Akra_Bazzi.Akra_Bazzi")
locale akra_bazzi_integral =
  fixes
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
  assumes "akra_bazzi_integral integrable integral"
locale akra_bazzi_params =
  fixes k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
  assumes "akra_bazzi_params k as bs"
locale akra_bazzi_params_nonzero =
  fixes k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
  assumes "akra_bazzi_params_nonzero k as bs"
locale akra_bazzi_real_recursion =
  fixes as :: "real list" 
    and bs :: "real list" 
    and hs :: "(real \<Rightarrow> real) list" 
    and k :: "nat" 
    and x\<^sub>0 :: "real" 
    and x\<^sub>1 :: "real" 
    and hb :: "real" 
    and e :: "real" 
    and p :: "real" 
  assumes "akra_bazzi_real_recursion as bs hs k x\<^sub>0 x\<^sub>1 hb e p"
locale akra_bazzi_real =
  fixes as :: "real list" 
    and bs :: "real list" 
    and hs :: "(real \<Rightarrow> real) list" 
    and k :: "nat" 
    and x\<^sub>0 :: "real" 
    and x\<^sub>1 :: "real" 
    and hb :: "real" 
    and e :: "real" 
    and p :: "real" 
    and
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
    and f :: "real \<Rightarrow> real" 
    and g :: "real \<Rightarrow> real" 
    and C :: "real" 
  assumes
    "akra_bazzi_real as bs hs k x\<^sub>0 x\<^sub>1 hb e p integrable
      integral f g C"
locale akra_bazzi_nat_to_real =
  fixes as :: "real list" 
    and bs :: "real list" 
    and hs :: "(real \<Rightarrow> real) list" 
    and k :: "nat" 
    and x\<^sub>0 :: "real" 
    and x\<^sub>1 :: "real" 
    and hb :: "real" 
    and e :: "real" 
    and p :: "real" 
    and f :: "nat \<Rightarrow> real" 
    and g :: "real \<Rightarrow> real" 
  assumes "akra_bazzi_nat_to_real as bs hs k x\<^sub>0 x\<^sub>1 hb e p f g"
locale akra_bazzi_real_lower =
  fixes as :: "real list" 
    and bs :: "real list" 
    and hs :: "(real \<Rightarrow> real) list" 
    and k :: "nat" 
    and x\<^sub>0 :: "real" 
    and x\<^sub>1 :: "real" 
    and hb :: "real" 
    and e :: "real" 
    and p :: "real" 
    and
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
    and f :: "real \<Rightarrow> real" 
    and g :: "real \<Rightarrow> real" 
    and C :: "real" 
    and fb2 :: "real" 
    and gb2 :: "real" 
    and c2 :: "real" 
  assumes
    "akra_bazzi_real_lower as bs hs k x\<^sub>0 x\<^sub>1 hb e p integrable
      integral f g C fb2 gb2 c2"
locale akra_bazzi_real_upper =
  fixes as :: "real list" 
    and bs :: "real list" 
    and hs :: "(real \<Rightarrow> real) list" 
    and k :: "nat" 
    and x\<^sub>0 :: "real" 
    and x\<^sub>1 :: "real" 
    and hb :: "real" 
    and e :: "real" 
    and p :: "real" 
    and
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
    and f :: "real \<Rightarrow> real" 
    and g :: "real \<Rightarrow> real" 
    and C :: "real" 
    and fb1 :: "real" 
    and c1 :: "real" 
  assumes
    "akra_bazzi_real_upper as bs hs k x\<^sub>0 x\<^sub>1 hb e p integrable
      integral f g C fb1 c1"
### theory "Akra_Bazzi.Akra_Bazzi_Real"
### 1.258s elapsed time, 2.516s cpu time, 0.228s GC time
Loading theory "Akra_Bazzi.Akra_Bazzi"
locale akra_bazzi_recursion =
  fixes x\<^sub>0 :: "nat" 
    and x\<^sub>1 :: "nat" 
    and k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
    and ts :: "(nat \<Rightarrow> nat) list" 
    and f :: "nat \<Rightarrow> real" 
  assumes "akra_bazzi_recursion x\<^sub>0 x\<^sub>1 k as bs ts"
locale akra_bazzi_function =
  fixes x\<^sub>0 :: "nat" 
    and x\<^sub>1 :: "nat" 
    and k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
    and ts :: "(nat \<Rightarrow> nat) list" 
    and f :: "nat \<Rightarrow> real" 
    and
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
    and g :: "nat \<Rightarrow> real" 
  assumes
    "akra_bazzi_function x\<^sub>0 x\<^sub>1 k as bs ts f integrable
      integral g"
locale akra_bazzi_lower =
  fixes x\<^sub>0 :: "nat" 
    and x\<^sub>1 :: "nat" 
    and k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
    and ts :: "(nat \<Rightarrow> nat) list" 
    and f :: "nat \<Rightarrow> real" 
    and
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
    and g :: "nat \<Rightarrow> real" 
    and g' :: "real \<Rightarrow> real" 
  assumes
    "akra_bazzi_lower x\<^sub>0 x\<^sub>1 k as bs ts f integrable integral g
      g'"
locale akra_bazzi_upper =
  fixes x\<^sub>0 :: "nat" 
    and x\<^sub>1 :: "nat" 
    and k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
    and ts :: "(nat \<Rightarrow> nat) list" 
    and f :: "nat \<Rightarrow> real" 
    and
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
    and g :: "nat \<Rightarrow> real" 
    and g' :: "real \<Rightarrow> real" 
  assumes
    "akra_bazzi_upper x\<^sub>0 x\<^sub>1 k as bs ts f integrable integral g
      g'"
locale akra_bazzi =
  fixes x\<^sub>0 :: "nat" 
    and x\<^sub>1 :: "nat" 
    and k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
    and ts :: "(nat \<Rightarrow> nat) list" 
    and f :: "nat \<Rightarrow> real" 
    and
    integrable ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
      
    and
    integral ::
      "(real \<Rightarrow> real)
       \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
      
    and g :: "nat \<Rightarrow> real" 
    and g' :: "real \<Rightarrow> real" 
  assumes
    "akra_bazzi x\<^sub>0 x\<^sub>1 k as bs ts f integrable integral g g'"
### theory "Akra_Bazzi.Akra_Bazzi"
### 2.007s elapsed time, 3.996s cpu time, 0.228s GC time
Loading theory "Akra_Bazzi.Master_Theorem"
locale master_theorem_function =
  fixes x\<^sub>0 :: "nat" 
    and x\<^sub>1 :: "nat" 
    and k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
    and ts :: "(nat \<Rightarrow> nat) list" 
    and f :: "nat \<Rightarrow> real" 
    and g :: "nat \<Rightarrow> real" 
  assumes "master_theorem_function x\<^sub>0 x\<^sub>1 k as bs ts f g"
### theory "Akra_Bazzi.Master_Theorem"
### 1.444s elapsed time, 2.740s cpu time, 0.000s GC time
Loading theory "Akra_Bazzi.Akra_Bazzi_Method"
locale master_theorem_function =
  fixes x\<^sub>0 :: "nat" 
    and x\<^sub>1 :: "nat" 
    and k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
    and ts :: "(nat \<Rightarrow> nat) list" 
    and f :: "nat \<Rightarrow> real" 
    and g :: "nat \<Rightarrow> real" 
  assumes "master_theorem_function x\<^sub>0 x\<^sub>1 k as bs ts f g"
### ML warning (line 369 of "~~/afp/thys/Akra_Bazzi/Akra_Bazzi_Method.thy"):
### Pattern is not exhaustive.
val generalize_master_thm = fn: Proof.context -> thm -> thm
val generalize_master_thm' = fn:
   binding * thm -> Proof.context -> local_theory
### ML warning (line 498 of "~~/afp/thys/Akra_Bazzi/akra_bazzi.ML"):
### Value identifier (find_funvar) has not been referenced.
signature AKRA_BAZZI =
  sig
    val akra_bazzi_measure_tac: Proof.context -> int -> tactic
    val akra_bazzi_relation_tac: Proof.context -> int -> tactic
    val akra_bazzi_sum_tac: Proof.context -> int -> tactic
    val akra_bazzi_term_tac: Proof.context -> int -> tactic
    val akra_bazzi_termination_tac: Proof.context -> int -> tactic
    val master_theorem_function_tac: bool -> Proof.context -> int -> tactic
    val master_theorem_tac:
       string option ->
         bool ->
           thm option ->
             term option ->
               term option -> term option -> Proof.context -> int -> tactic
    val setup_master_theorem:
       Context.generic * Token.T list ->
         (Proof.context -> Method.method) * (Context.generic * Token.T list)
  end
structure Akra_Bazzi: AKRA_BAZZI
### theory "Akra_Bazzi.Akra_Bazzi_Method"
### 1.564s elapsed time, 3.080s cpu time, 0.244s GC time
Loading theory "Akra_Bazzi.Akra_Bazzi_Approximation"
locale akra_bazzi_params_nonzero =
  fixes k :: "nat" 
    and as :: "real list" 
    and bs :: "real list" 
  assumes "akra_bazzi_params_nonzero k as bs"
signature AKRA_BAZZI_APPROXIMATION =
  sig
    val akra_bazzi_approximate_tac: int -> Proof.context -> int -> tactic
  end
structure Akra_Bazzi_Approximation: AKRA_BAZZI_APPROXIMATION
### theory "Akra_Bazzi.Akra_Bazzi_Approximation"
### 1.010s elapsed time, 2.024s cpu time, 0.000s GC time
Loading theory "Akra_Bazzi.Master_Theorem_Examples"
locale det_select =
  fixes b :: "real" 
  assumes "det_select b"
### theory "Akra_Bazzi.Master_Theorem_Examples"
### 2.352s elapsed time, 4.696s cpu time, 0.204s GC time
### Ignoring duplicate rewrite rule:
### of_nat (Suc ?m1) \<equiv> (1::?'a1) + of_nat ?m1
*** Interrupt