Loading theory "HOL-Cardinals.Order_Union" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_App" via "Lambda_Free_RPOs.Extension_Orders" via "HOL-Cardinals.Wellorder_Extension")
Loading theory "Lambda_Free_RPOs.Lambda_Free_Util" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_App" via "Lambda_Free_RPOs.Lambda_Free_Term")
### theory "HOL-Cardinals.Order_Union"
### 0.200s elapsed time, 0.704s cpu time, 0.000s GC time
Loading theory "HOL-Cardinals.Wellorder_Extension" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_App" via "Lambda_Free_RPOs.Extension_Orders")
### theory "HOL-Cardinals.Wellorder_Extension"
### 0.134s elapsed time, 0.532s cpu time, 0.000s GC time
### theory "Lambda_Free_RPOs.Lambda_Free_Util"
### 1.222s elapsed time, 4.628s cpu time, 0.156s GC time
Loading theory "Lambda_Free_RPOs.Infinite_Chain" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_App" via "Lambda_Free_RPOs.Extension_Orders")
Loading theory "Lambda_Free_RPOs.Lambda_Free_Term" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_App")
locale gt_sym
  fixes
    gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool"
      (infix \<open>>\<^sub>s\<close> 50)
  assumes "gt_sym (>\<^sub>s)"
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
***  1. \<And>Q x z.
***        \<lbrakk>x \<in> Q;
***         \<forall>y.
***            (y, f z) \<in> r \<longrightarrow> y \<notin> range f\<rbrakk>
***        \<Longrightarrow> \<exists>z\<in>Q.
***                             \<forall>y.
***                                (f y, f z) \<in> r \<longrightarrow>
***                                y \<notin> Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
consts
  worst_chain :: "nat \<Rightarrow> 'a"
### theory "Lambda_Free_RPOs.Infinite_Chain"
### 0.166s elapsed time, 0.668s cpu time, 0.000s GC time
Loading theory "Lambda_Free_RPOs.Extension_Orders" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_App")
locale ext
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext ext"
locale ext_irrefl
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_irrefl ext"
locale ext_trans
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_trans ext"
locale ext_irrefl_before_trans
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_irrefl_before_trans ext"
locale ext_trans_before_irrefl
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_trans_before_irrefl ext"
locale ext_irrefl_trans_strong
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_irrefl_trans_strong ext"
locale ext_snoc
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_snoc ext"
locale ext_compat_cons
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_compat_cons ext"
locale ext_compat_snoc
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_compat_snoc ext"
locale ext_compat_list
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_compat_list ext"
locale ext_singleton
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_singleton ext"
locale ext_compat_list_strong
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_compat_list_strong ext"
locale ext_total
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_total ext"
locale ext_wf
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_wf ext"
locale ext_hd_or_tl
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_hd_or_tl ext"
locale ext_wf_bounded
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_wf_bounded ext"
Proofs for inductive predicate(s) "lexext"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
overloading
  head0 \<equiv> head0 :: ('s, 'v) tm \<Rightarrow> ('s, 'v) hd
consts
  head0 :: "('s, 'v) tm \<Rightarrow> ('s, 'v) hd"
locale ext_cwiseext
  fixes
    ext ::
      "('a \<Rightarrow> 'a \<Rightarrow> bool)
       \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes "ext_cwiseext ext"
### theory "Lambda_Free_RPOs.Extension_Orders"
### 2.548s elapsed time, 9.852s cpu time, 0.456s GC time
Found termination order: "size <*mlex*> {}"
consts
  apps ::
    "('s, 'v) tm \<Rightarrow> ('s, 'v) tm list \<Rightarrow> ('s, 'v) tm"
consts
  vars_mset :: "('s, 'v) tm \<Rightarrow> 'v multiset"
consts
  subst ::
    "('v \<Rightarrow> ('s, 'v) tm)
     \<Rightarrow> ('s, 'v) tm \<Rightarrow> ('s, 'v) tm"
Proofs for inductive predicate(s) "sub"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale arity
  fixes arity_sym :: "'s \<Rightarrow> enat"
    and arity_var :: "'v \<Rightarrow> enat"
consts
  arity_hd :: "('s, 'v) hd \<Rightarrow> enat"
Proofs for inductive predicate(s) "wary"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "wary_fo"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale ground_heads
  fixes
    gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool"
      (infix \<open>>\<^sub>s\<close> 50)
    and arity_sym :: "'s \<Rightarrow> enat"
    and arity_var :: "'v \<Rightarrow> enat"
    and ground_heads_var :: "'v \<Rightarrow> 's set"
  assumes "ground_heads (>\<^sub>s) arity_sym arity_var ground_heads_var"
consts
  ground_heads :: "('s, 'v) hd \<Rightarrow> 's set"
### theory "Lambda_Free_RPOs.Lambda_Free_Term"
### 3.773s elapsed time, 14.416s cpu time, 0.756s GC time
Loading theory "Lambda_Free_RPOs.Lambda_Encoding" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs")
Loading theory "Lambda_Free_RPOs.Lambda_Free_RPO_App" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs")
Loading theory "Lambda_Free_RPOs.Lambda_Free_RPO_Std" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_Optim")
locale lambda_encoding
  fixes lam :: "'s"
    and db :: "nat \<Rightarrow> 's"
locale rpo_app
  fixes
    gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool"
      (infix \<open>>\<^sub>s\<close> 50)
    and
    ext ::
      "(('s, 'v) tm \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool)
       \<Rightarrow> ('s, 'v) tm list
                     \<Rightarrow> ('s, 'v) tm list \<Rightarrow> bool"
  assumes "rpo_app (>\<^sub>s) ext"
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
Proofs for inductive predicate(s) "gt"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Lambda_Free_RPOs.Lambda_Encoding"
### 0.428s elapsed time, 1.688s cpu time, 0.000s GC time
### theory "Lambda_Free_RPOs.Lambda_Free_RPO_App"
### 0.415s elapsed time, 1.660s cpu time, 0.000s GC time
locale rpo_basis
  fixes ground_heads_var :: "'v \<Rightarrow> 's set"
    and
    gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool"
      (infix \<open>>\<^sub>s\<close> 50)
    and arity_sym :: "'s \<Rightarrow> enat"
    and arity_var :: "'v \<Rightarrow> enat"
    and
    extf ::
      "'s \<Rightarrow> (('s, 'v) tm
                         \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool)
                        \<Rightarrow> ('s, 'v) tm list
\<Rightarrow> ('s, 'v) tm list \<Rightarrow> bool"
  assumes "rpo_basis ground_heads_var (>\<^sub>s) arity_sym arity_var extf"
locale rpo
  fixes ground_heads_var :: "'v \<Rightarrow> 's set"
    and
    gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool"
      (infix \<open>>\<^sub>s\<close> 50)
    and
    extf ::
      "'s \<Rightarrow> (('s, 'v) tm
                         \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool)
                        \<Rightarrow> ('s, 'v) tm list
\<Rightarrow> ('s, 'v) tm list \<Rightarrow> bool"
    and arity_sym :: "'s \<Rightarrow> enat"
    and arity_var :: "'v \<Rightarrow> enat"
  assumes "rpo ground_heads_var (>\<^sub>s) extf arity_sym arity_var"
Proofs for inductive predicate(s) "gt"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_sub"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_diff"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_same"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Lambda_Free_RPOs.Lambda_Free_RPO_Std"
### 1.305s elapsed time, 5.116s cpu time, 0.284s GC time
Loading theory "Lambda_Free_RPOs.Lambda_Free_RPO_Optim" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs")
locale rpo_optim
  fixes ground_heads_var :: "'v \<Rightarrow> 's set"
    and
    gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool"
      (infix \<open>>\<^sub>s\<close> 50)
    and
    extf ::
      "'s \<Rightarrow> (('s, 'v) tm
                         \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool)
                        \<Rightarrow> ('s, 'v) tm list
\<Rightarrow> ('s, 'v) tm list \<Rightarrow> bool"
    and arity_sym :: "'s \<Rightarrow> enat"
    and arity_var :: "'v \<Rightarrow> enat"
  assumes "rpo_optim ground_heads_var (>\<^sub>s) extf arity_sym arity_var"
Proofs for inductive predicate(s) "gt"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale rpo
  fixes ground_heads_var :: "'v \<Rightarrow> 's set"
    and
    gt_sym :: "'s \<Rightarrow> 's \<Rightarrow> bool"
      (infix \<open>>\<^sub>s\<close> 50)
    and
    extf ::
      "'s \<Rightarrow> (('s, 'v) tm
                         \<Rightarrow> ('s, 'v) tm \<Rightarrow> bool)
                        \<Rightarrow> ('s, 'v) tm list
\<Rightarrow> ('s, 'v) tm list \<Rightarrow> bool"
    and arity_sym :: "'s \<Rightarrow> enat"
    and arity_var :: "'v \<Rightarrow> enat"
  assumes "rpo ground_heads_var (>\<^sub>s) extf arity_sym arity_var"
### theory "Lambda_Free_RPOs.Lambda_Free_RPO_Optim"
### 0.491s elapsed time, 1.824s cpu time, 0.000s GC time
Loading theory "Lambda_Free_RPOs.Lambda_Free_RPOs"
locale simple_rpo_instances
### theory "Lambda_Free_RPOs.Lambda_Free_RPOs"
### 0.779s elapsed time, 3.020s cpu time, 0.180s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
***  1. \<And>Q x z.
***        \<lbrakk>x \<in> Q;
***         \<forall>y.
***            (y, f z) \<in> r \<longrightarrow> y \<notin> range f\<rbrakk>
***        \<Longrightarrow> \<exists>z\<in>Q.
***                             \<forall>y.
***                                (f y, f z) \<in> r \<longrightarrow>
***                                y \<notin> Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")