Loading theory "Deriving.Comparator" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator" via "Deriving.Comparator_Generator")
Loading theory "First_Order_Terms.Fun_More" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Subsumption")
Loading theory "Deriving.Generator_Aux" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator" via "Deriving.Comparator_Generator")
Loading theory "Deriving.Derive_Manager" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator" via "Deriving.Comparator_Generator")
signature BNF_ACCESS =
  sig
    val bnf_types: Proof.context -> string list -> typ list
    val case_consts: Proof.context -> string list -> term list
    val case_simps: Proof.context -> string list -> thm list list
    val case_thms: Proof.context -> string list -> thm list
    val constr_argument_types:
       Proof.context -> string list -> typ list list list
    val constr_terms: Proof.context -> string -> term list
    val distinct_thms: Proof.context -> string list -> thm list list
    val induct_thms: Proof.context -> string list -> thm list
    val inject_thms: Proof.context -> string list -> thm list list
    val map_comps: Proof.context -> string list -> thm list
    val map_simps: Proof.context -> string list -> thm list list
    val map_terms: Proof.context -> string list -> term list
    val set_simps: Proof.context -> string list -> thm list list
    val set_terms: Proof.context -> string list -> term list list
  end
structure Bnf_Access: BNF_ACCESS
signature DERIVE_MANAGER =
  sig
    val derive: string -> string -> string -> theory -> theory
    val derive_cmd: string -> string -> string -> theory -> theory
    val print_info: theory -> unit
    val register_derive:
       string ->
         string ->
           (string -> string -> theory -> theory) -> theory -> theory
  end
structure Derive_Manager: DERIVE_MANAGER
### theory "Deriving.Derive_Manager"
### 0.146s elapsed time, 0.592s cpu time, 0.000s GC time
Loading theory "First_Order_Terms.Term" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" via "First_Order_Terms.Unifiers")
### theory "First_Order_Terms.Fun_More"
### 0.172s elapsed time, 0.716s cpu time, 0.000s GC time
Loading theory "First_Order_Terms.Transitive_Closure_More" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Subsumption" via "First_Order_Terms.Seq_More")
### theory "First_Order_Terms.Transitive_Closure_More"
### 0.201s elapsed time, 0.796s cpu time, 0.000s GC time
Loading theory "HOL-Cardinals.Order_Union" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "HOL-Cardinals.Wellorder_Extension")
signature GENERATOR_AUX =
  sig
    val OF_option: thm -> thm option list -> thm
    val add_used_tycos:
       Proof.context -> string -> string list -> string list
    val alist_to_string: (string * 'a) list -> string
    val conjI_tac:
       thm list ->
         Proof.context ->
           'a list -> (Proof.context -> int -> tactic) -> tactic
    val create_map:
       (typ -> term) ->
         (string * typ -> 'a -> term) ->
           'a ->
             (typ -> bool) ->
               (local_theory -> string -> bool list) ->
                 (local_theory -> string -> term) ->
                   (local_theory -> string -> 'a -> term) ->
                     string list ->
                       (local_theory -> string -> 'a) ->
                         typ -> local_theory -> term
    val create_partial:
       'a ->
         (typ -> bool) ->
           (local_theory -> string -> bool list) ->
             (local_theory -> string -> term) ->
               (local_theory -> string -> 'a -> term) ->
                 string list ->
                   (local_theory -> string -> 'a) ->
                     typ -> local_theory -> term
    val define_overloaded:
       string * term -> local_theory -> thm * local_theory
    val define_overloaded_generic:
       Attrib.binding * term -> local_theory -> thm * local_theory
    val drop_last: 'a list -> 'a list
    val freeify_tvars: typ -> typ
    val ind_case_to_idxs: 'a list list -> int -> int * int
    val infer_type: Proof.context -> term -> term
    val ints_to_subscript: int list -> string
    val is_class_instance: theory -> string -> sort -> bool
    val lambdas: term list -> term -> term
    val mk_case_tac:
       Proof.context ->
         term option list list ->
           thm ->
             (int ->
                Proof.context * thm list * (string * cterm) list -> tactic)
               -> tactic
    val mk_def: typ -> string -> term -> term
    val mk_id: typ -> term
    val mk_infer_const: string -> Proof.context -> term -> term
    val mutual_recursive_types:
       string -> Proof.context -> string list * typ list
    val prove_multi_future:
       Proof.context ->
         string list ->
           term list ->
             term list ->
               ({context: Proof.context, prems: thm list} -> tactic) ->
                 thm list
    val recursor:
       (string -> 'a) * ('a -> bool list) * string list ->
         bool ->
           (typ -> 'b) ->
             (typ -> 'b) ->
               (typ -> 'b) ->
                 ((typ * 'b option) list * 'a -> 'b) -> typ -> 'b
    val rename_types: (typ * typ) list -> term -> term
    val split_IHs:
       (string -> 'a) * ('a -> bool list) * string list ->
         typ list -> thm list -> thm list list
    val std_recursor_tac:
       (string -> 'a) * ('a -> bool list) * string list ->
         typ list ->
           ('a -> thm) ->
             thm list -> typ -> thm list -> Proof.context -> tactic
    val sub: string -> string
    val subT: string -> typ -> string
    val typ_and_vs_of_typname:
       theory -> string -> sort -> typ * (string * sort) list
    val typ_and_vs_of_used_typname:
       string ->
         bool list -> string list -> typ * (string * string list) list
    val type_parameters:
       typ -> Proof.context -> (string * sort) list * typ list
  end
structure Generator_Aux: GENERATOR_AUX
### theory "Deriving.Generator_Aux"
### 0.469s elapsed time, 1.888s cpu time, 0.000s GC time
Loading theory "Deriving.Equality_Generator" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Equality_Instances")
### theory "HOL-Cardinals.Order_Union"
### 0.264s elapsed time, 1.048s cpu time, 0.000s GC time
Loading theory "HOL-Cardinals.Wellorder_Extension" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term")
### theory "HOL-Cardinals.Wellorder_Extension"
### 0.186s elapsed time, 0.736s cpu time, 0.000s GC time
Loading theory "First_Order_Terms.Option_Monad" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification")
Found termination order: "{}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale comparator
  fixes comp :: "'a \<Rightarrow> 'a \<Rightarrow> order"
  assumes "comparator comp"
signature EQUALITY_GENERATOR =
  sig
    val ensure_info: equality_type -> string -> local_theory -> local_theory
    datatype equality_type = BNF | EQ
    val generate_equality:
       equality_type -> string -> local_theory -> local_theory
    val generate_equalitys_from_bnf_fp:
       string ->
         local_theory ->
           ((term * thm list) list * (term * thm) list) * local_theory
    val get_info: Proof.context -> string -> info option
    type info =
       {equality: term,
        equality_def: thm option,
        equality_thm: thm,
        map: term,
        map_comp: thm option,
        partial_equality_thm: thm,
        pequality: term, used_positions: bool list}
    val register_equality_of: string -> local_theory -> local_theory
    val register_foreign_equality:
       typ -> term -> thm -> local_theory -> local_theory
    val register_foreign_partial_and_full_equality:
       string ->
         term ->
           term ->
             term ->
               thm option ->
                 thm option ->
                   thm -> thm -> bool list -> local_theory -> local_theory
  end
structure Equality_Generator: EQUALITY_GENERATOR
### theory "Deriving.Equality_Generator"
### 0.951s elapsed time, 3.680s cpu time, 0.436s GC time
Loading theory "Deriving.Equality_Instances" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive")
generating equality for type "Sum_Type.sum"
generating equality for type "List.list"
generating equality for type "Product_Type.prod"
generating equality for type "Option.option"
### theory "Deriving.Equality_Instances"
### 0.136s elapsed time, 0.544s cpu time, 0.000s GC time
Loading theory "Nested_Multisets_Ordinals.Multiset_More" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Abstract_Substitution" via "Ordered_Resolution_Prover.Clausal_Logic")
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "First_Order_Terms.Option_Monad"
### 0.795s elapsed time, 3.068s cpu time, 0.436s GC time
Loading theory "Abstract-Rewriting.Seq" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" via "Abstract-Rewriting.Abstract_Rewriting")
### theory "Deriving.Comparator"
### 1.689s elapsed time, 6.640s cpu time, 0.436s GC time
Loading theory "Deriving.Compare" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator")
class compare = type +
  fixes compare :: "'a \<Rightarrow> 'a \<Rightarrow> order"
  assumes "comparator_compare": "comparator compare"
locale infinitely_many
  fixes p :: "nat \<Rightarrow> bool"
  assumes "infinitely_many p"
Found termination order: "{}"
class compare_order = compare + ord +
  assumes
    "ord_defs": "le_of_comp compare = (\<le>)" "lt_of_comp compare = (<)"
Found termination order: "size <*mlex*> {}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
### Partially applied constant "Term.term.Var" on left hand side of equation, in theorem:
### monoid_mult.prod_list Var (\<circ>\<^sub>s) ?xs \<equiv>
### foldr (\<circ>\<^sub>s) ?xs Var
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
class compare_order = compare + linorder +
  assumes
    "ord_defs": "le_of_comp compare = (\<le>)" "lt_of_comp compare = (<)"
### theory "Abstract-Rewriting.Seq"
### 0.656s elapsed time, 2.624s cpu time, 0.000s GC time
Loading theory "Deriving.Comparator_Generator" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Compare_Instances" via "Deriving.Compare_Generator")
Found termination order: "{}"
signature COMPARE_CODE =
  sig
    val change_compare_code:
       term -> string list -> local_theory -> local_theory
  end
structure Compare_Code: COMPARE_CODE
### theory "Deriving.Compare"
### 0.688s elapsed time, 2.752s cpu time, 0.000s GC time
Loading theory "First_Order_Terms.Seq_More" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Subsumption")
Found termination order: "size <*mlex*> {}"
### theory "Nested_Multisets_Ordinals.Multiset_More"
### 1.006s elapsed time, 4.024s cpu time, 0.000s GC time
Loading theory "Ordered_Resolution_Prover.Clausal_Logic" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Abstract_Substitution")
### theory "First_Order_Terms.Seq_More"
### 0.217s elapsed time, 0.868s cpu time, 0.000s GC time
Loading theory "HOL-Word.Bits" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word" via "HOL-Word.Bits_Bit")
### theory "First_Order_Terms.Term"
### 2.451s elapsed time, 9.664s cpu time, 0.436s GC time
Loading theory "First_Order_Terms.Unifiers" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification")
class bit = type +
  fixes bitNOT :: "'a \<Rightarrow> 'a"
    and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
class bits = bit +
  fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"
    and lsb :: "'a \<Rightarrow> bool"
    and
    set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
    and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"
    and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
    and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
class bitss = bits +
  fixes msb :: "'a \<Rightarrow> bool"
### theory "HOL-Word.Bits"
### 0.153s elapsed time, 0.612s cpu time, 0.000s GC time
Loading theory "First_Order_Terms.Term_Pair_Multiset" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification")
Found termination order: "size_list size <*mlex*> {}"
### theory "First_Order_Terms.Unifiers"
### 0.274s elapsed time, 1.100s cpu time, 0.000s GC time
Loading theory "First_Order_Terms.Subsumption" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term")
### theory "First_Order_Terms.Term_Pair_Multiset"
### 0.823s elapsed time, 3.224s cpu time, 0.824s GC time
Loading theory "HOL-Word.Bits_Bit" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word")
signature COMPARATOR_GENERATOR =
  sig
    datatype comparator_type = BNF | Linorder
    val ensure_info:
       comparator_type -> string -> local_theory -> local_theory
    val generate_comparator:
       comparator_type -> string -> local_theory -> local_theory
    val generate_comparators_from_bnf_fp:
       string ->
         local_theory ->
           ((term * thm list) list * (term * thm) list) * local_theory
    val get_info: Proof.context -> string -> info option
    type info =
       {comp: term,
        comp_def: thm option,
        comp_thm: thm,
        map: term,
        map_comp: thm option,
        partial_comp_thms: thm list, pcomp: term, used_positions: bool list}
    val register_comparator_of: string -> local_theory -> local_theory
    val register_foreign_comparator:
       typ -> term -> thm -> local_theory -> local_theory
    val register_foreign_partial_and_full_comparator:
       string ->
         term ->
           term ->
             term ->
               thm option ->
                 thm option ->
                   thm ->
                     thm ->
                       thm ->
                         thm -> bool list -> local_theory -> local_theory
  end
structure Comparator_Generator: COMPARATOR_GENERATOR
### theory "Deriving.Comparator_Generator"
### 1.340s elapsed time, 5.292s cpu time, 0.824s GC time
Loading theory "Deriving.Compare_Generator" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Compare_Instances")
instantiation
  literal :: (type) uminus
  uminus_literal == uminus :: 'a literal \<Rightarrow> 'a literal
locale subsumable
  fixes subsumeseq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "subsumable subsumeseq"
instantiation
  literal :: (preorder) preorder
  less_eq_literal == less_eq ::
    'a literal \<Rightarrow> 'a literal \<Rightarrow> bool
  less_literal == less ::
    'a literal \<Rightarrow> 'a literal \<Rightarrow> bool
instantiation
  bit :: bit
  bitNOT_bit == bitNOT :: bit \<Rightarrow> bit
  bitAND_bit == bitAND :: bit \<Rightarrow> bit \<Rightarrow> bit
  bitOR_bit == bitOR :: bit \<Rightarrow> bit \<Rightarrow> bit
  bitXOR_bit == bitXOR :: bit \<Rightarrow> bit \<Rightarrow> bit
instantiation
  literal :: (order) order
Proofs for inductive predicate(s) "subsumeseq_term"
consts
  bitNOT_bit :: "bit \<Rightarrow> bit"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
instantiation
  literal :: (linorder) linorder
instantiation
  literal :: (wellorder) wellorder
consts
  bitAND_bit :: "bit \<Rightarrow> bit \<Rightarrow> bit"
consts
  bitOR_bit :: "bit \<Rightarrow> bit \<Rightarrow> bit"
consts
  bitXOR_bit :: "bit \<Rightarrow> bit \<Rightarrow> bit"
### theory "HOL-Word.Bits_Bit"
### 0.342s elapsed time, 1.372s cpu time, 0.000s GC time
Loading theory "HOL-Word.Misc_Numeric" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word" via "HOL-Word.Bool_List_Representation" via "HOL-Word.Bits_Int" via "HOL-Word.Bit_Representation")
### theory "HOL-Word.Misc_Numeric"
### 0.056s elapsed time, 0.224s cpu time, 0.000s GC time
Loading theory "HOL-Word.Bit_Representation" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word" via "HOL-Word.Bool_List_Representation" via "HOL-Word.Bits_Int")
### theory "Ordered_Resolution_Prover.Clausal_Logic"
### 1.395s elapsed time, 5.512s cpu time, 0.824s GC time
Loading theory "Ordered_Resolution_Prover.Herbrand_Interpretation" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Ordered_Ground_Resolution" via "Ordered_Resolution_Prover.Inference_System")
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
consts
  bin_nth :: "int \<Rightarrow> nat \<Rightarrow> bool"
### theory "Ordered_Resolution_Prover.Herbrand_Interpretation"
### 0.217s elapsed time, 0.868s cpu time, 0.000s GC time
Loading theory "Ordered_Resolution_Prover.Ground_Resolution_Model" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Ordered_Ground_Resolution")
Proofs for inductive predicate(s) "emv"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
signature COMPARE_GENERATOR =
  sig
    val compare_instance:
       Comparator_Generator.comparator_type -> string -> theory -> theory
    val compare_order_instance_via_comparator_of: string -> theory -> theory
    val compare_order_instance_via_compare: string -> theory -> theory
  end
structure Compare_Generator: COMPARE_GENERATOR
### theory "Deriving.Compare_Generator"
### 0.559s elapsed time, 2.240s cpu time, 0.000s GC time
Loading theory "Ordered_Resolution_Prover.Inference_System" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Ordered_Ground_Resolution")
locale selection
  fixes S :: "'a literal multiset \<Rightarrow> 'a literal multiset"
  assumes "selection S"
consts
  bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
locale ground_resolution_with_selection
  fixes S :: "'a literal multiset \<Rightarrow> 'a literal multiset"
  assumes "ground_resolution_with_selection S"
consts
  sbintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
### theory "First_Order_Terms.Subsumption"
### 1.440s elapsed time, 5.696s cpu time, 0.824s GC time
Loading theory "Deriving.Compare_Instances" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive")
deriving "compare_order" instance for type "Int.int"
deriving "compare" instance for type "Int.int"
deriving "compare_order" instance for type "Code_Numeral.integer"
deriving "compare" instance for type "Code_Numeral.integer"
consts
  bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int"
deriving "compare_order" instance for type "Nat.nat"
deriving "compare" instance for type "Nat.nat"
consts
  bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int"
### theory "HOL-Word.Bit_Representation"
### 0.672s elapsed time, 2.692s cpu time, 0.000s GC time
Loading theory "HOL-Word.Bits_Int" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word" via "HOL-Word.Bool_List_Representation")
deriving "compare_order" instance for type "String.char"
deriving "compare" instance for type "String.char"
deriving "compare" instance for type "Sum_Type.sum"
generating comparator for type "Sum_Type.sum"
deriving "compare" instance for type "List.list"
generating comparator for type "List.list"
deriving "compare" instance for type "Product_Type.prod"
generating comparator for type "Product_Type.prod"
deriving "compare" instance for type "Option.option"
generating comparator for type "Option.option"
### theory "Ordered_Resolution_Prover.Ground_Resolution_Model"
### 0.634s elapsed time, 2.544s cpu time, 0.000s GC time
Loading theory "HOL-Word.Word_Miscellaneous" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word")
Found termination order: "{}"
instantiation
  int :: bit
  bitNOT_int == bitNOT :: int \<Rightarrow> int
  bitAND_int == bitAND :: int \<Rightarrow> int \<Rightarrow> int
  bitOR_int == bitOR :: int \<Rightarrow> int \<Rightarrow> int
  bitXOR_int == bitXOR :: int \<Rightarrow> int \<Rightarrow> int
Found termination order: "{}"
deriving "compare" instance for type "HOL.bool"
deriving "compare" instance for type "Product_Type.unit"
deriving "compare_order" instance for type "HOL.bool"
deriving "compare_order" instance for type "Product_Type.unit"
### theory "Deriving.Compare_Instances"
### 0.761s elapsed time, 3.052s cpu time, 0.000s GC time
Loading theory "HOL-Word.Misc_Typedef" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word")
locale type_definition
  fixes Rep :: "'b \<Rightarrow> 'a"
    and Abs :: "'a \<Rightarrow> 'b"
    and A :: "'a set"
  assumes "type_definition Rep Abs A"
locale td_ext
  fixes Rep :: "'a \<Rightarrow> 'b"
    and Abs :: "'b \<Rightarrow> 'a"
    and A :: "'b set"
    and norm :: "'b \<Rightarrow> 'b"
  assumes "td_ext Rep Abs A norm"
### theory "HOL-Word.Misc_Typedef"
### 0.432s elapsed time, 1.656s cpu time, 0.984s GC time
Loading theory "Deriving.Countable_Generator" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive")
### theory "HOL-Word.Word_Miscellaneous"
### 0.883s elapsed time, 3.448s cpu time, 0.984s GC time
Loading theory "Coinductive.Coinductive_Nat" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Standard_Redundancy" via "Ordered_Resolution_Prover.Proving_Process" via "Ordered_Resolution_Prover.Lazy_List_Chain" via "Ordered_Resolution_Prover.Lazy_List_Liminf" via "Coinductive.Coinductive_List")
locale inference_system
  fixes \<Gamma> :: "'a inference set"
### theory "Deriving.Countable_Generator"
### 0.344s elapsed time, 1.348s cpu time, 0.000s GC time
Loading theory "Matrix.Utility" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Polynomial_Factorization.Missing_List")
locale sat_preserving_inference_system
  fixes \<Gamma> :: "'a inference set"
  assumes "sat_preserving_inference_system \<Gamma>"
consts
  bin_sc :: "nat \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> int"
locale sound_inference_system
  fixes \<Gamma> :: "'a inference set"
  assumes "sound_inference_system \<Gamma>"
locale reductive_inference_system
  fixes \<Gamma> :: "'a inference set"
  assumes "reductive_inference_system \<Gamma>"
locale counterex_reducing_inference_system
  fixes \<Gamma> :: "'a inference set"
    and I_of :: "'a literal multiset set \<Rightarrow> 'a set"
  assumes "counterex_reducing_inference_system \<Gamma> I_of"
locale inference_system
  fixes \<Gamma> :: "'a inference set"
Proofs for inductive predicate(s) "saturatep"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale sound_inference_system
  fixes \<Gamma> :: "'a inference set"
  assumes "sound_inference_system \<Gamma>"
Found termination order:
  "(\<lambda>p. length (snd p)) <*mlex*>
   (\<lambda>p. length (fst p)) <*mlex*> {}"
locale sat_preserving_inference_system
  fixes \<Gamma> :: "'a inference set"
  assumes "sat_preserving_inference_system \<Gamma>"
locale sound_counterex_reducing_inference_system
  fixes \<Gamma> :: "'a inference set"
    and I_of :: "'a literal multiset set \<Rightarrow> 'a set"
  assumes "sound_counterex_reducing_inference_system \<Gamma> I_of"
### theory "Ordered_Resolution_Prover.Inference_System"
### 2.021s elapsed time, 7.984s cpu time, 0.984s GC time
Loading theory "Ordered_Resolution_Prover.Ordered_Ground_Resolution" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution")
Found termination order: "(\<lambda>p. size (fst (snd p))) <*mlex*> {}"
Proofs for coinductive predicate(s) "enat_setp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
Found termination order: "size_list size <*mlex*> {}"
### theory "Matrix.Utility"
### 0.541s elapsed time, 2.148s cpu time, 0.000s GC time
Loading theory "Ordered_Resolution_Prover.Unordered_Ground_Resolution" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Standard_Redundancy" via "Ordered_Resolution_Prover.Proving_Process")
locale co
locale ground_resolution_with_selection
  fixes S :: "'a literal multiset \<Rightarrow> 'a literal multiset"
  assumes "ground_resolution_with_selection S"
Proofs for inductive predicate(s) "eligible"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "ord_resolve"
locale ground_resolution_without_selection
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "unord_resolve"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Ordered_Resolution_Prover.Unordered_Ground_Resolution"
### 0.352s elapsed time, 1.392s cpu time, 0.000s GC time
Loading theory "Polynomial_Factorization.Missing_List" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover")
Proofs for coinductive predicate(s) "Le_enatp"
Found termination order: "(\<lambda>p. size (fst (snd p))) <*mlex*> {}"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
### theory "Ordered_Resolution_Prover.Ordered_Ground_Resolution"
### 0.599s elapsed time, 2.384s cpu time, 0.000s GC time
Loading theory "Open_Induction.Restricted_Predicates" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term")
### theory "HOL-Word.Bits_Int"
### 2.272s elapsed time, 8.972s cpu time, 0.984s GC time
Loading theory "HOL-Word.Bool_List_Representation" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc" via "HOL-Word.Word")
consts
  bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
consts
  bin_to_bl_aux ::
    "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
consts
  bl_of_nth ::
    "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list"
consts
  takefill ::
    "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
consts
  rbl_succ :: "bool list \<Rightarrow> bool list"
consts
  rbl_pred :: "bool list \<Rightarrow> bool list"
Found termination order: "size_list length <*mlex*> {}"
consts
  rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
consts
  rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
### theory "Coinductive.Coinductive_Nat"
### 1.543s elapsed time, 6.136s cpu time, 0.000s GC time
Loading theory "Coinductive.Coinductive_List" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Standard_Redundancy" via "Ordered_Resolution_Prover.Proving_Process" via "Ordered_Resolution_Prover.Lazy_List_Chain" via "Ordered_Resolution_Prover.Lazy_List_Liminf")
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
Proofs for inductive predicate(s) "accessible_on"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Open_Induction.Restricted_Predicates"
### 0.938s elapsed time, 3.688s cpu time, 0.668s GC time
Loading theory "Ordered_Resolution_Prover.Map2" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Abstract_Substitution")
Found termination order: "length <*mlex*> {}"
### theory "Ordered_Resolution_Prover.Map2"
### 0.089s elapsed time, 0.356s cpu time, 0.000s GC time
Loading theory "Ordered_Resolution_Prover.Abstract_Substitution" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution")
instantiation
  int :: bitss
  msb_int == msb :: int \<Rightarrow> bool
  test_bit_int == test_bit :: int \<Rightarrow> nat \<Rightarrow> bool
  lsb_int == lsb :: int \<Rightarrow> bool
  set_bit_int == set_bit ::
    int \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> int
  set_bits_int == set_bits :: (nat \<Rightarrow> bool) \<Rightarrow> int
  shiftl_int == shiftl :: int \<Rightarrow> nat \<Rightarrow> int
  shiftr_int == shiftr :: int \<Rightarrow> nat \<Rightarrow> int
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
consts
  list_union :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
locale substitution_ops
  fixes subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
### theory "HOL-Word.Bool_List_Representation"
### 1.297s elapsed time, 5.124s cpu time, 0.668s GC time
Loading theory "Native_Word.More_Bits_Int" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc")
Found termination order: "(\<lambda>p. length (fst p)) <*mlex*> {}"
consts
  list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
### Ignoring duplicate rewrite rule:
### set ?xs1 \<subseteq> set ?ys1 \<equiv>
### list_all (\<lambda>x. x \<in> set ?ys1) ?xs1
consts
  bin_mask :: "nat \<Rightarrow> int"
Found termination order:
  "(\<lambda>p. length (snd p)) <*mlex*>
   (\<lambda>p. length (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. length (snd p)) <*mlex*>
   (\<lambda>p. length (fst p)) <*mlex*> {}"
### Missing patterns in function definition:
### min_list [] = undefined
Found termination order: "length <*mlex*> {}"
consts
  permut_aux ::
    "'a list
     \<Rightarrow> (nat \<Rightarrow> nat)
                   \<Rightarrow> 'a list \<Rightarrow> 'a list"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
consts
  unfold_llist ::
    "('a \<Rightarrow> bool)
     \<Rightarrow> ('a \<Rightarrow> 'b)
                   \<Rightarrow> ('a \<Rightarrow> 'a)
                                 \<Rightarrow> 'a \<Rightarrow> 'b llist"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Proofs for inductive predicate(s) "lsetp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "lfinite"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
### Ignoring duplicate rewrite rule:
### lnull (lappend ?xs1 ?ys1) \<equiv> lnull ?xs1 \<and> lnull ?ys1
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
Proofs for coinductive predicate(s) "lprefix"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
consts
  lSup :: "'a llist set \<Rightarrow> 'a llist"
Proofs for inductive predicate(s) "wf_set_bits_int"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Polynomial_Factorization.Missing_List"
### 3.950s elapsed time, 15.652s cpu time, 1.648s GC time
Loading theory "HOL-Word.Word" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32" via "Native_Word.Word_Misc")
locale substitution
  fixes subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"
    and atm_of_atms :: "'a list \<Rightarrow> 'a"
  assumes
    "substitution (\<cdot>a) id_subst (\<odot>) renamings_apart atm_of_atms"
### theory "Native_Word.More_Bits_Int"
### 4.019s elapsed time, 15.352s cpu time, 5.296s GC time
Loading theory "Native_Word.Bits_Integer" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32")
instantiation
  integer :: bitss
  msb_integer == msb :: integer \<Rightarrow> bool
  test_bit_integer == test_bit ::
    integer \<Rightarrow> nat \<Rightarrow> bool
  lsb_integer == lsb :: integer \<Rightarrow> bool
  set_bit_integer == set_bit ::
    integer \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> integer
  set_bits_integer == set_bits ::
    (nat \<Rightarrow> bool) \<Rightarrow> integer
  shiftl_integer == shiftl ::
    integer \<Rightarrow> nat \<Rightarrow> integer
  shiftr_integer == shiftr ::
    integer \<Rightarrow> nat \<Rightarrow> integer
  bitNOT_integer == bitNOT :: integer \<Rightarrow> integer
  bitAND_integer == bitAND ::
    integer \<Rightarrow> integer \<Rightarrow> integer
  bitOR_integer == bitOR ::
    integer \<Rightarrow> integer \<Rightarrow> integer
  bitXOR_integer == bitXOR ::
    integer \<Rightarrow> integer \<Rightarrow> integer
consts
  iterates ::
    "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
consts
  llist_of :: "'a list \<Rightarrow> 'a llist"
consts
  ltake :: "enat \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
### Ambiguous input (line 1019 of "$AFP/Coinductive/Coinductive_List.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" ldrop)
###       ("_cargs" ("_position" n) ("_position" xs)))
###     ("_case_syntax" ("_position" n)
###       ("_case2"
###         ("_case1" ("\<^const>Groups.zero_class.zero") ("_position" xs))
###         ("_case1" ("_applC" ("_position" eSuc) ("_position" n'))
###           ("_case_syntax" ("_position" xs)
###             ("_case2" ("_case1" ("_position" LNil) ("_position" LNil))
###               ("_case1"
###                 ("_applC" ("_position" LCons)
###                   ("_cargs" ("_position" x) ("_position" xs')))
###                 ("_applC" ("_position" ldrop)
###                   ("_cargs" ("_position" n') ("_position" xs')))))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" ldrop)
###       ("_cargs" ("_position" n) ("_position" xs)))
###     ("_case_syntax" ("_position" n)
###       ("_case2"
###         ("_case1" ("\<^const>Groups.zero_class.zero") ("_position" xs))
###         ("_case2"
###           ("_case1" ("_applC" ("_position" eSuc) ("_position" n'))
###             ("_case_syntax" ("_position" xs)
###               ("_case1" ("_position" LNil) ("_position" LNil))))
###           ("_case1"
###             ("_applC" ("_position" LCons)
###               ("_cargs" ("_position" x) ("_position" xs')))
###             ("_applC" ("_position" ldrop)
###               ("_cargs" ("_position" n') ("_position" xs')))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
consts
  ltakeWhile ::
    "('a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
consts
  lnth :: "'a llist \<Rightarrow> nat \<Rightarrow> 'a"
consts
  lzip ::
    "'a llist \<Rightarrow> 'b llist \<Rightarrow> ('a \<times> 'b) llist"
Proofs for coinductive predicate(s) "ldistinct"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
Proofs for coinductive predicate(s) "llexord"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
locale mgu
  fixes subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and atm_of_atms :: "'a list \<Rightarrow> 'a"
    and renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"
    and mgu :: "'a set set \<Rightarrow> 's option"
  assumes
    "mgu (\<cdot>a) id_subst (\<odot>) atm_of_atms renamings_apart mgu"
### theory "Ordered_Resolution_Prover.Abstract_Substitution"
### 5.602s elapsed time, 21.508s cpu time, 5.584s GC time
Loading theory "Regular-Sets.Regular_Set" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking" via "Regular-Sets.NDerivative" via "Regular-Sets.Regular_Exp")
### Ambiguous input (line 1508 of "$AFP/Coinductive/Coinductive_List.thy") produces 2 parse trees:
### ("\<^const>Pure.eq" ("_position" F)
###   ("_lambda"
###     ("_pttrns" ("_position" ltake)
###       ("_pttrns" ("_position" n) ("_position" xs)))
###     ("_case_syntax" ("_position" xs)
###       ("_case2" ("_case1" ("_position" LNil) ("_position" LNil))
###         ("_case2"
###           ("_case1"
###             ("_applC" ("_position" LCons)
###               ("_cargs" ("_position" x) ("_position" xs)))
###             ("_case_syntax" ("_position" n)
###               ("_case1" ("\<^const>Groups.zero_class.zero")
###                 ("_position" LNil))))
###           ("_case1" ("_applC" ("_position" eSuc) ("_position" n))
###             ("_applC" ("_position" LCons)
###               ("_cargs" ("_position" x)
###                 ("_applC" ("_position" ltake)
###                   ("_cargs" ("_position" n) ("_position" xs)))))))))))
### ("\<^const>Pure.eq" ("_position" F)
###   ("_lambda"
###     ("_pttrns" ("_position" ltake)
###       ("_pttrns" ("_position" n) ("_position" xs)))
###     ("_case_syntax" ("_position" xs)
###       ("_case2" ("_case1" ("_position" LNil) ("_position" LNil))
###         ("_case1"
###           ("_applC" ("_position" LCons)
###             ("_cargs" ("_position" x) ("_position" xs)))
###           ("_case_syntax" ("_position" n)
###             ("_case2"
###               ("_case1" ("\<^const>Groups.zero_class.zero")
###                 ("_position" LNil))
###               ("_case1" ("_applC" ("_position" eSuc) ("_position" n))
###                 ("_applC" ("_position" LCons)
###                   ("_cargs" ("_position" x)
###                     ("_applC" ("_position" ltake)
###                       ("_cargs" ("_position" n) ("_position" xs)))))))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
instantiation
  word :: (len0) size
  size_word == size :: 'a word \<Rightarrow> nat
instantiation
  word :: (len0) equal
  equal_word == equal_class.equal ::
    'a word \<Rightarrow> 'a word \<Rightarrow> bool
instantiation
  word :: ({len0,typerep}) random
  random_word == random_class.random ::
    natural
    \<Rightarrow> natural \<times> natural
                  \<Rightarrow> ('a word \<times>
                                 (unit \<Rightarrow> term)) \<times>
                                natural \<times> natural
### Ignoring duplicate rewrite rule:
### lnull (lzip ?xs1 ?ys1) \<equiv> lnull ?xs1 \<or> lnull ?ys1
### Ambiguous input (line 2485 of "$AFP/Coinductive/Coinductive_List.thy") produces 2 parse trees:
### ("\<^const>Pure.eq" ("_position" F)
###   ("_lambda"
###     ("_pttrns" ("_position" lzip)
###       ("_pattern" ("_position" xs) ("_position" ys)))
###     ("_case_syntax" ("_position" xs)
###       ("_case2" ("_case1" ("_position" LNil) ("_position" LNil))
###         ("_case2"
###           ("_case1"
###             ("_applC" ("_position" LCons)
###               ("_cargs" ("_position" x) ("_position" xs')))
###             ("_case_syntax" ("_position" ys)
###               ("_case1" ("_position" LNil) ("_position" LNil))))
###           ("_case1"
###             ("_applC" ("_position" LCons)
###               ("_cargs" ("_position" y) ("_position" ys')))
###             ("_applC" ("_position" LCons)
###               ("_cargs"
###                 ("_tuple" ("_position" x) ("_tuple_arg" ("_position" y)))
###                 ("_applC" ("_position" curry)
###                   ("_cargs" ("_position" lzip)
###                     ("_cargs" ("_position" xs') ("_position" ys'))))))))))))
### ("\<^const>Pure.eq" ("_position" F)
###   ("_lambda"
###     ("_pttrns" ("_position" lzip)
###       ("_pattern" ("_position" xs) ("_position" ys)))
###     ("_case_syntax" ("_position" xs)
###       ("_case2" ("_case1" ("_position" LNil) ("_position" LNil))
###         ("_case1"
###           ("_applC" ("_position" LCons)
###             ("_cargs" ("_position" x) ("_position" xs')))
###           ("_case_syntax" ("_position" ys)
###             ("_case2" ("_case1" ("_position" LNil) ("_position" LNil))
###               ("_case1"
###                 ("_applC" ("_position" LCons)
###                   ("_cargs" ("_position" y) ("_position" ys')))
###                 ("_applC" ("_position" LCons)
###                   ("_cargs"
###                     ("_tuple" ("_position" x)
###                       ("_tuple_arg" ("_position" y)))
###                     ("_applC" ("_position" curry)
###                       ("_cargs" ("_position" lzip)
###                         ("_cargs" ("_position" xs')
###                           ("_position" ys'))))))))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
instantiation
  word :: (len0) {comm_monoid_mult,neg_numeral,comm_ring,modulo}
  modulo_word == modulo ::
    'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
  divide_word == divide ::
    'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
  minus_word == minus :: 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
  uminus_word == uminus :: 'a word \<Rightarrow> 'a word
  zero_word == zero_class.zero :: 'a word
  plus_word == plus :: 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
  one_word == one_class.one :: 'a word
  times_word == times :: 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
instantiation
  word :: (len0) linorder
  less_eq_word == less_eq ::
    'a word \<Rightarrow> 'a word \<Rightarrow> bool
  less_word == less :: 'a word \<Rightarrow> 'a word \<Rightarrow> bool
instantiation
  word :: (len0) bits
  test_bit_word == test_bit :: 'a word \<Rightarrow> nat \<Rightarrow> bool
  lsb_word == lsb :: 'a word \<Rightarrow> bool
  set_bit_word == set_bit ::
    'a word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a word
  set_bits_word == set_bits ::
    (nat \<Rightarrow> bool) \<Rightarrow> 'a word
  shiftl_word == shiftl :: 'a word \<Rightarrow> nat \<Rightarrow> 'a word
  shiftr_word == shiftr :: 'a word \<Rightarrow> nat \<Rightarrow> 'a word
  bitNOT_word == bitNOT :: 'a word \<Rightarrow> 'a word
  bitAND_word == bitAND ::
    'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
  bitOR_word == bitOR :: 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
  bitXOR_word == bitXOR ::
    'a word \<Rightarrow> 'a word \<Rightarrow> 'a word
instantiation
  word :: (len) bitss
  msb_word == msb :: 'a word \<Rightarrow> bool
class ord = type +
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
Proofs for coinductive predicate(s) "lsorted"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
### Partially applied constant "Sublist.list_emb" on left hand side of equation, in theorem:
### subseq_order.lsorted LNil \<equiv> True
### Partially applied constant "Sublist.list_emb" on left hand side of equation, in theorem:
### subseq_order.lsorted (LCons ?x LNil) \<equiv> True
### Partially applied constant "Sublist.list_emb" on left hand side of equation, in theorem:
### subseq_order.lsorted (LCons ?x (LCons ?y ?xs)) \<equiv>
### subseq ?x ?y \<and> subseq_order.lsorted (LCons ?y ?xs)
### Partially applied constant "Sublist.sublist" on left hand side of equation, in theorem:
### sublist_order.lsorted LNil \<equiv> True
### Partially applied constant "Sublist.sublist" on left hand side of equation, in theorem:
### sublist_order.lsorted (LCons ?x LNil) \<equiv> True
### Partially applied constant "Sublist.sublist" on left hand side of equation, in theorem:
### sublist_order.lsorted (LCons ?x (LCons ?y ?xs)) \<equiv>
### sublist ?x ?y \<and> sublist_order.lsorted (LCons ?y ?xs)
### Partially applied constant "Sublist.suffix" on left hand side of equation, in theorem:
### suffix_order.lsorted LNil \<equiv> True
### Partially applied constant "Sublist.suffix" on left hand side of equation, in theorem:
### suffix_order.lsorted (LCons ?x LNil) \<equiv> True
### Partially applied constant "Sublist.suffix" on left hand side of equation, in theorem:
### suffix_order.lsorted (LCons ?x (LCons ?y ?xs)) \<equiv>
### suffix ?x ?y \<and> suffix_order.lsorted (LCons ?y ?xs)
### Partially applied constant "Sublist.prefix" on left hand side of equation, in theorem:
### prefix_order.lsorted LNil \<equiv> True
### Partially applied constant "Sublist.prefix" on left hand side of equation, in theorem:
### prefix_order.lsorted (LCons ?x LNil) \<equiv> True
### Partially applied constant "Sublist.prefix" on left hand side of equation, in theorem:
### prefix_order.lsorted (LCons ?x (LCons ?y ?xs)) \<equiv>
### prefix ?x ?y \<and> prefix_order.lsorted (LCons ?y ?xs)
class preorder = ord +
  assumes
    "less_le_not_le":
      "\<And>x y. (x < y) = (x \<le> y \<and> \<not> y \<le> x)"
    and "order_refl": "\<And>x. x \<le> x"
    and
    "order_trans":
      "\<And>x y z.
          \<lbrakk>x \<le> y; y \<le> z\<rbrakk>
          \<Longrightarrow> x \<le> z"
class linorder = order +
  assumes "linear": "\<And>x y. x \<le> y \<or> y \<le> x"
### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem:
### linorder.Min word_sle (set (?x # ?xs)) \<equiv> fold signed.min ?xs ?x
### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem:
### linorder.Max word_sle (set (?x # ?xs)) \<equiv> fold signed.max ?xs ?x
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 \<equiv> compow ::
    nat \<Rightarrow> 'a list set \<Rightarrow> 'a list set
consts
  lang_pow :: "nat \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem:
### signed.sorted [] \<equiv> True
### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem:
### signed.sorted [?x] \<equiv> True
### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem:
### signed.sorted (?x # ?y # ?zs) \<equiv>
### ?x <=s ?y \<and> signed.sorted (?y # ?zs)
### Partially applied constant "Word.word_sle" on left hand side of equation, in theorem:
### signed.sorted_list_of_set (set ?xs) \<equiv> signed.sort (remdups ?xs)
datatype 'a ref = ref of 'a
structure Bits_Integer:
  sig
    val set_bit: int -> int -> bool -> int
    val shiftl: int -> int -> int
    val shiftr: int -> int -> int
    val test_bit: int -> int -> bool
  end
ROOT.ML:38: warning: Pattern 3 is redundant.
Found near
  fun
     equal_boola p true = p |
        equal_boola p ... = not p |
        equal_boola ... = p |
        equal_boola ... = ...
ROOT.ML:39: warning: Pattern 4 is redundant.
Found near
  fun
     equal_boola p true = p |
        equal_boola p ... = not p |
        equal_boola ... = p |
        equal_boola ... = ...
ROOT.ML:85: warning: Value identifier (times) has not been referenced.
ROOT.ML:88: warning: Value identifier (one_power) has not been referenced.
ROOT.ML:89: warning: Value identifier (times_power) has not been referenced.
ROOT.ML:98: warning: Value identifier (semigroup_add_ab_semigroup_add) has not been referenced.
ROOT.ML:102: warning: Value identifier (times_semigroup_mult) has not been referenced.
ROOT.ML:108: warning: Value identifier (ab_semigroup_add_semiring) has not been referenced.
ROOT.ML:110: warning: Value identifier (semigroup_mult_semiring) has not been referenced.
ROOT.ML:126: warning: Value identifier (times_mult_zero) has not been referenced.
ROOT.ML:135: warning: Value identifier (semigroup_add_monoid_add) has not been referenced.
ROOT.ML:137: warning: Value identifier (zero_monoid_add) has not been referenced.
ROOT.ML:142: warning: Value identifier (ab_semigroup_add_comm_monoid_add) has not been referenced.
ROOT.ML:144: warning: Value identifier (monoid_add_comm_monoid_add) has not been referenced.
ROOT.ML:150: warning: Value identifier (comm_monoid_add_semiring_0) has not been referenced.
ROOT.ML:154: warning: Value identifier (semiring_semiring_0) has not been referenced.
ROOT.ML:175: warning: Value identifier (semigroup_mult_monoid_mult) has not been referenced.
ROOT.ML:177: warning: Value identifier (power_monoid_mult) has not been referenced.
ROOT.ML:183: warning: Value identifier (monoid_mult_semiring_numeral) has not been referenced.
ROOT.ML:187: warning: Value identifier (semiring_semiring_numeral) has not been referenced.
ROOT.ML:191: warning: Value identifier (one_zero_neq_one) has not been referenced.
ROOT.ML:192: warning: Value identifier (zero_zero_neq_one) has not been referenced.
ROOT.ML:202: warning: Value identifier (zero_neq_one_semiring_1) has not been referenced.
ROOT.ML:247: warning: Value identifier (inc) has not been referenced.
ROOT.ML:247: warning: Value identifier (A_) has not been referenced.
ROOT.ML:280: warning: Value identifier (A_) has not been referenced.
ROOT.ML:277: warning: Value identifier (x22) has not been referenced.
ROOT.ML:277: warning: Value identifier (x21) has not been referenced.
ROOT.ML:277: warning: Value identifier (A_) has not been referenced.
ROOT.ML:276: warning: Value identifier (x22) has not been referenced.
ROOT.ML:276: warning: Value identifier (x21) has not been referenced.
ROOT.ML:276: warning: Value identifier (A_) has not been referenced.
structure Generated_Code:
  sig val bit_integer_test: bool type nat type num end
### Introduced fixed type variable(s): 'a in "P__" or "xs__"
### Introduced fixed type variable(s): 'a in "P__" or "xs__"
### Introduced fixed type variable(s): 'a in "P__" or "Q__"
val uint_arith_simpset = fn: Proof.context -> Proof.context
val uint_arith_tacs = fn: Proof.context -> tactic list
val uint_arith_tac = fn: Proof.context -> int -> tactic
### theory "Regular-Sets.Regular_Set"
### 3.219s elapsed time, 7.288s cpu time, 0.512s GC time
Loading theory "Regular-Sets.Regular_Exp" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking" via "Regular-Sets.NDerivative")
val unat_arith_simpset = fn: Proof.context -> Proof.context
val unat_arith_tacs = fn: Proof.context -> tactic list
val unat_arith_tac = fn: Proof.context -> int -> tactic
### Introduced fixed type variable(s): 'a in "xs__"
### Ignoring duplicate rewrite rule:
### ?y AND - 1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?x1 OR - 1 \<equiv> - 1
### Ignoring duplicate rewrite rule:
### ?x1 XOR - 1 \<equiv> NOT ?x1
### Ignoring duplicate rewrite rule:
### - 1 AND ?y \<equiv> ?y
### Ignoring duplicate rewrite rule:
### - 1 OR ?x1 \<equiv> - 1
### Ignoring duplicate rewrite rule:
### - 1 XOR ?x1 \<equiv> NOT ?x1
class preorder = ord +
  assumes
    "less_le_not_le":
      "\<And>x y. (x < y) = (x \<le> y \<and> \<not> y \<le> x)"
    and "order_refl": "\<And>x. x \<le> x"
    and
    "order_trans":
      "\<And>x y z.
          \<lbrakk>x \<le> y; y \<le> z\<rbrakk>
          \<Longrightarrow> x \<le> z"
class monoid_add = semigroup_add + zero +
  assumes "add_0_left": "\<And>a. (0::'a) + a = a"
    and "add_0_right": "\<And>a. a + (0::'a) = a"
### ISABELLE_OCAMLEXEC not set; skipped checking code for OCaml
consts
  lang :: "'a rexp \<Rightarrow> 'a list set"
consts
  nullable :: "'a rexp \<Rightarrow> bool"
consts
  rexp_empty :: "'a rexp \<Rightarrow> bool"
instantiation
  rexp :: (order) order
  less_eq_rexp == less_eq ::
    'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool
  less_rexp == less :: 'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool
### theory "Coinductive.Coinductive_List"
### 11.110s elapsed time, 36.136s cpu time, 6.692s GC time
Loading theory "Ordered_Resolution_Prover.Lazy_List_Liminf" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Standard_Redundancy" via "Ordered_Resolution_Prover.Proving_Process" via "Ordered_Resolution_Prover.Lazy_List_Chain")
locale word_rotate
### theory "Ordered_Resolution_Prover.Lazy_List_Liminf"
### 0.128s elapsed time, 0.388s cpu time, 0.000s GC time
Loading theory "Ordered_Resolution_Prover.Lazy_List_Chain" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Standard_Redundancy" via "Ordered_Resolution_Prover.Proving_Process")
signature WORD_LIB =
  sig
    val dest_binT: typ -> int
    val dest_wordT: typ -> int
    val is_wordT: typ -> bool
    val mk_wordT: int -> typ
  end
structure Word_Lib: WORD_LIB
structure SMT_Word: sig end
### theory "HOL-Word.Word"
### 8.351s elapsed time, 24.696s cpu time, 5.712s GC time
Loading theory "Native_Word.Word_Misc" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode" via "Native_Word.Uint32")
Proofs for coinductive predicate(s) "chain"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
consts
  prepend :: "'a list \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
Proofs for coinductive predicate(s) "emb"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "prepend_cong1"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for coinductive predicate(s) "chain'"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
locale quickcheck_narrowing_samples
  fixes a_of_integer :: "integer \<Rightarrow> 'a \<times> 'a"
    and zero :: "'a"
    and tr :: "typerep"
### theory "Native_Word.Word_Misc"
### 1.155s elapsed time, 3.592s cpu time, 0.620s GC time
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
instantiation
  rexp :: (linorder) linorder
### theory "Regular-Sets.Regular_Exp"
### 4.268s elapsed time, 13.092s cpu time, 1.216s GC time
Loading theory "Regular-Sets.NDerivative" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method" via "Regular-Sets.Equivalence_Checking")
Loading theory "Regular-Sets.Relation_Interpretation" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" via "Abstract-Rewriting.Abstract_Rewriting" via "Regular-Sets.Regexp_Method")
consts
  rel ::
    "('a \<Rightarrow> ('b \<times> 'b) set)
     \<Rightarrow> 'a rexp \<Rightarrow> ('b \<times> 'b) set"
consts
  word_rel ::
    "('a \<Rightarrow> ('b \<times> 'b) set)
     \<Rightarrow> 'a list \<Rightarrow> ('b \<times> 'b) set"
### theory "Regular-Sets.Relation_Interpretation"
### 0.077s elapsed time, 0.232s cpu time, 0.000s GC time
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (fst p)) <*mlex*>
   (\<lambda>p. size (snd p)) <*mlex*> {}"
### Ignoring duplicate rewrite rule:
### mset (filter ?P1 ?xs1) \<equiv> filter_mset ?P1 (mset ?xs1)
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
consts
  norm :: "'a rexp \<Rightarrow> 'a rexp"
consts
  nderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
### theory "Regular-Sets.NDerivative"
### 5.231s elapsed time, 17.164s cpu time, 0.836s GC time
Loading theory "Regular-Sets.Equivalence_Checking" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" 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 \<Rightarrow> 'a list \<Rightarrow> 'a list"
### theory "Regular-Sets.Equivalence_Checking"
### 0.479s elapsed time, 1.872s cpu time, 0.328s GC time
Loading theory "Regular-Sets.Regexp_Method" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification" via "Abstract-Rewriting.Abstract_Rewriting")
### theory "Native_Word.Bits_Integer"
### 14.597s elapsed time, 44.836s cpu time, 3.180s GC time
Loading theory "Native_Word.Uint32" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator" via "Collections.HashCode")
consts
  rel_of_regexp ::
    "('a \<times> 'a) set list
     \<Rightarrow> nat rexp \<Rightarrow> ('a \<times> 'a) set"
consts
  rel_eq ::
    "nat rexp \<times> nat rexp
     \<Rightarrow> ('a \<times> 'a) set list \<Rightarrow> bool"
### Generation of a parametrized correspondence relation failed.
### Reason:  No relator for the type "Numeral_Type.bit0" found.
instantiation
  uint32 :: {comm_monoid_mult,neg_numeral,comm_ring,modulo}
  modulo_uint32 == modulo ::
    uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
  divide_uint32 == divide ::
    uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
  minus_uint32 == minus :: uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
  uminus_uint32 == uminus :: uint32 \<Rightarrow> uint32
  zero_uint32 == zero_class.zero :: uint32
  plus_uint32 == plus :: uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
  one_uint32 == one_class.one :: uint32
  times_uint32 == times :: uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
instantiation
  uint32 :: linorder
  less_eq_uint32 == less_eq ::
    uint32 \<Rightarrow> uint32 \<Rightarrow> bool
  less_uint32 == less :: uint32 \<Rightarrow> uint32 \<Rightarrow> bool
instantiation
  uint32 :: bitss
  msb_uint32 == msb :: uint32 \<Rightarrow> bool
  test_bit_uint32 == test_bit :: uint32 \<Rightarrow> nat \<Rightarrow> bool
  lsb_uint32 == lsb :: uint32 \<Rightarrow> bool
  set_bit_uint32 == set_bit ::
    uint32 \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint32
  set_bits_uint32 == set_bits ::
    (nat \<Rightarrow> bool) \<Rightarrow> uint32
  shiftl_uint32 == shiftl :: uint32 \<Rightarrow> nat \<Rightarrow> uint32
  shiftr_uint32 == shiftr :: uint32 \<Rightarrow> nat \<Rightarrow> uint32
  bitNOT_uint32 == bitNOT :: uint32 \<Rightarrow> uint32
  bitAND_uint32 == bitAND ::
    uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
  bitOR_uint32 == bitOR :: uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
  bitXOR_uint32 == bitXOR ::
    uint32 \<Rightarrow> uint32 \<Rightarrow> uint32
val regexp_conv = fn: Proof.context -> conv
### theory "Regular-Sets.Regexp_Method"
### 0.978s elapsed time, 3.920s cpu time, 0.000s GC time
Loading theory "Abstract-Rewriting.Abstract_Rewriting" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification" via "First_Order_Terms.Abstract_Unification")
consts
  wit :: "'a llist \<Rightarrow> 'a llist"
instantiation
  uint32 :: equal
  equal_uint32 == equal_class.equal ::
    uint32 \<Rightarrow> uint32 \<Rightarrow> bool
Proofs for coinductive predicate(s) "full_chain"
  Proving monotonicity ...
  Proving the introduction rules ...
instantiation
  uint32 :: size
  size_uint32 == size :: uint32 \<Rightarrow> nat
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
### theory "Ordered_Resolution_Prover.Lazy_List_Chain"
### 9.336s elapsed time, 31.480s cpu time, 2.164s GC time
Loading theory "Ordered_Resolution_Prover.Proving_Process" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution" via "Ordered_Resolution_Prover.Standard_Redundancy")
### Code generator: dropping subsumed code equation
### (!!) ?x \<equiv> (!!) (Rep_uint32 ?x)
### Code generator: dropping subsumed code equation
### lsb ?x \<equiv> lsb (Rep_uint32 ?x)
### Ambiguous input (line 565 of "$AFP/Native_Word/Uint32.thy") produces 2 parse trees:
### ("\<^const>Pure.imp"
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Orderings.ord_class.less_eq"
###       ("_applC" ("_position" size) ("_position" x)) ("_position" n)))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Word.sshiftr" ("_position" x) ("_position" n))
###       ("\<^const>HOL.If"
###         ("\<^const>Bits.bits_class.test_bit" ("_position" x)
###           ("\<^const>Groups.minus_class.minus"
###             ("_applC" ("_position" size) ("_position" x))
###             ("\<^const>Groups.one_class.one")))
###         ("\<^const>Groups.uminus_class.uminus"
###           ("\<^const>Groups.one_class.one"))
###         ("\<^const>Groups.zero_class.zero")))))
### ("\<^const>Pure.imp"
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>Orderings.ord_class.less_eq"
###       ("_applC" ("_position" size) ("_position" x)) ("_position" n)))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Uint32.sshiftr_uint32" ("_position" x) ("_position" n))
###       ("\<^const>HOL.If"
###         ("\<^const>Bits.bits_class.test_bit" ("_position" x)
###           ("\<^const>Groups.minus_class.minus"
###             ("_applC" ("_position" size) ("_position" x))
###             ("\<^const>Groups.one_class.one")))
###         ("\<^const>Groups.uminus_class.uminus"
###           ("\<^const>Groups.one_class.one"))
###         ("\<^const>Groups.zero_class.zero")))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 569 of "$AFP/Native_Word/Uint32.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Word.sshiftr" ("_position" x) ("_position" n))
###     ("\<^const>HOL.If"
###       ("\<^const>Orderings.ord_class.less" ("_position" n)
###         ("_Numeral" ("_constify" ("_position" 32))))
###       ("_applC" ("_position" uint32_sshiftr)
###         ("_cargs" ("_position" x)
###           ("_applC" ("_position" integer_of_nat) ("_position" n))))
###       ("\<^const>HOL.If"
###         ("\<^const>Bits.bits_class.test_bit" ("_position" x)
###           ("_Numeral" ("_constify" ("_position" 31))))
###         ("\<^const>Groups.uminus_class.uminus"
###           ("\<^const>Groups.one_class.one"))
###         ("\<^const>Groups.zero_class.zero")))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Uint32.sshiftr_uint32" ("_position" x) ("_position" n))
###     ("\<^const>HOL.If"
###       ("\<^const>Orderings.ord_class.less" ("_position" n)
###         ("_Numeral" ("_constify" ("_position" 32))))
###       ("_applC" ("_position" uint32_sshiftr)
###         ("_cargs" ("_position" x)
###           ("_applC" ("_position" integer_of_nat) ("_position" n))))
###       ("\<^const>HOL.If"
###         ("\<^const>Bits.bits_class.test_bit" ("_position" x)
###           ("_Numeral" ("_constify" ("_position" 31))))
###         ("\<^const>Groups.uminus_class.uminus"
###           ("\<^const>Groups.one_class.one"))
###         ("\<^const>Groups.zero_class.zero")))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 575 of "$AFP/Native_Word/Uint32.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" Rep_uint32)
###       ("_applC" ("_position" uint32_sshiftr)
###         ("_cargs" ("_position" w) ("_position" n))))
###     ("\<^const>HOL.If"
###       ("\<^const>HOL.disj"
###         ("\<^const>Orderings.ord_class.less" ("_position" n)
###           ("\<^const>Groups.zero_class.zero"))
###         ("\<^const>Orderings.ord_class.less_eq"
###           ("_Numeral" ("_constify" ("_position" 32))) ("_position" n)))
###       ("_applC" ("_position" Rep_uint32)
###         ("_applC" ("_position" undefined)
###           ("_cargs" ("_position" sshiftr_uint32)
###             ("_cargs" ("_position" w) ("_position" n)))))
###       ("\<^const>Uint32.sshiftr_uint32"
###         ("_applC" ("_position" Rep_uint32) ("_position" w))
###         ("_applC" ("_position" nat_of_integer) ("_position" n))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" Rep_uint32)
###       ("_applC" ("_position" uint32_sshiftr)
###         ("_cargs" ("_position" w) ("_position" n))))
###     ("\<^const>HOL.If"
###       ("\<^const>HOL.disj"
###         ("\<^const>Orderings.ord_class.less" ("_position" n)
###           ("\<^const>Groups.zero_class.zero"))
###         ("\<^const>Orderings.ord_class.less_eq"
###           ("_Numeral" ("_constify" ("_position" 32))) ("_position" n)))
###       ("_applC" ("_position" Rep_uint32)
###         ("_applC" ("_position" undefined)
###           ("_cargs" ("_position" sshiftr_uint32)
###             ("_cargs" ("_position" w) ("_position" n)))))
###       ("\<^const>Word.sshiftr"
###         ("_applC" ("_position" Rep_uint32) ("_position" w))
###         ("_applC" ("_position" nat_of_integer) ("_position" n))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Code generator: dropping subsumed code equation
### msb ?x \<equiv> msb (Rep_uint32 ?x)
instantiation
  uint32 :: {exhaustive,full_exhaustive,random}
  random_uint32 == random_class.random ::
    natural
    \<Rightarrow> natural \<times> natural
                  \<Rightarrow> (uint32 \<times>
                                 (unit \<Rightarrow> term)) \<times>
                                natural \<times> natural
  full_exhaustive_uint32 == full_exhaustive_class.full_exhaustive ::
    (uint32 \<times> (unit \<Rightarrow> term)
     \<Rightarrow> (bool \<times> term list) option)
    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option
  exhaustive_uint32 == exhaustive_class.exhaustive ::
    (uint32 \<Rightarrow> (bool \<times> term list) option)
    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option
instantiation
  uint32 :: narrowing
  narrowing_uint32 == narrowing ::
    integer \<Rightarrow> uint32 ??.Quickcheck_Narrowing.narrowing_cons
locale redundancy_criterion
  fixes \<Gamma> :: "'a inference set"
    and
    Rf :: "'a literal multiset set \<Rightarrow> 'a literal multiset set"
    and Ri :: "'a literal multiset set \<Rightarrow> 'a inference set"
  assumes "redundancy_criterion \<Gamma> Rf Ri"
Proofs for inductive predicate(s) "derive"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Native_Word.Uint32"
### 2.212s elapsed time, 8.824s cpu time, 0.380s GC time
Loading theory "Collections.HashCode" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances" via "Deriving.Hash_Generator")
locale sat_preserving_redundancy_criterion
  fixes \<Gamma> :: "'a inference set"
    and
    Rf :: "'a literal multiset set \<Rightarrow> 'a literal multiset set"
    and Ri :: "'a literal multiset set \<Rightarrow> 'a inference set"
  assumes "sat_preserving_redundancy_criterion \<Gamma> Rf Ri"
class hashable = type +
  fixes hashcode :: "'a \<Rightarrow> uint32"
    and def_hashmap_size :: "'a itself \<Rightarrow> nat"
  assumes "def_hashmap_size": "1 < def_hashmap_size TYPE('a)"
instantiation
  unit :: hashable
  hashcode_unit == hashcode :: unit \<Rightarrow> uint32
  def_hashmap_size_unit == def_hashmap_size :: unit itself \<Rightarrow> nat
Found termination order: "{}"
instantiation
  bool :: hashable
  hashcode_bool == hashcode :: bool \<Rightarrow> uint32
  def_hashmap_size_bool == def_hashmap_size :: bool itself \<Rightarrow> nat
locale effective_redundancy_criterion
  fixes \<Gamma> :: "'a inference set"
    and
    Rf :: "'a literal multiset set \<Rightarrow> 'a literal multiset set"
    and Ri :: "'a literal multiset set \<Rightarrow> 'a inference set"
  assumes "effective_redundancy_criterion \<Gamma> Rf Ri"
instantiation
  int :: hashable
  hashcode_int == hashcode :: int \<Rightarrow> uint32
  def_hashmap_size_int == def_hashmap_size :: int itself \<Rightarrow> nat
instantiation
  integer :: hashable
  hashcode_integer == hashcode :: integer \<Rightarrow> uint32
  def_hashmap_size_integer == def_hashmap_size ::
    integer itself \<Rightarrow> nat
instantiation
  nat :: hashable
  hashcode_nat == hashcode :: nat \<Rightarrow> uint32
  def_hashmap_size_nat == def_hashmap_size :: nat itself \<Rightarrow> nat
locale sat_preserving_effective_redundancy_criterion
  fixes \<Gamma> :: "'a inference set"
    and
    Rf :: "'a literal multiset set \<Rightarrow> 'a literal multiset set"
    and Ri :: "'a literal multiset set \<Rightarrow> 'a inference set"
  assumes "sat_preserving_effective_redundancy_criterion \<Gamma> Rf Ri"
instantiation
  char :: hashable
  hashcode_char == hashcode :: char \<Rightarrow> uint32
  def_hashmap_size_char == def_hashmap_size :: char itself \<Rightarrow> nat
locale trivial_redundancy_criterion
  fixes \<Gamma> :: "'a inference set"
instantiation
  prod :: (hashable, hashable) hashable
  hashcode_prod == hashcode :: 'a \<times> 'b \<Rightarrow> uint32
  def_hashmap_size_prod == def_hashmap_size ::
    ('a \<times> 'b) itself \<Rightarrow> nat
instantiation
  sum :: (hashable, hashable) hashable
  hashcode_sum == hashcode :: 'a + 'b \<Rightarrow> uint32
  def_hashmap_size_sum == def_hashmap_size ::
    ('a + 'b) itself \<Rightarrow> nat
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 ...
instantiation
  list :: (hashable) hashable
  hashcode_list == hashcode :: 'a list \<Rightarrow> uint32
  def_hashmap_size_list == def_hashmap_size ::
    'a list itself \<Rightarrow> nat
### theory "Ordered_Resolution_Prover.Proving_Process"
### 1.257s elapsed time, 5.040s cpu time, 0.000s GC time
Loading theory "Ordered_Resolution_Prover.Standard_Redundancy" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution")
instantiation
  option :: (hashable) hashable
  hashcode_option == hashcode :: 'a option \<Rightarrow> uint32
  def_hashmap_size_option == def_hashmap_size ::
    'a option itself \<Rightarrow> nat
instantiation
  String.literal :: hashable
  hashcode_literal == hashcode :: String.literal \<Rightarrow> uint32
  def_hashmap_size_literal == def_hashmap_size ::
    String.literal itself \<Rightarrow> nat
locale standard_redundancy_criterion
  fixes \<Gamma> :: "'a inference set"
### theory "Collections.HashCode"
### 0.419s elapsed time, 1.680s cpu time, 0.000s GC time
Loading theory "Deriving.Hash_Generator" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive" via "Deriving.Hash_Instances")
locale standard_redundancy_criterion_reductive
  fixes \<Gamma> :: "'a inference set"
  assumes "standard_redundancy_criterion_reductive \<Gamma>"
### theory "Abstract-Rewriting.Abstract_Rewriting"
### 2.095s elapsed time, 8.320s cpu time, 0.812s GC time
Loading theory "First_Order_Terms.Abstract_Matching" (required by "Functional_Ordered_Resolution_Prover.Executable_Subsumption" via "First_Order_Terms.Matching")
Loading theory "First_Order_Terms.Abstract_Unification" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "First_Order_Terms.Unification")
locale standard_redundancy_criterion_counterex_reducing
  fixes \<Gamma> :: "'a inference set"
    and I_of :: "'a literal multiset set \<Rightarrow> 'a set"
  assumes "standard_redundancy_criterion_counterex_reducing \<Gamma> I_of"
### theory "Ordered_Resolution_Prover.Standard_Redundancy"
### 0.419s elapsed time, 1.644s cpu time, 0.432s GC time
Loading theory "Ordered_Resolution_Prover.FO_Ordered_Resolution" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" via "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover")
Proofs for inductive predicate(s) "MATCH1"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Proofs for inductive predicate(s) "UNIF1"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
signature HASHCODE_GENERATOR =
  sig
    val ensure_info: hash_type -> string -> local_theory -> local_theory
    val generate_hash: hash_type -> string -> local_theory -> local_theory
    val generate_hashs_from_bnf_fp:
       string ->
         local_theory ->
           ((term * thm list) list * (term * thm) list) * local_theory
    val get_info: Proof.context -> string -> info option
    datatype hash_type = BNF | HASHCODE
    val hashable_instance: string -> theory -> theory
    type info =
       {hash: term,
        hash_def: thm option,
        map: term,
        map_comp: thm option, phash: term, used_positions: bool list}
    val register_foreign_hash: typ -> term -> local_theory -> local_theory
    val register_foreign_partial_and_full_hash:
       string ->
         term ->
           term ->
             term ->
               thm option ->
                 thm option -> bool list -> local_theory -> local_theory
    val register_hash_of: string -> local_theory -> local_theory
  end
structure Hashcode_Generator: HASHCODE_GENERATOR
### theory "Deriving.Hash_Generator"
### 0.913s elapsed time, 3.612s cpu time, 0.432s GC time
Loading theory "Deriving.Hash_Instances" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term" via "Deriving.Derive")
generating hash-function for type "Product_Type.prod"
Proofs for inductive predicate(s) "UNIF"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "First_Order_Terms.Abstract_Matching"
### 0.643s elapsed time, 2.568s cpu time, 0.000s GC time
generating hash-function for type "Sum_Type.sum"
generating hash-function for type "Option.option"
generating hash-function for type "List.list"
### theory "Deriving.Hash_Instances"
### 0.139s elapsed time, 0.556s cpu time, 0.000s GC time
Loading theory "Deriving.Derive" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term")
### theory "First_Order_Terms.Abstract_Unification"
### 0.846s elapsed time, 3.384s cpu time, 0.000s GC time
Loading theory "First_Order_Terms.Unification" (required by "Functional_Ordered_Resolution_Prover.IsaFoR_Term")
locale FO_resolution
  fixes subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"
    and atm_of_atms :: "'a list \<Rightarrow> 'a"
    and mgu :: "'a set set \<Rightarrow> 's option"
    and less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes
    "FO_resolution (\<cdot>a) id_subst (\<odot>) renamings_apart atm_of_atms
      mgu less_atm"
Proofs for inductive predicate(s) "eligible"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "ord_resolve"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
(if ?x \<le> ?y then if ?x = ?y then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?y = ?x then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?y \<le> ?x then ?P else ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x \<le> ?y then if ?x < ?y then ?Q else ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?x \<le> ?y then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?y < ?x then ?R else ?P) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?x = ?y then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x < ?y then ?Q else if ?y = ?x then ?P else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?y < ?x then ?R else ?Q) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?x < ?y then ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?y \<le> ?x then ?R else ?Q) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
(if ?x = ?y then ?P else if ?x \<le> ?y then ?Q else ?R) =
(case compare ?x ?y of Eq \<Rightarrow> ?P | Lt \<Rightarrow> ?Q
 | Gt \<Rightarrow> ?R)
Proofs for inductive predicate(s) "ord_resolve_rename"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "{}"
### theory "Deriving.Derive"
### 1.206s elapsed time, 4.796s cpu time, 0.672s GC time
### theory "Ordered_Resolution_Prover.FO_Ordered_Resolution"
### 1.963s elapsed time, 7.820s cpu time, 0.672s GC time
Loading theory "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover" via "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover")
### theory "First_Order_Terms.Unification"
### 1.160s elapsed time, 4.612s cpu time, 0.672s GC time
Loading theory "First_Order_Terms.Matching" (required by "Functional_Ordered_Resolution_Prover.Executable_Subsumption")
Loading theory "Functional_Ordered_Resolution_Prover.IsaFoR_Term"
locale FO_resolution_prover
  fixes S :: "'a literal multiset \<Rightarrow> 'a literal multiset"
    and subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"
    and atm_of_atms :: "'a list \<Rightarrow> 'a"
    and mgu :: "'a set set \<Rightarrow> 's option"
    and less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes
    "FO_resolution_prover S (\<cdot>a) id_subst (\<odot>) renamings_apart
      atm_of_atms mgu less_atm"
Found termination order: "{}"
Found termination order: "{}"
### theory "First_Order_Terms.Matching"
### 0.702s elapsed time, 2.812s cpu time, 0.000s GC time
Found termination order: "{}"
Proofs for inductive predicate(s) "RP"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  renamings_apart ::
    "('f, nat) Term.term literal multiset list
     \<Rightarrow> (nat \<Rightarrow> ('f, nat) Term.term) list"
Found termination order: "length <*mlex*> {}"
deriving "compare" instance for type "Term.term"
generating comparator for type "Term.term"
deriving "compare" instance for type "Clausal_Logic.literal"
generating comparator for type "Clausal_Logic.literal"
### theory "Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover"
### 2.187s elapsed time, 8.720s cpu time, 0.424s GC time
Loading theory "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover" (required by "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover")
deriving "linorder" instance for type "Product_Type.prod"
deriving "linorder" instance for type "List.list"
Found termination order: "{}"
### theory "Functional_Ordered_Resolution_Prover.IsaFoR_Term"
### 2.405s elapsed time, 9.568s cpu time, 0.424s GC time
Loading theory "Functional_Ordered_Resolution_Prover.Executable_Subsumption"
locale weighted_FO_resolution_prover
  fixes S :: "'a literal multiset \<Rightarrow> 'a literal multiset"
    and subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"
    and atm_of_atms :: "'a list \<Rightarrow> 'a"
    and mgu :: "'a set set \<Rightarrow> 's option"
    and less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and weight :: "'a literal multiset \<times> nat \<Rightarrow> nat"
  assumes
    "weighted_FO_resolution_prover S (\<cdot>a) id_subst (\<odot>)
      renamings_apart atm_of_atms mgu less_atm weight"
Found termination order: "{}"
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
Found termination order: "{}"
### Rewrite rule not in simpset:
### \<bar>1::?'a1\<bar> \<equiv> 1::?'a1
Found termination order: "{}"
Found termination order: "{}"
Proofs for inductive predicate(s) "weighted_RP"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "Functional_Ordered_Resolution_Prover.Executable_Subsumption"
### 1.676s elapsed time, 6.512s cpu time, 0.344s GC time
### Metis: Unused theorems: "Fun.comp_apply"
locale weighted_FO_resolution_prover_with_size_timestamp_factors
  fixes S :: "'a literal multiset \<Rightarrow> 'a literal multiset"
    and subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"
    and atm_of_atms :: "'a list \<Rightarrow> 'a"
    and mgu :: "'a set set \<Rightarrow> 's option"
    and less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and size_atm :: "'a \<Rightarrow> nat"
    and size_factor :: "nat"
    and timestamp_factor :: "nat"
  assumes
    "weighted_FO_resolution_prover_with_size_timestamp_factors S (\<cdot>a)
      id_subst (\<odot>) renamings_apart atm_of_atms mgu less_atm
      timestamp_factor"
Found termination order: "{}"
### theory "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover"
### 2.980s elapsed time, 11.488s cpu time, 0.712s GC time
Loading theory "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover"
### Rule already declared as introduction (intro)
### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A
locale deterministic_FO_resolution_prover
  fixes S :: "'a literal multiset \<Rightarrow> 'a literal multiset"
    and subst_atm :: "'a \<Rightarrow> 's \<Rightarrow> 'a"
    and id_subst :: "'s"
    and comp_subst :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    and renamings_apart :: "'a literal multiset list \<Rightarrow> 's list"
    and atm_of_atms :: "'a list \<Rightarrow> 'a"
    and mgu :: "'a set set \<Rightarrow> 's option"
    and less_atm :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and size_atm :: "'a \<Rightarrow> nat"
    and timestamp_factor :: "nat"
    and size_factor :: "nat"
  assumes
    "deterministic_FO_resolution_prover S (\<cdot>a) id_subst (\<odot>)
      renamings_apart atm_of_atms mgu less_atm size_factor"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
consts
  reduce ::
    "'a literal list list
     \<Rightarrow> 'a literal list
                   \<Rightarrow> 'a literal list
                                 \<Rightarrow> 'a literal list"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd p)) (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd p)) (snd p)) <*mlex*> {}"
Found termination order: "{}"
consts
  derivation_from ::
    "('a literal list \<times> nat) list \<times>
     ('a literal list \<times> nat) list \<times>
     ('a literal list \<times> nat) list \<times> nat
     \<Rightarrow> (('a literal list \<times> nat) list \<times>
                    ('a literal list \<times> nat) list \<times>
                    ('a literal list \<times> nat) list \<times> nat) llist"
### theory "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover"
### 5.420s elapsed time, 21.148s cpu time, 0.920s GC time
### Ignoring duplicate rewrite rule:
### ?y1 AND ?x1 AND ?z1 \<equiv> ?x1 AND ?y1 AND ?z1
Testing conjecture with Quickcheck-narrowing...
Testing conjecture with Quickcheck-random...
Quickcheck found a counterexample:
  xs = LCons a\<^sub>1 LNil
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
  xs = LCons a\<^sub>1 LNil
Evaluated terms:
  LNil = LNil
### Rule already declared as introduction (intro)
### \<lbrakk>?P ?a; \<And>x. ?P x \<Longrightarrow> x = ?a\<rbrakk>
### \<Longrightarrow> (THE x. ?P x) = ?a
### Ignoring duplicate rewrite rule:
### \<exists>x\<in>?A1. \<not> lnull x \<Longrightarrow>
### lhd (lSup ?A1) \<equiv>
### THE x. x \<in> lhd ` (?A1 \<inter> {xs. \<not> lnull xs})
### Rule already declared as introduction (intro)
### \<lbrakk>?P ?a; \<And>x. ?P x \<Longrightarrow> x = ?a\<rbrakk>
### \<Longrightarrow> (THE x. ?P x) = ?a
### Rule already declared as introduction (intro)
### \<lbrakk>?P ?a; \<And>x. ?P x \<Longrightarrow> x = ?a\<rbrakk>
### \<Longrightarrow> (THE x. ?P x) = ?a
[1 of 4] Compiling Typerep          ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Typerep.hs.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Typerep.hs.o )
[2 of 4] Compiling Generated_Code   ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Generated_Code.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Generated_Code.o )
[3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Narrowing_Engine.o )
[4 of 4] Compiling Main             ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Main.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/Main.o )
Linking /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4499144/isabelle_quickcheck_narrowing ...
### Rule already declared as introduction (intro)
### \<lbrakk>?P ?a; \<And>x. ?P x \<Longrightarrow> x = ?a\<rbrakk>
### \<Longrightarrow> (THE x. ?P x) = ?a
### Rule already declared as introduction (intro)
### \<lbrakk>?P ?a; \<And>x. ?P x \<Longrightarrow> x = ?a\<rbrakk>
### \<Longrightarrow> (THE x. ?P x) = ?a
### Metis: Unused theorems: "More_Bits_Int.int_shiftl_numeral_2"
### Ignoring duplicate rewrite rule:
### ?x1 BIT ?b1 >> Suc ?n1 \<equiv> ?x1 >> ?n1
### Metis: Unused theorems: "Nat.neq0_conv", "Num.numeral_class.numeral.numeral_One", "Num.semiring_char_0_class.zero_neq_numeral"
### Ignoring duplicate rewrite rule:
### class.ccpo lSup (\<sqsubseteq>) (mk_less (\<sqsubseteq>)) \<equiv> True
[1 of 4] Compiling Typerep          ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Typerep.hs.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Typerep.hs.o )
[2 of 4] Compiling Generated_Code   ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Generated_Code.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Generated_Code.o )
[3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Narrowing_Engine.o )
[4 of 4] Compiling Main             ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Main.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/Main.o )
Linking /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4504212/isabelle_quickcheck_narrowing ...
### 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
### Rule already declared as introduction (intro)
### ?P ?x \<Longrightarrow> \<exists>x. ?P x
[1 of 4] Compiling Typerep          ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Typerep.hs.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Typerep.hs.o )
[2 of 4] Compiling Generated_Code   ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Generated_Code.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Generated_Code.o )
[3 of 4] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Narrowing_Engine.o )
[4 of 4] Compiling Main             ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Main.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/Main.o )
Linking /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4506620/isabelle_quickcheck_narrowing ...
### Introduced fixed type variable(s): 'b in "zs__"
### Rule already declared as introduction (intro)
### ?P ?x \<Longrightarrow> \<exists>x. ?P x
Quickcheck found no counterexample.
### Metis: Unused theorems: "Coinductive_List.lappend_llist_of_llist_of"
### Metis: Unused theorems: "Coinductive_List.lfinite_lappend", "Coinductive_List.lfinite_llist_of", "Coinductive_List.list_of_lappend", "Coinductive_List.list_of_llist_of"
### Rule already declared as introduction (intro)
### ?P ?x \<Longrightarrow> \<exists>x. ?P x
### Introduced fixed type variable(s): 'b in "xs__"
### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_2"
### Metis: Unused theorems: "Coinductive_Nat.enat_le_plus_same_1"
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Rule already declared as elimination (elim)
### \<lbrakk>?w \<in> ?A @@ ?B;
###  \<And>u v.
###     \<lbrakk>u \<in> ?A; v \<in> ?B; ?w = u @ v\<rbrakk>
###     \<Longrightarrow> ?thesis\<rbrakk>
### \<Longrightarrow> ?thesis
### Rule already declared as introduction (intro)
### ?P ?x \<Longrightarrow> \<exists>x. ?P x
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Metis: Unused theorems: "Rings.comm_ring_1_class.minus_dvd_iff"
### Rule already declared as introduction (intro)
### (\<And>x y. ?A x y \<Longrightarrow> ?B (?f x) (?g y)) \<Longrightarrow>
### (?A ===> ?B) ?f ?g
### Metis: Unused theorems: "Word.word_sint.Rep_inverse'", "Word.wi_hom_neg"
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?k1; ?k1 < ?l1\<rbrakk>
### \<Longrightarrow> ?k1 div ?l1 \<equiv> 0
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y < ?n1 \<Longrightarrow> ?y mod ?n1 \<equiv> ?y
### Metis: Unused theorems: "Word.word_less_def"
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<lbrakk>0 \<le> ?y; ?y < ?l1\<rbrakk>
### \<Longrightarrow> ?y mod ?l1 \<equiv> ?y
### Metis: Unused theorems: "Nat.semiring_1_class.of_nat_mult"
Testing conjecture with Quickcheck-narrowing...
Testing conjecture with Quickcheck-random...
Quickcheck found a counterexample:
  x = 0
  y = - 1
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
  x = 0
  y = - 1
Evaluated terms:
  x AND y = 0
  x OR y = - 1
### Ignoring duplicate rewrite rule:
### Numeral1 \<equiv> 1::?'a1
### Ignoring duplicate rewrite rule:
### Numeral1 \<equiv> 1::?'a1
[1 of 5] Compiling Data_Bits        ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Data_Bits.hs.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Data_Bits.hs.o )
[2 of 5] Compiling Typerep          ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Typerep.hs.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Typerep.hs.o )
[3 of 5] Compiling Generated_Code   ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Generated_Code.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Generated_Code.o )
[4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Narrowing_Engine.o )
[5 of 5] Compiling Main             ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Main.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/Main.o )
Linking /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4553504/isabelle_quickcheck_narrowing ...
Quickcheck found no counterexample.
The following sorts can be derived
comparator: generate comparators for given types, options: (linorder) or ()
compare: register types in class compare, options: (linorder) or ()
compare_order: register types in class compare_order, options: (linorder) or ()
countable: register datatypes is class countable
equality: generate an equality function, options are () and (eq)
hash_code: generate a hash function, options are () and (hashcode)
hashable: register types in class hashable
linorder: register types in class linorder, options: (linorder) or ()
*** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.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 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy")
### Ignoring duplicate rewrite rule:
### mset (filter ?P1 ?xs1) \<equiv> filter_mset ?P1 (mset ?xs1)
Testing conjecture with Quickcheck-narrowing...
[1 of 5] Compiling Data_Bits        ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Data_Bits.hs.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Data_Bits.hs.o )
[2 of 5] Compiling Typerep          ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Typerep.hs.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Typerep.hs.o )
[3 of 5] Compiling Generated_Code   ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Generated_Code.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Generated_Code.o )
[4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Narrowing_Engine.o )
[5 of 5] Compiling Main             ( /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Main.hs, /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/Main.o )
Linking /tmp/isabelle-jenkins/process4227127210108451432/Quickcheck_Narrowing4615200/isabelle_quickcheck_narrowing ...
Quickcheck found no counterexample.
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.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 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy")