Loading theory "HOL-Data_Structures.Cmp" (required by "Random_BSTs.Random_BSTs" via "HOL-Data_Structures.Tree_Set")
Loading theory "HOL-Data_Structures.Less_False" (required by "Random_BSTs.Random_BSTs" via "HOL-Data_Structures.Tree_Set" via "HOL-Data_Structures.Set_Specs" via "HOL-Data_Structures.List_Ins_Del" via "HOL-Data_Structures.Sorted_Less")
### theory "HOL-Data_Structures.Less_False"
### 0.040s elapsed time, 0.120s cpu time, 0.000s GC time
Loading theory "HOL-Data_Structures.Sorted_Less" (required by "Random_BSTs.Random_BSTs" via "HOL-Data_Structures.Tree_Set" via "HOL-Data_Structures.Set_Specs" via "HOL-Data_Structures.List_Ins_Del")
### theory "HOL-Data_Structures.Sorted_Less"
### 0.079s elapsed time, 0.220s cpu time, 0.000s GC time
Loading theory "HOL-Data_Structures.List_Ins_Del" (required by "Random_BSTs.Random_BSTs" via "HOL-Data_Structures.Tree_Set" via "HOL-Data_Structures.Set_Specs")
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "HOL-Data_Structures.Cmp"
### 0.536s elapsed time, 1.176s cpu time, 0.000s GC time
Loading theory "HOL-Library.Function_Algebras" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort" via "Landau_Symbols.Landau_More" via "Landau_Symbols.Landau_Simprocs" via "Landau_Symbols.Landau_Real_Products")
### theory "HOL-Data_Structures.List_Ins_Del"
### 0.414s elapsed time, 0.828s cpu time, 0.000s GC time
Loading theory "HOL-Data_Structures.Set_Specs" (required by "Random_BSTs.Random_BSTs" via "HOL-Data_Structures.Tree_Set")
instantiation
  fun :: (type, plus) plus
  plus_fun == plus ::
    ('a \<Rightarrow> 'b)
    \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b
instantiation
  fun :: (type, zero) zero
  zero_fun == zero_class.zero :: 'a \<Rightarrow> 'b
locale Set
  fixes empty :: "'s"
    and insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    and delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    and isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
    and set :: "'s \<Rightarrow> 'a set"
    and invar :: "'s \<Rightarrow> bool"
  assumes "Set empty insert delete isin set invar"
instantiation
  fun :: (type, times) times
  times_fun == times ::
    ('a \<Rightarrow> 'b)
    \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b
instantiation
  fun :: (type, one) one
  one_fun == one_class.one :: 'a \<Rightarrow> 'b
locale Set_by_Ordered
  fixes empty :: "'t"
    and insert :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    and delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
    and isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
    and inorder :: "'t \<Rightarrow> 'a list"
    and inv :: "'t \<Rightarrow> bool"
  assumes "Set_by_Ordered empty insert delete isin inorder inv"
locale Set2
  fixes empty :: "'s"
    and delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    and isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
    and set :: "'s \<Rightarrow> 'a set"
    and invar :: "'s \<Rightarrow> bool"
    and insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
    and union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and diff :: "'s \<Rightarrow> 's \<Rightarrow> 's"
  assumes "Set2 empty delete isin set invar insert union inter diff"
### theory "HOL-Library.Function_Algebras"
### 0.169s elapsed time, 0.336s cpu time, 0.000s GC time
Loading theory "HOL-Library.Landau_Symbols" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort" via "Landau_Symbols.Landau_More")
### theory "HOL-Data_Structures.Set_Specs"
### 0.170s elapsed time, 0.340s cpu time, 0.000s GC time
Loading theory "HOL-Data_Structures.Tree_Set" (required by "Random_BSTs.Random_BSTs")
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
locale landau_symbol
  fixes
    L :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    L' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    Lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
  assumes "landau_symbol L L' Lr"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
### Missing patterns in function definition:
### split_min \<langle>\<rangle> = undefined
Found termination order: "size <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
locale landau_pair
  fixes
    L :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    l :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    L' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    l' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    Lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
    and
    lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
    and R :: "real \<Rightarrow> real \<Rightarrow> bool"
  assumes "landau_pair L l L' l' Lr lr R"
### theory "HOL-Data_Structures.Tree_Set"
### 1.316s elapsed time, 2.572s cpu time, 0.400s GC time
Loading theory "Landau_Symbols.Group_Sort" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort" via "Landau_Symbols.Landau_More" via "Landau_Symbols.Landau_Simprocs" via "Landau_Symbols.Landau_Real_Products")
locale landau_pair
  fixes
    L :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    l :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    L' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    l' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    Lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
    and
    lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
    and R :: "real \<Rightarrow> real \<Rightarrow> bool"
  assumes "landau_pair L l L' l' Lr lr R"
locale groupsort
  fixes f :: "'a \<Rightarrow> 'b"
    and merge :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and g :: "'a list \<Rightarrow> 'c"
  assumes "groupsort f merge g"
locale landau_pair
  fixes
    L :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    l :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    L' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    l' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    Lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
    and
    lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
    and R :: "real \<Rightarrow> real \<Rightarrow> bool"
  assumes "landau_pair L l L' l' Lr lr R"
locale landau_symbol
  fixes
    L :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    L' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    Lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
  assumes "landau_symbol L L' Lr"
Found termination order: "length <*mlex*> {}"
locale landau_symbol
  fixes
    L :: "'a filter
          \<Rightarrow> ('a \<Rightarrow> 'b)
                        \<Rightarrow> ('a \<Rightarrow> 'b) set"
    and
    L' ::
      "'c filter
       \<Rightarrow> ('c \<Rightarrow> 'b)
                     \<Rightarrow> ('c \<Rightarrow> 'b) set"
    and
    Lr ::
      "'a filter
       \<Rightarrow> ('a \<Rightarrow> real)
                     \<Rightarrow> ('a \<Rightarrow> real) set"
  assumes "landau_symbol L L' Lr"
### theory "Landau_Symbols.Group_Sort"
### 1.274s elapsed time, 2.532s cpu time, 0.000s GC time
Loading theory "List-Index.List_Index" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort" via "Comparison_Sort_Lower_Bound.Linorder_Relations")
consts
  find_index ::
    "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
bundle asymp_equiv_notation
consts
  map_index' ::
    "nat
     \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'b)
                   \<Rightarrow> 'a list \<Rightarrow> 'b list"
consts
  insert_nth ::
    "nat \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
### theory "HOL-Library.Landau_Symbols"
### 3.142s elapsed time, 5.976s cpu time, 0.400s GC time
Loading theory "Landau_Symbols.Landau_Real_Products" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort" via "Landau_Symbols.Landau_More" via "Landau_Symbols.Landau_Simprocs")
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "List-Index.List_Index"
### 0.809s elapsed time, 1.268s cpu time, 0.000s GC time
Loading theory "Comparison_Sort_Lower_Bound.Linorder_Relations" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort")
Proofs for inductive predicate(s) "sorted_wrt"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  insert_wrt ::
    "('a \<times> 'a) set
     \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
### theory "Comparison_Sort_Lower_Bound.Linorder_Relations"
### 0.854s elapsed time, 1.592s cpu time, 0.000s GC time
consts
  bigtheta_pow ::
    "'a filter
     \<Rightarrow> ('a \<Rightarrow> 'b) set
                   \<Rightarrow> nat
                                 \<Rightarrow> ('a \<Rightarrow> 'b) set"
locale landau_function_family
  fixes F :: "'a filter"
    and H :: "('a \<Rightarrow> real) set"
  assumes "landau_function_family F H"
locale landau_function_family_pair
  fixes F :: "'a filter"
    and G :: "('a \<Rightarrow> real) set"
    and H :: "('a \<Rightarrow> real) set"
    and g :: "'a \<Rightarrow> real"
  assumes "landau_function_family_pair F G H g"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
consts
  landau_dominating_chain' ::
    "'a filter
     \<Rightarrow> ('a \<Rightarrow> real) list \<Rightarrow> bool"
consts
  nonneg_list :: "'a list \<Rightarrow> bool"
consts
  pos_list :: "'a list \<Rightarrow> bool"
locale landau_function_family_chain
  fixes F :: "'b filter"
    and gs :: "'a list"
    and get_param :: "'a \<Rightarrow> real"
    and get_fun :: "'a \<Rightarrow> 'b \<Rightarrow> real"
  assumes "landau_function_family_chain F gs get_fun"
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
instantiation
  primfun :: linorder
  less_eq_primfun == less_eq ::
    primfun \<Rightarrow> primfun \<Rightarrow> bool
  less_primfun == less :: primfun \<Rightarrow> primfun \<Rightarrow> bool
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
### Rule already declared as introduction (intro)
### ?f \<in> L ?F ?g \<Longrightarrow> L ?F ?f \<subseteq> L ?F ?g
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
### Rule already declared as introduction (intro)
### ?f \<in> L ?F ?g \<Longrightarrow> l ?F ?f \<subseteq> l ?F ?g
Found termination order: "size_list size <*mlex*> {}"
### Ignoring duplicate rewrite rule:
### (\<lambda>x. - ?f1 x) \<in> o[?F1](?g1) \<equiv> ?f1 \<in> o[?F1](?g1)
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
### Ignoring duplicate rewrite rule:
### (\<lambda>x. norm (?f1 x)) \<in> O[?F1](\<lambda>x. norm (?g1 x)) \<equiv>
### ?f1 \<in> O[?F1](?g1)
### Ignoring duplicate rewrite rule:
### ?c1 \<noteq> (0::?'b1) \<Longrightarrow>
### O[?F1](\<lambda>x. ?c1 * ?f1 x) \<equiv> O[?F1](?f1)
### Ignoring duplicate rewrite rule:
### ?c1 \<noteq> (0::?'b1) \<Longrightarrow>
### \<Omega>[?F1](\<lambda>x. ?c1 * ?f1 x) \<equiv> \<Omega>[?F1](?f1)
### Ignoring duplicate rewrite rule:
### ?c1 \<noteq> (0::?'b1) \<Longrightarrow>
### (\<lambda>x. ?c1 * ?f1 x) \<in> O[?F1](?g1) \<equiv> ?f1 \<in> O[?F1](?g1)
### Ignoring duplicate rewrite rule:
### ?c1 \<noteq> (0::?'b1) \<Longrightarrow>
### (\<lambda>x. ?c1 * ?f1 x) \<in> \<Omega>[?F1](?g1) \<equiv>
### ?f1 \<in> \<Omega>[?F1](?g1)
### Ignoring duplicate rewrite rule:
### pos_primfun_list [] \<equiv> False
### Ignoring duplicate rewrite rule:
### pos_primfun_list ((?uu1, ?x1) # ?xs1) \<equiv>
### (0::?'b1) < ?x1 \<or> ?x1 = (0::?'b1) \<and> pos_primfun_list ?xs1
### Ignoring duplicate rewrite rule:
### nonneg_primfun_list [] \<equiv> True
### Ignoring duplicate rewrite rule:
### nonneg_primfun_list ((?uu1, ?x1) # ?xs1) \<equiv>
### (0::?'b1) < ?x1 \<or> ?x1 = (0::?'b1) \<and> nonneg_primfun_list ?xs1
### Ignoring duplicate rewrite rule:
### iszero_primfun_list [] \<equiv> True
### Ignoring duplicate rewrite rule:
### iszero_primfun_list ((?uu1, ?x1) # ?xs1) \<equiv>
### ?x1 = (0::?'b1) \<and> iszero_primfun_list ?xs1
### theory "Landau_Symbols.Landau_Real_Products"
### 4.729s elapsed time, 9.212s cpu time, 1.012s GC time
Loading theory "Landau_Symbols.Landau_Simprocs" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort" via "Landau_Symbols.Landau_More")
### ML warning (line 63 of "~~/afp/thys/Landau_Symbols/landau_simprocs.ML"):
### Value identifier (dest_bigtheta) has not been referenced.
### ML warning (line 176 of "~~/afp/thys/Landau_Symbols/landau_simprocs.ML"):
### Value identifier (x_name2) has not been referenced.
### ML warning (line 185 of "~~/afp/thys/Landau_Symbols/landau_simprocs.ML"):
### Value identifier (rest2) has not been referenced.
### ML warning (line 185 of "~~/afp/thys/Landau_Symbols/landau_simprocs.ML"):
### Value identifier (rest1) has not been referenced.
### ML warning (line 318 of "~~/afp/thys/Landau_Symbols/landau_simprocs.ML"):
### Pattern is not exhaustive.
### ML warning (line 373 of "~~/afp/thys/Landau_Symbols/landau_simprocs.ML"):
### Pattern is not exhaustive.
signature LANDAU =
  sig
    val cancel_factor_conv: Proof.context -> cterm -> thm
    val cancel_factor_simproc: Proof.context -> cterm -> thm option
    val dest_landau: term -> term * term * term
    val landau_const_names: string list
    val landau_sum_limit: int Config.T
    val lift_landau_conv: conv -> conv
    val lift_landau_simproc:
       (Proof.context -> cterm -> thm option) ->
         Proof.context -> cterm -> thm option
    val simplify_landau_product_conv: Proof.context -> conv
    val simplify_landau_product_simproc:
       Proof.context -> cterm -> thm option
    val simplify_landau_real_prod_prop_conv: Proof.context -> conv
    val simplify_landau_real_prod_prop_simproc:
       Proof.context -> cterm -> thm option
    val simplify_landau_sum_conv: Proof.context -> conv
    val simplify_landau_sum_simproc: Proof.context -> cterm -> thm option
  end
structure Landau: LANDAU
### theory "Landau_Symbols.Landau_Simprocs"
### 0.604s elapsed time, 1.200s cpu time, 0.000s GC time
Loading theory "Landau_Symbols.Landau_More" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case" via "Quick_Sort_Cost.Randomised_Quick_Sort")
### theory "Landau_Symbols.Landau_More"
### 0.239s elapsed time, 0.476s cpu time, 0.000s GC time
Loading theory "Quick_Sort_Cost.Randomised_Quick_Sort" (required by "Random_BSTs.Random_BSTs" via "Quick_Sort_Cost.Quick_Sort_Average_Case")
### Ignoring duplicate rewrite rule:
### (\<lambda>x. inverse (?f1 x))
### \<in> \<Theta>[?F1](\<lambda>x. inverse (?g1 x)) \<equiv>
### ?f1 \<in> \<Theta>[?F1](?g1)
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
### theory "Quick_Sort_Cost.Randomised_Quick_Sort"
### 3.172s elapsed time, 6.316s cpu time, 0.324s GC time
Loading theory "Quick_Sort_Cost.Quick_Sort_Average_Case" (required by "Random_BSTs.Random_BSTs")
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "Quick_Sort_Cost.Quick_Sort_Average_Case"
### 1.179s elapsed time, 2.364s cpu time, 0.000s GC time
Loading theory "Random_BSTs.Random_BSTs"
### Ignoring duplicate rewrite rule:
### set_tree ?t1 = {} \<equiv> ?t1 = \<langle>\<rangle>
Found termination order: "length <*mlex*> {}"
### theory "Random_BSTs.Random_BSTs"
### 2.773s elapsed time, 5.504s cpu time, 0.392s GC time
### Rule already declared as introduction (intro)
### \<lbrakk>linorder_on ?A ?R; set (?x # ?xs) \<subseteq> ?A;
###  Linorder_Relations.sorted_wrt ?R ?xs\<rbrakk>
### \<Longrightarrow> Linorder_Relations.sorted_wrt ?R (insert_wrt ?R ?x ?xs)
### Rule already declared as introduction (intro)
### \<lbrakk>linorder_on ?A ?R; set ?xs \<subseteq> ?A\<rbrakk>
### \<Longrightarrow> Linorder_Relations.sorted_wrt ?R (insort_wrt ?R ?xs)
### Rule already declared as introduction (intro)
### \<lbrakk>linorder_on ?A ?R; set ?xs \<subseteq> ?A\<rbrakk>
### \<Longrightarrow> Linorder_Relations.sorted_wrt ?R (insort_wrt ?R ?xs)
### Ignoring duplicate rewrite rule:
### (\<lambda>x. ?f1 x powr ?p1) \<in> powr_closure ?f1 \<equiv> True
### Ignoring duplicate rewrite rule:
### (\<lambda>x. ?f1 x powr ?p1) \<in> powr_closure ?f1 \<equiv> True
\<forall>\<^sub>F n in ?F. ?P n = ?Q n \<Longrightarrow>
eventually ?P ?F = eventually ?Q ?F
\<forall>\<^sub>F x in F. f x = g x
val it =
   "(\<lambda>x.
        5 * (ln (ln x))\<^sup>2 / (2 * x) powr (15 / 10) * inverse 2)
    \<in> \<omega>(\<lambda>x.
                      3 * ln x * ln x / x * ln (ln (ln (ln x)))) \<equiv>
    3 = 0 \<or>
    5 * inverse (2 powr (15 / 10)) * inverse 2 \<noteq> 0 \<and>
    pos_primfun_list
     (group_primfuns
       [(LnChain 1, - 1), (LnChain 1, - 1), (LnChain 0, 1),
        (LnChain 4, - 1), (LnChain 2, real 2), (LnChain 0, - (15 / 10))])":
   thm
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Ignoring duplicate simplification procedure "Landau_Simprocs.simplify_landau_sum"
### Rule already declared as introduction (intro)
### finite ?F \<Longrightarrow> finite (?h ` ?F)
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Treaps/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Treaps/outline -o pdf -n outline -t /proof,/ML
*** Type unification failed: Clash of types "_ list" and "_ tree"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  Tree_Set.set :: ??'a tree \<Rightarrow> ??'a set
*** Operand:   xs :: ??'b list
*** 
*** Coercion Inference:
*** 
*** Local coercion insertion on the operand failed:
*** No coercion known for type constructors: "list" and "tree"
*** At command "lemma" (line 120 of "~~/afp/thys/Random_BSTs/Random_BSTs.thy")