(*  Title:  test/Tools/isac/build_thydata.sml

    Author: Walther Neuper, TU Graz, 2010

    (c) due to copyright terms

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

"--------------------------------------------------------";

"--------------------------------------------------------";

"table of contents --------------------------------------";

"--------------------------------------------------------";

"-------- OLD compute rlsthmsNOTisac by eq_thmID --------";

"-------- retrieve isa-b/c theories from Isabelle -------";

"-------- prop_of thm .. Theory.axioms_of ---------------";

"-------- compute val rlsthmsNOTisac --------------------";

"-------- hard-coded val rlsthmsNOTisac -----------------";

"-------- the_hier (! thehier) (collect_thydata ())------";

"-------- retrieve errpats ------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"-------- OLD compute rlsthmsNOTisac by eq_thmID --------";

"-------- OLD compute rlsthmsNOTisac by eq_thmID --------";

"-------- OLD compute rlsthmsNOTisac by eq_thmID --------";

(* WN1204xx:

   view src/Pure/isac/IsacKnowledge/Isac.ML @ 37874:331e38464ada

   date 	Thu Jul 22 10:45:18 2010 +0200

local

    val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 

		       (map (thms_of_rls o #2 o #2))) (!ruleset');

    val isacthms = (flat o (map (thms_of o #2))) (!theory');

in

    val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);

end;

*)

    val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 

		       (map (thms_of_rls o #2 o #2))) (!ruleset'):  (thmID * thm) list;

(* THIS IS TOO EXPENSIVE:

val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"});

length all_ListC_thms = 19860 <<<<<-----*)

val isacthys = (union Theory.eq_thy (! knowthys) (! progthys));

  val isacthms''''' = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list; 

    val rlsthmsNOTisac''''' = gen_diff eq_thmI' (isacrlsthms''''', isacthms'''''); 

(*  vvvvvvvvvvvvvv also contains all sym; ???: put ###sym_* to isacthms'''''

                                          ??? ..NO: some are from isab, some from isac !!!

val rlsthmsNOTisac''''' =

   [("refl", "?t = ?t"),   |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)

  |> flat

  |> map thm_of_thm

  |> gen_distinct Thm.eq_thm

  |> map (` I)

  |> map (apfst Thm.derivation_name) (*WN120319 returns "" after num_str, see below*)

  |> map (apsnd prop_of);            (*adapt to Theory.axioms_of below*)

    ("o_apply", "(?f \<circ> ?g) ?x = ?f (?g ?x)"), 

    (*/------------these are not found in ListC.thy, because they are no axioms---\*)

    ("del_base", "del [] ?x = []"), 

    ("del_rec", "del (?y # ?ys) ?x = (if ?x = ?y then ?ys else ?y # del ?ys ?x)"),

    ("LENGTH_CONS", "LENGTH (?x # ?xs) = 1 + LENGTH ?xs"), 

    ("LENGTH_NIL", "LENGTH [] = 0"), 

    ("list_diff_def", "?a -- ?b \<equiv> foldl del ?a ?b"), 

    (*\------------these are not found in ListC.thy, because they are no axioms---/*)

    ("take_Nil", "take ?n [] = []"),

    ("take_Cons", "take ?n (?x # ?xs) = (case ?n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> ?x # take m ?xs)"), 

    ("if_True", "(if True then ?x else ?y) = ?x"), 

    ("if_False", "(if False then ?x else ?y) = ?y"),

    (*###*)("sym_real_mult_minus1", "- ?z1 = -1 * ?z1"), 

    ("distrib_right", "(?a + ?b) * ?c = ?a * ?c + ?b * ?c"), 

    ("distrib_left", "?a * (?b + ?c) = ?a * ?b + ?a * ?c"), 

    (*###*)(sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2"),

    (*###*)(sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)"), 

    ("mult_1_right", "?a * 1 = ?a"), 

    (*###*)(sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"), 

    ("mult_1_left", "1 * ?a = ?a"),

    ("mult_zero_left", "0 * ?a = 0"), 

    ("mult_zero_right", "?a * 0 = 0"), 

    ("add_0_left", "0 + ?a = ?a"), 

    ("add_0_right", "?a + 0 = ?a"), 

    ("divide_zero_left", "0 / ?a = 0"),

    (*###*)(sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"), 

    ("order_refl", "?w \<le> ?w"), 

    ("minus_minus", "- (- ?a) = ?a"), 

    ("mult_commute", "?z * ?w = ?w * ?z"),

    ("mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), 

    ("add_commute", "?a + ?b = ?b + ?a"), 

    ("add_left_commute", "?b + (?a + ?c) = ?a + (?b + ?c)"),

    ("add_assoc", "?a + ?b + ?c = ?a + (?b + ?c)"), 

    ("minus_mult_left", "- ?a1 * ?b1 = - (?a1 * ?b1)"), 

    ("right_minus", "?a + - ?a = 0"), 

    (*###*)("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),

    ("left_diff_distrib", "(?a - ?b) * ?c = ?a * ?c - ?b * ?c"), 

    ("right_diff_distrib", "?a * (?b - ?c) = ?a * ?b - ?a * ?c"), 

    ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),

    ("times_divide_eq_right", "?a * (?b / ?c) = ?a * ?b / ?c"), 

    ("times_divide_eq_left", "?b / ?c * ?a = ?b * ?a / ?c"), 

    ("divide_divide_eq_left", "?a / ?b / ?c = ?a / (?b * ?c)"),

    ("divide_divide_eq_right", "?a / (?b / ?c) = ?a * ?c / ?b"), 

    ("divide_1", "?a / 1 = ?a"), 

    ("add_divide_distrib", "(?a + ?b) / ?c = ?a / ?c + ?b / ?c"),

    (*###*)("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")]: (string * thm) list

*)

"-------- retrieve isa-b/c theories from Isabelle -------";

"-------- retrieve isa-b/c theories from Isabelle -------";

"-------- retrieve isa-b/c theories from Isabelle -------";

  val first_ProgLang_thy = @{theory ListC}

  val first_Knowledge_thy = @{theory Delete}  (*see WN120321.TODO rearrange theories*)

  val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory};

  val isabthys' =

    drop ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);

  val isacthys' =

    take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);

  val knowthys' =

    take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys');

  val progthys' =                   (*WN120321.TODO rearrange theories -------vvv*)

    drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');

map Context.theory_name allthys;

map Context.theory_name isabthys';

map Context.theory_name isacthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", 

  "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",

  "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", 

  "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript", 

  "Delete", "xmlsrc", "Interpret", "ProgLang", "Script", "Tools", "ListC"];  (*WN120201 true*)

(*see WN120321.TODO rearrange theories: ATTENTION with ProgLang.thy etc*)

map Context.theory_name knowthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", 

  "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",

  "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", 

  "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript", 

  "Delete"];  (*WN120201 true*)

map Context.theory_name progthys' = ["Script", "Tools", "ListC"];  (*WN120201 true*)

"-------- prop_of thm .. Theory.axioms_of ---------------";

"-------- prop_of thm .. Theory.axioms_of ---------------";

"-------- prop_of thm .. Theory.axioms_of ---------------";

val isacrlsthms''''' = ! ruleset'

  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)

  |> flat

  |> map thm_of_thm

  |> gen_distinct Thm.eq_thm

  |> map (` I)

  |> map (apfst Thm.derivation_name) (*WN120319 returns "" after num_str, see below*)

  |> map (apsnd prop_of);            (*adapt to Theory.axioms_of below*)

val isacthms''''' = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;

"---------------------------------------------------------------------------------";

"the formats of prop_of thm .. Theory.axioms_of are too different for comparison: ";

"---------------------------------------------------------------------------------";

(*assoc (isacrlsthms''''', "Poly.realpow_oneI") = NONE; ---thus:*)

val one1 = num_str @{thm realpow_oneI};

atomty (prop_of one1);

(**** 

*** Const (HOL.Trueprop, bool => prop)

*** . Const (HOL.eq, real => real => bool)

*** . . Const (Atools.pow, real => real => real)

*** . . . Var ((r, 0), real)

*** . . . Free (1, real)

*** . . Var ((r, 0), real)

*** *)

val SOME coll2 = assoc (isacthms''''', "Poly.realpow_oneI");

atomty coll2;

(**** 

*** Const (all, (real => prop) => prop)

*** . Abs (r, real,..

*** . . Const (HOL.Trueprop, bool => prop)

*** . . . Const (HOL.eq, real => real => bool)

*** . . . . Const (Atools.pow, real => real => real)

*** . . . . . Bound 0

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

*** . . . . Bound 0

***  *)

(*assoc (isacrlsthms''''', "Poly.realpow_plus_1_atom") = NONE; ---thus:*)

val one1 = num_str @{thm realpow_plus_1_atom};

atomty (prop_of one1);

(**** 

*** Const (==>, prop => prop => prop)

*** . Const (HOL.Trueprop, bool => prop)

*** . . Const (Atools.is'_atom, real => bool)

*** . . . Var ((r, 0), real)

*** . Const (HOL.Trueprop, bool => prop)

*** . . Const (HOL.eq, real => real => bool)

*** . . . Const (Groups.times_class.times, real => real => real)

*** . . . . Var ((r, 0), real)

*** . . . . Const (Atools.pow, real => real => real)

*** . . . . . Var ((r, 0), real)

*** . . . . . Var ((n, 0), real)

*** . . . Const (Atools.pow, real => real => real)

*** . . . . Var ((r, 0), real)

*** . . . . Const (Groups.plus_class.plus, real => real => real)

*** . . . . . Free (1, real)

*** . . . . . Var ((n, 0), real)

*** *)

val SOME coll2 = assoc (isacthms''''', "Poly.realpow_plus_1_atom");

atomty coll2;

(**** 

*** Const (all, (real => prop) => prop)

*** . Abs (r, real,..

*** . . Const (all, (real => prop) => prop)

*** . . . Abs (n, real,..

*** . . . . Const (==>, prop => prop => prop)

*** . . . . . Const (HOL.Trueprop, bool => prop)

*** . . . . . . Const (Atools.is'_atom, real => bool)

*** . . . . . . . Bound 1

*** . . . . . Const (HOL.Trueprop, bool => prop)

*** . . . . . . Const (HOL.eq, real => real => bool)

*** . . . . . . . Const (Groups.times_class.times, real => real => real)

*** . . . . . . . . Bound 1

*** . . . . . . . . Const (Atools.pow, real => real => real)

*** . . . . . . . . . Bound 1

*** . . . . . . . . . Bound 0

*** . . . . . . . Const (Atools.pow, real => real => real)

*** . . . . . . . . Bound 1

*** . . . . . . . . Const (Groups.plus_class.plus, real => real => real)

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

*** . . . . . . . . . Bound 0

*** *)

"-------- compute val rlsthmsNOTisac --------------------";

"-------- compute val rlsthmsNOTisac --------------------";

"-------- compute val rlsthmsNOTisac --------------------";

(*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac.

*)

(*DECISION.WN120201 wrt. identifiers of theorems, thmID, in building html presentation:

  eg. Thm.derivation_name @{thm add_0} = "Groups.comm_monoid_add_class.add_0";

  is long identifier, "add_0" is simple identifier

  given:

  (1) simple identifiers, without points, conform with usage in TP-PL

  (2) Thm (id, thm) in rls, id is simple id; entered manyally -- error prone

        all this might change due to further automation

  thus decision

  (a) retrieve id (and theory) from thm or axiom (avoids errors from (2))

  (b) hold long identifiers, with points, as long as possible

  (c) use thmID_of_derivation_name, thyID_of_derivation_name for retrieval.

*)

(*WN110722 saved investigations:

val all_ListC_thms = PureThy.all_thms_of (@{theory "ListC"});

val all_Complex_Main_thms = PureThy.all_thms_of (@{theory "Complex_Main"});

   delivers [] after 100 secs ...

subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms); 

... because ListC contains no thms, but axioms only.

"----- so we cannot get isacthms as thm, only as term ---";

"----- but we can retain isacrlsthms as thm ---";

*)

val isacrlsthms = ! ruleset'

  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)

  |> flat

  |> map thm_of_thm

  |> gen_distinct Thm.eq_thm

  |> map (` I)

  |> map (apfst Thm.derivation_name); (*WN120319 returns "" after num_str, see below*)

length isacrlsthms = 450; (*WN120319*)

(*[("HOL.refl", "?t = ?t"),

   ("Fun.o_apply", "(?f \<circ> ?g) ?x = ?f (?g ?x)"),

   ("", "1 < ?n \<Longrightarrow> NTH ?n (?x # ?xs) = NTH (?n + - 1) ?xs"), (*destroyed by num_str*)

   ("", "NTH 1 (?x # ?xs) = ?x"),                             (*destroyed by num_str*)

   ("ListC.append_Cons", "(?x # ?xs) @ ?ys = ?x # ?xs @ ?ys"), ...]: (string * thm) list

*)

val isacthms = (flat o (map Theory.axioms_of)) isacthys: (thmID * term) list;

length isacthms = 517; (*WN120319, WN120201 509!?!*)

(*[("Inverse_Z_Transform.rule1", Const ("==>...", "prop \<Rightarrow> prop \<Rightarrow> prop") $ (Const (...) $ ...),

   ("Inverse_Z_Transform.rule2", Const (...) $ Abs ("z...", "RealDef.real",...),

   ...]: (thmID * term) list

*)

(*WN120319: since num_str destoys derivation_name to "", we hardcode rlsthmsNOTisac:

val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);

map fst rlsthmsNOTisac;

(*val it = ["HOL.refl", "Fun.o_apply", "", "", "ListC.del.del_base", "ListC.del.del_rec", "", "",

  "ListC.list_diff_def", "List.take.take_Nil", ...]

*)

length rlsthmsNOTisac = 46; (*WN120201*)

*)

"-------- hard-coded val rlsthmsNOTisac -----------------";

"-------- hard-coded val rlsthmsNOTisac -----------------";

"-------- hardcode val rlsthmsNOTisac -------------------";

(*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:*)

val rlsthmsNOTisac =

 [("HOL.refl", (prop_of o num_str) @{thm refl}),

  ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}),

  (*/------------these are not found in ListC.thy, because they are no axioms---\*)

  ("ListC.del.del_base", (prop_of o num_str) @{thm del_base}), 

  ("ListC.del.del_rec", (prop_of o num_str) @{thm del_rec}),

  ("ListC.LENGTH.LENGTH_CONS", (prop_of o num_str) @{thm LENGTH_CONS}), 

  ("ListC.LENGTH.LENGTH_NIL", (prop_of o num_str) @{thm LENGTH_NIL}), 

  ("ListC.list_diff_def", (prop_of o num_str) @{thm list_diff_def}), 

  (*\------------these are not found in ListC.thy, because they are no axioms---/*)

  ("List.take_Nil", (prop_of o num_str) @{thm take_Nil}),

  ("List.take_Cons", (prop_of o num_str) @{thm take_Cons}),

  ("List.if_True", (prop_of o num_str) @{thm if_True}),

  ("HOL.if_False", (prop_of o num_str) @{thm if_False}),

  (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)

  ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),

  ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),

  (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)

  (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)

  ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),

  (*("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1")*)

  ("Groups.monoid_mult_class.mult_1_left", (prop_of o num_str) @{thm mult_1_left}),

  ("Rings.mult_zero_class.mult_zero_left", (prop_of o num_str) @{thm mult_zero_left}),

  ("Rings.mult_zero_class.mult_zero_right", (prop_of o num_str) @{thm mult_zero_right}),

  ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}),

  ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),

  ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),

  (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)

  ("RealDef.order_refl", (prop_of o num_str) @{thm order_refl}),

  ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),

  ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }),

  ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),

  ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),

  ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),

  ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),

  ("Rings.ring_class.minus_mult_left", (prop_of o num_str) @{thm minus_mult_left}),

  ("Groups.group_add_class.right_minus", (prop_of o num_str) @{thm right_minus}),

  (*###("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),*)

  ("Rings.ring_class.left_diff_distrib", (prop_of o num_str) @{thm left_diff_distrib}),

  ("Rings.ring_class.right_diff_distrib", (prop_of o num_str) @{thm right_diff_distrib}),

  ("Rings.division_ring_class.minus_divide_left", (prop_of o num_str) @{thm minus_divide_left}),

  ("Rings.division_ring_class.times_divide_eq_right", (prop_of o num_str) @{thm times_divide_eq_right}),

  ("Fields.field_class.times_divide_eq_left", (prop_of o num_str) @{thm times_divide_eq_left}),

  ("Fields.field_inverse_zero_class.divide_divide_eq_left", (prop_of o num_str) @{thm divide_divide_eq_left}),

  ("Fields.field_inverse_zero_class.divide_divide_eq_right", (prop_of o num_str) @{thm divide_divide_eq_right}),

  ("Rings.division_ring_class.divide_1", (prop_of o num_str) @{thm divide_1}),

  ("Rings.division_ring_class.add_divide_distrib", (prop_of o num_str) @{thm add_divide_distrib }),

  (*###("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")*)

  (* thms in Scripts: *)

  ("Int.divide_minus1", (prop_of o num_str) @{thm divide_minus1}),

  ("Groups.group_add_class.neg_equal_iff_equal", (prop_of o num_str) @{thm neg_equal_iff_equal})]

  : (thmDeriv * term) list;

"-------- the_hier (! thehier) (collect_thydata ())------";

"-------- the_hier (! thehier) (collect_thydata ())------";

"-------- the_hier (! thehier) (collect_thydata ())------";

collect_thydata; (* = fn: unit -> (theID * thydata) list*)

thehier; (* = ref [Ptyp ("IsacKnowledge", [Html {guh = "thy_isac_IsacKnowledge-part", ...}],

                    [Ptyp ("Biegelinie", [Html {guh = "thy_isac_Biegelinie", ...}],

                      [Ptyp ("Theorems", [Html {guh = "thy_isac_Biegelinie-Theorems", ...}],

                        [Ptyp ("Belastung_Querkraft", [Hthm {guh = "thy_isac_B ...}],[]),

                         Ptyp ("Moment_Neigung", [Hthm {guh = "thy_isac_Biegeli...}],[]),

                   [])])])])]     : thehier ref *)

the_hier (! thehier) (collect_thydata ());

(*

*** insert: preserved ["Isabelle"] 

 *** insert: preserved ["Isabelle","HOL","Theorems","refl"] 

 *** insert: preserved ["Isabelle","Fun","Theorems","o_apply"]

                see WN120320.TODO check-improve rlsthmsNOTisac: ------\

 *** insert: preserved ["Isabelle","ListC","Theorems","del_base"] 

 *** insert: preserved ["Isabelle","ListC","Theorems","del_rec"] 

 *** insert: preserved ["Isabelle","ListC","Theorems","LENGTH_CONS"] 

 *** insert: preserved ["Isabelle","ListC","Theorems","LENGTH_NIL"] 

 *** insert: preserved ["Isabelle","ListC","Theorems","list_diff_def"] 

                see WN120320.TODO check-improve rlsthmsNOTisac: ------/

 *** insert: preserved ["Isabelle","List","Theorems","take_Nil"] 

 *** insert: preserved ["Isabelle","List","Theorems","take_Cons"] 

 *** insert: preserved ["Isabelle","List","Theorems","if_True"] 

              Thm.get_name_hint @{t^^^^^^True} = "HOL.if_True";

 *** insert: preserved ["Isabelle","HOL","Theorems","if_False"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","distrib_right"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","distrib_left"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_right"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","mult_1_left"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_left"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","mult_zero_right"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","add_0_left"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","add_0_right"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","divide_zero_left"] 

 *** insert: preserved ["Isabelle","RealDef","Theorems","order_refl"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","minus_minus"] 

 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_commute"] 

 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","add_commute"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","add_left_commute"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","add_assoc"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","minus_mult_left"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","right_minus"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","left_diff_distrib"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","right_diff_distrib"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","minus_divide_left"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","times_divide_eq_right"] 

 *** insert: preserved ["Isabelle","Fields","Theorems","times_divide_eq_left"] 

 *** insert: preserved ["Isabelle","Fields","Theorems","divide_divide_eq_left"] 

 *** insert: preserved ["Isabelle","Fields","Theorems","divide_divide_eq_right"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","divide_1"] 

 *** insert: preserved ["Isabelle","Rings","Theorems","add_divide_distrib"] 

 *** insert: preserved ["Isabelle","Int","Theorems","divide_minus1"] 

 *** insert: preserved ["Isabelle","Groups","Theorems","neg_equal_iff_equal"]

                                                       ??? vvvvvvvvvvvvvv ------\

 *** insert: preserved ["IsacScripts","Script","Theorems","arity_type_ID"] 

 *** insert: preserved ["IsacScripts","Script","Theorems","arity_type_arg"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_cpy"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_nam"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_str"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_una"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_unl"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_toreal"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_unknow"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_tobooll"] 

 *** insert: preserved ["IsacScripts","Tools","Theorems","arity_type_toreall"] 

                                                       ??? vvvvvvvvvvvvvv ------/

 *** insert: preserved ["IsacScripts","Tools","Rulesets","e_rls"] 

 *** insert: preserved ["IsacScripts","Tools","Rulesets","e_rrls"] 

                 see WN120320.TODO check-improve rlsthmsNOTisac: ------\

 *** insert: preserved ["IsacScripts","ListC","Theorems","LAST"]  = ["IsacKnowledge","ListC"---\

 *** insert: preserved ["IsacScripts","ListC","Theorems","hd_thm"]

 *** insert: preserved ["IsacScripts","ListC","Theorems","tl_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","NTH_NIL"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","del_def"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","map_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","mem_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","rev_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","tl_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","zip_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","NTH_CONS"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","map_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","mem_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","null_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","rev_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","zip_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","foldr_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","null_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","LENGTH_def"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","append_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","concat_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","filter_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","foldr_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","append_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","butlast_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","concat_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","filter_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","remdups_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","butlast_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","distinct_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","remdups_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","distinct_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","dropWhile_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","takeWhile_Nil"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","dropWhile_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","takeWhile_Cons"] 

 *** insert: preserved ["IsacScripts","ListC","Theorems","list_diff_def_raw"] =["IsacKnowledge"---/

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule1"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule2"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule3"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule4"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule5"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","rule6"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","ruleYZ"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Theorems","ruleZY"] 

 *** insert: preserved ["IsacKnowledge","Inverse_Z_Transform","Rulesets","inverse_z"] 

 *** insert: preserved ["IsacKnowledge","DiophantEq","Theorems","int_isolate_add"] 

 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Moment_Neigung"] 

 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Neigung_Moment"] 

 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Moment_Querkraft"] 

 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Querkraft_Moment"] 

 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","make_fun_explicit"] 

 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"] 

 *** insert: preserved ["IsacKnowledge","Biegelinie","Theorems","Querkraft_Belastung"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","x_quadrat"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","null_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_mal"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_1"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vor_minus_mal"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_mal_mal"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_mal"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_plus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","addiere_vor_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_von_1"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus_plus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_vor_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_mult"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_plus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_mult_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_plus_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus_plus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_plus_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","klammer_minus_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","tausche_minus_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_vor_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg1"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg2"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg3"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","vorzeichen_minus_weg4"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","addiere_eins_vor_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_plus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus1_plus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_plus1"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus1_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_plus_minus1"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_eins_vor_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus1_minus"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Theorems","subtrahiere_x_minus_minus1"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","ordne_alphabetisch"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","fasse_zusammen"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","verschoenere"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","ordne_monome"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","klammern_aufloesen"] 

 *** insert: preserved ["IsacKnowledge","PolyMinus","Rulesets","klammern_ausmultiplizieren"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_2nd_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_3rd_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","ansatz_4th_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_2nd_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_3rd_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","multiply_4th_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_2nd_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_3rd_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Theorems","equival_trans_4th_order"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","ansatz_rls"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","multiply_ansatz"] 

 *** insert: preserved ["IsacKnowledge","Partial_Fractions","Rulesets","equival_trans"] 

 *** insert: preserved ["IsacKnowledge","DiffApp","Theorems","filterVar_Nil"] 

 *** insert: preserved ["IsacKnowledge","DiffApp","Theorems","filterVar_Const"] 

 *** insert: preserved ["IsacKnowledge","DiffApp","Rulesets","list_rls"] 

 *** insert: preserved ["IsacKnowledge","DiffApp","Rulesets","eval_rls"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_0"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rsqare"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","exp_pow"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","power_1"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_0"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_1"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_assoc"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0_1"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_ge0_2"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","mult_square"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcancel_den"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_assoc"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_0_right"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_commute"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","root_add_ge0"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcancel_const"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_0_right"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_1_right"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_commute"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rbinom_power_2"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_right"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","constant_square"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_real_const"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equality"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_div_right"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_add"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_square_inv"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rshift_nominator"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_left_commute"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_mult"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_add"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_div"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs_mult"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equality_0"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_mult_distrib2"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","radd_real_const_eq"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_right_assoc"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_root_mult"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rmult_left_commute"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rnorm_equation_add"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","constant_mult_square"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rdistr_right_assoc_p"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation_left"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","risolate_bdv_mult_add"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_to_lhs_add_mult"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","square_equation_right"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root_assoc"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same_assoc"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left_assoc"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rroot_times_root_assoc_p"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rtwo_of_the_same_assoc_p"] 

 *** insert: preserved ["IsacKnowledge","Test","Theorems","rcollect_one_left_assoc_p"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","testerls"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","Test_simplify"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","tval_rls"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","isolate_root"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","isolate_bdv"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","matches"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","norm_equation"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","ac_plus_times"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","rearrange_assoc"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","make_polytest"] 

 *** insert: preserved ["IsacKnowledge","Test","Rulesets","expand_binomtest"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs0"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","order_system_NxN"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","commute_0_equality"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add1"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_add2"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Theorems","separate_bdvs_mult"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","simplify_System_parenthesized"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","simplify_System"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","isolate_bdvs"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","isolate_bdvs_4x4"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","order_system"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","order_add_mult_System"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","norm_System_noadd_fractions"] 

 *** insert: preserved ["IsacKnowledge","EqSystem","Rulesets","norm_System"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_add"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_pow"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_var"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_mult"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Theorems","integral_const"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","integration_rules"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","add_new_c"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","simplify_Integral"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","integration"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","separate_bdv2"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","norm_Rational_noadd_fractions"] 

 *** insert: preserved ["IsacKnowledge","Integrate","Rulesets","norm_Rational_rls_noadd_fractions"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_ln"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_cos"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_dif"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_exp"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_pow"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sin"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sum"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_var"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_prod"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_quot"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","frac_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","root_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_const"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_ln_chain"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","frac_sym_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","root_sym_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv_bdv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_sym_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_cos_chain"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_exp_chain"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_pow_chain"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_sin_chain"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","diff_prod_const"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","realpow_pow_bdv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Theorems","sqrt_conv_bdv_n"] 

 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_rules"] 

 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","norm_diff"] 

 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","diff_sym_conv"] 

 *** insert: preserved ["IsacKnowledge","Diff","Rulesets","erls"] 

 *** insert: preserved ["IsacKnowledge","LogExp","Theorems","equality_pow"] 

 *** insert: preserved ["IsacKnowledge","LogExp","Theorems","equality_power"] 

 *** insert: preserved ["IsacKnowledge","LogExp","Theorems","exp_invers_log"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d0_true"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","all_left"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d0_false"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","makex1_x"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","plus_leq"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d4_sub_u1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","minus_leq"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_prescind4"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_assoc_1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_assoc_2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_bdv"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_explicit3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula4"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula5"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula6"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula7"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula8"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula9"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_div"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula4"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula5"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula6"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula7"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula8"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula9"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_div"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula10"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_div"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","real_minus_div"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_1_bdv"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_bdv_n"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_add1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d1_isolate_add2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula10"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_add1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_isolate_add2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_add1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_isolate_add2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square4"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","complete_square5"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","separate_1_bdv_n"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","square_explicit1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","square_explicit2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula1_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula2_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula3_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula4_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula9_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_root_equation1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_root_equation2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula1_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula2_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula3_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula4_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula5_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_abcformula6_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_pqformula10_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_reduce_equation1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_reduce_equation2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation4"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation5"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation6"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation7"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation8"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation9"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc1_3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_collect_assoc2_3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation10"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation11"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation12"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation13"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation14"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation15"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d3_reduce_equation16"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff4"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff5"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff6"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff7"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff8"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff9"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","d2_sqrt_equation1_neg"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc1_3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_1"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_2"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","bdv_n_collect_assoc2_3"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff10"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff11"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff12"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Theorems","cancel_leading_coeff13"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","cancel_leading_coeff"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","complete_square"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","PolyEq_erls"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","polyeq_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d0_polyeq_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d1_polyeq_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_bdv_only_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_sq_only_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_pqFormula_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d2_polyeq_abcFormula_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d3_polyeq_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","d4_polyeq_simplify"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","order_add_mult_in"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","collect_bdv"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","make_polynomial_in"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","make_ratpoly_in"] 

 *** insert: preserved ["IsacKnowledge","PolyEq","Rulesets","separate_bdvs"] 

 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_left_1"] 

 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_left_2"] 

 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_right_1"] 

 *** insert: preserved ["IsacKnowledge","RootRatEq","Theorems","rootrat_equation_right_2"] 

 *** insert: preserved ["IsacKnowledge","RootRatEq","Rulesets","RooRatEq_erls"] 

 *** insert: preserved ["IsacKnowledge","RootRatEq","Rulesets","rootrat_solve"] 

 *** insert: preserved ["IsacKnowledge","RootRat","Rulesets","rootrat_erls"] 

 *** insert: preserved ["IsacKnowledge","RootRat","Rulesets","calculate_RootRat"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_pow"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_1"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_2"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","real_rat_mult_3"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_1"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_2"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_double_rat_3"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_both"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_left"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Theorems","rat_mult_denominator_right"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","rateq_erls"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","RatEq_eliminate"] 

 *** insert: preserved ["IsacKnowledge","RatEq","Rulesets","RatEq_simplify"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","makex1_x"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","real_assoc_1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","real_assoc_2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_times_root_1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_times_root_2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add3"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add4"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add5"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_l_add6"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add3"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add4"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add5"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_isolate_r_add6"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_3"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_both_4"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_3"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_4"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_5"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_left_6"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_1"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_2"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_3"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_4"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_5"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Theorems","sqrt_square_equation_right_6"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","RootEq_erls"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","rooteq_srls"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","sqrt_isolate"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","l_sqrt_isolate"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","r_sqrt_isolate"] 

 *** insert: preserved ["IsacKnowledge","RootEq","Rulesets","rooteq_simplify"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","all_left"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","makex1_x"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","real_assoc_1"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","real_assoc_2"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_div"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_add1"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Theorems","lin_isolate_add2"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinEq_erls"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinPoly_simplify"] 

 *** insert: preserved ["IsacKnowledge","LinEq","Rulesets","LinEq_simplify"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","root_false"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","realpow_mul"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_diff_minus"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","root_plus_minus"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_root_negative"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_root_positive"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_mm_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_mp_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_pm_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_pp_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_pow2"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_pow3"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_pow2"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_pow3"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_minus_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_minus_binom1"] 

 *** insert: preserved ["IsacKnowledge","Root","Theorems","real_plus_minus_binom2"] 

 *** insert: preserved ["IsacKnowledge","Root","Rulesets","Root_erls"] 

 *** insert: preserved ["IsacKnowledge","Root","Rulesets","make_rooteq"] 

 *** insert: preserved ["IsacKnowledge","Root","Rulesets","expand_rootbinoms"] 

 *** insert: preserved ["IsacKnowledge","Equation","Rulesets","univariate_equation_prls"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add1"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add2"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add3"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","add_minus"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult2"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_power"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","add_minus1"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross1"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","mult_cross2"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add_assoc"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add1_assoc"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add2_assoc"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_add3_assoc"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult_poly_l"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","rat_mult_poly_r"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_divide_divide1"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_mult_div_cancel2"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_times_divide_num"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_divide_divide1_mg"] 

 *** insert: preserved ["IsacKnowledge","Rational","Theorems","real_times_divide_1_eq"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","discard_minus"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","calculate_Rational"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","calc_rat_erls"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rational_erls"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel_p"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","common_nominator_p"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","common_nominator_p_rls"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","common_nominator"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","powers_erls"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","powers"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_divide"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","reduce_0_1_2"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_reduce_1"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_rat_erls"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational_rls"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_poly"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","rat_mult_div_pow"] 

 *** insert: preserved ["IsacKnowledge","Rational","Rulesets","cancel_p_rls"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_pow"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_oneI"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_multI"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_zeroI"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_diff_plus"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_diff_minus"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_eq_oneI"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_def_atom"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_two_atom"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_atom"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_odd"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_even"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_minus_oneI"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_multI_poly"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mm_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mp_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc_l"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_mult_2_assoc_r"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_pm_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_pp_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_atom"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow2"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow3"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow4"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow5"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_assoc_l"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_addI_assoc_r"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI_assoc_l"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_twoI_assoc_r"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow2"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow3"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_times"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times1"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_times2"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_l"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_r"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow2_p"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_minus_binom_pow3_p"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","realpow_plus_1_assoc_l2"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc_l"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_num_collect_assoc_r"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc_l"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_one_collect_assoc_r"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom1_p"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_minus_binom2_p"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow2_poly"] 

 *** insert: preserved ["IsacKnowledge","Poly","Theorems","real_plus_binom_pow3_poly"]