0.00/0.32 YES 0.00/0.32 Proof: 0.00/0.32 To show the infeasibility of the given CoCo INF problem, 0.00/0.32 we transform the problem into a word problem by the split-if encoding (Claessen and Smallbone, 2018). 0.00/0.32 It suffices to show that the follwing ES does not entail true__ = false__ . 0.00/0.32 ES: 0.00/0.32 pin(a) = pout(b) 0.00/0.32 pin(b) = pout(c) 0.00/0.32 tc(x) = x 0.00/0.32 f1(pout(z),x,y) = tc(x) 0.00/0.32 f2(tc(z),x,y) = f1(pin(x),x,y) 0.00/0.32 f2(y,x,y) = y 0.00/0.32 f3(pout(z)) = true__ 0.00/0.32 f4(tc(z),x1) = f3(pin(x1)) 0.00/0.32 f4(x2,x1) = false__ 0.00/0.32 f5(false__) = false__ 0.00/0.32 f5(true__) = true__ 0.00/0.32 0.00/0.32 The ES admits the following equivalent ground-complete ordered rewrite system: 0.00/0.32 LPO with precedence: tc > f4 > f5 > f1 > f2 > c > b > pin > a > pout > true__ > f3 > false__ > z 0.00/0.32 ES: 0.00/0.32 f4(x201,x112) -> false__ 0.00/0.32 f3(pin(x12)) -> false__ 0.00/0.32 pout(b) -> pin(a) 0.00/0.32 pout(c) -> pin(b) 0.00/0.32 tc(x) -> x 0.00/0.32 f1(pout(z),x,y) -> x 0.00/0.32 f1(pin(x),x,y) -> f2(z,x,y) 0.00/0.32 f2(y,x,y) -> y 0.00/0.32 f3(pout(z)) -> true__ 0.00/0.32 f5(false__) -> false__ 0.00/0.32 f5(true__) -> true__ 0.00/0.32 0.00/0.32 Since true__ and false__ are not joinable, 0.00/0.32 the original problem is infeasible. 0.00/0.33 EOF