Last active
January 17, 2024 17:21
-
-
Save saitouena/79c870aea8a4a0533722b603aec0fb51 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
<?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>min</name> | |
<var>xs</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
<condition> | |
<funapp> | |
<name>le</name> | |
<var>x</var> | |
<var>y</var> | |
</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> | |
<var>y</var> | |
<conditions> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>xs</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
<condition> | |
<funapp> | |
<name>le</name> | |
<var>x</var> | |
<var>y</var> | |
</funapp> | |
<funapp> | |
<name>false</name> | |
</funapp> | |
</condition> | |
</conditions> | |
</rule> | |
</rules> | |
</ctrs> | |
<infeasibilityQuery> | |
<rule> | |
<funapp> | |
<name>min</name> | |
<var>x2</var> | |
</funapp> | |
<var>y</var> | |
</rule> | |
<rule> | |
<funapp> | |
<name>le</name> | |
<var>x1</var> | |
<var>y</var> | |
</funapp> | |
<funapp> | |
<name>true</name> | |
</funapp> | |
</rule> | |
<rule> | |
<funapp> | |
<name>min</name> | |
<var>x2</var> | |
</funapp> | |
<var>x3</var> | |
</rule> | |
<rule> | |
<funapp> | |
<name>le</name> | |
<var>x1</var> | |
<var>x3</var> | |
</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> | |
<rightInlineConditions> | |
<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> | |
<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> | |
</rules> | |
<inlinedRules> | |
<inlinedRule> | |
<rule> | |
<funapp> | |
<name>min</name> | |
<funapp> | |
<name>cons</name> | |
<var>x</var> | |
<var>xs</var> | |
</funapp> | |
</funapp> | |
<var>x</var> | |
<conditions> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>xs</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
<condition> | |
<funapp> | |
<name>le</name> | |
<var>x</var> | |
<var>y</var> | |
</funapp> | |
<funapp> | |
<name>true</name> | |
</funapp> | |
</condition> | |
</conditions> | |
</rule> | |
<inlinedConditions> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>xs</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
</inlinedConditions> | |
</inlinedRule> | |
<inlinedRule> | |
<rule> | |
<funapp> | |
<name>min</name> | |
<funapp> | |
<name>cons</name> | |
<var>x</var> | |
<var>xs</var> | |
</funapp> | |
</funapp> | |
<var>y</var> | |
<conditions> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>xs</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
<condition> | |
<funapp> | |
<name>le</name> | |
<var>x</var> | |
<var>y</var> | |
</funapp> | |
<funapp> | |
<name>false</name> | |
</funapp> | |
</condition> | |
</conditions> | |
</rule> | |
<inlinedConditions> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>xs</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
</inlinedConditions> | |
</inlinedRule> | |
<inlinedRule> | |
<rule> | |
<funapp> | |
<name>true__</name> | |
</funapp> | |
<funapp> | |
<name>false__</name> | |
</funapp> | |
<conditions> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>x2</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
<condition> | |
<funapp> | |
<name>le</name> | |
<var>x1</var> | |
<var>y</var> | |
</funapp> | |
<funapp> | |
<name>true</name> | |
</funapp> | |
</condition> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>x2</var> | |
</funapp> | |
<var>x3</var> | |
</condition> | |
<condition> | |
<funapp> | |
<name>le</name> | |
<var>x1</var> | |
<var>x3</var> | |
</funapp> | |
<funapp> | |
<name>false</name> | |
</funapp> | |
</condition> | |
</conditions> | |
</rule> | |
<inlinedConditions> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>x2</var> | |
</funapp> | |
<var>y</var> | |
</condition> | |
<condition> | |
<funapp> | |
<name>min</name> | |
<var>x2</var> | |
</funapp> | |
<var>x3</var> | |
</condition> | |
</inlinedConditions> | |
</inlinedRule> | |
</inlinedRules> | |
<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> | |
</rightInlineConditions> | |
</infeasibilityProof> | |
</infeasibleGoalLifting> | |
</infeasibilityProof> | |
</proof> | |
</certificationProblem> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment