Exercise algebra.equations.linear.balance

Description
Solve a linear equation using only balance rules.

Strategy

<label name="balanceequation">
  <interleave>
    <sequence>
      <label name="phase1">
        <let>
          <decl var="3">
            <orelse>
              <sequence>
                <choice>
                  <rule name="algebra.equations.linear.balance.collect"/>
                  <rule name="algebra.equations.linear.balance.distribute"/>
                  <rule name="algebra.equations.linear.balance.remove-div"/>
                  <let>
                    <decl var="1">
                      <choice>
                        <rule name="algebra.equations.linear.balance.div-to-fraction"/>
                        <sequence>
                          <rule name="navigator.down"/>
                          <succeed/>
                          <let>
                            <decl var="2">
                              <choice>
                                <var var="1"/>
                                <sequence>
                                  <rule name="navigator.right"/>
                                  <succeed/>
                                  <var var="2"/>
                                </sequence>
                              </choice>
                            </decl>
                            <var var="2"/>
                          </let>
                          <orelse>
                            <rule name="navigator.up"/>
                            <succeed/>
                          </orelse>
                        </sequence>
                      </choice>
                    </decl>
                    <var var="1"/>
                  </let>
                  <rule name="algebra.equations.linear.balance.negate"/>
                  <rule name="algebra.equations.linear.balance.intro-true"/>
                  <rule name="algebra.equations.linear.balance.intro-false"/>
                </choice>
                <var var="3"/>
              </sequence>
              <succeed/>
            </orelse>
          </decl>
          <var var="3"/>
        </let>
      </label>
      <label name="phase2">
        <sequence>
          <let>
            <decl var="0">
              <orelse>
                <sequence>
                  <choice>
                    <rule name="algebra.equations.linear.balance.var-left-minus"/>
                    <rule name="algebra.equations.linear.balance.var-left-plus"/>
                    <rule name="algebra.equations.linear.balance.con-right-minus"/>
                    <rule name="algebra.equations.linear.balance.con-right-plus"/>
                    <rule name="algebra.equations.linear.balance.intro-true"/>
                    <rule name="algebra.equations.linear.balance.intro-false"/>
                    <atomic>
                      <sequence>
                        <rule name="check"/>
                        <choice>
                          <rule name="algebra.equations.linear.balance.var-right-minus"/>
                          <rule name="algebra.equations.linear.balance.var-right-plus"/>
                        </choice>
                      </sequence>
                    </atomic>
                    <atomic>
                      <sequence>
                        <rule name="check"/>
                        <choice>
                          <rule name="algebra.equations.linear.balance.con-left-minus"/>
                          <rule name="algebra.equations.linear.balance.con-left-plus"/>
                        </choice>
                      </sequence>
                    </atomic>
                  </choice>
                  <var var="0"/>
                </sequence>
                <succeed/>
              </orelse>
            </decl>
            <var var="0"/>
          </let>
          <orelse>
            <rule name="algebra.equations.linear.balance.scale-to-one"/>
            <succeed/>
          </orelse>
          <orelse>
            <rule name="algebra.equations.linear.balance.calculate"/>
            <succeed/>
          </orelse>
        </sequence>
      </label>
    </sequence>
    <orelse>
      <atomic>
        <sequence>
          <rule name="check"/>
          <rule name="algebra.equations.linear.flip"/>
        </sequence>
      </atomic>
      <succeed/>
    </orelse>
    <let>
      <decl var="0">
        <choice>
          <succeed/>
          <sequence>
            <atomic>
              <sequence>
                <not>
                  <rule name="algebra.equations.linear.balance.scale-to-one"/>
                </not>
                <rule name="algebra.equations.linear.balance.smart-div"/>
              </sequence>
            </atomic>
            <var var="0"/>
          </sequence>
        </choice>
      </decl>
      <var var="0"/>
    </let>
  </interleave>
</label>

Locations