WN130922 Build_Thydata.thy:

   writeln "======= ! ruleset' ordered =======";

   ! ruleset' |> rev (*!!!!!*) 

     |> map check_kestore_rls |> enumerate_strings |> sort string_ord |> map writeln;

   writeln "======= end ! ruleset' =======";

 --------------------------------------------------------------------------------------

 ======= length (! ruleset')   = 123

 --------------------------------------------------------------------------------------

 Legend:

 # (*a small difference to KEStore_Elems.get_rlss*)

 # -----RULESET: an entry missing here in comparison to KEStore_Elems.get_rlss

 --------------------------------------------------------------------------------------

 ======= ! ruleset' ordered =======

 (LinEq_erls, (LinEq, Rls {#calc = 0, #rules = 26, ...))--92

 (LinEq_simplify, (LinEq, Rls {#calc = 0, #rules = 3, ...))--90

 (LinPoly_simplify, (LinEq, Rls {#calc = 4, #rules = 5, ...))--91

 (PolyEq_erls, (PolyEq, Rls {#calc = 1, #rules = 42, ...))--47

 (Poly_erls, (Poly, Rls {#calc = 0 (*11*), #rules = 25, ...))--118

 (RatEq_eliminate, (RatEq, Rls {#calc = 0, #rules = 3, ...))--64

 (RatEq_simplify, (RatEq, Rls {#calc = 0, #rules = 8, ...))--63

 (RooRatEq_erls, (RootRatEq, Rls {#calc = 2, #rules = 43, ...))--54

 (RootEq_erls, (RootEq, Rls {#calc = 0, #rules = 28, ...))--71

 (Root_erls, (Root, Rls {#calc = 0, #rules = 27, ...))--95

 (Test_simplify, (Test, Rls {#calc = 4, #rules = 37, ...))--10

 (ac_plus_times, (Test, Rls {#calc = 0, #rules = 6, ...))--4

 (add_fractions_p, (Rational, Rrls {...}))--85

 (add_fractions_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))--84

 (add_new_c, (Integrate, Seq {#calc = 0, #rules = 1, ...))--25

 (ansatz_rls, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))--52

 (calc_add_mult_pow_, (Poly, Rls {#calc = 3, #rules = 3, ...))--102

 (calc_rat_erls, (Rational, Rls {#calc = 2, #rules = 4, ...))--88

 (calculate_Rational, (Rational, Rls {#calc = 1, #rules = 15, ...))--89

 (calculate_RootRat, (RootRat, Rls {#calc = 2, #rules = 19, ...))--61

 (cancel_leading_coeff, (PolyEq, Rls {#calc = 0, #rules = 13, ...))--49

 (cancel_p, (Rational, Rrls {...}))--86

 (cancel_p_rls, (Rational, Rls {#calc = 0, #rules = 1, ...))--72

 (collect_bdv, (PolyEq, Rls {#calc = 0, #rules = 18, ...))--35

 (collect_numerals, (Poly, Rls {#calc = 3, #rules = 7, ...))--113

 (collect_numerals_, (Poly, Rls {#calc = 1, #rules = 7, ...))--112

 (complete_square, (PolyEq, Rls {#calc = 0, #rules = 5, ...))--48

 (d0_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 2, ...))--45

 (d1_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 3, ...))--44

 (d2_polyeq_abcFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))--39

 (d2_polyeq_bdv_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 10, ...))--42

 (d2_polyeq_pqFormula_simplify, (PolyEq, Rls {#calc = 0, #rules = 18, ...))--40

 (d2_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 24, ...))--43

 (d2_polyeq_sq_only_simplify, (PolyEq, Rls {#calc = 0, #rules = 6, ...))--41

 (d3_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 21, ...))--38

 (d4_polyeq_simplify, (PolyEq, Rls {#calc = 0, #rules = 1, ...))--37

 (diff_conv, (Diff, Rls {#calc = 1, #rules = 10, ...))--29

 (diff_rules, (Diff, Rls {#calc = 0, #rules = 2, ...))--31

 (diff_sym_conv, (Diff, Rls {#calc = 1, #rules = 8, ...))--28

 (discard_minus, (Poly, Rls {#calc = 0, #rules = 2, ...))--106

 (discard_parentheses, (Poly, Rls {#calc = 0, #rules = 2, ...))--110

 (discard_parentheses1, (Poly, Rls {#calc = 0, #rules = 1, ...))--99

 (e_rls, (Tools (*KEStore*), Rls {#calc = 0, #rules = 0, ...))--123

 (e_rrls, (Tools (*KEStore*), Rrls {...}))--122

 (equival_trans, (Partial_Fractions, Rls {#calc = 0, #rules = 2, ...))--50

 (eval_rls, (DiffApp, Rls {#calc = 0, #rules = 19, ...))--27

 (expand, (Poly, Rls {#calc = 0, #rules = 2, ...))--117

 (expand_binoms, (Poly, Rls {#calc = 3, #rules = 29, ...))--108

 (expand_binomtest, (Test, Rls {#calc = 3, #rules = 29, ...))--1

 (expand_poly, (Poly, Rls {#calc = 0, #rules = 9, ...))--116

 (expand_poly_, (Poly, Rls {#calc = 0, #rules = 8, ...))--105

 (expand_poly_rat_, (Poly, Rls {#calc = 0, #rules = 10, ...))--104

 (expand_rootbinoms, (Root, Rls {#calc = 6, #rules = 33, ...))--93

 (fasse_zusammen, (PolyMinus, Rls {#calc = 2, #rules = 24, ...))--59

 (integration, (Integrate, Seq {#calc = 0, #rules = 3, ...))--23

 (integration_rules, (Integrate, Rls {#calc = 1, #rules = 6, ...))--26

 -----KESTORE: (inverse_z, (Inverse_Z_Transform, Rls {#calc = 0, #rules = 1, ...))--1

 (isolate_bdv, (Test, Rls {#calc = 0, #rules = 6, ...))--7

 (isolate_bdvs, (EqSystem, Rls {#calc = 0, #rules = 3, ...))--16

 (isolate_bdvs_4x4, (EqSystem, Rls {#calc = 0, #rules = 5, ...))--15

 (isolate_root, (Test, Rls {#calc = 0, #rules = 6, ...))--8

 (klammern_aufloesen, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))--56

 (klammern_ausmultiplizieren, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))--55

 (l_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))--68

 (list_rls, (DiffApp (*ListC*), Rls {#calc = 8, #rules = 53, ...))--121

 (make_polynomial, (Poly, Seq {#calc = 1, #rules = 11, ...))--109

 (make_polynomial_in, (PolyEq, Seq {#calc = 0, #rules = 8, ...))--34

 (make_polytest, (Test, Rls {#calc = 3, #rules = 25, ...))--2

 (make_rat_poly_with_parentheses, (Poly, Seq {#calc = 1, #rules = 10, ...))--96

 (make_ratpoly_in, (PolyEq, Seq {#calc = 0, #rules = 5, ...))--33

 (make_rooteq, (Root, Rls {#calc = 3, #rules = 25, ...))--94

 (matches, (Test, Rls {#calc = 8, #rules = 20, ...))--6

 (multiply_ansatz, (Partial_Fractions, Rls {#calc = 0, #rules = 1, ...))--51

 (norm_Poly, (Poly, Seq {#calc = 1, #rules = 11, ...))--119

 (norm_Rational, (Rational, Seq {#calc = 0, #rules = 6, ...))--77

 (norm_Rational_noadd_fractions, (Integrate, Seq {#calc = 0, #rules = 6, ...))--21

 (norm_Rational_parenthesized, (Rational, Seq {#calc = 0, #rules = 2, ...))--75

 (norm_Rational_rls, (Rational, Rls {#calc = 0, #rules = 5, ...))--76

 (norm_Rational_rls_noadd_fractions, (Integrate, Rls {#calc = 0, #rules = 4, ...))--20

 (norm_System, (EqSystem, Rls {#calc = 0, #rules = 9, ...))--11

 (norm_System_noadd_fractions, (EqSystem, Rls {#calc = 0, #rules = 8, ...))--12

 (norm_diff, (Diff, Rls {#calc = 0, #rules = 2, ...))--30

 (norm_equation, (Test, Rls {#calc = 0, #rules = 1, ...))--5

 (norm_rat_erls, (Rational, Rls {#calc = 1, #rules = 1, ...))--78

 (order_add_mult, (Poly, Rls {#calc = 0, #rules = 6, ...))--114

 (order_add_mult_System, (EqSystem, Rls {#calc = 0, #rules = 6, ...))--13

 (order_add_mult_in, (PolyEq, Rls {#calc = 0, #rules = 6, ...))--36

 (order_add_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))--97

 (order_mult_rls_, (Poly, Rls {#calc = 0, #rules = 1, ...))--98

 (order_system, (EqSystem, Rls {#calc = 0, #rules = 1, ...))--14

 (ordne_alphabetisch, (PolyMinus, Rls {#calc = 0, #rules = 8, ...))--60

 (ordne_monome, (PolyMinus, Rls {#calc = 0, #rules = 4, ...))--57

 (polyeq_simplify, (PolyEq, Rls {#calc = 6, #rules = 12, ...))--46

 (powers, (Rational, Rls {#calc = 1, #rules = 11, ...))--82

 (powers_erls, (Rational, Rls {#calc = 4, #rules = 6, ...))--83

 (r_sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 16, ...))--67

 (rat_mult_div_pow, (Rational, Rls {#calc = 1, #rules = 8, ...))--73

 (rat_mult_divide, (Rational, Rls {#calc = 1, #rules = 6, ...))--81

 (rat_mult_poly, (Rational, Rls {#calc = 0, #rules = 2, ...))--74

 (rat_reduce_1, (Rational, Rls {#calc = 0, #rules = 2, ...))--79

 (rateq_erls, (RatEq, Rls {#calc = 1, #rules = 41, ...))--65

 (rational_erls, (Rational, Rls {#calc = 1, #rules = 35, ...))--87

 (rearrange_assoc, (Test, Rls {#calc = 0, #rules = 2, ...))--3

 (reduce_012, (Poly, Rls {#calc = 0, #rules = 7, ...))--111

 (reduce_012_, (Poly, Rls {#calc = 0, #rules = 6, ...))--100

 (reduce_012_mult_, (Poly, Rls {#calc = 0, #rules = 4, ...))--101

 (reduce_0_1_2, (Rational, Rls {#calc = 0, #rules = 6, ...))--80

 (rev_rew_p, (Poly, Seq {#calc = 3, #rules = 25, ...))--107

 (rooteq_simplify, (RootEq, Rls {#calc = 6, #rules = 15, ...))--66

 (rooteq_srls, (RootEq, Rls {#calc = 0, #rules = 3, ...))--70

 (rootrat_erls, (RootRat, Rls {#calc = 14, #rules = 41, ...))--62

 (rootrat_solve, (RootRatEq, Rls {#calc = 0, #rules = 4, ...))--53

 (separate_bdv2, (Integrate, Rls {#calc = 0, #rules = 22, ...))--22

 (separate_bdvs, (PolyEq, Rls {#calc = 0, #rules = 23, ...))--32

 (simplify_Integral, (Integrate, Seq {#calc = 1, #rules = 7, ...))--24

 (simplify_System, (EqSystem, Seq {#calc = 1, #rules = 6, ...))--17

 (simplify_System_parenthesized, (EqSystem, Seq {#calc = 1, #rules = 8, ...))--18

 (simplify_power, (Poly, Rls {#calc = 0, #rules = 7, ...))--115

 (simplify_power_, (Poly, Rls {#calc = 0, #rules = 8, ...))--103

 (sqrt_isolate, (RootEq, Rls {#calc = 0, #rules = 32, ...))--69

 (testerls, (Test, Rls {#calc = 8, #rules = 19, ...))--19

 (tval_rls, (Test, Rls {#calc = 11, #rules = 27, ...))--9

 (univariate_equation_prls, (Equation, Rls {#calc = 1, #rules = 1, ...))--120

 (verschoenere, (PolyMinus, Rls {#calc = 1, #rules = 10, ...))--58

 ======= end ! ruleset' =======