(*  Title:  build the Isac-Kernel: MathEngine & Knowledge

    Author: Walther Neuper, TU Graz, 100808

   (c) due to copyright terms

For creating a heap image of isac see ~~/ROOT.

For debugging see text at begin below, e.g. theory dependencies:

  ~$ evince file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf &

ATTENTION: no errors in this theory do not mean that there are no errors in Isac ..

.. open theories collecting files from folders: BaseDefinitions.thy, ProgLang.thy etc.

Errors are rigorously detected by isabelle build.

*)

theory Build_Isac

imports

(*  theory Know_Store imports Complex_Main

    $ISABELLE_ISAC/BaseDefinitions

      ML_file libraryC.sml

      ML_file theoryC.sml

      ML_file unparseC.sml

      ML_file "rule-def.sml"

      ML_file "thmC-def.sml"

      ML_file "eval-def.sml"

      ML_file "rewrite-order.sml"

      ML_file rule.sml

      ML_file "error-pattern-def.sml"

      ML_file "rule-set.sml"

      ML_file "store.sml"

      ML_file "check-unique.sml"

      ML_file "specification.sml"

      ML_file "model-pattern.sml"

      ML_file "problem-def.sml"

      ML_file "method-def.sml"

      ML_file "cas-def.sml"

      ML_file "thy-write.sml"

  theory BaseDefinitions imports Know_Store

  $ISABELLE_ISAC/BaseDefinitions

    ML_file termC.sml

    ML_file substitution.sml

    ML_file contextC.sml

    ML_file environment.sml

( ** )    "BaseDefinitions/BaseDefinitions"( **)

(*

      theory Calc_Binop imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

        at $ISABELLE_ISAC/ProgLang

        ML_file evaluate.sml

      theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

      theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

    theory Prog_Expr imports Calc_Binop ListC Program

     theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

      theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

    theory Auto_Prog imports Prog_Tac Tactical

  theory ProgLang imports Prog_Expr Auto_Prog

    at $ISABELLE_ISAC/ProgLang

( ** )    "ProgLang/ProgLang"( **)

(*

  theory MathEngBasic imports

    "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"

    at $ISABELLE_ISAC/MathEngBasic

    ML_file thmC.sml

    ML_file problem.sml

    ML_file method.sml

    ML_file "cas-command.sml"

    ML_file rewrite.sml

    ML_file "model-def.sml"

    ML_file "istate-def.sml"

    ML_file "calc-tree-elem.sml"

    ML_file "pre-conds-def.sml"

    ML_file tactic.sml

    ML_file applicable.sml

    ML_file position.sml

    ML_file "ctree-basic.sml"

    ML_file "ctree-access.sml"

    ML_file "ctree-navi.sml"

    ML_file ctree.sml

    ML_file "state-steps.sml"

    ML_file calculation.sml

( ** )    "MathEngBasic/MathEngBasic"( **)

(*

    theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

    $ISABELLE_ISAC/Specify

  theory Specify imports "$ISABELLE_ISAC/ProgLang/ProgLang" Input_Descript

  $ISABELLE_ISAC/Specify

    ML_file formalise.sml

    ML_file "o-model.sml"

    ML_file "i-model.sml"

    ML_file "p-model.sml"

    ML_file model.sml

    ML_file "pre-conditions.sml"

    ML_file refine.sml

    ML_file "mstools.sml" (*..TODO review*)

    ML_file ptyps.sml     (*..TODO review*)

    ML_file "test-out.sml"

    ML_file "specify-step.sml"

    ML_file calchead.sml  (*..TODO review*)

    ML_file "input-calchead.sml"

    ML_file "step-specify.sml"

    ML_file specify.sml

( ** )    "Specify/Specify"( **)

(*

  theory Interpret imports "$ISABELLE_ISAC/Specify/Specify"

  $ISABELLE_ISAC/Interpret

    ML_file istate.sml

    ML_file "sub-problem.sml"

    ML_file "thy-read.sml"

    ML_file "solve-step.sml"

    ML_file "error-pattern.sml"

    ML_file derive.sml

    ML_file "li-tool.sml"

    ML_file "lucas-interpreter.sml"

    ML_file "step-solve.sml"

( ** )    "Interpret/Interpret"( **)

(*

  theory MathEngine imports Interpret.Interpret

  $ISABELLE_ISAC/MathEngine

    ML_file "fetch-tactics.sml"

    ML_file solve.sml

    ML_file step.sml

    ML_file "detail-step.sml"

    ML_file "mathengine-stateless.sml"

    ML_file messages.sml

    ML_file states.sml

( ** )    "MathEngine/MathEngine"( **)

(*

  theory Test_Code imports "$ISABELLE_ISAC/MathEngine/MathEngine"

  $ISABELLE_ISAC/Test_Code

    ML_file "test-code.sml"

( ** )    "Test_Code/Test_Code"( **)

(*

  theory BridgeLibisabelle imports "$ISABELLE_ISAC/MathEngine/MathEngine"

  $ISABELLE_ISAC/BridgeLibisabelle

    ML_file "thy-present.sml"

    ML_file mathml.sml   

    ML_file datatypes.sml

    ML_file "pbl-met-hierarchy.sml"

    ML_file "thy-hierarchy.sml" 

    ML_file "interface-xml.sml"

    ML_file interface.sml

( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)

(*

    theory Calculation imports Calculation (*preliminary for starting Isabelle/Isac*)

    $ISABELLE_ISAC/BridgeJEdit

      ML_file parseC.sml

      ML_file preliminary.sml

  theory BridgeJEdit imports Calculation (*preliminary for starting Isabelle/Isac*)

  $ISABELLE_ISAC/BridgeJEdit

( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)

(*

    theory Isac imports  "$ISABELLE_ISAC/MathEngine/MathEngine"

      ML_file parseC.sml

  theory BridgeJEdit imports Isac    

( **)    "BridgeJEdit/BridgeJEdit"  (*DEactivate after devel.of BridgeJEdit*)

          "Knowledge/Build_Thydata" (*imports Isac.thy etc*)

(*//-----------------------------------------------------------------------------------------\\*)

(*\\-----------------------------------------------------------------------------------------//*)

begin

text \<open>

  show theory dependencies using the graph browser, 

  open "browser_info/HOL/Isac/session.graph"

  and proceed from the ancestors towards the siblings.

\<close>

section \<open>check presence of definitions from directories\<close>

(*declare [[ML_print_depth = 999]]*)

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open> (* \<rightarrow> termC.sml*)

\<close> ML \<open> (* \<rightarrow> model-pattern.sml*)

\<close> ML \<open>

Model_Pattern.adapt_term_to_type: Proof.context -> term -> term ;

Model_Pattern.adapt_to_type: Proof.context -> Model_Pattern.single -> Model_Pattern.single

\<close> ML \<open>

\<close> ML \<open> (* \<rightarrow> problem.sml*)

\<close> ML \<open>

val id = ["univariate", "equation", "test"]

\<close> ML \<open>

Problem.from_store_PIDE: Proof.context -> Problem.id -> Problem.T

\<close> ML \<open>

\<close> ML \<open> (* \<rightarrow> refine.sml*)

\<close> ML \<open>

\<close> text \<open>  local

refin_PIDE

\<close> ML \<open>

\<close> text \<open>  \<isac_test>

refine_PIDE

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>(*---------------------------- why "real" in pbl? ----------------------------*)

Test_Tool.show_ptyps ();

\<close> ML \<open>

KEStore_Elems.get_pbls @{theory Poly}; (*! real ! due to Simplify :: "real => real" etc*)

\<close> ML \<open>

Problem.from_store_PIDE @{context} ["polynomial", "simplification"]

\<close> ML \<open>

val input = (["polynomial", "simplification"], 

  [("#Given", ["Simplify t_t"]), ("#Find", ["normalform n_n"])], 

  Rule_Set.empty, NONE (*cas*), 

  [["simplification","for_polynomials"]]) : Problem.input

\<close> ML \<open>

Problem.prep_input_PIDE @{theory Poly} "guh" ["math-author-1"] ["polynomial", "simplification"]

  input; (*! real !*)

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

"~~~~~ fun prep_input_PIDE , args:"; val (thy, guh, maa, init, (pblID, dsc_dats, ev, ca, metIDs)) =

  (@{theory Poly}, "guh", ["math-author-1"], ["polynomial", "simplification"], input);

\<close> ML \<open>

      fun eq f (f', _) = f = f';

\<close> ML \<open>

      val gi = filter (eq "#Given") dsc_dats;

\<close> ML \<open>

        val (_, gi') :: [] = (*case*) gi (*of*);

\<close> ML \<open>

      map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) gi'

\<close> ML \<open>

\<close> ML \<open>

(*+*)Syntax.read_term_global thy "Simplify t_t" (*Simplify :: "real => real"*)

\<close> ML \<open>

(*+*)TermC.parse_patt thy "matches (?a = 0) e_e"

(* = Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ 

Var (("a", 0), "real") $ Const ("Groups.zero_class.zero", "real")) $ Free ("e_e", "bool")*)

\<close> ML \<open>

(*+*)TermC.parse_patt_PIDE thy "matches (?a = 0) e_e"

(*t = Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("HOL.eq", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $ 

  Var (("a", 0), "?'a1") $ Const ("Groups.zero_class.zero", "?'a1")) $ Free ("e_e", "bool")*)

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

KEStore_Elems.get_pbls @{theory Isac_Knowledge}; (*! real ! due to Simplify :: "real => real" etc*)

(*val it =

   [Node ("empty_probl_id", [{cas = NONE, guh = "pbl_empty", init = ["empty_probl_id"], mathauthors = [], met = [], ppc = [], prls = Empty, thy = {Pure}, where_ = []}], []),

    Node

     ("simplification",

      [{cas = SOME (Const ("Simplify.Simplify", "real \<Rightarrow> real") $ Free ("t_t", "real")), guh = "pbl_simp", init = ["empty_probl_id"], mathauthors = [], met = [], ppc =

        [("#Given", (Const ("Simplify.Term", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Find", (Const ("Simplify.normalform", "real \<Rightarrow> una"), Free ("n_n", "real")))], prls =

        Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}, thy =

        {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

          HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

          HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

          HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

          HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

          HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List, HOL.Groups_List,

          HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random,

          HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction,

          HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces,

          HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store,

          Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript,

          Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify:30},

        where_ = []}],

      [Node

        ("polynomial",

         [{cas = SOME (Const ("Simplify.Simplify", "real \<Rightarrow> real") $ Free ("t_t", "real")), guh = "pbl_simp_poly", init = ["empty_probl_id"], mathauthors = [], met = [["simplification", "for_polynomials"]],

           ppc = [("#Given", (Const ("Simplify.Term", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Find", (Const ("Simplify.normalform", "real \<Rightarrow> una"), Free ("n_n", "real")))], prls =

           Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], rew_ord = ("dummy_ord", fn), rules = [Eval ("Poly.is_polyexp", fn)], scr = Empty_Prog, srls = Empty}, thy =

           {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

             HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

             HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

             HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

             HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

             HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

             HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

             HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

             HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

             HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

             Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

             Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

             Isac.Poly:734},

           where_ = [Const ("Poly.is_polyexp", "real \<Rightarrow> bool") $ Free ("t_t", "real")]}],

         []),

       Node

        ("rational",

         [{cas = SOME (Const ("Simplify.Simplify", "real \<Rightarrow> real") $ Free ("t_t", "real")), guh = "pbl_simp_rat", init = ["empty_probl_id"], mathauthors = [], met = [["simplification", "of_rationals"]], ppc =

           [("#Given", (Const ("Simplify.Term", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Find", (Const ("Simplify.normalform", "real \<Rightarrow> una"), Free ("n_n", "real")))], prls =

           Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}, thy =

           {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

             HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

             HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

             HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

             HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

             HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

             HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

             HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

             HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

             HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

             Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

             Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

             Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational:315},

           where_ = [Const ("Rational.is_ratpolyexp", "real \<Rightarrow> bool") $ Free ("t_t", "real")]}],

         [Node

           ("partial_fraction",

            [{cas = NONE, guh = "pbl_simp_rat_partfrac", init = ["empty_probl_id"], mathauthors = [], met = [["simplification", "of_rationals", "to_partial_fraction"]], ppc =

              [("#Given", (Const ("Input_Descript.functionTerm", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

               ("#Find", (Const ("Partial_Fractions.decomposedFunction", "real \<Rightarrow> una"), Free ("p_p'''", "real")))],

              prls = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}, thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.Root, Isac.Equation, Isac.GCD_Poly_ML, Isac.Rational, Isac.LinEq, Isac.RootEq, Isac.RatEq, Isac.RootRat, Isac.RootRatEq, Isac.Partial_Fractions:136},

              where_ = []}],

            [])])]),

    Node

     ("vereinfachen",

      [{cas = SOME (Const ("Simplify.Vereinfache", "real \<Rightarrow> real") $ Free ("t_t", "real")), guh = "pbl_vereinfache", init = ["empty_probl_id"], mathauthors = [], met = [], ppc =

        [("#Given", (Const ("Simplify.Term", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Find", (Const ("Simplify.normalform", "real \<Rightarrow> una"), Free ("n_n", "real")))], prls =

        Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}, thy =

        {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

          HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

          HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

          HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

          HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

          HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List, HOL.Groups_List,

          HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random,

          HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction,

          HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces,

          HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store,

          Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript,

          Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify:40},

        where_ = []}],

      [Node

        ("polynom",

         [{cas = NONE, guh = "pbl_vereinf_poly", init = ["empty_probl_id"], mathauthors = [], met = [], ppc = [], prls = Empty, thy =

           {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

             HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

             HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

             HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

             HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

             HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

             HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

             HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

             HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

             HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

             Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

             Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

             Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational, Isac.PolyMinus:199},

           where_ = []}],

         [Node

           ("plus_minus",

            [{cas = SOME (Const ("Simplify.Vereinfache", "real \<Rightarrow> real") $ Free ("t_t", "real")), guh = "pbl_vereinf_poly_minus", init = ["empty_probl_id"], mathauthors = [], met =

              [["simplification", "for_polynomials", "with_minus"]], ppc =

              [("#Given", (Const ("Simplify.Term", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Find", (Const ("Simplify.normalform", "real \<Rightarrow> una"), Free ("n_n", "real")))], prls =

              Repeat

               {calc = [], erls = Empty, errpatts = [], id = "prls_pbl_vereinf_poly", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                [Eval ("Poly.is_polyexp", fn), Eval ("Prog_Expr.matchsub", fn), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a"), Thm ("not_true", "(\<not> True) = False"),

                 Thm ("not_false", "(\<not> False) = True")],

                scr = Empty_Prog, srls = Empty},

              thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational, Isac.PolyMinus:209},

              where_ =

              [Const ("Poly.is_polyexp", "real \<Rightarrow> bool") $ Free ("t_t", "real"),

               Const ("HOL.Not", "bool \<Rightarrow> bool") $

                 (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                   (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                     (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                       (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                     Free ("t_t", "?'a1")) $

                   (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                     (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                       (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                         (Const ("Groups.minus_class.minus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                       Free ("t_t", "?'a1")) $

                     (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                       (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                         (Const ("Groups.minus_class.minus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                           (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                         Free ("t_t", "?'a1")) $

                       (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                         (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                           (Const ("Groups.minus_class.minus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                         Free ("t_t", "?'a1"))))),

               Const ("HOL.Not", "bool \<Rightarrow> bool") $

                 (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                   (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                     (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                       (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                     Free ("t_t", "?'a1")) $

                   (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                     (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                       (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                         (Const ("Groups.minus_class.minus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                       Free ("t_t", "?'a1")) $

                     (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                       (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                         (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1")) $

                           Var (("a", 0), "?'a1")) $

                         Free ("t_t", "?'a1")) $

                       (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                         (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ (Const ("Groups.minus_class.minus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1")) $

                           Var (("a", 0), "?'a1")) $

                         Free ("t_t", "?'a1")))))]}],

            []),

          Node

           ("klammer",

            [{cas = SOME (Const ("Simplify.Vereinfache", "real \<Rightarrow> real") $ Free ("t_t", "real")), guh = "pbl_vereinf_poly_klammer", init = ["empty_probl_id"], mathauthors = [], met =

              [["simplification", "for_polynomials", "with_parentheses"]], ppc =

              [("#Given", (Const ("Simplify.Term", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Find", (Const ("Simplify.normalform", "real \<Rightarrow> una"), Free ("n_n", "real")))], prls =

              Repeat

               {calc = [], erls = Empty, errpatts = [], id = "prls_pbl_vereinf_poly_klammer", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                [Eval ("Poly.is_polyexp", fn), Eval ("Prog_Expr.matchsub", fn), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a"), Thm ("not_true", "(\<not> True) = False"),

                 Thm ("not_false", "(\<not> False) = True")],

                scr = Empty_Prog, srls = Empty},

              thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational, Isac.PolyMinus:219},

              where_ =

              [Const ("Poly.is_polyexp", "real \<Rightarrow> bool") $ Free ("t_t", "real"),

               Const ("HOL.Not", "bool \<Rightarrow> bool") $

                 (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                   (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                     (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                       (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                     Free ("t_t", "?'a1")) $

                   (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                     (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                       (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("a", 0), "?'a1") $

                         (Const ("Groups.minus_class.minus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1"))) $

                       Free ("t_t", "?'a1")) $

                     (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                       (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                         (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ (Const ("Groups.plus_class.plus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1")) $

                           Var (("a", 0), "?'a1")) $

                         Free ("t_t", "?'a1")) $

                       (Const ("Prog_Expr.matchsub", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $

                         (Const ("Groups.times_class.times", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ (Const ("Groups.minus_class.minus", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> ?'a1") $ Var (("b", 0), "?'a1") $ Var (("c", 0), "?'a1")) $

                           Var (("a", 0), "?'a1")) $

                         Free ("t_t", "?'a1")))))]}],

            []),

          Node

           ("binom_klammer",

            [{cas = SOME (Const ("Simplify.Vereinfache", "real \<Rightarrow> real") $ Free ("t_t", "real")), guh = "pbl_vereinf_poly_klammer_mal", init = ["empty_probl_id"], mathauthors = [], met =

              [["simplification", "for_polynomials", "with_parentheses_mult"]], ppc =

              [("#Given", (Const ("Simplify.Term", "real \<Rightarrow> una"), Free ("t_t", "real"))), ("#Find", (Const ("Simplify.normalform", "real \<Rightarrow> una"), Free ("n_n", "real")))], prls =

              Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], rew_ord = ("dummy_ord", fn), rules = [Eval ("Poly.is_polyexp", fn)], scr = Empty_Prog, srls = Empty}, thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational, Isac.PolyMinus:229},

              where_ = [Const ("Poly.is_polyexp", "real \<Rightarrow> bool") $ Free ("t_t", "real")]}],

            [])])]),

    Node

     ("probe",

      [{cas = NONE, guh = "pbl_probe", init = ["empty_probl_id"], mathauthors = [], met = [], ppc = [], prls = Empty, thy =

        {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

          HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

          HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

          HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

          HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

          HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List, HOL.Groups_List,

          HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random,

          HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction,

          HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces,

          HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store,

          Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript,

          Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational,

          Isac.PolyMinus:239},

        where_ = []}],

      [Node

        ("polynom",

         [{cas = SOME (Const ("PolyMinus.Probe", "bool \<Rightarrow> bool list \<Rightarrow> bool") $ Free ("e_e", "bool") $ Free ("w_w", "bool list")), guh = "pbl_probe_poly", init = ["empty_probl_id"], mathauthors = [], met =

           [["probe", "fuer_polynom"]], ppc =

           [("#Given", (Const ("PolyMinus.Pruefe", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("PolyMinus.mitWert", "bool list \<Rightarrow> tobooll"), Free ("w_w", "bool list"))),

            ("#Find", (Const ("PolyMinus.Geprueft", "bool \<Rightarrow> una"), Free ("p_p", "bool")))],

           prls = Repeat {calc = [], erls = Empty, errpatts = [], id = "prls_pbl_probe_poly", preconds = [], rew_ord = ("dummy_ord", fn), rules = [Eval ("Poly.is_polyexp", fn)], scr = Empty_Prog, srls = Empty},

           thy =

           {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

             HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

             HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

             HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

             HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

             HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

             HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

             HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

             HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

             HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

             Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

             Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

             Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational, Isac.PolyMinus:249},

           where_ = [Const ("Poly.is_polyexp", "real \<Rightarrow> bool") $ Free ("e_e", "real")]}],

         []),

       Node

        ("bruch",

         [{cas = SOME (Const ("PolyMinus.Probe", "bool \<Rightarrow> bool list \<Rightarrow> bool") $ Free ("e_e", "bool") $ Free ("w_w", "bool list")), guh = "pbl_probe_bruch", init = ["empty_probl_id"], mathauthors = [], met =

           [["probe", "fuer_bruch"]], ppc =

           [("#Given", (Const ("PolyMinus.Pruefe", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("PolyMinus.mitWert", "bool list \<Rightarrow> tobooll"), Free ("w_w", "bool list"))),

            ("#Find", (Const ("PolyMinus.Geprueft", "bool \<Rightarrow> una"), Free ("p_p", "bool")))],

           prls =

           Repeat {calc = [], erls = Empty, errpatts = [], id = "prls_pbl_probe_bruch", preconds = [], rew_ord = ("dummy_ord", fn), rules = [Eval ("Rational.is_ratpolyexp", fn)], scr = Empty_Prog, srls = Empty},

           thy =

           {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

             HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

             HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

             HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

             HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

             HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

             HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

             HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

             HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

             HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

             Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

             Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

             Isac.Poly, Isac.GCD_Poly_ML, Isac.Rational, Isac.PolyMinus:259},

           where_ = [Const ("Rational.is_ratpolyexp", "real \<Rightarrow> bool") $ Free ("e_e", "real")]}],

         [])]),

    Node

     ("equation",

      [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh = "pbl_equ", init =

        ["empty_probl_id"], mathauthors = [], met = [], ppc =

        [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

         ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

        prls = Repeat {calc = [], erls = Empty, errpatts = [], id = "equation_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules = [Eval ("Prog_Expr.matches", fn)], scr = Empty_Prog, srls = Empty}, thy =

        {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

          HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

          HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

          HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

          HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

          HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List, HOL.Groups_List,

          HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random,

          HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction,

          HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces,

          HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store,

          Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript,

          Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Equation:50},

        where_ = [Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("HOL.eq", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $ Var (("a", 0), "?'a1") $ Var (("b", 0), "?'a1")) $ Free ("e_e", "bool")]}],

      [Node

        ("univariate",

         [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh = "pbl_equ_univ",

           init = ["empty_probl_id"], mathauthors = [], met = [], ppc =

           [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

            ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

           prls =

           Repeat {calc = [], erls = Empty, errpatts = [], id = "univariate_equation_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules = [Eval ("Prog_Expr.matches", fn)], scr = Empty_Prog, srls = Empty},

           thy =

           {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

             HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

             HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

             HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

             HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

             HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

             HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

             HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

             HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

             HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

             Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

             Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Equation:60},

           where_ = [Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("HOL.eq", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $ Var (("a", 0), "?'a1") $ Var (("b", 0), "?'a1")) $ Free ("e_e", "bool")]}],

         [Node

           ("rootX",

            [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

              "pbl_equ_univ_root", init = ["empty_probl_id"], mathauthors = [], met = [], ppc =

              [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

               ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

              prls =

              Repeat

               {calc = [], erls = Empty, errpatts = [], id = "RootEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("RootEq.is_sqrtTerm_in", fn), Eval ("RootEq.is_rootTerm_in", fn),

                 Eval ("RootEq.is_normSqrtTerm_in", fn), Eval ("HOL.eq", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"),

                 Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                scr = Empty_Prog, srls = Empty},

              thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.Root, Isac.Equation, Isac.RootEq:252},

              where_ =

              [Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("RootEq.is_rootTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                 (Const ("RootEq.is_rootTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"))]}],

            [Node

              ("sq",

               [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

                 "pbl_equ_univ_root_sq", init = ["empty_probl_id"], mathauthors = [], met = [["RootEq", "solve_sq_root_equation"]], ppc =

                 [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

                  ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

                 prls =

                 Repeat

                  {calc = [], erls = Empty, errpatts = [], id = "RootEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                   [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("RootEq.is_sqrtTerm_in", fn), Eval ("RootEq.is_rootTerm_in", fn),

                    Eval ("RootEq.is_normSqrtTerm_in", fn), Eval ("HOL.eq", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"),

                    Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                   scr = Empty_Prog, srls = Empty},

                 thy =

                 {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,

                   HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                   HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                   HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                   HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                   HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                   HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                   HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                   HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull,

                   HOL.Modules, HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex,

                   HOL.MacLaurin, Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr,

                   Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle,

                   Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.Root, Isac.Equation, Isac.RootEq:262},

                 where_ =

                 [Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                    (Const ("HOL.conj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                      (Const ("RootEq.is_sqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                      (Const ("RootEq.is_normSqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"))) $

                    (Const ("HOL.conj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                      (Const ("RootEq.is_sqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                      (Const ("RootEq.is_normSqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")))]}],

               [Node

                 ("rat",

                  [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

                    "pbl_equ_univ_root_sq_rat", init = ["empty_probl_id"], mathauthors = [], met = [["RootRatEq", "elim_rootrat_equation"]], ppc =

                    [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

                     ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

                    prls =

                    Repeat

                     {calc = [], erls = Empty, errpatts = [], id = "RootRatEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                      [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("RootEq.is_rootTerm_in", fn),

                       Eval ("RootRatEq.is_rootRatAddTerm_in", fn), Eval ("HOL.eq", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"),

                       Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                      scr = Empty_Prog, srls = Empty},

                    thy =

                    {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,

                      HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                      HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base,

                      HOL.BNF_Def, HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power,

                      HOL.Groups_Big, HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big,

                      HOL.Euclidean_Division, HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer,

                      HOL.Lifting_Set, HOL.List, HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence,

                      HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick,

                      HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main,

                      HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series,

                      HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac,

                      Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine,

                      Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.Root, Isac.Equation, Isac.GCD_Poly_ML, Isac.Rational, Isac.LinEq, Isac.RootEq, Isac.RatEq,

                      Isac.RootRat, Isac.RootRatEq:108},

                    where_ =

                    [Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                       (Const ("RootRatEq.is_rootRatAddTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                       (Const ("RootRatEq.is_rootRatAddTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"))]}],

                  [])]),

             Node

              ("normalise",

               [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

                 "pbl_equ_univ_root_norm", init = ["empty_probl_id"], mathauthors = [], met = [["RootEq", "norm_sq_root_equation"]], ppc =

                 [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

                  ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

                 prls =

                 Repeat

                  {calc = [], erls = Empty, errpatts = [], id = "RootEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                   [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("RootEq.is_sqrtTerm_in", fn), Eval ("RootEq.is_rootTerm_in", fn),

                    Eval ("RootEq.is_normSqrtTerm_in", fn), Eval ("HOL.eq", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"),

                    Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                   scr = Empty_Prog, srls = Empty},

                 thy =

                 {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,

                   HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                   HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                   HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                   HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                   HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                   HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                   HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                   HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull,

                   HOL.Modules, HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex,

                   HOL.MacLaurin, Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr,

                   Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle,

                   Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.Root, Isac.Equation, Isac.RootEq:272},

                 where_ =

                 [Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                    (Const ("HOL.conj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                      (Const ("RootEq.is_sqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                      (Const ("HOL.Not", "bool \<Rightarrow> bool") $

                        (Const ("RootEq.is_normSqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")))) $

                    (Const ("HOL.conj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                      (Const ("RootEq.is_sqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                      (Const ("HOL.Not", "bool \<Rightarrow> bool") $

                        (Const ("RootEq.is_normSqrtTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"))))]}],

               [])]),

          Node

           ("LINEAR",

            [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

              "pbl_equ_univ_lin", init = ["empty_probl_id"], mathauthors = [], met = [["LinEq", "solve_lineq_equation"]], ppc =

              [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

               ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

              prls =

              Repeat

               {calc = [], erls = Empty, errpatts = [], id = "LinEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                [Eval ("HOL.eq", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("Poly.has_degree_in", fn), Eval ("Poly.is_polyrat_in", fn),

                 Eval ("Prog_Expr.occurs_in", fn), Eval ("Prog_Expr.ident", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"),

                 Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                scr = Empty_Prog, srls = Empty},

              thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.Equation, Isac.LinEq:107},

              where_ =

              [Const ("HOL.False", "bool"),

               Const ("HOL.Not", "bool \<Rightarrow> bool") $ (Const ("Poly.is_polyrat_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")),

               Const ("HOL.Not", "bool \<Rightarrow> bool") $ (Const ("Poly.is_polyrat_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")),

               Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Poly.has_degree_in", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                 Const ("Groups.one_class.one", "real"),

               Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Poly.has_degree_in", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                 Const ("Groups.one_class.one", "real")]}],

            []),

          Node

           ("rational",

            [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

              "pbl_equ_univ_rat", init = ["empty_probl_id"], mathauthors = [], met = [["RatEq", "solve_rat_equation"]], ppc =

              [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

               ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

              prls =

              Repeat

               {calc = [], erls = Empty, errpatts = [], id = "RatEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("RatEq.is_ratequation_in", fn), Eval ("HOL.eq", fn),

                 Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"),

                 Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                scr = Empty_Prog, srls = Empty},

              thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.GCD_Poly_ML, Isac.Equation, Isac.Rational, Isac.LinEq, Isac.RatEq:163},

              where_ = [Const ("RatEq.is_ratequation_in", "bool \<Rightarrow> real \<Rightarrow> bool") $ Free ("e_e", "bool") $ Free ("v_v", "real")]}],

            []),

          Node

           ("polynomial",

            [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

              "pbl_equ_univ_poly", init = ["empty_probl_id"], mathauthors = [], met = [], ppc =

              [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

               ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

              prls =

              Repeat

               {calc = [], erls = Empty, errpatts = [], id = "PolyEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("Poly.is_expanded_in", fn), Eval ("Poly.is_poly_in", fn),

                 Eval ("Poly.has_degree_in", fn), Eval ("Poly.is_polyrat_in", fn), Eval ("HOL.eq", fn), Eval ("RootEq.is_rootTerm_in", fn), Eval ("RatEq.is_ratequation_in", fn),

                 Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"),

                 Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                scr = Empty_Prog, srls = Empty},

              thy =

              {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

                HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules,

                HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin,

                Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog,

                Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify,

                Isac.Poly, Isac.Root, Isac.Equation, Isac.GCD_Poly_ML, Isac.Rational, Isac.LinEq, Isac.RootEq, Isac.RatEq, Isac.RootRat, Isac.RootRatEq, Isac.PolyEq:502},

              where_ =

              [Const ("HOL.Not", "bool \<Rightarrow> bool") $ (Const ("RatEq.is_ratequation_in", "bool \<Rightarrow> real \<Rightarrow> bool") $ Free ("e_e", "bool") $ Free ("v_v", "real")),

               Const ("HOL.Not", "bool \<Rightarrow> bool") $ (Const ("RootEq.is_rootTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")),

               Const ("HOL.Not", "bool \<Rightarrow> bool") $ (Const ("RootEq.is_rootTerm_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.rhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"))]}],

            [Node

              ("degree_0",

               [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

                 "pbl_equ_univ_poly_deg0", init = ["empty_probl_id"], mathauthors = [], met = [["PolyEq", "solve_d0_polyeq_equation"]], ppc =

                 [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

                  ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

                 prls =

                 Repeat

                  {calc = [], erls = Empty, errpatts = [], id = "PolyEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                   [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("Poly.is_expanded_in", fn), Eval ("Poly.is_poly_in", fn),

                    Eval ("Poly.has_degree_in", fn), Eval ("Poly.is_polyrat_in", fn), Eval ("HOL.eq", fn), Eval ("RootEq.is_rootTerm_in", fn), Eval ("RatEq.is_ratequation_in", fn),

                    Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"),

                    Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                   scr = Empty_Prog, srls = Empty},

                 thy =

                 {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,

                   HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                   HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                   HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                   HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                   HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                   HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                   HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                   HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull,

                   HOL.Modules, HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex,

                   HOL.MacLaurin, Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr,

                   Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle,

                   Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.Root, Isac.Equation, Isac.GCD_Poly_ML, Isac.Rational, Isac.LinEq, Isac.RootEq, Isac.RatEq, Isac.RootRat, Isac.RootRatEq, Isac.PolyEq:512},

                 where_ =

                 [Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("HOL.eq", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $ Var (("a", 0), "?'a1") $ Const ("Groups.zero_class.zero", "?'a1")) $ Free ("e_e", "bool"),

                  Const ("Poly.is_poly_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"),

                  Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Poly.has_degree_in", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                    Const ("Groups.zero_class.zero", "real")]}],

               []),

             Node

              ("degree_1",

               [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

                 "pbl_equ_univ_poly_deg1", init = ["empty_probl_id"], mathauthors = [], met = [["PolyEq", "solve_d1_polyeq_equation"]], ppc =

                 [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

                  ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

                 prls =

                 Repeat

                  {calc = [], erls = Empty, errpatts = [], id = "PolyEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                   [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("Poly.is_expanded_in", fn), Eval ("Poly.is_poly_in", fn),

                    Eval ("Poly.has_degree_in", fn), Eval ("Poly.is_polyrat_in", fn), Eval ("HOL.eq", fn), Eval ("RootEq.is_rootTerm_in", fn), Eval ("RatEq.is_ratequation_in", fn),

                    Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"),

                    Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                   scr = Empty_Prog, srls = Empty},

                 thy =

                 {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,

                   HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                   HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                   HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                   HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                   HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                   HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                   HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                   HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull,

                   HOL.Modules, HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex,

                   HOL.MacLaurin, Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr,

                   Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle,

                   Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.Root, Isac.Equation, Isac.GCD_Poly_ML, Isac.Rational, Isac.LinEq, Isac.RootEq, Isac.RatEq, Isac.RootRat, Isac.RootRatEq, Isac.PolyEq:522},

                 where_ =

                 [Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("HOL.eq", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $ Var (("a", 0), "?'a1") $ Const ("Groups.zero_class.zero", "?'a1")) $ Free ("e_e", "bool"),

                  Const ("Poly.is_poly_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"),

                  Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Poly.has_degree_in", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                    Const ("Groups.one_class.one", "real")]}],

               []),

             Node

              ("degree_2",

               [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

                 "pbl_equ_univ_poly_deg2", init = ["empty_probl_id"], mathauthors = [], met = [["PolyEq", "solve_d2_polyeq_equation"]], ppc =

                 [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

                  ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

                 prls =

                 Repeat

                  {calc = [], erls = Empty, errpatts = [], id = "PolyEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                   [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("Poly.is_expanded_in", fn), Eval ("Poly.is_poly_in", fn),

                    Eval ("Poly.has_degree_in", fn), Eval ("Poly.is_polyrat_in", fn), Eval ("HOL.eq", fn), Eval ("RootEq.is_rootTerm_in", fn), Eval ("RatEq.is_ratequation_in", fn),

                    Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"),

                    Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                   scr = Empty_Prog, srls = Empty},

                 thy =

                 {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,

                   HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                   HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base, HOL.BNF_Def,

                   HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power, HOL.Groups_Big,

                   HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big, HOL.Euclidean_Division,

                   HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List,

                   HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation,

                   HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing,

                   HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main, HOL.Archimedean_Field, HOL.Rat, HOL.Hull,

                   HOL.Modules, HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series, HOL.NthRoot, HOL.Transcendental, HOL.Complex,

                   HOL.MacLaurin, Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac, Specify.Tactical, Specify.Prog_Expr,

                   Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code, Isac.BridgeLibisabelle,

                   Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.Root, Isac.Equation, Isac.GCD_Poly_ML, Isac.Rational, Isac.LinEq, Isac.RootEq, Isac.RatEq, Isac.RootRat, Isac.RootRatEq, Isac.PolyEq:532},

                 where_ =

                 [Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $ (Const ("HOL.eq", "?'a1 \<Rightarrow> ?'a1 \<Rightarrow> bool") $ Var (("a", 0), "?'a1") $ Const ("Groups.zero_class.zero", "?'a1")) $ Free ("e_e", "bool"),

                  Const ("Poly.is_poly_in", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real"),

                  Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Poly.has_degree_in", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Prog_Expr.lhs", "bool \<Rightarrow> real") $ Free ("e_e", "bool")) $ Free ("v_v", "real")) $

                    (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))]}],

               [Node

                 ("sq_only",

                  [{cas = SOME (Const ("Equation.solve", "bool \<times> real \<Rightarrow> bool list") $ (Const ("Product_Type.Pair", "bool \<Rightarrow> real \<Rightarrow> bool \<times> real") $ Free ("e_e", "bool") $ Free ("v_v", "real"))), guh =

                    "pbl_equ_univ_poly_deg2_sqonly", init = ["empty_probl_id"], mathauthors = [], met = [["PolyEq", "solve_d2_polyeq_sqonly_equation"]], ppc =

                    [("#Given", (Const ("Input_Descript.equality", "bool \<Rightarrow> una"), Free ("e_e", "bool"))), ("#Given", (Const ("Input_Descript.solveFor", "real \<Rightarrow> una"), Free ("v_v", "real"))),

                     ("#Find", (Const ("Input_Descript.solutions", "bool list \<Rightarrow> toreall"), Free ("v_v'i'", "bool list")))],

                    prls =

                    Repeat

                     {calc = [], erls = Empty, errpatts = [], id = "PolyEq_prls", preconds = [], rew_ord = ("dummy_ord", fn), rules =

                      [Eval ("Prog_Expr.ident", fn), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.lhs", fn), Eval ("Prog_Expr.rhs", fn), Eval ("Poly.is_expanded_in", fn), Eval ("Poly.is_poly_in", fn),

                       Eval ("Poly.has_degree_in", fn), Eval ("Poly.is_polyrat_in", fn), Eval ("HOL.eq", fn), Eval ("RootEq.is_rootTerm_in", fn), Eval ("RatEq.is_ratequation_in", fn),

                       Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"),

                       Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a")],

                      scr = Empty_Prog, srls = Empty},

                    thy =

                    {Pure, Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras, HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive,

                      HOL.Rings, HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation, HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

                      HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn, HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic, HOL.Fun_Def_Base,

                      HOL.BNF_Def, HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base, HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Transfer, HOL.Num, HOL.Power,

                      HOL.Groups_Big, HOL.Equiv_Relations, HOL.Lifting, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo, HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Fun_Def, HOL.Int, HOL.Lattices_Big,

                      HOL.Euclidean_Division, HOL.Parity, HOL.Divides, HOL.Numeral_Simprocs, HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Presburger, HOL.SMT, HOL.Sledgehammer,

                      HOL.Lifting_Set, HOL.List, HOL.Groups_List, HOL.Bit_Operations, HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep, HOL.Limited_Sequence,

                      HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random, HOL.Random_Pred, HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD, HOL.Nitpick,

                      HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku, HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main,

                      HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces, HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series,

                      HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store, Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac,

                      Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Specify.Input_Descript, Specify.MathEngBasic, Specify.Specify, Interpret.Interpret, Isac.MathEngine,

                      Isac.Test_Code, Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.Root, Isac.Equation, Isac.GCD_Poly_ML, Isac.Rational, Isac.LinEq, Isac.RootEq, Isac.RatEq,

                      Isac.RootRat, Isac.RootRatEq, Isac.PolyEq:542},

                    where_ =

                    [Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                       (Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                         (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

                           (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("a", 0), "real") $

                             (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("v_", 0), "real") $

                               (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $

                           Const ("Groups.zero_class.zero", "real")) $

                         Free ("e_e", "bool")) $

                       (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                         (Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                           (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

                             (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("a", 0), "real") $

                               (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("b", 0), "real") $

                                 (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("v_", 0), "real") $

                                   (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))))) $

                             Const ("Groups.zero_class.zero", "real")) $

                           Free ("e_e", "bool")) $

                         (Const ("HOL.disj", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                           (Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                             (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

                               (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("v_", 0), "real") $

                                 (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $

                               Const ("Groups.zero_class.zero", "real")) $

                             Free ("e_e", "bool")) $

                           (Const ("Prog_Expr.matches", "bool \<Rightarrow> bool \<Rightarrow> bool") $

                             (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

                               (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("b", 0), "real") $

                                 (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $ Var (("v_", 0), "real") $

                                   (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $

                               Const ("Groups.zero_class.zero", "real")) $

                             Free ("e_e", "bool")))),