MAYBE 72.09/23.11 MAYBE 72.09/23.11 72.09/23.11 Problem: 72.09/23.11 R(x1) -> r(x1) 72.09/23.11 r(p(x1)) -> p(p(r(P(x1)))) 72.09/23.11 r(r(x1)) -> x1 72.09/23.11 r(P(P(x1))) -> P(P(r(x1))) 72.09/23.11 p(P(x1)) -> x1 72.09/23.11 P(p(x1)) -> x1 72.09/23.11 r(R(x1)) -> x1 72.09/23.11 R(r(x1)) -> x1 72.09/23.11 72.09/23.11 Proof: 72.09/23.11 Open 72.09/23.11 EOF