847 (["polynomial","univariate","equation"], |
847 (["polynomial","univariate","equation"], |
848 [("#Given" ,["equality e_e","solveFor v_v"]), |
848 [("#Given" ,["equality e_e","solveFor v_v"]), |
849 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))", |
849 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))", |
850 "~((lhs e_e) is_rootTerm_in (v_v::real))", |
850 "~((lhs e_e) is_rootTerm_in (v_v::real))", |
851 "~((rhs e_e) is_rootTerm_in (v_v::real))"]), |
851 "~((rhs e_e) is_rootTerm_in (v_v::real))"]), |
852 ("#Find" ,["solutions v_i"]) |
852 ("#Find" ,["solutions v_i'''"]) |
853 ], |
853 ], |
854 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
854 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
855 [])); |
855 [])); |
856 (*--- d0 ---*) |
856 (*--- d0 ---*) |
857 store_pbt |
857 store_pbt |
860 [("#Given" ,["equality e_e","solveFor v_v"]), |
860 [("#Given" ,["equality e_e","solveFor v_v"]), |
861 ("#Where" ,["matches (?a = 0) e_e", |
861 ("#Where" ,["matches (?a = 0) e_e", |
862 "(lhs e_e) is_poly_in v_v", |
862 "(lhs e_e) is_poly_in v_v", |
863 "((lhs e_e) has_degree_in v_v ) = 0" |
863 "((lhs e_e) has_degree_in v_v ) = 0" |
864 ]), |
864 ]), |
865 ("#Find" ,["solutions v_i"]) |
865 ("#Find" ,["solutions v_i'''"]) |
866 ], |
866 ], |
867 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
867 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
868 [["PolyEq","solve_d0_polyeq_equation"]])); |
868 [["PolyEq","solve_d0_polyeq_equation"]])); |
869 |
869 |
870 (*--- d1 ---*) |
870 (*--- d1 ---*) |
874 [("#Given" ,["equality e_e","solveFor v_v"]), |
874 [("#Given" ,["equality e_e","solveFor v_v"]), |
875 ("#Where" ,["matches (?a = 0) e_e", |
875 ("#Where" ,["matches (?a = 0) e_e", |
876 "(lhs e_e) is_poly_in v_v", |
876 "(lhs e_e) is_poly_in v_v", |
877 "((lhs e_e) has_degree_in v_v ) = 1" |
877 "((lhs e_e) has_degree_in v_v ) = 1" |
878 ]), |
878 ]), |
879 ("#Find" ,["solutions v_i"]) |
879 ("#Find" ,["solutions v_i'''"]) |
880 ], |
880 ], |
881 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
881 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
882 [["PolyEq","solve_d1_polyeq_equation"]])); |
882 [["PolyEq","solve_d1_polyeq_equation"]])); |
883 *} |
883 *} |
884 ML{* |
884 ML{* |
888 (["degree_2","polynomial","univariate","equation"], |
888 (["degree_2","polynomial","univariate","equation"], |
889 [("#Given" ,["equality e_e","solveFor v_v"]), |
889 [("#Given" ,["equality e_e","solveFor v_v"]), |
890 ("#Where" ,["matches (?a = 0) e_e", |
890 ("#Where" ,["matches (?a = 0) e_e", |
891 "(lhs e_e) is_poly_in v_v ", |
891 "(lhs e_e) is_poly_in v_v ", |
892 "((lhs e_e) has_degree_in v_v ) = 2"]), |
892 "((lhs e_e) has_degree_in v_v ) = 2"]), |
893 ("#Find" ,["solutions v_i"]) |
893 ("#Find" ,["solutions v_i'''"]) |
894 ], |
894 ], |
895 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
895 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
896 [["PolyEq","solve_d2_polyeq_equation"]])); |
896 [["PolyEq","solve_d2_polyeq_equation"]])); |
897 |
897 |
898 store_pbt |
898 store_pbt |
909 "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_e) &" ^ |
909 "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_e) &" ^ |
910 "Not (matches ( ?v_ + ?v_^^^2 = 0) e_e) &" ^ |
910 "Not (matches ( ?v_ + ?v_^^^2 = 0) e_e) &" ^ |
911 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^ |
911 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^ |
912 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^ |
912 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^ |
913 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]), |
913 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]), |
914 ("#Find" ,["solutions v_i"]) |
914 ("#Find" ,["solutions v_i'''"]) |
915 ], |
915 ], |
916 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
916 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
917 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); |
917 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); |
918 |
918 |
919 store_pbt |
919 store_pbt |
924 "matches ( ?v_ + ?v_^^^2 = 0) e_e | " ^ |
924 "matches ( ?v_ + ?v_^^^2 = 0) e_e | " ^ |
925 "matches ( ?v_ + ?b*?v_^^^2 = 0) e_e | " ^ |
925 "matches ( ?v_ + ?b*?v_^^^2 = 0) e_e | " ^ |
926 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^ |
926 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^ |
927 "matches ( ?v_^^^2 = 0) e_e | " ^ |
927 "matches ( ?v_^^^2 = 0) e_e | " ^ |
928 "matches ( ?b*?v_^^^2 = 0) e_e "]), |
928 "matches ( ?b*?v_^^^2 = 0) e_e "]), |
929 ("#Find" ,["solutions v_i"]) |
929 ("#Find" ,["solutions v_i'''"]) |
930 ], |
930 ], |
931 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
931 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
932 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); |
932 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); |
933 |
933 |
934 store_pbt |
934 store_pbt |
935 (prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID |
935 (prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID |
936 (["pqFormula","degree_2","polynomial","univariate","equation"], |
936 (["pqFormula","degree_2","polynomial","univariate","equation"], |
937 [("#Given" ,["equality e_e","solveFor v_v"]), |
937 [("#Given" ,["equality e_e","solveFor v_v"]), |
938 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^ |
938 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^ |
939 "matches (?a + ?v_^^^2 = 0) e_e"]), |
939 "matches (?a + ?v_^^^2 = 0) e_e"]), |
940 ("#Find" ,["solutions v_i"]) |
940 ("#Find" ,["solutions v_i'''"]) |
941 ], |
941 ], |
942 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
942 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
943 [["PolyEq","solve_d2_polyeq_pq_equation"]])); |
943 [["PolyEq","solve_d2_polyeq_pq_equation"]])); |
944 |
944 |
945 store_pbt |
945 store_pbt |
946 (prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID |
946 (prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID |
947 (["abcFormula","degree_2","polynomial","univariate","equation"], |
947 (["abcFormula","degree_2","polynomial","univariate","equation"], |
948 [("#Given" ,["equality e_e","solveFor v_v"]), |
948 [("#Given" ,["equality e_e","solveFor v_v"]), |
949 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^ |
949 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^ |
950 "matches (?a + ?b*?v_^^^2 = 0) e_e"]), |
950 "matches (?a + ?b*?v_^^^2 = 0) e_e"]), |
951 ("#Find" ,["solutions v_i"]) |
951 ("#Find" ,["solutions v_i'''"]) |
952 ], |
952 ], |
953 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
953 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
954 [["PolyEq","solve_d2_polyeq_abc_equation"]])); |
954 [["PolyEq","solve_d2_polyeq_abc_equation"]])); |
955 *} |
955 *} |
956 ML{* |
956 ML{* |
960 (["degree_3","polynomial","univariate","equation"], |
960 (["degree_3","polynomial","univariate","equation"], |
961 [("#Given" ,["equality e_e","solveFor v_v"]), |
961 [("#Given" ,["equality e_e","solveFor v_v"]), |
962 ("#Where" ,["matches (?a = 0) e_e", |
962 ("#Where" ,["matches (?a = 0) e_e", |
963 "(lhs e_e) is_poly_in v_v ", |
963 "(lhs e_e) is_poly_in v_v ", |
964 "((lhs e_e) has_degree_in v_v) = 3"]), |
964 "((lhs e_e) has_degree_in v_v) = 3"]), |
965 ("#Find" ,["solutions v_i"]) |
965 ("#Find" ,["solutions v_i'''"]) |
966 ], |
966 ], |
967 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
967 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
968 [["PolyEq","solve_d3_polyeq_equation"]])); |
968 [["PolyEq","solve_d3_polyeq_equation"]])); |
969 |
969 |
970 (*--- d4 ---*) |
970 (*--- d4 ---*) |
973 (["degree_4","polynomial","univariate","equation"], |
973 (["degree_4","polynomial","univariate","equation"], |
974 [("#Given" ,["equality e_e","solveFor v_v"]), |
974 [("#Given" ,["equality e_e","solveFor v_v"]), |
975 ("#Where" ,["matches (?a = 0) e_e", |
975 ("#Where" ,["matches (?a = 0) e_e", |
976 "(lhs e_e) is_poly_in v_v ", |
976 "(lhs e_e) is_poly_in v_v ", |
977 "((lhs e_e) has_degree_in v_v) = 4"]), |
977 "((lhs e_e) has_degree_in v_v) = 4"]), |
978 ("#Find" ,["solutions v_i"]) |
978 ("#Find" ,["solutions v_i'''"]) |
979 ], |
979 ], |
980 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
980 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
981 [(*["PolyEq","solve_d4_polyeq_equation"]*)])); |
981 [(*["PolyEq","solve_d4_polyeq_equation"]*)])); |
982 |
982 |
983 (*--- normalize ---*) |
983 (*--- normalize ---*) |
985 (prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID |
985 (prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID |
986 (["normalize","polynomial","univariate","equation"], |
986 (["normalize","polynomial","univariate","equation"], |
987 [("#Given" ,["equality e_e","solveFor v_v"]), |
987 [("#Given" ,["equality e_e","solveFor v_v"]), |
988 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ |
988 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ |
989 "(Not(((lhs e_e) is_poly_in v_v)))"]), |
989 "(Not(((lhs e_e) is_poly_in v_v)))"]), |
990 ("#Find" ,["solutions v_i"]) |
990 ("#Find" ,["solutions v_i'''"]) |
991 ], |
991 ], |
992 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
992 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
993 [["PolyEq","normalize_poly"]])); |
993 [["PolyEq","normalize_poly"]])); |
994 (*-------------------------expanded-----------------------*) |
994 (*-------------------------expanded-----------------------*) |
995 store_pbt |
995 store_pbt |
996 (prep_pbt thy "pbl_equ_univ_expand" [] e_pblID |
996 (prep_pbt thy "pbl_equ_univ_expand" [] e_pblID |
997 (["expanded","univariate","equation"], |
997 (["expanded","univariate","equation"], |
998 [("#Given" ,["equality e_e","solveFor v_v"]), |
998 [("#Given" ,["equality e_e","solveFor v_v"]), |
999 ("#Where" ,["matches (?a = 0) e_e", |
999 ("#Where" ,["matches (?a = 0) e_e", |
1000 "(lhs e_e) is_expanded_in v_v "]), |
1000 "(lhs e_e) is_expanded_in v_v "]), |
1001 ("#Find" ,["solutions v_i"]) |
1001 ("#Find" ,["solutions v_i'''"]) |
1002 ], |
1002 ], |
1003 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
1003 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
1004 [])); |
1004 [])); |
1005 |
1005 |
1006 (*--- d2 ---*) |
1006 (*--- d2 ---*) |
1007 store_pbt |
1007 store_pbt |
1008 (prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID |
1008 (prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID |
1009 (["degree_2","expanded","univariate","equation"], |
1009 (["degree_2","expanded","univariate","equation"], |
1010 [("#Given" ,["equality e_e","solveFor v_v"]), |
1010 [("#Given" ,["equality e_e","solveFor v_v"]), |
1011 ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]), |
1011 ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]), |
1012 ("#Find" ,["solutions v_i"]) |
1012 ("#Find" ,["solutions v_i'''"]) |
1013 ], |
1013 ], |
1014 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
1014 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
1015 [["PolyEq","complete_square"]])); |
1015 [["PolyEq","complete_square"]])); |
1016 |
1016 |
1017 *} |
1017 *} |
1041 (prep_met thy "met_polyeq_norm" [] e_metID |
1041 (prep_met thy "met_polyeq_norm" [] e_metID |
1042 (["PolyEq","normalize_poly"], |
1042 (["PolyEq","normalize_poly"], |
1043 [("#Given" ,["equality e_e","solveFor v_v"]), |
1043 [("#Given" ,["equality e_e","solveFor v_v"]), |
1044 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ |
1044 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^ |
1045 "(Not(((lhs e_e) is_poly_in v_v)))"]), |
1045 "(Not(((lhs e_e) is_poly_in v_v)))"]), |
1046 ("#Find" ,["solutions v_i"]) |
1046 ("#Find" ,["solutions v_i'''"]) |
1047 ], |
1047 ], |
1048 {rew_ord'="termlessI", |
1048 {rew_ord'="termlessI", |
1049 rls'=PolyEq_erls, |
1049 rls'=PolyEq_erls, |
1050 srls=e_rls, |
1050 srls=e_rls, |
1051 prls=PolyEq_prls, |
1051 prls=PolyEq_prls, |
1068 (prep_met thy "met_polyeq_d0" [] e_metID |
1068 (prep_met thy "met_polyeq_d0" [] e_metID |
1069 (["PolyEq","solve_d0_polyeq_equation"], |
1069 (["PolyEq","solve_d0_polyeq_equation"], |
1070 [("#Given" ,["equality e_e","solveFor v_v"]), |
1070 [("#Given" ,["equality e_e","solveFor v_v"]), |
1071 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1071 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1072 "((lhs e_e) has_degree_in v_v) = 0"]), |
1072 "((lhs e_e) has_degree_in v_v) = 0"]), |
1073 ("#Find" ,["solutions v_i"]) |
1073 ("#Find" ,["solutions v_i'''"]) |
1074 ], |
1074 ], |
1075 {rew_ord'="termlessI", |
1075 {rew_ord'="termlessI", |
1076 rls'=PolyEq_erls, |
1076 rls'=PolyEq_erls, |
1077 srls=e_rls, |
1077 srls=e_rls, |
1078 prls=PolyEq_prls, |
1078 prls=PolyEq_prls, |
1089 (prep_met thy "met_polyeq_d1" [] e_metID |
1089 (prep_met thy "met_polyeq_d1" [] e_metID |
1090 (["PolyEq","solve_d1_polyeq_equation"], |
1090 (["PolyEq","solve_d1_polyeq_equation"], |
1091 [("#Given" ,["equality e_e","solveFor v_v"]), |
1091 [("#Given" ,["equality e_e","solveFor v_v"]), |
1092 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1092 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1093 "((lhs e_e) has_degree_in v_v) = 1"]), |
1093 "((lhs e_e) has_degree_in v_v) = 1"]), |
1094 ("#Find" ,["solutions v_i"]) |
1094 ("#Find" ,["solutions v_i'''"]) |
1095 ], |
1095 ], |
1096 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, |
1096 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, |
1097 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1097 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1098 crls=PolyEq_crls, nrls=norm_Rational}, |
1098 crls=PolyEq_crls, nrls=norm_Rational}, |
1099 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1099 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^ |
1110 (prep_met thy "met_polyeq_d22" [] e_metID |
1110 (prep_met thy "met_polyeq_d22" [] e_metID |
1111 (["PolyEq","solve_d2_polyeq_equation"], |
1111 (["PolyEq","solve_d2_polyeq_equation"], |
1112 [("#Given" ,["equality e_e","solveFor v_v"]), |
1112 [("#Given" ,["equality e_e","solveFor v_v"]), |
1113 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1113 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1114 "((lhs e_e) has_degree_in v_v) = 2"]), |
1114 "((lhs e_e) has_degree_in v_v) = 2"]), |
1115 ("#Find" ,["solutions v_i"]) |
1115 ("#Find" ,["solutions v_i'''"]) |
1116 ], |
1116 ], |
1117 {rew_ord'="termlessI", |
1117 {rew_ord'="termlessI", |
1118 rls'=PolyEq_erls, |
1118 rls'=PolyEq_erls, |
1119 srls=e_rls, |
1119 srls=e_rls, |
1120 prls=PolyEq_prls, |
1120 prls=PolyEq_prls, |
1137 (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID |
1137 (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID |
1138 (["PolyEq","solve_d2_polyeq_bdvonly_equation"], |
1138 (["PolyEq","solve_d2_polyeq_bdvonly_equation"], |
1139 [("#Given" ,["equality e_e","solveFor v_v"]), |
1139 [("#Given" ,["equality e_e","solveFor v_v"]), |
1140 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1140 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1141 "((lhs e_e) has_degree_in v_v) = 2"]), |
1141 "((lhs e_e) has_degree_in v_v) = 2"]), |
1142 ("#Find" ,["solutions v_i"]) |
1142 ("#Find" ,["solutions v_i'''"]) |
1143 ], |
1143 ], |
1144 {rew_ord'="termlessI", |
1144 {rew_ord'="termlessI", |
1145 rls'=PolyEq_erls, |
1145 rls'=PolyEq_erls, |
1146 srls=e_rls, |
1146 srls=e_rls, |
1147 prls=PolyEq_prls, |
1147 prls=PolyEq_prls, |
1164 (prep_met thy "met_polyeq_d2_sqonly" [] e_metID |
1164 (prep_met thy "met_polyeq_d2_sqonly" [] e_metID |
1165 (["PolyEq","solve_d2_polyeq_sqonly_equation"], |
1165 (["PolyEq","solve_d2_polyeq_sqonly_equation"], |
1166 [("#Given" ,["equality e_e","solveFor v_v"]), |
1166 [("#Given" ,["equality e_e","solveFor v_v"]), |
1167 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1167 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1168 "((lhs e_e) has_degree_in v_v) = 2"]), |
1168 "((lhs e_e) has_degree_in v_v) = 2"]), |
1169 ("#Find" ,["solutions v_i"]) |
1169 ("#Find" ,["solutions v_i'''"]) |
1170 ], |
1170 ], |
1171 {rew_ord'="termlessI", |
1171 {rew_ord'="termlessI", |
1172 rls'=PolyEq_erls, |
1172 rls'=PolyEq_erls, |
1173 srls=e_rls, |
1173 srls=e_rls, |
1174 prls=PolyEq_prls, |
1174 prls=PolyEq_prls, |
1188 (prep_met thy "met_polyeq_d2_pq" [] e_metID |
1188 (prep_met thy "met_polyeq_d2_pq" [] e_metID |
1189 (["PolyEq","solve_d2_polyeq_pq_equation"], |
1189 (["PolyEq","solve_d2_polyeq_pq_equation"], |
1190 [("#Given" ,["equality e_e","solveFor v_v"]), |
1190 [("#Given" ,["equality e_e","solveFor v_v"]), |
1191 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1191 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1192 "((lhs e_e) has_degree_in v_v) = 2"]), |
1192 "((lhs e_e) has_degree_in v_v) = 2"]), |
1193 ("#Find" ,["solutions v_i"]) |
1193 ("#Find" ,["solutions v_i'''"]) |
1194 ], |
1194 ], |
1195 {rew_ord'="termlessI", |
1195 {rew_ord'="termlessI", |
1196 rls'=PolyEq_erls, |
1196 rls'=PolyEq_erls, |
1197 srls=e_rls, |
1197 srls=e_rls, |
1198 prls=PolyEq_prls, |
1198 prls=PolyEq_prls, |
1212 (prep_met thy "met_polyeq_d2_abc" [] e_metID |
1212 (prep_met thy "met_polyeq_d2_abc" [] e_metID |
1213 (["PolyEq","solve_d2_polyeq_abc_equation"], |
1213 (["PolyEq","solve_d2_polyeq_abc_equation"], |
1214 [("#Given" ,["equality e_e","solveFor v_v"]), |
1214 [("#Given" ,["equality e_e","solveFor v_v"]), |
1215 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1215 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1216 "((lhs e_e) has_degree_in v_v) = 2"]), |
1216 "((lhs e_e) has_degree_in v_v) = 2"]), |
1217 ("#Find" ,["solutions v_i"]) |
1217 ("#Find" ,["solutions v_i'''"]) |
1218 ], |
1218 ], |
1219 {rew_ord'="termlessI", |
1219 {rew_ord'="termlessI", |
1220 rls'=PolyEq_erls, |
1220 rls'=PolyEq_erls, |
1221 srls=e_rls, |
1221 srls=e_rls, |
1222 prls=PolyEq_prls, |
1222 prls=PolyEq_prls, |
1236 (prep_met thy "met_polyeq_d3" [] e_metID |
1236 (prep_met thy "met_polyeq_d3" [] e_metID |
1237 (["PolyEq","solve_d3_polyeq_equation"], |
1237 (["PolyEq","solve_d3_polyeq_equation"], |
1238 [("#Given" ,["equality e_e","solveFor v_v"]), |
1238 [("#Given" ,["equality e_e","solveFor v_v"]), |
1239 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1239 ("#Where" ,["(lhs e_e) is_poly_in v_v ", |
1240 "((lhs e_e) has_degree_in v_v) = 3"]), |
1240 "((lhs e_e) has_degree_in v_v) = 3"]), |
1241 ("#Find" ,["solutions v_i"]) |
1241 ("#Find" ,["solutions v_i'''"]) |
1242 ], |
1242 ], |
1243 {rew_ord'="termlessI", |
1243 {rew_ord'="termlessI", |
1244 rls'=PolyEq_erls, |
1244 rls'=PolyEq_erls, |
1245 srls=e_rls, |
1245 srls=e_rls, |
1246 prls=PolyEq_prls, |
1246 prls=PolyEq_prls, |
1269 (prep_met thy "met_polyeq_complsq" [] e_metID |
1269 (prep_met thy "met_polyeq_complsq" [] e_metID |
1270 (["PolyEq","complete_square"], |
1270 (["PolyEq","complete_square"], |
1271 [("#Given" ,["equality e_e","solveFor v_v"]), |
1271 [("#Given" ,["equality e_e","solveFor v_v"]), |
1272 ("#Where" ,["matches (?a = 0) e_e", |
1272 ("#Where" ,["matches (?a = 0) e_e", |
1273 "((lhs e_e) has_degree_in v_v) = 2"]), |
1273 "((lhs e_e) has_degree_in v_v) = 2"]), |
1274 ("#Find" ,["solutions v_i"]) |
1274 ("#Find" ,["solutions v_i'''"]) |
1275 ], |
1275 ], |
1276 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
1276 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
1277 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1277 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], |
1278 crls=PolyEq_crls, nrls=norm_Rational}, |
1278 crls=PolyEq_crls, nrls=norm_Rational}, |
1279 "Script Complete_square (e_e::bool) (v_v::real) = " ^ |
1279 "Script Complete_square (e_e::bool) (v_v::real) = " ^ |