882.proof.xml

<?xml version='1.0' ?><certificationProblem xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" noNamespaceSchemaLocation="cpf3.xsd"><cpfVersion>3.0</cpfVersion><lookupTables /><input><infeasibilityInput><ctrs><conditionType><oriented /></conditionType><rules><rule><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp><var>x</var><conditions><condition><var>y</var><funapp><name>nil</name></funapp></condition></conditions></rule><rule><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp><var>z</var><conditions><condition><var>y</var><funapp><name>cons</name><var>u</var><var>v</var></funapp></condition><condition><funapp><name>last</name><var>y</var></funapp><var>z</var></condition></conditions></rule></rules></ctrs><infeasibilityQuery><rule><var>x4</var><funapp><name>nil</name></funapp></rule><rule><var>x4</var><funapp><name>cons</name><var>x1</var><var>x2</var></funapp></rule><rule><funapp><name>last</name><var>x4</var></funapp><var>x5</var></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>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp><var>x</var><conditions><condition><var>y</var><funapp><name>nil</name></funapp></condition></conditions></rule><rule><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp><funapp><name>last</name><var>y</var></funapp><conditions><condition><var>y</var><funapp><name>cons</name><var>u</var><var>v</var></funapp></condition></conditions></rule><rule><funapp><name>true__</name></funapp><funapp><name>false__</name></funapp><conditions><condition><var>x4</var><funapp><name>nil</name></funapp></condition><condition><var>x4</var><funapp><name>cons</name><var>x1</var><var>x2</var></funapp></condition></conditions></rule></rules><inlinedRules><inlinedRule><rule><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp><var>z</var><conditions><condition><var>y</var><funapp><name>cons</name><var>u</var><var>v</var></funapp></condition><condition><funapp><name>last</name><var>y</var></funapp><var>z</var></condition></conditions></rule><inlinedConditions><condition><funapp><name>last</name><var>y</var></funapp><var>z</var></condition></inlinedConditions></inlinedRule><inlinedRule><rule><funapp><name>true__</name></funapp><funapp><name>false__</name></funapp><conditions><condition><var>x4</var><funapp><name>nil</name></funapp></condition><condition><var>x4</var><funapp><name>cons</name><var>x1</var><var>x2</var></funapp></condition><condition><funapp><name>last</name><var>x4</var></funapp><var>x5</var></condition></conditions></rule><inlinedConditions><condition><funapp><name>last</name><var>x4</var></funapp><var>x5</var></condition></inlinedConditions></inlinedRule></inlinedRules><infeasibilityProof><infeasibleSplitIf><splitIfInformation><funapp><name>true__</name></funapp><funapp><name>false__</name></funapp><normalUnravelingEntry><rule><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp><var>x</var><conditions><condition><var>y</var><funapp><name>nil</name></funapp></condition></conditions></rule><name>c1</name><var>x</var><var>y</var><var>X0</var><var>X1</var></normalUnravelingEntry><normalUnravelingEntry><rule><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp><funapp><name>last</name><var>y</var></funapp><conditions><condition><var>y</var><funapp><name>cons</name><var>u</var><var>v</var></funapp></condition></conditions></rule><name>c1</name><var>x</var><var>y</var><var>u</var><var>v</var></normalUnravelingEntry><normalUnravelingEntry><rule><funapp><name>true__</name></funapp><funapp><name>false__</name></funapp><conditions><condition><var>x4</var><funapp><name>nil</name></funapp></condition><condition><var>x4</var><funapp><name>cons</name><var>x1</var><var>x2</var></funapp></condition></conditions></rule><name>c2</name><var>x4</var><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>last</name><funapp><name>cons</name><var>Y1</var><funapp><name>nil</name></funapp></funapp></funapp><var>Y1</var></rule><rule><funapp><name>c1</name><funapp><name>nil</name></funapp><var>x</var><var>y</var><var>X0</var><var>X1</var></funapp><var>x</var></rule><rule><funapp><name>c2</name><var>x4</var><var>x4</var><var>x4</var><var>x1</var><var>x2</var></funapp><funapp><name>true__</name></funapp></rule><rule><funapp><name>c2</name><funapp><name>nil</name></funapp><funapp><name>cons</name><var>x1</var><var>x2</var></funapp><var>x4</var><var>x1</var><var>x2</var></funapp><funapp><name>false__</name></funapp></rule><rule><funapp><name>c1</name><funapp><name>cons</name><var>u</var><var>v</var></funapp><var>x</var><var>y</var><var>u</var><var>v</var></funapp><funapp><name>last</name><var>y</var></funapp></rule><rule><funapp><name>c1</name><var>y</var><var>x</var><var>y</var><var>X0</var><var>X1</var></funapp><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp></rule><rule><funapp><name>last</name><funapp><name>cons</name><var>Y1</var><funapp><name>cons</name><var>Y2</var><var>Y3</var></funapp></funapp></funapp><funapp><name>last</name><funapp><name>cons</name><var>Y2</var><var>Y3</var></funapp></funapp></rule></rules></trs><approxCompletionProof><wcrProof><joinAutoNF /></wcrProof><trsTerminationProof><ruleRemoval><recursivePathOrder><statusPrecedence><statusPrecedenceEntry><name>true__</name><arity>0</arity><precedence>0</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>false__</name><arity>0</arity><precedence>1</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>c3</name><arity>1</arity><precedence>2</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>cons</name><arity>2</arity><precedence>3</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>nil</name><arity>0</arity><precedence>4</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>last</name><arity>1</arity><precedence>5</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>c1</name><arity>5</arity><precedence>6</precedence><lex /></statusPrecedenceEntry><statusPrecedenceEntry><name>c2</name><arity>5</arity><precedence>7</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>last</name><funapp><name>cons</name><var>Y1</var><funapp><name>nil</name></funapp></funapp></funapp><var>Y1</var></rule><rule><funapp><name>c1</name><funapp><name>nil</name></funapp><var>x</var><var>y</var><var>X0</var><var>X1</var></funapp><var>x</var></rule><rule><funapp><name>c2</name><var>x4</var><var>x4</var><var>x4</var><var>x1</var><var>x2</var></funapp><funapp><name>true__</name></funapp></rule><rule><funapp><name>c2</name><funapp><name>nil</name></funapp><funapp><name>cons</name><var>x1</var><var>x2</var></funapp><var>x4</var><var>x1</var><var>x2</var></funapp><funapp><name>false__</name></funapp></rule><rule><funapp><name>c1</name><funapp><name>cons</name><var>u</var><var>v</var></funapp><var>x</var><var>y</var><var>u</var><var>v</var></funapp><funapp><name>last</name><var>y</var></funapp></rule><rule><funapp><name>c1</name><var>y</var><var>x</var><var>y</var><var>X0</var><var>X1</var></funapp><funapp><name>last</name><funapp><name>cons</name><var>x</var><var>y</var></funapp></funapp></rule><rule><funapp><name>last</name><funapp><name>cons</name><var>Y1</var><funapp><name>cons</name><var>Y2</var><var>Y3</var></funapp></funapp></funapp><funapp><name>last</name><funapp><name>cons</name><var>Y2</var><var>Y3</var></funapp></funapp></rule></rules></trs><trsTerminationProof><rIsEmpty /></trsTerminationProof></ruleRemoval></trsTerminationProof></approxCompletionProof></approxAndCompletionAndNormalization></equationalDisproof></nonreachableEquationalDisproof></nonreachabilityProof></infeasibleSplitIf></infeasibilityProof></rightInlineConditions></infeasibilityProof></infeasibleGoalLifting></infeasibilityProof></proof></certificationProblem>