Skip to content

Instantly share code, notes, and snippets.

@saitouena

saitouena/908.proof.xml

Last active January 17, 2024 14:17
Show Gist options
  • Save saitouena/1fb80f85992cdd76a60336598d4589da to your computer and use it in GitHub Desktop.
Save saitouena/1fb80f85992cdd76a60336598d4589da to your computer and use it in GitHub Desktop.
Download ZIP
Raw
908.proof.xml
<?xml version="1.0"?>
<certificationProblem noNamespaceSchemaLocation="cpf3.xsd" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<cpfVersion>3.0</cpfVersion>
<lookupTables/>
<input>
<infeasibilityInput>
<ctrs>
<conditionType>
<oriented/>
</conditionType>
<rules>
<rule>
<funapp>
<name>le</name>
<var>x</var>
<funapp>
<name>0</name>
</funapp>
</funapp>
<funapp>
<name>false</name>
</funapp>
<conditions/>
</rule>
<rule>
<funapp>
<name>le</name>
<funapp>
<name>0</name>
</funapp>
<funapp>
<name>s</name>
<var>y</var>
</funapp>
</funapp>
<funapp>
<name>true</name>
</funapp>
<conditions/>
</rule>
<rule>
<funapp>
<name>le</name>
<funapp>
<name>s</name>
<var>x</var>
</funapp>
<funapp>
<name>s</name>
<var>y</var>
</funapp>
</funapp>
<funapp>
<name>le</name>
<var>x</var>
<var>y</var>
</funapp>
<conditions/>
</rule>
<rule>
<funapp>
<name>min</name>
<funapp>
<name>cons</name>
<var>x</var>
<funapp>
<name>nil</name>
</funapp>
</funapp>
</funapp>
<var>x</var>
<conditions/>
</rule>
<rule>
<funapp>
<name>min</name>
<funapp>
<name>cons</name>
<var>x</var>
<var>xs</var>
</funapp>
</funapp>
<var>x</var>
<conditions>
<condition>
<funapp>
<name>le</name>
<var>x</var>
<funapp>
<name>min</name>
<var>xs</var>
</funapp>
</funapp>
<funapp>
<name>true</name>
</funapp>
</condition>
</conditions>
</rule>
<rule>
<funapp>
<name>min</name>
<funapp>
<name>cons</name>
<var>x</var>
<var>xs</var>
</funapp>
</funapp>
<funapp>
<name>min</name>
<var>xs</var>
</funapp>
<conditions>
<condition>
<funapp>
<name>le</name>
<var>x</var>
<funapp>
<name>min</name>
<var>xs</var>
</funapp>
</funapp>
<funapp>
<name>false</name>
</funapp>
</condition>
</conditions>
</rule>
</rules>
</ctrs>
<infeasibilityQuery>
<rule>
<funapp>
<name>le</name>
<var>x1</var>
<funapp>
<name>min</name>
<var>x2</var>
</funapp>
</funapp>
<funapp>
<name>true</name>
</funapp>
</rule>
<rule>
<funapp>
<name>le</name>
<var>x1</var>
<funapp>
<name>min</name>
<var>x2</var>
</funapp>
</funapp>
<funapp>
<name>false</name>
</funapp>
</rule>
</infeasibilityQuery>
</infeasibilityInput>
</input>
<property>
<infeasibility/>
</property>
<answer>
<yes/>
</answer>
<proof>
<infeasibilityProof>
<infeasibleGoalLifting>
<name>true__</name>
<name>false__</name>
<infeasibilityProof>
<infeasibleSplitIf>
<splitIfInformation>
<funapp>
<name>true__</name>
</funapp>
<funapp>
<name>false__</name>
</funapp>
<normalUnravelingEntry>
<rule>
<funapp>
<name>min</name>
<funapp>
<name>cons</name>
<var>x</var>
<var>xs</var>
</funapp>
</funapp>
<var>x</var>
<conditions>
<condition>
<funapp>
<name>le</name>
<var>x</var>
<funapp>
<name>min</name>
<var>xs</var>
</funapp>
</funapp>
<funapp>
<name>true</name>
</funapp>
</condition>
</conditions>
</rule>
<name>c1</name>
<var>x</var>
<var>xs</var>
</normalUnravelingEntry>
<normalUnravelingEntry>
<rule>
<funapp>
<name>min</name>
<funapp>
<name>cons</name>
<var>x</var>
<var>xs</var>
</funapp>
</funapp>
<funapp>
<name>min</name>
<var>xs</var>
</funapp>
<conditions>
<condition>
<funapp>
<name>le</name>
<var>x</var>
<funapp>
<name>min</name>
<var>xs</var>
</funapp>
</funapp>
<funapp>
<name>false</name>
</funapp>
</condition>
</conditions>
</rule>
<name>c1</name>
<var>x</var>
<var>xs</var>
</normalUnravelingEntry>
<normalUnravelingEntry>
<rule>
<funapp>
<name>true__</name>
</funapp>
<funapp>
<name>false__</name>
</funapp>
<conditions>
<condition>
<funapp>
<name>le</name>
<var>x1</var>
<funapp>
<name>min</name>
<var>x2</var>
</funapp>
</funapp>
<funapp>
<name>true</name>
</funapp>
</condition>
<condition>
<funapp>
<name>le</name>
<var>x1</var>
<funapp>
<name>min</name>
<var>x2</var>
</funapp>
</funapp>
<funapp>
<name>false</name>
</funapp>
</condition>
</conditions>
</rule>
<name>c2</name>
<var>x1</var>
<var>x2</var>
</normalUnravelingEntry>
<normalUnravelingEntry>
<rule>
<funapp>
<name>false__</name>
</funapp>
<funapp>
<name>true__</name>
</funapp>
<conditions>
<condition>
<funapp>
<name>true__</name>
</funapp>
<funapp>
<name>false__</name>
</funapp>
</condition>
</conditions>
</rule>
<name>c3</name>
</normalUnravelingEntry>
</splitIfInformation>
<nonreachabilityProof>
<nonreachableEquationalDisproof>
<equationalDisproof>
<approxAndCompletionAndNormalization>
<trs>
<rules>
<rule>
<funapp>
<name>c3</name>
<funapp>
<name>false__</name>
</funapp>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c3</name>
<funapp>
<name>true__</name>
</funapp>
</funapp>
<funapp>
<name>false__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>le</name>
<var>X0</var>
<funapp>
<name>0</name>
</funapp>
</funapp>
<funapp>
<name>false</name>
</funapp>
</rule>
<rule>
<funapp>
<name>le</name>
<funapp>
<name>0</name>
</funapp>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
<funapp>
<name>true</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c1</name>
<funapp>
<name>true</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<var>X0</var>
</rule>
<rule>
<funapp>
<name>c1</name>
<funapp>
<name>false</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<funapp>
<name>min</name>
<var>X1</var>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>false</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<funapp>
<name>false__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>false</name>
</funapp>
<funapp>
<name>false</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>0</name>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>le</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
<funapp>
<name>s</name>
<var>X1</var>
</funapp>
</funapp>
<funapp>
<name>le</name>
<var>X0</var>
<var>X1</var>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c1</name>
<funapp>
<name>le</name>
<var>X0</var>
<funapp>
<name>min</name>
<funapp>
<name>nil</name>
</funapp>
</funapp>
</funapp>
<var>X0</var>
<funapp>
<name>nil</name>
</funapp>
</funapp>
<var>X0</var>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<var>X0</var>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>min</name>
<funapp>
<name>cons</name>
<var>X0</var>
<var>X1</var>
</funapp>
</funapp>
<funapp>
<name>c1</name>
<funapp>
<name>le</name>
<var>X0</var>
<funapp>
<name>min</name>
<var>X1</var>
</funapp>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
</rules>
</trs>
<approxCompletionProof>
<wcrProof>
<joinAutoNF/>
</wcrProof>
<trsTerminationProof>
<ruleRemoval>
<recursivePathOrder>
<statusPrecedence>
<statusPrecedenceEntry>
<name>false__</name>
<arity>0</arity>
<precedence>0</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>true__</name>
<arity>0</arity>
<precedence>1</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>c3</name>
<arity>1</arity>
<precedence>2</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>nil</name>
<arity>0</arity>
<precedence>3</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>false</name>
<arity>0</arity>
<precedence>4</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>min</name>
<arity>1</arity>
<precedence>5</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>s</name>
<arity>1</arity>
<precedence>6</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>le</name>
<arity>2</arity>
<precedence>7</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>true</name>
<arity>0</arity>
<precedence>8</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>0</name>
<arity>0</arity>
<precedence>9</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>c2</name>
<arity>4</arity>
<precedence>10</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>c1</name>
<arity>3</arity>
<precedence>11</precedence>
<lex/>
</statusPrecedenceEntry>
<statusPrecedenceEntry>
<name>cons</name>
<arity>2</arity>
<precedence>12</precedence>
<lex/>
</statusPrecedenceEntry>
</statusPrecedence>
</recursivePathOrder>
<trs>
<rules>
<rule>
<funapp>
<name>c3</name>
<funapp>
<name>false__</name>
</funapp>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c3</name>
<funapp>
<name>true__</name>
</funapp>
</funapp>
<funapp>
<name>false__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>le</name>
<var>X0</var>
<funapp>
<name>0</name>
</funapp>
</funapp>
<funapp>
<name>false</name>
</funapp>
</rule>
<rule>
<funapp>
<name>le</name>
<funapp>
<name>0</name>
</funapp>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
<funapp>
<name>true</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c1</name>
<funapp>
<name>true</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<var>X0</var>
</rule>
<rule>
<funapp>
<name>c1</name>
<funapp>
<name>false</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<funapp>
<name>min</name>
<var>X1</var>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>false</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<funapp>
<name>false__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>false</name>
</funapp>
<funapp>
<name>false</name>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>0</name>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>le</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
<funapp>
<name>s</name>
<var>X1</var>
</funapp>
</funapp>
<funapp>
<name>le</name>
<var>X0</var>
<var>X1</var>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c1</name>
<funapp>
<name>le</name>
<var>X0</var>
<funapp>
<name>min</name>
<funapp>
<name>nil</name>
</funapp>
</funapp>
</funapp>
<var>X0</var>
<funapp>
<name>nil</name>
</funapp>
</funapp>
<var>X0</var>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<var>X0</var>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>min</name>
<funapp>
<name>cons</name>
<var>X0</var>
<var>X1</var>
</funapp>
</funapp>
<funapp>
<name>c1</name>
<funapp>
<name>le</name>
<var>X0</var>
<funapp>
<name>min</name>
<var>X1</var>
</funapp>
</funapp>
<var>X0</var>
<var>X1</var>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>true</name>
</funapp>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>0</name>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X0</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
<rule>
<funapp>
<name>c2</name>
<var>Z1</var>
<var>Z1</var>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<funapp>
<name>s</name>
<var>X0</var>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
</funapp>
<var>X2</var>
</funapp>
<funapp>
<name>true__</name>
</funapp>
</rule>
</rules>
</trs>
<trsTerminationProof>
<rIsEmpty/>
</trsTerminationProof>
</ruleRemoval>
</trsTerminationProof>
</approxCompletionProof>
</approxAndCompletionAndNormalization>
</equationalDisproof>
</nonreachableEquationalDisproof>
</nonreachabilityProof>
</infeasibleSplitIf>
</infeasibilityProof>
</infeasibleGoalLifting>
</infeasibilityProof>
</proof>
</certificationProblem>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment