Exercise algebra.inequalities.linear

Description
solve a linear inequation

Strategy

<label name="linearinequation">
  <sequence>
    <label name="phase1">
      <let>
        <decl var="4">
          <orelse>
            <sequence>
              <choice>
                <rule name="algebra.equations.linear.remove-div"/>
                <label name="algebra.equations.linear.distr-times" collapsed="true">
                  <sequence>
                    <let>
                      <decl var="1">
                        <orelse>
                          <rule name="algebra.equations.linear.distr-times"/>
                          <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>
                        </orelse>
                      </decl>
                      <var var="1"/>
                    </let>
                    <let>
                      <decl var="3">
                        <orelse>
                          <sequence>
                            <let>
                              <decl var="1">
                                <orelse>
                                  <rule name="algebra.equations.linear.distr-times"/>
                                  <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>
                                </orelse>
                              </decl>
                              <var var="1"/>
                            </let>
                            <var var="3"/>
                          </sequence>
                          <succeed/>
                        </orelse>
                      </decl>
                      <var var="3"/>
                    </let>
                  </sequence>
                </label>
                <label name="algebra.equations.linear.merge" collapsed="true">
                  <sequence>
                    <rule name="navigator.down"/>
                    <succeed/>
                    <let>
                      <decl var="0">
                        <choice>
                          <rule name="algebra.equations.linear.merge"/>
                          <sequence>
                            <rule name="navigator.right"/>
                            <succeed/>
                            <var var="0"/>
                          </sequence>
                        </choice>
                      </decl>
                      <var var="0"/>
                    </let>
                    <orelse>
                      <rule name="navigator.up"/>
                      <succeed/>
                    </orelse>
                    <let>
                      <decl var="1">
                        <orelse>
                          <sequence>
                            <rule name="navigator.down"/>
                            <succeed/>
                            <let>
                              <decl var="0">
                                <choice>
                                  <rule name="algebra.equations.linear.merge"/>
                                  <sequence>
                                    <rule name="navigator.right"/>
                                    <succeed/>
                                    <var var="0"/>
                                  </sequence>
                                </choice>
                              </decl>
                              <var var="0"/>
                            </let>
                            <orelse>
                              <rule name="navigator.up"/>
                              <succeed/>
                            </orelse>
                            <var var="1"/>
                          </sequence>
                          <succeed/>
                        </orelse>
                      </decl>
                      <var var="1"/>
                    </let>
                  </sequence>
                </label>
              </choice>
              <var var="4"/>
            </sequence>
            <succeed/>
          </orelse>
        </decl>
        <var var="4"/>
      </let>
    </label>
    <label name="phase2">
      <sequence>
        <orelse>
          <rule name="algebra.equations.linear.var-left"/>
          <succeed/>
        </orelse>
        <orelse>
          <choice>
            <rule name="algebra.equations.coverup.onevar.plus"/>
            <rule name="algebra.equations.coverup.onevar.minus-left"/>
            <rule name="algebra.equations.coverup.onevar.minus-right"/>
            <fail/>
          </choice>
          <succeed/>
        </orelse>
        <orelse>
          <rule name="algebra.inequalities.flip-sign"/>
          <succeed/>
        </orelse>
        <orelse>
          <rule name="algebra.equations.coverup.times-positive"/>
          <succeed/>
        </orelse>
      </sequence>
    </label>
  </sequence>
</label>

Locations