Loading theory "HOL-Datatype_Examples.Compat"
Loading theory "HOL-Datatype_Examples.Datatype_Simproc_Tests"
Loading theory "HOL-Datatype_Examples.Lift_BNF"
Loading theory "HOL-Datatype_Examples.Milner_Tofte"
Loading theory "HOL-Datatype_Examples.TLList"
Loading theory "HOL-Datatype_Examples.TreeFI" (required by "HOL-Datatype_Examples.Koenig")
val check_len = fn: int -> 'a list -> string -> bool
val check_lens = fn: int * int * int -> 'a list * 'b list * 'c list -> bool
val get_descrs = fn:
   theory ->
     int * int * int ->
       string ->
         (int *
          (string * Old_Datatype_Data.dtyp list *
           (string * Old_Datatype_Data.dtyp list) list)
         )
         list
         *
         (int *
          (string * Old_Datatype_Aux.dtyp list *
           (string * Old_Datatype_Aux.dtyp list) list)
         )
         list
         *
         (int *
          (string * Old_Datatype_Aux.dtyp list *
           (string * Old_Datatype_Aux.dtyp list) list)
         )
         list
### theory "HOL-Datatype_Examples.TreeFI"
### 0.656s elapsed time, 4.004s cpu time, 0.000s GC time
Loading theory "HOL-Datatype_Examples.Cyclic_List"
Proofs for inductive predicate(s) "cyclic1"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
val it =
   ([],
    [(0, ("Compat.w", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.w.W", []),
           ("Compat.w.W'",
            [DtType
              ("Product_Type.prod",
               [DtRec 0,
                DtType
                 ("List.list", [DtTFree ("'b", ["HOL.type"])])])])]))],
    [(0, ("Compat.w", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.w.W", []),
           ("Compat.w.W'",
            [DtType
              ("Product_Type.prod",
               [DtRec 0,
                DtType
                 ("List.list", [DtTFree ("'b", ["HOL.type"])])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
Proofs for inductive predicate(s) "lfinite"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "HOL-Datatype_Examples.Cyclic_List"
### 0.449s elapsed time, 2.624s cpu time, 0.724s GC time
Loading theory "HOL-Datatype_Examples.Free_Idempotent_Monoid"
Proofs for inductive predicate(s) "cancel1"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "pcancel1"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
val it =
   ([(0, ("Compat.w", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.w.W", []), ("Compat.w.W'", [DtRec 1])])),
     (1, ("Product_Type.prod",
          [DtRec 0, DtType ("List.list", [DtTFree ("'b", ["HOL.type"])])],
          [("Product_Type.Pair",
            [DtRec 0,
             DtType ("List.list", [DtTFree ("'b", ["HOL.type"])])])]))],
    [(0, ("Compat.w", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.w.W", []), ("Compat.w.W'", [DtRec 1])])),
     (1, ("Product_Type.prod",
          [DtRec 0, DtType ("List.list", [DtTFree ("'b", ["HOL.type"])])],
          [("Product_Type.Pair",
            [DtRec 0,
             DtType ("List.list", [DtTFree ("'b", ["HOL.type"])])])]))],
    [(0, ("Compat.w", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.w.W", []),
           ("Compat.w.W'",
            [DtType
              ("Product_Type.prod",
               [DtRec 0,
                DtType
                 ("List.list", [DtTFree ("'b", ["HOL.type"])])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### theory "HOL-Datatype_Examples.Free_Idempotent_Monoid"
### 0.380s elapsed time, 2.328s cpu time, 0.000s GC time
Loading theory "HOL-Datatype_Examples.LDL"
### theory "HOL-Datatype_Examples.TLList"
### 1.490s elapsed time, 8.980s cpu time, 0.724s GC time
Loading theory "HOL-Datatype_Examples.Koenig"
Proofs for coinductive predicate(s) "infiniteTr"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
Proofs for coinductive predicate(s) "properPath"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
### theory "HOL-Datatype_Examples.Koenig"
### 0.430s elapsed time, 2.584s cpu time, 0.000s GC time
Loading theory "HOL-Datatype_Examples.Process"
val it =
   ([],
    [(0, ("Compat.s",
          [DtTFree ("'c", ["HOL.type"]), DtTFree ("'b", ["HOL.type"])],
          [("Compat.s.L", [DtTFree ("'c", ["HOL.type"])]),
           ("Compat.s.R", [DtTFree ("'b", ["HOL.type"])])]))],
    [(0, ("Compat.s",
          [DtTFree ("'c", ["HOL.type"]), DtTFree ("'b", ["HOL.type"])],
          [("Compat.s.L", [DtTFree ("'c", ["HOL.type"])]),
           ("Compat.s.R", [DtTFree ("'b", ["HOL.type"])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
Proofs for inductive predicate(s) "ACI"
  Proving monotonicity ...
Proofs for inductive predicate(s) "eval"
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "elab"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "ACIEQ"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for coinductive predicate(s) "hasty"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
### No map function defined for LDL.rexp. This will cause problems later on.
### theory "HOL-Datatype_Examples.Milner_Tofte"
### 3.000s elapsed time, 17.848s cpu time, 2.076s GC time
Loading theory "HOL-Datatype_Examples.Stream_Processor"
Proofs for coinductive predicate(s) "trace"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
val it =
   ([],
    [(0, ("Compat.x", [DtTFree ("'d", ["HOL.type"])],
          [("Compat.x.X", []),
           ("Compat.x.X'",
            [DtType
              ("Compat.s",
               [DtType ("List.list", [DtRec 0]),
                DtType
                 ("List.list", [DtTFree ("'d", ["HOL.type"])])])])]))],
    [(0, ("Compat.x", [DtTFree ("'d", ["HOL.type"])],
          [("Compat.x.X", []),
           ("Compat.x.X'",
            [DtType
              ("Compat.s",
               [DtType ("List.list", [DtRec 0]),
                DtType
                 ("List.list", [DtTFree ("'d", ["HOL.type"])])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.s",
          [DtTFree ("'c", ["HOL.type"]), DtTFree ("'b", ["HOL.type"])],
          [("Compat.s.L", [DtTFree ("'c", ["HOL.type"])]),
           ("Compat.s.R", [DtTFree ("'b", ["HOL.type"])])]))],
    [(0, ("Compat.s",
          [DtTFree ("'c", ["HOL.type"]), DtTFree ("'b", ["HOL.type"])],
          [("Compat.s.L", [DtTFree ("'c", ["HOL.type"])]),
           ("Compat.s.R", [DtTFree ("'b", ["HOL.type"])])]))],
    [(0, ("Compat.s",
          [DtTFree ("'c", ["HOL.type"]), DtTFree ("'b", ["HOL.type"])],
          [("Compat.s.L", [DtTFree ("'c", ["HOL.type"])]),
           ("Compat.s.R", [DtTFree ("'b", ["HOL.type"])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([],
    [(0, ("Compat.x", [DtTFree ("'d", ["HOL.type"])],
          [("Compat.x.X", []),
           ("Compat.x.X'",
            [DtType
              ("Compat.s",
               [DtType ("List.list", [DtRec 0]),
                DtType
                 ("List.list", [DtTFree ("'d", ["HOL.type"])])])])]))],
    [(0, ("Compat.x", [DtTFree ("'d", ["HOL.type"])],
          [("Compat.x.X", []),
           ("Compat.x.X'",
            [DtType
              ("Compat.s",
               [DtType ("List.list", [DtRec 0]),
                DtType
                 ("List.list", [DtTFree ("'d", ["HOL.type"])])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### theory "HOL-Datatype_Examples.LDL"
### 2.315s elapsed time, 13.612s cpu time, 2.504s GC time
Loading theory "HOL-Datatype_Examples.Lambda_Term"
### theory "HOL-Datatype_Examples.Datatype_Simproc_Tests"
### 3.863s elapsed time, 22.952s cpu time, 3.228s GC time
Loading theory "HOL-Datatype_Examples.Misc_Codatatype"
val it =
   ([(0, ("Compat.x", [DtTFree ("'d", ["HOL.type"])],
          [("Compat.x.X", []), ("Compat.x.X'", [DtRec 2])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 0, DtRec 1])])),
     (2, ("Compat.s",
          [DtType ("List.list", [DtRec 0]),
           DtType ("List.list", [DtTFree ("'d", ["HOL.type"])])],
          [("Compat.s.L", [DtRec 1]),
           ("Compat.s.R",
            [DtType ("List.list", [DtTFree ("'d", ["HOL.type"])])])]))],
    [(0, ("Compat.x", [DtTFree ("'d", ["HOL.type"])],
          [("Compat.x.X", []), ("Compat.x.X'", [DtRec 2])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 0, DtRec 1])])),
     (2, ("Compat.s",
          [DtType ("List.list", [DtRec 0]),
           DtType ("List.list", [DtTFree ("'d", ["HOL.type"])])],
          [("Compat.s.L", [DtRec 1]),
           ("Compat.s.R",
            [DtType ("List.list", [DtTFree ("'d", ["HOL.type"])])])]))],
    [(0, ("Compat.x", [DtTFree ("'d", ["HOL.type"])],
          [("Compat.x.X", []),
           ("Compat.x.X'",
            [DtType
              ("Compat.s",
               [DtType ("List.list", [DtRec 0]),
                DtType
                 ("List.list", [DtTFree ("'d", ["HOL.type"])])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### theory "HOL-Datatype_Examples.Lambda_Term"
### 0.843s elapsed time, 5.160s cpu time, 0.000s GC time
Loading theory "HOL-Datatype_Examples.Misc_Datatype"
val it =
   ([],
    [(0, ("Compat.tttre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tttre.TTTre",
            [DtTFree ("'a", ["HOL.type"]),
             DtType
              ("List.list",
               [DtType
                 ("List.list", [DtType ("List.list", [DtRec 0])])])])]))],
    [(0, ("Compat.tttre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tttre.TTTre",
            [DtTFree ("'a", ["HOL.type"]),
             DtType
              ("List.list",
               [DtType
                 ("List.list", [DtType ("List.list", [DtRec 0])])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
Found termination order: "{}"
### Missing patterns in function definition:
### \<And>a v va. PREF a (CH v va) = undefined
Found termination order: "{}"
### Missing patterns in function definition:
### \<And>a v va. CONT a (CH v va) = undefined
Found termination order: "{}"
### Missing patterns in function definition:
### \<And>a v va. CH1 a (ACT v va) = undefined
Found termination order: "{}"
### Missing patterns in function definition:
### \<And>a v va. CH2 a (ACT v va) = undefined
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
### theory "HOL-Datatype_Examples.Process"
### 4.589s elapsed time, 27.096s cpu time, 4.720s GC time
Loading theory "HOL-Datatype_Examples.Prelim" (required by "HOL-Datatype_Examples.Gram_Lang" via "HOL-Datatype_Examples.DTree")
### theory "HOL-Datatype_Examples.Prelim"
### 0.098s elapsed time, 0.596s cpu time, 0.000s GC time
Loading theory "HOL-Datatype_Examples.DTree" (required by "HOL-Datatype_Examples.Gram_Lang")
### theory "HOL-Datatype_Examples.DTree"
### 0.445s elapsed time, 2.692s cpu time, 0.000s GC time
Loading theory "HOL-Datatype_Examples.Gram_Lang"
val it =
   ([(0, ("Compat.tttre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tttre.TTTre",
            [DtTFree ("'a", ["HOL.type"]), DtRec 3])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 0, DtRec 1])])),
     (2, ("List.list", [DtType ("List.list", [DtRec 0])],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 1, DtRec 2])])),
     (3, ("List.list",
          [DtType ("List.list", [DtType ("List.list", [DtRec 0])])],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 2, DtRec 3])]))],
    [(0, ("Compat.tttre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tttre.TTTre",
            [DtTFree ("'a", ["HOL.type"]), DtRec 3])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 0, DtRec 1])])),
     (2, ("List.list", [DtType ("List.list", [DtRec 0])],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 1, DtRec 2])])),
     (3, ("List.list",
          [DtType ("List.list", [DtType ("List.list", [DtRec 0])])],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 2, DtRec 3])]))],
    [(0, ("Compat.tttre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tttre.TTTre",
            [DtTFree ("'a", ["HOL.type"]),
             DtType
              ("List.list",
               [DtType
                 ("List.list", [DtType ("List.list", [DtRec 0])])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
Proofs for inductive predicate(s) "inFr"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "inFr2"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "inItr"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "subtr"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "subtr2"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "HOL-Datatype_Examples.Stream_Processor"
### 6.061s elapsed time, 34.296s cpu time, 9.860s GC time
Loading theory "HOL-Datatype_Examples.Parallel_Composition"
val it =
   ([],
    [(0, ("Compat.ftre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ftre.FEmp", []),
           ("Compat.ftre.FTre",
            [DtType
              ("fun",
               [DtTFree ("'a", ["HOL.type"]),
                DtType ("List.list", [DtRec 0])])])]))],
    [(0, ("Compat.ftre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ftre.FEmp", []),
           ("Compat.ftre.FTre",
            [DtType
              ("fun",
               [DtTFree ("'a", ["HOL.type"]),
                DtType ("List.list", [DtRec 0])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
Proofs for coinductive predicate(s) "wf"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the coinduction rule ...
  Proving the simplification rules ...
Found termination order: "{}"
Proofs for inductive predicate(s) "path"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "{}"
### theory "HOL-Datatype_Examples.Parallel_Composition"
### 0.546s elapsed time, 3.216s cpu time, 0.568s GC time
Loading theory "HOL-Datatype_Examples.TreeFsetI"
val it =
   ([(0, ("Compat.ftre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ftre.FEmp", []),
           ("Compat.ftre.FTre",
            [DtType ("fun", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.ftre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ftre.FEmp", []),
           ("Compat.ftre.FTre",
            [DtType ("fun", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.ftre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ftre.FEmp", []),
           ("Compat.ftre.FTre",
            [DtType
              ("fun",
               [DtTFree ("'a", ["HOL.type"]),
                DtType ("List.list", [DtRec 0])])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### theory "HOL-Datatype_Examples.Gram_Lang"
### 2.787s elapsed time, 14.844s cpu time, 7.060s GC time
### theory "HOL-Datatype_Examples.TreeFsetI"
### 0.545s elapsed time, 3.304s cpu time, 0.000s GC time
val it =
   ([],
    [(0, ("Compat.btre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.btre.BTre",
            [DtTFree ("'a", ["HOL.type"]), DtType ("List.list", [DtRec 0]),
             DtType ("List.list", [DtRec 0])])]))],
    [(0, ("Compat.btre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.btre.BTre",
            [DtTFree ("'a", ["HOL.type"]), DtType ("List.list", [DtRec 0]),
             DtType ("List.list", [DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.btre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.btre.BTre",
            [DtTFree ("'a", ["HOL.type"]), DtRec 2, DtRec 1])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 0, DtRec 1])])),
     (2, ("List.list", [DtRec 0],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 0, DtRec 2])]))],
    [(0, ("Compat.btre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.btre.BTre",
            [DtTFree ("'a", ["HOL.type"]), DtRec 2, DtRec 1])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []), ("List.list.Cons", [DtRec 0, DtRec 1])])),
     (2, ("List.list", [DtRec 0],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 0, DtRec 2])]))],
    [(0, ("Compat.btre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.btre.BTre",
            [DtTFree ("'a", ["HOL.type"]), DtType ("List.list", [DtRec 0]),
             DtType ("List.list", [DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'",
            [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'",
            [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'",
            [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.foo", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.bar", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'",
            [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([],
    [(0, ("Compat.tre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tre.Tre",
            [DtTFree ("'a", ["HOL.type"]),
             DtType ("List.list", [DtRec 0])])]))],
    [(0, ("Compat.tre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tre.Tre",
            [DtTFree ("'a", ["HOL.type"]),
             DtType ("List.list", [DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.tre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tre.Tre", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.tre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tre.Tre", [DtTFree ("'a", ["HOL.type"]), DtRec 1])])),
     (1, ("List.list", [DtRec 0],
          [("List.list.Nil", []),
           ("List.list.Cons", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.tre", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.tre.Tre",
            [DtTFree ("'a", ["HOL.type"]),
             DtType ("List.list", [DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### Defined types not fully mutually recursive
### Alternative specification:
###   datatype g = \<dots>
###   datatype f = \<dots>
  \<lbrakk>?P X;
   \<And>xa. (\<And>xaa xaaa. \<lbrakk>xaa \<in> set1_s xa; xaaa \<in> set xaa\<rbrakk> \<Longrightarrow> ?P xaaa) \<Longrightarrow>
        ?P (X' xa)\<rbrakk>
  \<Longrightarrow> ?P ?x
  rec_x ?f1.0 ?f2.0 X = ?f1.0
  rec_x ?f1.0 ?f2.0 (X' ?x2.0) =
  ?f2.0 (map_s (map (\<lambda>x. (x, rec_x ?f1.0 ?f2.0 x))) id ?x2.0)
  \<lbrakk>?P1.0 X; \<And>xa. ?P3.0 xa \<Longrightarrow> ?P1.0 (X' xa); ?P2.0 [];
   \<And>x1 x2. \<lbrakk>?P1.0 x1; ?P2.0 x2\<rbrakk> \<Longrightarrow> ?P2.0 (x1 # x2);
   \<And>xa. ?P2.0 xa \<Longrightarrow> ?P3.0 (L xa); \<And>xa. ?P3.0 (R xa)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?x
  compat_x.rec_n2m_x ?f11.0 ?f12.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0 X = ?f11.0
  compat_x.rec_n2m_x ?f11.0 ?f12.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0 (X' ?x12.0) =
  ?f12.0 ?x12.0
   (compat_x_list_list_s.rec_n2m_x_list_list_s ?f11.0 ?f12.0 ?f21.0 ?f22.0
     ?f31.0 ?f32.0 ?x12.0)
*** Failed to finish proof (line 66 of "~~/src/HOL/Datatype_Examples/Stream_Processor.thy"):
*** goal (1 subgoal):
***  1. \<And>f b sp. \<lbrakk>(out sp, Put b sp) \<notin> sub; f b = Get f\<rbrakk> \<Longrightarrow> False
val it =
   ([],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### Introduced fixed type variable(s): 'b in "Y__"
val it =
   ([],
    [(0, ("Compat.h", [],
          [("Compat.h.H", [DtType ("Compat.f", [DtRec 0])]),
           ("Compat.h.H'", [])]))],
    [(0, ("Compat.h", [],
          [("Compat.h.H", [DtType ("Compat.f", [DtRec 0])]),
           ("Compat.h.H'", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
  (\<And>x1a x2a.
      (\<And>x2aa x2aaa x2aaaa.
          \<lbrakk>x2aa \<in> set x2a; x2aaa \<in> set x2aa; x2aaaa \<in> set x2aaa\<rbrakk>
          \<Longrightarrow> ?P x2aaaa) \<Longrightarrow>
      ?P (TTTre x1a x2a)) \<Longrightarrow>
  ?P ?tttre
  rec_tttre ?f (TTTre ?x1.0 ?x2.0) =
  ?f ?x1.0 (map (map (map (\<lambda>tttre. (tttre, rec_tttre ?f tttre)))) ?x2.0)
  \<lbrakk>\<And>x1 x2. ?P4.0 x2 \<Longrightarrow> ?P1.0 (TTTre x1 x2); ?P2.0 [];
   \<And>x1 x2. \<lbrakk>?P1.0 x1; ?P2.0 x2\<rbrakk> \<Longrightarrow> ?P2.0 (x1 # x2); ?P3.0 [];
   \<And>x1 x2. \<lbrakk>?P2.0 x1; ?P3.0 x2\<rbrakk> \<Longrightarrow> ?P3.0 (x1 # x2); ?P4.0 [];
   \<And>x1 x2. \<lbrakk>?P3.0 x1; ?P4.0 x2\<rbrakk> \<Longrightarrow> ?P4.0 (x1 # x2)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?tttre
  compat_tttre.rec_n2m_tttre ?f1.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0 ?f41.0 ?f42.0
   (TTTre ?x11.0 ?x12.0) =
  ?f1.0 ?x11.0 ?x12.0
   (compat_tttre_list_list_list.rec_n2m_tttre_list_list_list ?f1.0 ?f21.0
     ?f22.0 ?f31.0 ?f32.0 ?f41.0 ?f42.0 ?x12.0)
val it =
   ([(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))],
    [(0, ("Compat.f", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.f.F", [DtTFree ("'a", ["HOL.type"])])])),
     (1, ("Compat.g", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.g.G", [DtTFree ("'a", ["HOL.type"])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([],
    [(0, ("Compat.h", [],
          [("Compat.h.H", [DtType ("Compat.f", [DtRec 0])]),
           ("Compat.h.H'", [])]))],
    [(0, ("Compat.h", [],
          [("Compat.h.H", [DtType ("Compat.f", [DtRec 0])]),
           ("Compat.h.H'", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### Metis: Unused theorems: "Lattices.semilattice_sup_class.sup_commute"
### The following type of nonemptiness witness of the raw type's BNF was lost:
###   'a list
### You can specify a liftable witness (e.g., a term of one of the above types
### that satisfies the typedef's invariant) using the annotation [wits: <term>].
val it =
   ([(0, ("Compat.h", [],
          [("Compat.h.H", [DtRec 1]), ("Compat.h.H'", [])])),
     (1, ("Compat.f", [DtRec 0], [("Compat.f.F", [DtRec 0])])),
     (2, ("Compat.g", [DtRec 0], [("Compat.g.G", [DtRec 0])]))],
    [(0, ("Compat.h", [],
          [("Compat.h.H", [DtRec 1]), ("Compat.h.H'", [])])),
     (1, ("Compat.f", [DtRec 0], [("Compat.f.F", [DtRec 0])])),
     (2, ("Compat.g", [DtRec 0], [("Compat.g.G", [DtRec 0])]))],
    [(0, ("Compat.h", [],
          [("Compat.h.H", [DtType ("Compat.f", [DtRec 0])]),
           ("Compat.h.H'", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
Proofs for inductive predicate(s) "ignore_Inl"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
val it =
   ([], [(0, ("Compat.myunit", [], [("Compat.myunit.MyUnity", [])]))],
    [(0, ("Compat.myunit", [], [("Compat.myunit.MyUnity", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.myunit", [], [("Compat.myunit.MyUnity", [])]))],
    [(0, ("Compat.myunit", [], [("Compat.myunit.MyUnity", [])]))],
    [(0, ("Compat.myunit", [], [("Compat.myunit.MyUnity", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### theory "HOL-Datatype_Examples.Lift_BNF"
### 17.991s elapsed time, 105.812s cpu time, 18.388s GC time
val it =
   ([],
    [(0, ("Compat.mylist", [],
          [("Compat.mylist.MyNil", []),
           ("Compat.mylist.MyCons", [DtType ("Nat.nat", []), DtRec 0])]))],
    [(0, ("Compat.mylist", [],
          [("Compat.mylist.MyNil", []),
           ("Compat.mylist.MyCons", [DtType ("Nat.nat", []), DtRec 0])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.mylist", [],
          [("Compat.mylist.MyNil", []),
           ("Compat.mylist.MyCons", [DtType ("Nat.nat", []), DtRec 0])]))],
    [(0, ("Compat.mylist", [],
          [("Compat.mylist.MyNil", []),
           ("Compat.mylist.MyCons", [DtType ("Nat.nat", []), DtRec 0])]))],
    [(0, ("Compat.mylist", [],
          [("Compat.mylist.MyNil", []),
           ("Compat.mylist.MyCons", [DtType ("Nat.nat", []), DtRec 0])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
### Defined types not fully mutually recursive
### Alternative specification:
###   datatype bar' = \<dots>
###   datatype foo' = \<dots>
val it =
   ([],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
val it =
   ([(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))],
    [(0, ("Compat.foo'", [],
          [("Compat.foo'.FooNil", []),
           ("Compat.foo'.FooCons", [DtRec 1, DtRec 0])])),
     (1, ("Compat.bar'", [], [("Compat.bar'.Bar", [])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
  \<lbrakk>?P FEmp;
   \<And>x. (\<And>xa xaa. \<lbrakk>xa \<in> range x; xaa \<in> set xa\<rbrakk> \<Longrightarrow> ?P xaa) \<Longrightarrow> ?P (FTre x)\<rbrakk>
  \<Longrightarrow> ?P ?ftre
  rec_ftre ?f1.0 ?f2.0 FEmp = ?f1.0
  rec_ftre ?f1.0 ?f2.0 (FTre ?x2.0) =
  ?f2.0 (map (\<lambda>ftre. (ftre, rec_ftre ?f1.0 ?f2.0 ftre)) \<circ> ?x2.0)
  \<lbrakk>?P1.0 FEmp; \<And>x. (\<And>xa. ?P2.0 (x xa)) \<Longrightarrow> ?P1.0 (FTre x); ?P2.0 [];
   \<And>x1 x2. \<lbrakk>?P1.0 x1; ?P2.0 x2\<rbrakk> \<Longrightarrow> ?P2.0 (x1 # x2)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?ftre
  compat_ftre.rec_split_ftre ?f1.0 ?f2.0 ?f3.0 ?f4.0 FEmp = ?f1.0
  compat_ftre.rec_split_ftre ?f1.0 ?f2.0 ?f3.0 ?f4.0 (FTre ?g) =
  ?f2.0 ?g
   (\<lambda>uu. compat_ftre_list.rec_split_ftre_list ?f1.0 ?f2.0 ?f3.0 ?f4.0
          (?g uu))
val it =
   ([],
    [(0, ("Compat.tree", [],
          [("Compat.tree.Tree", [DtType ("Compat.foo", [DtRec 0])])]))],
    [(0, ("Compat.tree", [],
          [("Compat.tree.Tree", [DtType ("Compat.foo", [DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
  (\<And>x1a x2a x3a.
      \<lbrakk>\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> ?P x2aa; \<And>x3aa. x3aa \<in> set x3a \<Longrightarrow> ?P x3aa\<rbrakk>
      \<Longrightarrow> ?P (BTre x1a x2a x3a)) \<Longrightarrow>
  ?P ?btre
  rec_btre ?f (BTre ?x1.0 ?x2.0 ?x3.0) =
  ?f ?x1.0 (map (\<lambda>btre. (btre, rec_btre ?f btre)) ?x2.0)
   (map (\<lambda>btre. (btre, rec_btre ?f btre)) ?x3.0)
  \<lbrakk>\<And>x1 x2 x3. \<lbrakk>?P3.0 x2; ?P2.0 x3\<rbrakk> \<Longrightarrow> ?P1.0 (BTre x1 x2 x3); ?P2.0 [];
   \<And>x1 x2. \<lbrakk>?P1.0 x1; ?P2.0 x2\<rbrakk> \<Longrightarrow> ?P2.0 (x1 # x2); ?P3.0 [];
   \<And>x1 x2. \<lbrakk>?P1.0 x1; ?P3.0 x2\<rbrakk> \<Longrightarrow> ?P3.0 (x1 # x2)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?btre
  compat_btre.rec_n2m_btre ?f1.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0
   (BTre ?x11.0 ?x12.0 ?x13.0) =
  ?f1.0 ?x11.0 ?x12.0 ?x13.0
   (compat_btre_lista.rec_n2m_btre_lista ?f1.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0
     ?x12.0)
   (compat_btre_list.rec_n2m_btre_list ?f1.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0
     ?x13.0)
  (\<And>x1a x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> ?P x2aa) \<Longrightarrow> ?P (Tre x1a x2a)) \<Longrightarrow>
  ?P ?tre
  rec_tre ?f (Tre ?x1.0 ?x2.0) =
  ?f ?x1.0 (map (\<lambda>tre. (tre, rec_tre ?f tre)) ?x2.0)
  \<lbrakk>\<And>x1 x2. ?P2.0 x2 \<Longrightarrow> ?P1.0 (Tre x1 x2); ?P2.0 [];
   \<And>x1 x2. \<lbrakk>?P1.0 x1; ?P2.0 x2\<rbrakk> \<Longrightarrow> ?P2.0 (x1 # x2)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?tre
  compat_tre.rec_n2m_tre ?f1.0 ?f21.0 ?f22.0 (Tre ?x11.0 ?x12.0) =
  ?f1.0 ?x11.0 ?x12.0
   (compat_tre_list.rec_n2m_tre_list ?f1.0 ?f21.0 ?f22.0 ?x12.0)
  \<lbrakk>\<And>x. (\<And>xa. xa \<in> set_f x \<Longrightarrow> ?P xa) \<Longrightarrow> ?P (H x); ?P H'\<rbrakk> \<Longrightarrow> ?P ?h
  rec_h ?f1.0 ?f2.0 (H ?x1.0) =
  ?f1.0 (map_f (\<lambda>h. (h, rec_h ?f1.0 ?f2.0 h)) ?x1.0)
  rec_h ?f1.0 ?f2.0 H' = ?f2.0
  \<lbrakk>\<And>x. ?P2.0 x \<Longrightarrow> ?P1.0 (H x); ?P1.0 H'; \<And>x. ?P1.0 x \<Longrightarrow> ?P2.0 (F x);
   \<And>x. ?P1.0 x \<Longrightarrow> ?P3.0 (G x)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?h
  compat_h.rec_n2m_h ?f11.0 ?f12.0 ?f2.0 ?f3.0 (H ?x11.0) =
  ?f11.0 ?x11.0 (compat_h_f.rec_n2m_h_f ?f11.0 ?f12.0 ?f2.0 ?f3.0 ?x11.0)
  compat_h.rec_n2m_h ?f11.0 ?f12.0 ?f2.0 ?f3.0 H' = ?f12.0
val it =
   ([(0, ("Compat.tree", [], [("Compat.tree.Tree", [DtRec 1])])),
     (1, ("Compat.foo", [DtRec 0],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtRec 0, DtRec 2])])),
     (2, ("Compat.bar", [DtRec 0],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.tree", [], [("Compat.tree.Tree", [DtRec 1])])),
     (1, ("Compat.foo", [DtRec 0],
          [("Compat.foo.Foo", []),
           ("Compat.foo.Foo'", [DtRec 0, DtRec 2])])),
     (2, ("Compat.bar", [DtRec 0],
          [("Compat.bar.Bar", []),
           ("Compat.bar.Bar'", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.tree", [],
          [("Compat.tree.Tree", [DtType ("Compat.foo", [DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
  (\<And>xa. (\<And>xaa. xaa \<in> set_foo xa \<Longrightarrow> ?P xaa) \<Longrightarrow> ?P (Tree xa)) \<Longrightarrow> ?P ?tree
  rec_tree ?f (Tree ?x) = ?f (map_foo (\<lambda>tree. (tree, rec_tree ?f tree)) ?x)
  \<lbrakk>\<And>x. ?P2.0 x \<Longrightarrow> ?P1.0 (Tree x); ?P2.0 Foo;
   \<And>x1a x2. \<lbrakk>?P1.0 x1a; ?P3.0 x2\<rbrakk> \<Longrightarrow> ?P2.0 (Foo' x1a x2); ?P3.0 bar.Bar;
   \<And>x1a x2. \<lbrakk>?P1.0 x1a; ?P2.0 x2\<rbrakk> \<Longrightarrow> ?P3.0 (Bar' x1a x2)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?tree
  compat_tree.rec_n2m_tree ?f1.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0 (Tree ?x1.0) =
  ?f1.0 ?x1.0
   (compat_tree_foo.rec_n2m_tree_foo ?f1.0 ?f21.0 ?f22.0 ?f31.0 ?f32.0
     ?x1.0)
val l_specs =
   [(("l", [("'a", ["HOL.type"])], NoSyn),
     [("N", [], NoSyn), ("C", ["'a", "'a ??.Compat.l"], NoSyn)])]:
   ((binding * (string * string list) list * mixfix) *
    (binding * typ list * mixfix) list
   )
   list
val it = (): unit
val it =
   ([(0, ("Compat.l", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.l.N", []),
           ("Compat.l.C", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.l", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.l.N", []),
           ("Compat.l.C", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))],
    [(0, ("Compat.l", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.l.N", []),
           ("Compat.l.C", [DtTFree ("'a", ["HOL.type"]), DtRec 0])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
  \<lbrakk>?y = N \<Longrightarrow> ?P; \<And>x21 x22. ?y = C x21 x22 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
  map_l ?f N = N
  map_l ?f (C ?x21.0 ?x22.0) = C (?f ?x21.0) (map_l ?f ?x22.0)
  \<lbrakk>?P N; \<And>x1 x2. ?P x2 \<Longrightarrow> ?P (C x1 x2)\<rbrakk> \<Longrightarrow> ?P ?l
  rec_l ?f1.0 ?f2.0 N = ?f1.0
  rec_l ?f1.0 ?f2.0 (C ?x21.0 ?x22.0) =
  ?f2.0 ?x21.0 ?x22.0 (rec_l ?f1.0 ?f2.0 ?x22.0)
  size_l ?x N = 0
  size_l ?x (C ?x21.0 ?x22.0) = ?x ?x21.0 + size_l ?x ?x22.0 + Suc 0
  size N = 0
  size (C ?x21.0 ?x22.0) = size ?x22.0 + Suc 0
val t_specs =
   [(("t", [("'b", ["HOL.type"])], NoSyn),
     [("T", ["'b", "'b ??.Compat.t l"], NoSyn)])]:
   ((binding * (string * string list) list * mixfix) *
    (binding * typ list * mixfix) list
   )
   list
val it = (): unit
val it =
   ([(0, ("Compat.t", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.t.T", [DtTFree ("'b", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.l", [DtRec 0],
          [("Compat.l.N", []), ("Compat.l.C", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.t", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.t.T", [DtTFree ("'b", ["HOL.type"]), DtRec 1])])),
     (1, ("Compat.l", [DtRec 0],
          [("Compat.l.N", []), ("Compat.l.C", [DtRec 0, DtRec 1])]))],
    [(0, ("Compat.t", [DtTFree ("'b", ["HOL.type"])],
          [("Compat.t.T",
            [DtTFree ("'b", ["HOL.type"]),
             DtType ("Compat.l", [DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
  (\<And>x1 x2. ?y = T x1 x2 \<Longrightarrow> ?P) \<Longrightarrow> ?P
  map_t ?f (T ?x1.0 ?x2.0) = T (?f ?x1.0) (map_l (map_t ?f) ?x2.0)
  (\<And>x1a x2a. (\<And>x2aa. x2aa \<in> set_l x2a \<Longrightarrow> ?P x2aa) \<Longrightarrow> ?P (T x1a x2a)) \<Longrightarrow>
  ?P ?t
  rec_t ?f (T ?x1.0 ?x2.0) = ?f ?x1.0 (map_l (\<lambda>t. (t, rec_t ?f t)) ?x2.0)
  size_t ?x (T ?x1.0 ?x2.0) = ?x ?x1.0 + size_l (size_t ?x) ?x2.0 + Suc 0
  size (T ?x1.0 ?x2.0) = size_l size ?x2.0 + Suc 0
  \<lbrakk>\<And>x1 x2. ?P2.0 x2 \<Longrightarrow> ?P1.0 (T x1 x2); ?P2.0 N;
   \<And>x1 x2. \<lbrakk>?P1.0 x1; ?P2.0 x2\<rbrakk> \<Longrightarrow> ?P2.0 (C x1 x2)\<rbrakk>
  \<Longrightarrow> ?P1.0 ?t
  compat_t.rec_n2m_t ?f1.0 ?f21.0 ?f22.0 (T ?x11.0 ?x12.0) =
  ?f1.0 ?x11.0 ?x12.0 (compat_t_l.rec_n2m_t_l ?f1.0 ?f21.0 ?f22.0 ?x12.0)
val ft_specs =
   [(("ft", [("'a", ["HOL.type"])], NoSyn),
     [("FT0", [], NoSyn), ("FT", ["'a \<Rightarrow> 'a ??.Compat.ft"], NoSyn)])]:
   ((binding * (string * string list) list * mixfix) *
    (binding * typ list * mixfix) list
   )
   list
val it = (): unit
val it =
   ([(0, ("Compat.ft", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ft.FT0", []),
           ("Compat.ft.FT",
            [DtType ("fun", [DtTFree ("'a", ["HOL.type"]), DtRec 0])])]))],
    [(0, ("Compat.ft", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ft.FT0", []),
           ("Compat.ft.FT",
            [DtType ("fun", [DtTFree ("'a", ["HOL.type"]), DtRec 0])])]))],
    [(0, ("Compat.ft", [DtTFree ("'a", ["HOL.type"])],
          [("Compat.ft.FT0", []),
           ("Compat.ft.FT",
            [DtType ("fun", [DtTFree ("'a", ["HOL.type"]), DtRec 0])])]))]):
   (int *
    (string * Old_Datatype_Data.dtyp list *
     (string * Old_Datatype_Data.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
   *
   (int *
    (string * Old_Datatype_Aux.dtyp list *
     (string * Old_Datatype_Aux.dtyp list) list)
   )
   list
  \<lbrakk>?P FT0; \<And>x. (\<And>xa. ?P (x xa)) \<Longrightarrow> ?P (FT x)\<rbrakk> \<Longrightarrow> ?P ?ft
  compat_ft.rec_split_ft ?f1.0 ?f2.0 FT0 = ?f1.0
  compat_ft.rec_split_ft ?f1.0 ?f2.0 (FT ?g) =
  ?f2.0 ?g (\<lambda>uu. compat_ft.rec_split_ft ?f1.0 ?f2.0 (?g uu))
### theory "HOL-Datatype_Examples.Compat"
### 23.272s elapsed time, 137.548s cpu time, 21.544s GC time
  \<lbrakk>?y = FT0 \<Longrightarrow> ?P; \<And>x2. ?y = FT x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
  \<lbrakk>?P FT0; \<And>x. (\<And>xa. xa \<in> range x \<Longrightarrow> ?P xa) \<Longrightarrow> ?P (FT x)\<rbrakk> \<Longrightarrow> ?P ?ft
  rec_ft ?f1.0 ?f2.0 FT0 = ?f1.0
  rec_ft ?f1.0 ?f2.0 (FT ?x2.0) =
  ?f2.0 ((\<lambda>ft. (ft, rec_ft ?f1.0 ?f2.0 ft)) \<circ> ?x2.0)
  size_ft ?x FT0 = 0
  size_ft ?x (FT ?x2.0) = 0
  size FT0 = 0
  size (FT ?x2.0) = 0
### Defined types not fully mutually corecursive
### Alternative specification:
###   codatatype in_here = \<dots>
###   codatatype some_killing = \<dots>
### Defined types not fully mutually recursive
### Alternative specification:
###   datatype in_here = \<dots>
###   datatype some_killing = \<dots>
### Defined types not fully mutually corecursive
### Alternative specification:
###   codatatype in_here' = \<dots>
###   codatatype some_killing' = \<dots>
### Defined types not fully mutually corecursive
### Alternative specification:
###   codatatype in_here'' = \<dots>
###   codatatype some_killing'' = \<dots>
### Defined types not fully mutually recursive
### Alternative specification:
###   datatype t3 = \<dots>
###   datatype t1 = \<dots> and t2 = \<dots>
### Defined types not fully mutually recursive
### Alternative specification:
###   datatype t3' = \<dots>
###   datatype t1' = \<dots> and t2' = \<dots>
### Defined types not fully mutually recursive
### Alternative specification:
###   datatype k4 = \<dots>
###   datatype k3 = \<dots>
###   datatype k2 = \<dots>
###   datatype k1 = \<dots>
### Defined types not fully mutually corecursive
### Alternative specification:
###   codatatype wit3_F2 = \<dots>
###   codatatype wit3_F1 = \<dots>
###   codatatype wit3_F3 = \<dots>
### Defined types not fully mutually recursive
### Alternative specification:
###   datatype tt4 = \<dots>
###   datatype tt2 = \<dots>
###   datatype tt1 = \<dots> and tt3 = \<dots>
### Defined types not fully mutually corecursive
### Alternative specification:
###   codatatype ind_wit = \<dots>
###   codatatype coind_wit2 = \<dots>
###   codatatype coind_wit1 = \<dots>
### theory "HOL-Datatype_Examples.Misc_Codatatype"
### 67.393s elapsed time, 354.464s cpu time, 61.452s GC time
Loading theory "HOL-Datatype_Examples.Misc_Primcorec"
### theory "HOL-Datatype_Examples.Misc_Primcorec"
### 2.149s elapsed time, 9.604s cpu time, 0.844s GC time
### theory "HOL-Datatype_Examples.Misc_Datatype"
### 78.634s elapsed time, 374.924s cpu time, 63.324s GC time
Loading theory "HOL-Datatype_Examples.Misc_Primrec"
### theory "HOL-Datatype_Examples.Misc_Primrec"
### 1.884s elapsed time, 3.752s cpu time, 0.548s GC time
*** Failed to finish proof (line 66 of "~~/src/HOL/Datatype_Examples/Stream_Processor.thy"):
*** goal (1 subgoal):
***  1. ⋀f b sp. ⟦(out sp, Put b sp) ∉ sub; f b = Get f⟧ ⟹ False
*** At command "by" (line 66 of "~~/src/HOL/Datatype_Examples/Stream_Processor.thy")