YES Problem: f(a(),x) -> g(a(),x) g(a(),x) -> f(b(),x) f(a(),x) -> f(b(),x) Proof: Matrix Interpretation Processor: dim=3 interpretation: [0] [b] = [0] [0], [1 0 0] [1 0 0] [g](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [1 0 1] [1 0 0] [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [0] [a] = [0] [1] orientation: [1 0 0] [1] [1 0 0] f(a(),x) = [0 0 0]x + [0] >= [0 0 0]x = g(a(),x) [0 0 0] [0] [0 0 0] [1 0 0] [1 0 0] g(a(),x) = [0 0 0]x >= [0 0 0]x = f(b(),x) [0 0 0] [0 0 0] [1 0 0] [1] [1 0 0] f(a(),x) = [0 0 0]x + [0] >= [0 0 0]x = f(b(),x) [0 0 0] [0] [0 0 0] problem: g(a(),x) -> f(b(),x) Matrix Interpretation Processor: dim=3 interpretation: [0] [b] = [0] [0], [1 0 1] [1 0 0] [g](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [1 0 0] [1 0 0] [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [0] [a] = [0] [1] orientation: [1 0 0] [1] [1 0 0] g(a(),x) = [0 0 0]x + [0] >= [0 0 0]x = f(b(),x) [0 0 0] [0] [0 0 0] problem: Qed