637 Find: "solutions v_v'i'" |
637 Find: "solutions v_v'i'" |
638 |
638 |
639 (*--- d0 ---*) |
639 (*--- d0 ---*) |
640 problem pbl_equ_univ_poly_deg0 : "degree_0/polynomial/univariate/equation" = |
640 problem pbl_equ_univ_poly_deg0 : "degree_0/polynomial/univariate/equation" = |
641 \<open>PolyEq_prls\<close> |
641 \<open>PolyEq_prls\<close> |
642 Method: "PolyEq/solve_d0_polyeq_equation" |
642 Method_Ref: "PolyEq/solve_d0_polyeq_equation" |
643 CAS: "solve (e_e::bool, v_v)" |
643 CAS: "solve (e_e::bool, v_v)" |
644 Given: "equality e_e" "solveFor v_v" |
644 Given: "equality e_e" "solveFor v_v" |
645 Where: |
645 Where: |
646 "matches (?a = 0) e_e" |
646 "matches (?a = 0) e_e" |
647 "(lhs e_e) is_poly_in v_v" |
647 "(lhs e_e) is_poly_in v_v" |
649 Find: "solutions v_v'i'" |
649 Find: "solutions v_v'i'" |
650 |
650 |
651 (*--- d1 ---*) |
651 (*--- d1 ---*) |
652 problem pbl_equ_univ_poly_deg1 : "degree_1/polynomial/univariate/equation" = |
652 problem pbl_equ_univ_poly_deg1 : "degree_1/polynomial/univariate/equation" = |
653 \<open>PolyEq_prls\<close> |
653 \<open>PolyEq_prls\<close> |
654 Method: "PolyEq/solve_d1_polyeq_equation" |
654 Method_Ref: "PolyEq/solve_d1_polyeq_equation" |
655 CAS: "solve (e_e::bool, v_v)" |
655 CAS: "solve (e_e::bool, v_v)" |
656 Given: "equality e_e" "solveFor v_v" |
656 Given: "equality e_e" "solveFor v_v" |
657 Where: |
657 Where: |
658 "matches (?a = 0) e_e" |
658 "matches (?a = 0) e_e" |
659 "(lhs e_e) is_poly_in v_v" |
659 "(lhs e_e) is_poly_in v_v" |
661 Find: "solutions v_v'i'" |
661 Find: "solutions v_v'i'" |
662 |
662 |
663 (*--- d2 ---*) |
663 (*--- d2 ---*) |
664 problem pbl_equ_univ_poly_deg2 : "degree_2/polynomial/univariate/equation" = |
664 problem pbl_equ_univ_poly_deg2 : "degree_2/polynomial/univariate/equation" = |
665 \<open>PolyEq_prls\<close> |
665 \<open>PolyEq_prls\<close> |
666 Method: "PolyEq/solve_d2_polyeq_equation" |
666 Method_Ref: "PolyEq/solve_d2_polyeq_equation" |
667 CAS: "solve (e_e::bool, v_v)" |
667 CAS: "solve (e_e::bool, v_v)" |
668 Given: "equality e_e" "solveFor v_v" |
668 Given: "equality e_e" "solveFor v_v" |
669 Where: |
669 Where: |
670 "matches (?a = 0) e_e" |
670 "matches (?a = 0) e_e" |
671 "(lhs e_e) is_poly_in v_v " |
671 "(lhs e_e) is_poly_in v_v " |
672 "((lhs e_e) has_degree_in v_v ) = 2" |
672 "((lhs e_e) has_degree_in v_v ) = 2" |
673 Find: "solutions v_v'i'" |
673 Find: "solutions v_v'i'" |
674 |
674 |
675 problem pbl_equ_univ_poly_deg2_sqonly : "sq_only/degree_2/polynomial/univariate/equation" = |
675 problem pbl_equ_univ_poly_deg2_sqonly : "sq_only/degree_2/polynomial/univariate/equation" = |
676 \<open>PolyEq_prls\<close> |
676 \<open>PolyEq_prls\<close> |
677 Method: "PolyEq/solve_d2_polyeq_sqonly_equation" |
677 Method_Ref: "PolyEq/solve_d2_polyeq_sqonly_equation" |
678 CAS: "solve (e_e::bool, v_v)" |
678 CAS: "solve (e_e::bool, v_v)" |
679 Given: "equality e_e" "solveFor v_v" |
679 Given: "equality e_e" "solveFor v_v" |
680 Where: |
680 Where: |
681 "matches ( ?a + ?v_ \<up> 2 = 0) e_e | |
681 "matches ( ?a + ?v_ \<up> 2 = 0) e_e | |
682 matches ( ?a + ?b*?v_ \<up> 2 = 0) e_e | |
682 matches ( ?a + ?b*?v_ \<up> 2 = 0) e_e | |
692 Not (matches ( ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e)" |
692 Not (matches ( ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e)" |
693 Find: "solutions v_v'i'" |
693 Find: "solutions v_v'i'" |
694 |
694 |
695 problem pbl_equ_univ_poly_deg2_bdvonly : "bdv_only/degree_2/polynomial/univariate/equation" = |
695 problem pbl_equ_univ_poly_deg2_bdvonly : "bdv_only/degree_2/polynomial/univariate/equation" = |
696 \<open>PolyEq_prls\<close> |
696 \<open>PolyEq_prls\<close> |
697 Method: "PolyEq/solve_d2_polyeq_bdvonly_equation" |
697 Method_Ref: "PolyEq/solve_d2_polyeq_bdvonly_equation" |
698 CAS: "solve (e_e::bool, v_v)" |
698 CAS: "solve (e_e::bool, v_v)" |
699 Given: "equality e_e" "solveFor v_v" |
699 Given: "equality e_e" "solveFor v_v" |
700 Where: |
700 Where: |
701 "matches (?a*?v_ + ?v_ \<up> 2 = 0) e_e | |
701 "matches (?a*?v_ + ?v_ \<up> 2 = 0) e_e | |
702 matches ( ?v_ + ?v_ \<up> 2 = 0) e_e | |
702 matches ( ?v_ + ?v_ \<up> 2 = 0) e_e | |
706 matches ( ?b*?v_ \<up> 2 = 0) e_e " |
706 matches ( ?b*?v_ \<up> 2 = 0) e_e " |
707 Find: "solutions v_v'i'" |
707 Find: "solutions v_v'i'" |
708 |
708 |
709 problem pbl_equ_univ_poly_deg2_pq : "pqFormula/degree_2/polynomial/univariate/equation" = |
709 problem pbl_equ_univ_poly_deg2_pq : "pqFormula/degree_2/polynomial/univariate/equation" = |
710 \<open>PolyEq_prls\<close> |
710 \<open>PolyEq_prls\<close> |
711 Method: "PolyEq/solve_d2_polyeq_pq_equation" |
711 Method_Ref: "PolyEq/solve_d2_polyeq_pq_equation" |
712 CAS: "solve (e_e::bool, v_v)" |
712 CAS: "solve (e_e::bool, v_v)" |
713 Given: "equality e_e" "solveFor v_v" |
713 Given: "equality e_e" "solveFor v_v" |
714 Where: |
714 Where: |
715 "matches (?a + 1*?v_ \<up> 2 = 0) e_e | |
715 "matches (?a + 1*?v_ \<up> 2 = 0) e_e | |
716 matches (?a + ?v_ \<up> 2 = 0) e_e" |
716 matches (?a + ?v_ \<up> 2 = 0) e_e" |
717 Find: "solutions v_v'i'" |
717 Find: "solutions v_v'i'" |
718 |
718 |
719 problem pbl_equ_univ_poly_deg2_abc : "abcFormula/degree_2/polynomial/univariate/equation" = |
719 problem pbl_equ_univ_poly_deg2_abc : "abcFormula/degree_2/polynomial/univariate/equation" = |
720 \<open>PolyEq_prls\<close> |
720 \<open>PolyEq_prls\<close> |
721 Method: "PolyEq/solve_d2_polyeq_abc_equation" |
721 Method_Ref: "PolyEq/solve_d2_polyeq_abc_equation" |
722 CAS: "solve (e_e::bool, v_v)" |
722 CAS: "solve (e_e::bool, v_v)" |
723 Given: "equality e_e" "solveFor v_v" |
723 Given: "equality e_e" "solveFor v_v" |
724 Where: |
724 Where: |
725 "matches (?a + ?v_ \<up> 2 = 0) e_e | |
725 "matches (?a + ?v_ \<up> 2 = 0) e_e | |
726 matches (?a + ?b*?v_ \<up> 2 = 0) e_e" |
726 matches (?a + ?b*?v_ \<up> 2 = 0) e_e" |
727 Find: "solutions v_v'i'" |
727 Find: "solutions v_v'i'" |
728 |
728 |
729 (*--- d3 ---*) |
729 (*--- d3 ---*) |
730 problem pbl_equ_univ_poly_deg3 : "degree_3/polynomial/univariate/equation" = |
730 problem pbl_equ_univ_poly_deg3 : "degree_3/polynomial/univariate/equation" = |
731 \<open>PolyEq_prls\<close> |
731 \<open>PolyEq_prls\<close> |
732 Method: "PolyEq/solve_d3_polyeq_equation" |
732 Method_Ref: "PolyEq/solve_d3_polyeq_equation" |
733 CAS: "solve (e_e::bool, v_v)" |
733 CAS: "solve (e_e::bool, v_v)" |
734 Given: "equality e_e" "solveFor v_v" |
734 Given: "equality e_e" "solveFor v_v" |
735 Where: |
735 Where: |
736 "matches (?a = 0) e_e" |
736 "matches (?a = 0) e_e" |
737 "(lhs e_e) is_poly_in v_v" |
737 "(lhs e_e) is_poly_in v_v" |
751 Find: "solutions v_v'i'" |
751 Find: "solutions v_v'i'" |
752 |
752 |
753 (*--- normalise ---*) |
753 (*--- normalise ---*) |
754 problem pbl_equ_univ_poly_norm : "normalise/polynomial/univariate/equation" = |
754 problem pbl_equ_univ_poly_norm : "normalise/polynomial/univariate/equation" = |
755 \<open>PolyEq_prls\<close> |
755 \<open>PolyEq_prls\<close> |
756 Method: "PolyEq/normalise_poly" |
756 Method_Ref: "PolyEq/normalise_poly" |
757 CAS: "solve (e_e::bool, v_v)" |
757 CAS: "solve (e_e::bool, v_v)" |
758 Given: "equality e_e" "solveFor v_v" |
758 Given: "equality e_e" "solveFor v_v" |
759 Where: |
759 Where: |
760 "(Not((matches (?a = 0 ) e_e ))) | |
760 "(Not((matches (?a = 0 ) e_e ))) | |
761 (Not(((lhs e_e) is_poly_in v_v)))" |
761 (Not(((lhs e_e) is_poly_in v_v)))" |
772 Find: "solutions v_v'i'" |
772 Find: "solutions v_v'i'" |
773 |
773 |
774 (*--- d2 ---*) |
774 (*--- d2 ---*) |
775 problem pbl_equ_univ_expand_deg2 : "degree_2/expanded/univariate/equation" = |
775 problem pbl_equ_univ_expand_deg2 : "degree_2/expanded/univariate/equation" = |
776 \<open>PolyEq_prls\<close> |
776 \<open>PolyEq_prls\<close> |
777 Method: "PolyEq/complete_square" |
777 Method_Ref: "PolyEq/complete_square" |
778 CAS: "solve (e_e::bool, v_v)" |
778 CAS: "solve (e_e::bool, v_v)" |
779 Given: "equality e_e" "solveFor v_v" |
779 Given: "equality e_e" "solveFor v_v" |
780 Where: "((lhs e_e) has_degree_in v_v) = 2" |
780 Where: "((lhs e_e) has_degree_in v_v) = 2" |
781 Find: "solutions v_v'i'" |
781 Find: "solutions v_v'i'" |
782 |
782 |