CeTA (2.36)

CeTA is a tool that certifies (non)termination or (non)confluence or completion or complexity proofs provided by some automated (termination/complexity/...) tool.

An Isabelle/HOL Formalization of Rewriting for Certified Tool Assertions

Examples

Load own example

Syntax highlighting

Tool input

<?xml version="1.0"?>
<?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?><certificationProblem xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:noNamespaceSchemaLocation="../xml/cpf.xsd">
  <input>
    <trsInput>
      <trs>
        <rules>
          <rule>
            <lhs>
              <funapp>
                <name>f</name>
                <arg>
                  <var>x</var>
                </arg>
              </funapp>
            </lhs>
            <rhs>
              <funapp>
                <name>g</name>
              </funapp>
            </rhs>
          </rule>
        </rules>
      </trs>
    </trsInput>
  </input>
  <cpfVersion>2.1</cpfVersion>
  <proof>
    <trsTerminationProof>
      <bounds>
        <type>
          <match/>
        </type>
        <bound>1</bound>
        <finalStates>
          <state>2</state>
          <state>1</state>
        </finalStates>
        <treeAutomaton>
          <finalStates>
            <state>2</state>
            <state>1</state>
          </finalStates>
          <transitions>
            <transition>
              <lhs>
                <name>g</name>
                <height>0</height>
              </lhs>
              <rhs>
                <state>2</state>
              </rhs>
            </transition>
            <transition>
              <lhs>
                <name>f</name>
                <height>0</height>
                <state>1</state>
              </lhs>
              <rhs>
                <state>1</state>
              </rhs>
            </transition>
            <transition>
              <lhs>
                <name>f</name>
                <height>0</height>
                <state>2</state>
              </lhs>
              <rhs>
                <state>1</state>
              </rhs>
            </transition>
            <transition>
              <lhs>
                <name>g</name>
                <height>1</height>
              </lhs>
              <rhs>
                <state>4</state>
              </rhs>
            </transition>
            <transition>
              <lhs>
                <name>g</name>
                <height>1</height>
              </lhs>
              <rhs>
                <state>1</state>
              </rhs>
            </transition>
          </transitions>
        </treeAutomaton>
      </bounds>
    </trsTerminationProof>
  </proof>
  <origin>
    <proofOrigin>
      <tool>
        <name>unspecified</name>
        <version>unspecified</version>
      </tool>
    </proofOrigin>
  </origin>
</certificationProblem>

Department of Computer Science

University of Innsbruck

CeTA (2.36)