Loading theory "HOL-Cardinals.Order_Union" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Lambda_Free_RPOs.Extension_Orders" via "HOL-Cardinals.Wellorder_Extension") Loading theory "Abstract-Rewriting.Seq" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting") Loading theory "HOL-Library.While_Combinator" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking") Loading theory "Lambda_Free_RPOs.Lambda_Free_Util" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Lambda_Free_RPOs.Lambda_Free_Term") locale infinitely_many fixes p :: "nat \ bool" assumes "infinitely_many p" ### theory "HOL-Cardinals.Order_Union" ### 0.214s elapsed time, 0.960s cpu time, 0.000s GC time Loading theory "HOL-Cardinals.Wellorder_Extension" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Lambda_Free_RPOs.Extension_Orders") Found termination order: "size <*mlex*> {}" ### theory "HOL-Cardinals.Wellorder_Extension" ### 0.119s elapsed time, 0.476s cpu time, 0.000s GC time Loading theory "Matrix.Utility" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials") Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "{}" Found termination order: "(\p. length (snd p)) <*mlex*> (\p. length (fst p)) <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" ### theory "Abstract-Rewriting.Seq" ### 0.662s elapsed time, 2.744s cpu time, 0.000s GC time Loading theory "Regular-Sets.Regular_Set" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking" via "Regular-Sets.NDerivative" via "Regular-Sets.Regular_Exp") Found termination order: "{}" Found termination order: "size_list size <*mlex*> {}" ### theory "Matrix.Utility" ### 0.496s elapsed time, 1.984s cpu time, 0.000s GC time Found termination order: "{}" ### theory "HOL-Library.While_Combinator" ### 0.973s elapsed time, 3.864s cpu time, 0.000s GC time ### theory "Lambda_Free_RPOs.Lambda_Free_Util" ### 1.139s elapsed time, 4.368s cpu time, 0.000s GC time Loading theory "Lambda_Free_RPOs.Infinite_Chain" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Lambda_Free_RPOs.Extension_Orders") Loading theory "Lambda_Free_RPOs.Lambda_Free_Term" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util") consts worst_chain :: "nat \ 'a" locale gt_sym fixes gt_sym :: "'s \ 's \ bool" (infix \>\<^sub>s\ 50) assumes "gt_sym (>\<^sub>s)" ### theory "Lambda_Free_RPOs.Infinite_Chain" ### 0.193s elapsed time, 0.580s cpu time, 0.000s GC time Loading theory "Lambda_Free_RPOs.Extension_Orders" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util") locale ext fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext ext" locale ext_irrefl fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_irrefl ext" locale ext_trans fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_trans ext" locale ext_irrefl_before_trans fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_irrefl_before_trans ext" locale ext_trans_before_irrefl fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_trans_before_irrefl ext" locale ext_irrefl_trans_strong fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_irrefl_trans_strong ext" locale ext_snoc fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_snoc ext" locale ext_compat_cons fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_compat_cons ext" locale ext_compat_snoc fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_compat_snoc ext" locale ext_compat_list fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_compat_list ext" locale ext_singleton fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_singleton ext" locale ext_compat_list_strong fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_compat_list_strong ext" locale ext_total fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_total ext" locale ext_wf fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_wf ext" locale ext_hd_or_tl fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_hd_or_tl ext" locale ext_wf_bounded fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ 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 ... locale ext_cwiseext fixes ext :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" assumes "ext_cwiseext ext" datatype 'a ref = ref of 'a ROOT.ML:16: warning: Value identifier (A_) has not been referenced. ROOT.ML:13: warning: Value identifier (x22) has not been referenced. ROOT.ML:13: warning: Value identifier (x21) has not been referenced. ROOT.ML:13: warning: Value identifier (A_) has not been referenced. ROOT.ML:12: warning: Value identifier (x22) has not been referenced. ROOT.ML:12: warning: Value identifier (x21) has not been referenced. ROOT.ML:12: warning: Value identifier (A_) has not been referenced. ROOT.ML:23: warning: Value identifier (f) has not been referenced. ROOT.ML:25: warning: Value identifier (f) has not been referenced. ROOT.ML:28: warning: Value identifier (f) has not been referenced. ROOT.ML:31: warning: Matches are not exhaustive. Found near fun image f (... ...) = Set (... ... xs) ROOT.ML:33: warning: Value identifier (y) has not been referenced. ROOT.ML:33: warning: Value identifier (A_) has not been referenced. ROOT.ML:39: warning: Value identifier (x) has not been referenced. ROOT.ML:39: warning: Value identifier (A_) has not been referenced. ROOT.ML:48: warning: Value identifier (p) has not been referenced. ROOT.ML:56: warning: Matches are not exhaustive. Found near fun product (Set xs) (... ...) = Set (... ... xs) structure Generated_Code: sig val conc: 'a equal -> 'a list set -> 'a list set -> 'a list set type 'a equal type 'a set end overloading lang_pow \ compow :: nat \ 'a list set \ 'a list set consts lang_pow :: "nat \ 'a list set \ 'a list set" ### theory "Lambda_Free_RPOs.Extension_Orders" ### 2.599s elapsed time, 7.928s cpu time, 0.556s GC time overloading head0 \ head0 :: ('s, 'v) tm \ ('s, 'v) hd consts head0 :: "('s, 'v) tm \ ('s, 'v) hd" Found termination order: "size <*mlex*> {}" consts apps :: "('s, 'v) tm \ ('s, 'v) tm list \ ('s, 'v) tm" ### theory "Regular-Sets.Regular_Set" ### 3.902s elapsed time, 12.508s cpu time, 1.392s GC time Loading theory "Regular-Sets.Regular_Exp" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking" via "Regular-Sets.NDerivative") consts vars_mset :: "('s, 'v) tm \ 'v multiset" consts subst :: "('v \ ('s, 'v) tm) \ ('s, 'v) tm \ ('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 \ enat" and arity_var :: "'v \ enat" consts arity_hd :: "('s, 'v) hd \ 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 \ 's \ bool" (infix \>\<^sub>s\ 50) and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" and ground_heads_var :: "'v \ 's set" assumes "ground_heads (>\<^sub>s) arity_sym arity_var ground_heads_var" consts ground_heads :: "('s, 'v) hd \ 's set" ### theory "Lambda_Free_RPOs.Lambda_Free_Term" ### 4.321s elapsed time, 14.492s cpu time, 1.392s GC time Loading theory "Lambda_Free_RPOs.Lambda_Encoding" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Encoding_KBO") locale lambda_encoding fixes lam :: "'s" and db :: "nat \ 's" Found termination order: "(\p. size (snd (snd p))) <*mlex*> {}" ### theory "Lambda_Free_RPOs.Lambda_Encoding" ### 0.330s elapsed time, 1.344s cpu time, 0.000s GC time *** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"): *** goal (1 subgoal): *** 1. \Q x z. *** \x \ Q; *** \y. *** (y, f z) \ r \ y \ range f\ *** \ \z\Q. *** \y. *** (f y, f z) \ r \ *** y \ Q *** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy") consts lang :: "'a rexp \ 'a list set" consts nullable :: "'a rexp \ bool" consts rexp_empty :: "'a rexp \ bool" instantiation rexp :: (order) order less_eq_rexp == less_eq :: 'a rexp \ 'a rexp \ bool less_rexp == less :: 'a rexp \ 'a rexp \ bool Found termination order: "(\p. size (snd p)) <*mlex*> {}" instantiation rexp :: (linorder) linorder ### theory "Regular-Sets.Regular_Exp" ### 4.308s elapsed time, 16.220s cpu time, 0.940s GC time Loading theory "Regular-Sets.NDerivative" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking") Loading theory "Regular-Sets.Relation_Interpretation" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method") consts rel :: "('a \ ('b \ 'b) set) \ 'a rexp \ ('b \ 'b) set" consts word_rel :: "('a \ ('b \ 'b) set) \ 'a list \ ('b \ 'b) set" ### theory "Regular-Sets.Relation_Interpretation" ### 0.113s elapsed time, 0.452s cpu time, 0.000s GC time Found termination order: "(\p. size (fst p)) <*mlex*> (\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size (fst p)) <*mlex*> {}" ### Rule already declared as elimination (elim) ### \?w \ ?A @@ ?B; ### \u v. ### \u \ ?A; v \ ?B; ?w = u @ v\ ### \ ?thesis\ ### \ ?thesis consts norm :: "'a rexp \ 'a rexp" consts nderiv :: "'a \ 'a rexp \ 'a rexp" ### theory "Regular-Sets.NDerivative" ### 4.372s elapsed time, 16.164s cpu time, 0.580s GC time Loading theory "Regular-Sets.Equivalence_Checking" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method") Proofs for coinductive predicate(s) "bisimilar" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the coinduction rule ... Proving the simplification rules ... consts add_atoms :: "'a rexp \ 'a list \ 'a list" ### theory "Regular-Sets.Equivalence_Checking" ### 0.418s elapsed time, 1.684s cpu time, 0.000s GC time Loading theory "Regular-Sets.Regexp_Method" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders" via "Abstract-Rewriting.Abstract_Rewriting") consts rel_of_regexp :: "('a \ 'a) set list \ nat rexp \ ('a \ 'a) set" consts rel_eq :: "nat rexp \ nat rexp \ ('a \ 'a) set list \ bool" val regexp_conv = fn: Proof.context -> conv ### theory "Regular-Sets.Regexp_Method" ### 1.042s elapsed time, 4.008s cpu time, 0.136s GC time Loading theory "Abstract-Rewriting.Abstract_Rewriting" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials" via "Abstract-Rewriting.SN_Orders") Found termination order: "{}" Proofs for inductive predicate(s) "SN_partp" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory "Abstract-Rewriting.Abstract_Rewriting" ### 2.377s elapsed time, 9.188s cpu time, 0.292s GC time Loading theory "Abstract-Rewriting.SN_Orders" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util" via "Polynomials.Polynomials") class non_strict_order = ord + assumes "ge_refl": "\x. x \ x" and "ge_trans": "\y x z. \y \ x; z \ y\ \ z \ x" and "max_comm": "\x y. max x y = max y x" and "max_ge_x": "\x y. x \ max x y" and "max_id": "\y x. y \ x \ max x y = x" and "max_mono": "\y x z. y \ x \ max z y \ max z x" class ordered_ab_semigroup = ab_semigroup_add + monoid_add + non_strict_order + assumes "plus_left_mono": "\y x z. y \ x \ y + z \ x + z" class SN_Orders.ordered_semiring_0 = semiring_0 + ordered_ab_semigroup + assumes "times_left_mono": "\z y x. $0::'a) \ z; y \ x\ \ y * z \ x * z" and "times_right_mono": "\x z y. \(0::'a) \ x; z \ y\ \ x * z \ x * y" and "times_left_anti_mono": "\y x z. \y \ x; z \ (0::'a)\ \ x * z \ y * z" class ordered_semiring_1 = semiring_1 + SN_Orders.ordered_semiring_0 + assumes "one_ge_zero": "(0::'a) \ (1::'a)" locale order_pair fixes gt :: "'a \ 'a \ bool" (infix \\\ 50) and default :: "'a" assumes "order_pair ($ default" locale one_mono_ordered_semiring_1 fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) assumes "one_mono_ordered_semiring_1 default (\)" locale SN_one_mono_ordered_semiring_1 fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) assumes "SN_one_mono_ordered_semiring_1 default (\)" locale SN_strict_mono_ordered_semiring_1 fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and mono :: "'a \ bool" assumes "SN_strict_mono_ordered_semiring_1 default (\) mono" locale both_mono_ordered_semiring_1 fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and arc_pos :: "'a \ bool" assumes "both_mono_ordered_semiring_1 default (\) arc_pos" locale SN_both_mono_ordered_semiring_1 fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and arc_pos :: "'a \ bool" assumes "SN_both_mono_ordered_semiring_1 default (\) arc_pos" locale weak_SN_strict_mono_ordered_semiring_1 fixes weak_gt :: "'a \ 'a \ bool" and default :: "'a" and mono :: "'a \ bool" assumes "weak_SN_strict_mono_ordered_semiring_1 weak_gt default mono" locale weak_SN_both_mono_ordered_semiring_1 fixes weak_gt :: "'a \ 'a \ bool" and default :: "'a" and arc_pos :: "'a \ bool" assumes "weak_SN_both_mono_ordered_semiring_1 weak_gt default arc_pos" locale poly_order_carrier fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and power_mono :: "bool" and discrete :: "bool" assumes "poly_order_carrier default (\) power_mono discrete" class large_ordered_semiring_1 = poly_carrier + assumes "ex_large_of_nat": "\y. \x. y \ of_nat x" class ordered_semiring_1 = semiring_1 + SN_Orders.ordered_semiring_0 + assumes "one_ge_zero": "(0::'a) \ (1::'a)" ### theory "Abstract-Rewriting.SN_Orders" ### 2.038s elapsed time, 8.044s cpu time, 0.312s GC time Loading theory "Polynomials.Polynomials" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App" via "Lambda_Free_KBOs.Lambda_Free_KBO_Util") consts eval_tpoly :: "('v \ 'a) \ ('v, 'a) tpoly \ 'a" class linorder = order + assumes "linear": "\x y. x \ y \ y \ x" Found termination order: "(\p. size_list (\p. size (snd p)) (snd p)) <*mlex*> {}" Found termination order: "(\p. size_list (\p. size (snd p)) (snd p)) <*mlex*> (\p. size_list (\p. size (snd p)) (fst p)) <*mlex*> {}" instantiation monom :: (linorder) comm_monoid_mult one_monom == one_class.one :: 'a monom times_monom == times :: 'a monom \ 'a monom \ 'a monom instantiation monom :: ({equal,linorder}) equal equal_monom == equal_class.equal :: 'a monom \ 'a monom \ bool consts eval_poly :: "('v \ 'a) \ ('v monom \ 'a) list \ 'a" Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" Found termination order: "size <*mlex*> {}" Found termination order: "(\p. size (snd p)) <*mlex*> {}" Found termination order: "(\p. size_list (\p. size (snd p)) (snd p)) <*mlex*> {}" Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" locale poly_order_carrier fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and power_mono :: "bool" and discrete :: "bool" assumes "poly_order_carrier default (\) power_mono discrete" locale poly_order_carrier fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and power_mono :: "bool" and discrete :: "bool" assumes "poly_order_carrier default (\) power_mono discrete" Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" Found termination order: "(\p. size_list size (fst p)) <*mlex*> {}" locale poly_order_carrier fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and power_mono :: "bool" and discrete :: "bool" assumes "poly_order_carrier default (\) power_mono discrete" Found termination order: "{}" locale poly_order_carrier fixes default :: "'a" and gt :: "'a \ 'a \ bool" (infix \\\ 50) and power_mono :: "bool" and discrete :: "bool" assumes "poly_order_carrier default (\) power_mono discrete" ### theory "Polynomials.Polynomials" ### 6.999s elapsed time, 25.024s cpu time, 0.976s GC time Loading theory "Lambda_Free_KBOs.Lambda_Free_KBO_Util" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_App") locale kbo_basic_basis fixes gt_sym :: "'s \ 's \ bool" (infix \>\<^sub>s\ 50) and wt_sym :: "'s \ nat" and \ :: "nat" and ground_heads_var :: "'v \ 's set" and extf :: "'s \ (('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" assumes "kbo_basic_basis (>\<^sub>s) wt_sym \ ground_heads_var extf" locale kbo_std_basis fixes ground_heads_var :: "'v \ 's set" and gt_sym :: "'s \ 's \ bool" (infix \>\<^sub>s\ 50) and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" and wt_sym :: "'s \ 'n" and \ :: "nat" and \ :: "nat" and extf :: "'s \ (('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" assumes "kbo_std_basis ground_heads_var (>\<^sub>s) arity_sym arity_var wt_sym \ \ extf" ### theory "Lambda_Free_KBOs.Lambda_Free_KBO_Util" ### 1.024s elapsed time, 2.052s cpu time, 0.000s GC time Loading theory "Lambda_Free_KBOs.Lambda_Free_KBO_App" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs") locale kbo_app fixes gt_sym :: "'s \ 's \ bool" (infix \>\<^sub>s\ 50) and wt_sym :: "'s \ nat" and \ :: "nat" and ext :: "(('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" assumes "kbo_app (>\<^sub>s) wt_sym \ ext" Found termination order: "size <*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_KBOs.Lambda_Free_KBO_App" ### 0.444s elapsed time, 1.044s cpu time, 0.328s GC time Loading theory "Lambda_Free_KBOs.Lambda_Free_KBO_Std" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_Basic") locale kbo_std fixes ground_heads_var :: "'v \ 's set" and gt_sym :: "'s \ 's \ bool" (infix \>\<^sub>s\ 50) and \ :: "nat" and \ :: "nat" and extf :: "'s \ (('s, 'v) tm \ ('s, 'v) tm \ bool) \ ('s, 'v) tm list \ ('s, 'v) tm list \ bool" and arity_sym :: "'s \ enat" and arity_var :: "'v \ enat" and wt_sym :: "'s \ nat" assumes "kbo_std ground_heads_var (>\<^sub>s) \ \ extf arity_sym arity_var wt_sym" consts wt :: "('s, 'v) tm \ nat" 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_wt" 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_unary" 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_KBOs.Lambda_Free_KBO_Std" ### 0.846s elapsed time, 1.704s cpu time, 0.000s GC time Loading theory "Lambda_Free_KBOs.Lambda_Free_KBO_Basic" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs") locale kbo_basic fixes gt_sym :: "'s \ 's \ bool" (infix \