%mathpiper,def="RulebaseElementaryAlgebra"
{
RulebaseHoldArguments("RulebaseElementaryAlgebra", []);
Local(ruleName, rule);
?rulebaseElementaryAlgebra := [];
Constant('MOVE?RIGHTMOST, True);
Constant('HIGHER?UNKNOWNS, True);
Constant('CLOSER?UNKNOWNS?PATH, True);
Constant('CLOSER?UNKNOWNS?HORIZONTAL, True);
Constant('MAKE?COEFFICIENT?EXPLICIT, True);
Constant('ELIMINATE?UNKNOWN, True);
Constant('OTHERSIDE, True);
Constant('REMOVE?DENOMINATORS, True);
Constant('TEXTBOOK, True);
Constant('INTRODUCE, True);
Constant('ELIMINATE, True);
Constant('UNDEFINE?UNARY?MINUS, True);
Constant('UNDEFINE?BINARY?MINUS, True);
// ================================ Manual
ruleName := "Arithmetic";
rule := [];
rule["RuleName"] := ruleName;
rule["Head"] := '( q_ );
rule["Guard"] := ''( CanEvaluate?(q) );
rule["Body"] := ''( EvaluateDo(q) );
rule["DescriptionObjectLevel"] := "Arithmetic";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 3;
rule["HeadLatex"] := "q\\_";
rule["BodyLatex"] := "Evaluate(q)";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Commute +";
rule := [];
rule["RuleName"] := ruleName;
rule["Head"] := '( q_ +$ r_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( r +$ q );
rule["DescriptionObjectLevel"] := "Commute the operands of a + operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 4;
rule["HeadLatex"] := "q\\_ \\textcolor{green}{+} r\\_";
rule["BodyLatex"] := "r + q";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Commute *";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [MOVE?RIGHTMOST];
rule["Head"] := '( q_ *$ r_ );
rule["Guard"] := ''( q =? _unknown &? r !=? _unknown |? UnderscoreConstant?(q) &? Number?(r));
rule["Body"] := ''( r *$ q );
rule["DescriptionObjectLevel"] := "Commute the operands of a * operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 5;
rule["HeadLatex"] := "q\\_ \\textcolor{green}{*} r\\_";
rule["BodyLatex"] := "r * q";
?rulebaseElementaryAlgebra[ruleName] := rule;
/*
// Maybe rules like this can be proved and added by the user?
ruleName := "Commute * * *";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [MOVE?RIGHTMOST];
rule["Head"] := '( (q_ *$ r_) *$ (s_ *$ t_) );
rule["Guard"] := ''( r =? _unknown &? s !=? _unknown |? UnderscoreConstant?(r) &? Number?(s));
rule["Body"] := ''( (q *$ s) *$ (r *$ t) );
rule["DescriptionObjectLevel"] := "Commute the operands of a * operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 5.5;
rule["HeadLatex"] := "(q\\_ * r\\_) \\textcolor{green}{*} (s\\_ * t\\_)";
rule["BodyLatex"] := "(q * s) * (r * t)";
?rulebaseElementaryAlgebra[ruleName] := rule;
*/
ruleName := "Commute =";
rule := [];
rule["RuleName"] := ruleName;
rule["Head"] := '( q_ ==$ r_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( r ==$ q );
rule["DescriptionObjectLevel"] := "Commute the operands of an = operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 6;
rule["HeadLatex"] := "q\\_ \\textcolor{green}{=} r\\_";
rule["BodyLatex"] := "r = q";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Otherside 1 [=]";
rule := [];
rule["RuleName"] := ruleName;
rule["Head"] := '( q_ ==$ r_ );
rule["Guard"] := ''( Function?(q) &? Length(q) >? 1 );
rule["Body"] := ''( Otherside(1, q ==$ r) );
rule["DescriptionObjectLevel"] := "Move a subexpression to right side of the = operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 7;
rule["HeadLatex"] := "q\\_ \\ \\textcolor{ProcessBlue}{op}\\ \\textcolor{orange}{r\\_} \\textcolor{green}{=} s\\_";
rule["BodyLatex"] := "q = s \\ antiop\\ r";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Otherside 2 [=]";
rule := [];
rule["RuleName"] := ruleName;
rule["Head"] := '( q_ ==$ r_ );
rule["Guard"] := ''( Function?(q) &? Length(q) >? 1 );
rule["Body"] := ''( Otherside(2, q ==$ r) );
rule["DescriptionObjectLevel"] := "Move a subexpression to right side of the = operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 8;
rule["HeadLatex"] := "\\textcolor{orange}{q\\_} \\ \\textcolor{ProcessBlue}{op}\\ r\\_ \\textcolor{green}{=} s\\_";
rule["BodyLatex"] := "r = s \\ antiop\\ q";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Make Coefficient Explicit";
rule := [];
rule["RuleName"] := ruleName;
rule["Head"] := '( q_UnderscoreConstant? );
rule["Body"] := ''( 1 *$ q );
rule["DescriptionObjectLevel"] := "Make a coefficient explicit.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 20;
rule["HeadLatex"] := "q\\_";
rule["BodyLatex"] := "1*q";
?rulebaseElementaryAlgebra[ruleName] := rule;
// ================================ Manual and automatic
ruleName := "Otherside RHS";
rule := [];
rule["RuleName"] := ruleName;
rule["Head"] := '(q_ ==$ r_);
rule["Body"] := ''(q -$ r ==$ 0);
rule["DescriptionObjectLevel"] := ''("Subtract " ~ r ~ " from both sides.");
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 9;
rule["HeadLatex"] := "q\\_ \\textcolor{green}{=} \\textcolor{orange}{r\\_}";
rule["BodyLatex"] := "q - r = 0";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Undefine -q_";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [UNDEFINE?UNARY?MINUS];
rule["Head"] := -$ q_;
rule["Guard"] := ''( True );
rule["Body"] := ''(SubtractN(0,1) *$ q);
rule["DescriptionObjectLevel"] := "Undefine a negation operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 1;
rule["HeadLatex"] := "\\textcolor{green}{-} q\\_";
rule["BodyLatex"] := "-1 * q";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Undefine q_ - r_";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [UNDEFINE?BINARY?MINUS];
rule["Head"] := q_ -$ r_;
rule["Body"] := ''(q +$ SubtractN(0,1) *$ r);
rule["Guard"] := ''( ??position =? [] |? ??position[1] =? 1 ); // Either the expression is not an equation or the match is in the LHS.
rule["DescriptionObjectLevel"] := "Undefine a binary '-' operator.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 2;
rule["HeadLatex"] := "q\\_ \\textcolor{green}{-} r\\_";
rule["BodyLatex"] := "q + -1 * r";
?rulebaseElementaryAlgebra[ruleName] := rule;
// ---------------------------------------------
ruleName := "Higher Unknowns 1";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [HIGHER?UNKNOWNS];
rule["Head"] := '( q_ *$ (r_ +$ s_) );
rule["Guard"] := ''( OccurrencesCount(r, _unknown) !=? 0 |? OccurrencesCount(s, _unknown) !=? 0);
rule["Body"] := ''( q *$ r +$ q *$ s );
rule["DescriptionObjectLevel"] := "Move occurrences of the unknown higher.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 18;
rule["HeadLatex"] := "q\\_ \\textcolor{green}{*} (r\\_ + s\\_)";
rule["BodyLatex"] := "q * r + q * s";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Higher Unknowns 2";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [HIGHER?UNKNOWNS];
rule["Head"] := '( ( q_ *$ r_) /$ s_ );
rule["Guard"] := ''( OccurrencesCount(r, _unknown) !=? 0 );
rule["Body"] := ''( ( q /$ s ) *$ r );
rule["DescriptionObjectLevel"] := "Move occurrences of the unknown higher.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 19;
rule["HeadLatex"] := "(q\\_ * r\\_) \\textcolor{green}{/} s\\_";
rule["BodyLatex"] := "(q / s) * r";
?rulebaseElementaryAlgebra[ruleName] := rule;
// --------------------------------------------
ruleName := "Closer Unknowns (r_, s_) [+ +]";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [CLOSER?UNKNOWNS?PATH];
rule["Head"] := '( (q_ +$ r_) +$ s_ );
rule["Body"] := ''( q +$ (r +$ s) );
rule["DescriptionGuard"] := "TwoCopiesOfTheUnknownWillBecomeCloserAlongAPath?()"; // Only used by CLOSER?UNKNOWNS?PATH.
rule["DescriptionObjectLevel"] := "Change the association of + operators.";
rule["DescriptionMetaLevel"] := "Move two copies of the unknown closer to each other along a path.";
rule["ManualSequence"] := 14;
rule["HeadLatex"] := "(q\\_ + \\textcolor{orange}{r\\_}) \\textcolor{green}{+} \\textcolor{orange}{s\\_}";
rule["BodyLatex"] := "q + (r + s)";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Closer Unknowns (q_, r_) [+ +]";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [CLOSER?UNKNOWNS?PATH];
rule["Head"] := '(q_ +$ (r_ +$ s_));
rule["Body"] := ''( (q +$ r) +$ s );
rule["DescriptionGuard"] := "TwoCopiesOfTheUnknownWillBecomeCloserAlongAPath?()"; // Only used by CLOSER?UNKNOWNS?PATH.
rule["DescriptionObjectLevel"] := "Change the association of + operators.";
rule["DescriptionMetaLevel"] := "Move two copies of the unknown closer to each other along a path.";
rule["ManualSequence"] := 15;
rule["HeadLatex"] := "\\textcolor{orange}{q\\_} \\textcolor{green}{+} (\\textcolor{orange}{r\\_} + s\\_)";
rule["BodyLatex"] := "(q + r) + s";
?rulebaseElementaryAlgebra[ruleName] := rule;
// --------------------------------------------
ruleName := "Closer Unknowns (r_, s_) [* *]";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [CLOSER?UNKNOWNS?PATH]; //, MOVE?RIGHTMOST
rule["Head"] := '( (q_ *$ r_) *$ s_ );
rule["Guard"] := ''( r =? _unknown ); // Only used by MOVE?RIGHTMOST.
rule["Body"] := ''( q *$ (r *$ s) );
rule["DescriptionGuard"] := "TwoCopiesOfTheUnknownWillBecomeCloserAlongAPath?()"; // Only used by CLOSER?UNKNOWNS?PATH.
rule["DescriptionObjectLevel"] := "Change the association of * operators.";
rule["DescriptionMetaLevel"] := "Move two copies of the unknown closer to each other along a path.";
rule["ManualSequence"] := 16;
rule["HeadLatex"] := "(q\\_ * \\textcolor{orange}{r\\_}) \\textcolor{green}{*} \\textcolor{orange}{s\\_}";
rule["BodyLatex"] := "q * (r * s)";
// rule["DescriptionObjectLevel"] := "Move an copy of the unknown left or right.";
// rule["DescriptionMetaLevel"] := "Move an copy of the unknown to the right.";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Closer Unknowns (q_, r_) [* *]";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [CLOSER?UNKNOWNS?PATH]; //, MOVE?RIGHTMOST
rule["Head"] := '( q_ *$ (r_ *$ s_) );
rule["Guard"] := ''( UnderscoreConstant?(q) &? Number?(r) |? s =? _unknown); // Only used by MOVE?RIGHTMOST.
rule["Body"] := ''( (q *$ r) *$ s );
rule["DescriptionGuard"] := "TwoCopiesOfTheUnknownWillBecomeCloserAlongAPath?()"; // Only used by CLOSER?UNKNOWNS?PATH.
rule["DescriptionObjectLevel"] := "Change the association of * operators.";
rule["DescriptionMetaLevel"] := "Move two copies of the unknown closer to each other along a path.";
rule["ManualSequence"] := 17;
rule["HeadLatex"] := "\\textcolor{orange}{q\\_} \\textcolor{green}{*} (\\textcolor{orange}{r\\_} * s\\_)";
rule["BodyLatex"] := "(q * r) * s";
/*
rule["DescriptionObjectLevel"] := "Move an copy of the unknown left or right.";
rule["DescriptionMetaLevel"] := "Move an copy of the unknown to the right.";
*/
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Eliminate Unknown 1";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [ELIMINATE?UNKNOWN];
rule["Head"] := '( q_ *$ s_ +$ r_ *$ s_ );
rule["Guard"] := ''( s =? _unknown );
rule["Body"] := ''( (q +$ r) *$ s );
rule["DescriptionObjectLevel"] := "Eliminate one copy of the unknown.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 10;
rule["HeadLatex"] := "q\\_ * \\textcolor{orange}{s\\_} \\textcolor{green}{+} r\\_ * \\textcolor{orange}{s\\_}";
rule["BodyLatex"] := "(q + r) * s";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Eliminate Unknown 2";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [ELIMINATE?UNKNOWN];
rule["Head"] := '( r_ *$ q_ +$ q_ );
rule["Guard"] := ''( q =? _unknown );
rule["Body"] := ''( (r +$ 1) *$ q );
rule["DescriptionObjectLevel"] := "Eliminate one copy of the unknown.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 11;
rule["HeadLatex"] := "r\\_ * \\textcolor{orange}{q\\_} \\textcolor{green}{+} \\textcolor{orange}{q\\_}";
rule["BodyLatex"] := "(r + 1) * q";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Eliminate Unknown 3";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [ELIMINATE?UNKNOWN];
rule["Head"] := '( q_ +$ q_ );
rule["Guard"] := ''( q =? _unknown );
rule["Body"] := ''( 2 *$ q );
rule["DescriptionObjectLevel"] := "Eliminate one copy of the unknown.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 12;
rule["HeadLatex"] := "\\textcolor{orange}{q\\_} \\textcolor{green}{+} \\textcolor{orange}{q\\_}";
rule["BodyLatex"] := "2 * q";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Eliminate Unknown 4";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [ELIMINATE?UNKNOWN];
rule["Head"] := '( q_ *$ q_ );
rule["Guard"] := ''( q =? _unknown );
rule["Body"] := ''( q ^$ 2 );
rule["DescriptionObjectLevel"] := "Eliminate one copy of the unknown.";
rule["DescriptionMetaLevel"] := "";
rule["ManualSequence"] := 13;
rule["HeadLatex"] := "\\textcolor{orange}{q\\_} \\textcolor{green}{*} \\textcolor{orange}{q\\_}";
rule["BodyLatex"] := "q ^ 2";
?rulebaseElementaryAlgebra[ruleName] := rule;
// ----------------------------------
//Old introduce.
ruleName := "Make Unknown Coefficient Explicit 1";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [MAKE?COEFFICIENT?EXPLICIT];
rule["Head"] := '( q_ +$ r_ *$ q_ );
rule["Guard"] := ''( q =? _unknown );
rule["Body"] := ''( 1 *$ q +$ r *$ q );
rule["DescriptionObjectLevel"] := "Make a coefficient of the unknown explicit.";
rule["DescriptionMetaLevel"] := "";
rule["Subposition"] := "1";
rule["ManualRuleEquivalent"] := "Make Coefficient Explicit";
?rulebaseElementaryAlgebra[ruleName] := rule;
//Old introduce.
ruleName := "Make Unknown Coefficient Explicit 2";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [MAKE?COEFFICIENT?EXPLICIT];
rule["Head"] := '( q_ *$ r_ +$ r_ );
rule["Guard"] := ''( r =? _unknown );
rule["Body"] := ''( q *$ r +$ 1 *$ r );
rule["DescriptionObjectLevel"] := "Make a coefficient of the unknown explicit.";
rule["DescriptionMetaLevel"] := "";
rule["Subposition"] := "2";
rule["ManualRuleEquivalent"] := "Make Coefficient Explicit";
?rulebaseElementaryAlgebra[ruleName] := rule;
// ==================================== Automatic
// ------------------------------------------
ruleName := "Closer Unknowns Horizontal 1";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [CLOSER?UNKNOWNS?HORIZONTAL];
rule["Head"] := '( q_ +$ (r_ +$ s_) );
rule["Guard"] := ''( OccurrencesCount(q, _unknown) !=? 0 &? OccurrencesCount(r, _unknown) =? 0 &? OccurrencesCount(s, _unknown) !=? 0 );
rule["Body"] := ''( q +$ (s +$ r) );
rule["DescriptionObjectLevel"] := "Move a copy of the unknown to the left.";
rule["DescriptionMetaLevel"] := "Move two copies of the unknown closer horizontally linearly.";
rule["Subposition"] := "2";
rule["ManualRuleEquivalent"] := "Commute +";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "Closer Unknowns Horizontal 2";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [CLOSER?UNKNOWNS?HORIZONTAL];
rule["Head"] := '( (q_ +$ r_) +$ s_ );
rule["Guard"] := ''( OccurrencesCount(q, _unknown) !=? 0 &? OccurrencesCount(r, _unknown) =? 0 &? OccurrencesCount(s, _unknown) !=? 0 );
rule["Body"] := ''( (r +$ q) +$ s );
rule["DescriptionObjectLevel"] := "Move a copy of the unknown to the right.";
rule["DescriptionMetaLevel"] := "Move two copies of the unknown closer horizontally linearly.";
rule["Subposition"] := "1";
rule["ManualRuleEquivalent"] := "Commute +";
?rulebaseElementaryAlgebra[ruleName] := rule;
// ========================================== In progress (not used yet)
ruleName := "RemoveDenominators 1";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [REMOVE?DENOMINATORS];
rule["Head"] := '( q_ +$ r_ *$ (s_ /$ t_) +$ u_ ==$ rhs_ );
rule["Guard"] := ''( OccurrencesCount(s, _unknown) !=? 0 );
rule["Body"] := ''( t *$ (q +$ r *$ (s /$ t) +$ u) ==$ t * rhs );
rule["DescriptionObjectLevel"] := ''( "Multiply both sides by " ~ t ~ "." );
rule["DescriptionMetaLevel"] := "";
?rulebaseElementaryAlgebra[ruleName] := rule;
// ==================================== Unbury.
ruleName := "UnaryMinusOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 1;
rule["Head"] := '( -$ lhs_ ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( lhs ==$ -$ rhs );
rule["DescriptionGuard"] := "The unknown is in lhs.";
rule["DescriptionObjectLevel"] := ''( "Multiply both sides by -1." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [-$ lhs *$ SubtractN(0,1) ==$ rhs *$ SubtractN(0,1), [["1,1", a_Atom?, "ORANGE"], ["1,1,2", _, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", _, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "PlusLeftOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 1;
rule["Head"] := '( (q_ +$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( q ==$ rhs -$ r );
rule["DescriptionGuard"] := "UnknownIn?(q)";
rule["DescriptionObjectLevel"] := ''("Subtract " ~ r ~ " from both sides.");
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [q +$ r -$ r ==$ rhs -$ r, [["1", a_Atom?, "ORANGE"], ["1,2", _, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", _, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "PlusRightOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 2;
rule["Head"] := '( (q_ +$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( r ==$ rhs -$ q );
rule["DescriptionGuard"] := "UnknownIn?(r)";
rule["DescriptionObjectLevel"] := ''( "Subtract " ~ q ~ " from both sides." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [q +$ r -$ q ==$ rhs -$ q, [["1", a_Atom?, "ORANGE"], ["1,2", a_Atom?, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", a_Atom?, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "MinusLeftOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 1;
rule["Head"] := '( (q_ -$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( q ==$ rhs +$ r );
rule["DescriptionGuard"] := "UnknownIn?(q)";
rule["DescriptionObjectLevel"] := ''( "Add " ~ r ~ " to both sides." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [q -$ r +$ r ==$ rhs +$ r, [["2", a_Atom?, "ORANGE"], ["2,2", a_Atom?, "ORANGE"], ["1,1", a_Atom?, "ORANGE"], ["1,1,1", a_Atom?, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "MinusRightOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 2;
rule["Head"] := '( (q_ -$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( -$ r ==$ rhs -$ q );
rule["DescriptionGuard"] := "UnknownIn?(r)";
rule["DescriptionObjectLevel"] := ''( "Subtract " ~ q ~ " from both sides." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [q -$ r -$ q ==$ rhs -$ q, [["2", a_Atom?, "ORANGE"], ["2,2", _, "ORANGE"], ["1,1", a_Atom?, "ORANGE"], ["1,1,1", _, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "TimesLeftOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 1;
rule["Head"] := '( (q_ *$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( q ==$ rhs /$ r );
rule["DescriptionGuard"] := "UnknownIn?(q)";
rule["DescriptionObjectLevel"] := ''( "Divide both sides by " ~ r ~ "." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [(q *$ r) /$ r ==$ rhs /$ r, [["1", a_Atom?, "ORANGE"], ["1,2", a_Atom?, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", a_Atom?, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "TimesRightOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 2;
rule["Head"] := '( (q_ *$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( r ==$ rhs /$ q );
rule["DescriptionGuard"] := "UnknownIn?(r)";
rule["DescriptionObjectLevel"] := ''( "Divide both sides by " ~ q ~ "." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [(q *$ r) /$ q ==$ rhs /$ q, [["1", a_Atom?, "ORANGE"], ["1,2", a_Atom?, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", a_Atom?, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "DivideLeftOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 1;
rule["Head"] := '( (q_ /$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( q ==$ rhs *$ r );
rule["DescriptionGuard"] := "UnknownIn?(q)";
rule["DescriptionObjectLevel"] := ''( "Multiply both sides by " ~ r ~ "." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [(q /$ r) *$ r ==$ rhs *$ r, [["1", a_Atom?, "ORANGE"], ["1,2", _, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", _, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "DivideRightOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 2;
rule["Head"] := '( (q_ /$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( [rhs *$ r ==$ q, r ==$ q /$ rhs] );
rule["DescriptionGuard"] := "UnknownIn?(r)";
rule["DescriptionObjectLevel"] := ''( ["Multiply both sides by " ~ r ~ " and exchange sides.", "Divide both sides by " ~ ToString(TexFormNoDollarSigns(rhs)) ~ "."] );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''[ [(q /$ r) *$ r ==$ rhs *$ r, [["1", a_Atom?, "ORANGE"], ["1,2", _, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", _, "ORANGE"]]], [(rhs *$ r) /$ rhs ==$ q /$ rhs, [["1", a_Atom?, "ORANGE"], ["1,2", _, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", _, "ORANGE"]]] ];
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "ExponentRightOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 1;
rule["Head"] := '( (q_ ^$ r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( q ==$ rhs^$(1 /$ r) );
rule["DescriptionGuard"] := "UnknownIn?(q)";
rule["DescriptionObjectLevel"] := ''( "Take root " ~ r ~ " of both sides" ~ "." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [(q ^$ r)^$(1 /$ r) ==$ rhs^$(1 /$ r), [["1", a_Atom?, "ORANGE"], ["1,2", _, "ORANGE"], ["2", a_Atom?, "ORANGE"], ["2,2", _, "ORANGE"]]] );
?rulebaseElementaryAlgebra[ruleName] := rule;
/*
ruleName := "LogOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 2;
rule["Head"] := '( Log(q_, r_) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( r ==$ q^$rhs );
rule["DescriptionGuard"] := "UnknownIn?(r)";
rule["DescriptionObjectLevel"] := ''( "Raise the base " ~ q ~ " to both sides" ~ "." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [q^$Log(q,r) ==$ q^$rhs, []] );
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "SquareRootOtherside";
rule := [];
rule["RuleName"] := ruleName;
rule["StructuralEffect"] := [OTHERSIDE];
rule["Side"] := 1;
rule["Head"] := '( q_^$(1/$2) ==$ rhs_ );
rule["Guard"] := ''( True );
rule["Body"] := ''( q ==$ rhs^$2 );
rule["DescriptionGuard"] := "UnknownIn?(q)";
rule["DescriptionObjectLevel"] := ''( "Square both sides" ~ "." );
rule["DescriptionMetaLevel"] := "";
rule["Before"] := ''( [Sqrt(q)^$2 ==$ rhs^$2, []] );
?rulebaseElementaryAlgebra[ruleName] := rule;
*/
// ======================================
/*
logarithms log(base, argument)
isolax( 1 , log(U,1)=0 , U=N , arbint(N) ).
isolax( 1 , log(U,V)=W , U=V^W1 , non_zero(W) ) :- tidy(1/W,W1).
isolax( 2 , log(U,V)=W , V=U^W , true ) .
//1 -> (q_ ^$ 2 ==$ rhs_) <- [q ==$ Sqrt(rhs), "Exponentiation1a", "\\text{Take the square root of both sides}", Sqrt(q ^$ 2) ==$ Sqrt(rhs)],
//"Exponentiation2" # 2 :: q_ ^ r_ ==$ rhs_ <- r ==$ Log(rhs)//Log(base(q), rhs)
*/
// ================ Textbook
// q + 0
ruleName := "IdentityIntroduce1 q_ + 0";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, INTRODUCE];
rule["Head"] := '( q_ );
rule["Body"] := ''( q +$ 0 );
rule["DescriptionObjectLevel"] := "Introduce additive identity 1.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "q";
rule["BodyLatex"] := "q\\_ \\textcolor{green}{+} 0";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "IdentityEliminate1 q_ + 0";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, ELIMINATE];
rule["Head"] := '( q_ +$ 0 );
rule["Body"] := ''( q );
rule["DescriptionObjectLevel"] := "Eliminate additive identity 1.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "q\\_ \\textcolor{green}{+} 0";
rule["BodyLatex"] := "q";
?rulebaseElementaryAlgebra[ruleName] := rule;
// 0 + q
ruleName := "IdentityIntroduce2 0 + q_";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, INTRODUCE];
rule["Head"] := '( q_ );
rule["Body"] := ''( 0 +$ q );
rule["DescriptionObjectLevel"] := "Introduce additive identity 2.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "q";
rule["BodyLatex"] := "0 \\textcolor{green}{+} q\\_";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "IdentityEliminate2 0 + q_";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, ELIMINATE];
rule["Head"] := '( 0 +$ q_ );
rule["Body"] := ''( q );
rule["DescriptionObjectLevel"] := "Introduce additive identity 2.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "0 \\textcolor{green}{+} q\\_";
rule["BodyLatex"] := "q";
?rulebaseElementaryAlgebra[ruleName] := rule;
// q*1
ruleName := "IdentityIntroduce1 q_ * 1";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, INTRODUCE];
rule["Head"] := '( q_ );
rule["Body"] := ''( q *$ 1 );
rule["DescriptionObjectLevel"] := "Introduce multiplicative identity 1.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "q";
rule["BodyLatex"] := "q\\_ \\textcolor{green}{*} 1";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "IdentityEliminate1 q_ * 1";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, ELIMINATE];
rule["Head"] := '( q_ *$ 1 );
rule["Body"] := ''( q );
rule["DescriptionObjectLevel"] := "Eliminate multiplicative identity 1.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "q\\_ \\textcolor{green}{*} 1";
rule["BodyLatex"] := "q";
?rulebaseElementaryAlgebra[ruleName] := rule;
// 1*q
ruleName := "IdentityIntroduce2 1 * q_";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, INTRODUCE];
rule["Head"] := '( q_ );
rule["Body"] := ''( 1 *$ q );
rule["DescriptionObjectLevel"] := "Introduce multiplicative identity 2.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "q";
rule["BodyLatex"] := "1 \\textcolor{green}{*} q\\_";
?rulebaseElementaryAlgebra[ruleName] := rule;
ruleName := "IdentityEliminate2 1 * q_";
rule := [];
rule["RuleName"] := ruleName;
rule["Type"] := [TEXTBOOK, ELIMINATE];
rule["Head"] := '( 1 *$ q_ );
rule["Body"] := ''( q );
rule["DescriptionObjectLevel"] := "Eliminate multiplicative identity 2.";
rule["DescriptionMetaLevel"] := "";
rule["HeadLatex"] := "q";
rule["BodyLatex"] := "1 \\textcolor{green}{*} q\\_";
?rulebaseElementaryAlgebra[ruleName] := rule;
?rulebaseMetaLevel := [];
rule := [];
rule["RuleName"] := "HigherUnknowns";
?rulebaseMetaLevel[HIGHER?UNKNOWNS] := rule;
rule := [];
rule["RuleName"] := "EliminateUnknown";
?rulebaseMetaLevel[ELIMINATE?UNKNOWN] := rule;
rule := [];
rule["RuleName"] := "MakeCoefficientsExplicit";
?rulebaseMetaLevel[MAKE?COEFFICIENT?EXPLICIT] := rule;
rule := [];
rule["RuleName"] := "MoveUnknownsToRightmostPositions";
?rulebaseMetaLevel[MOVE?RIGHTMOST] := rule;
rule := [];
rule["RuleName"] := "UndefineUnaryMinus";
?rulebaseMetaLevel[UNDEFINE?UNARY?MINUS] := rule;
rule := [];
rule["RuleName"] := "UndefineBinaryMinus";
?rulebaseMetaLevel[UNDEFINE?BINARY?MINUS] := rule;
}
%/mathpiper