YES Problem: f(g(x)) -> f(h(x,x)) g(a()) -> g(g(a())) h(a(),a()) -> g(g(a())) Proof: Church Rosser Transformation Processor: strict: weak: critical peaks: 1 f(g(g(a()))) <-1|0[]- f(g(a())) -0|[]-> f(h(a(),a())) Shift Processor lab=left (dd) (force): strict: f(g(a())) -> f(g(g(a()))) f(g(a())) -> f(h(a(),a())) f(h(a(),a())) -> f(g(g(a()))) weak: f(g(x)) -> f(h(x,x)) g(a()) -> g(g(a())) h(a(),a()) -> g(g(a())) Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [f](x0) = [0 0 0]x0 [0 1 0] , [0] [a] = [1] [0], [1 0 0] [g](x0) = [1 0 0]x0 [1 1 0] , [1 0 0] [1 0 0] [h](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] orientation: [1] [0] f(g(a())) = [0] >= [0] = f(g(g(a()))) [0] [0] [1] [0] f(g(a())) = [0] >= [0] = f(h(a(),a())) [0] [0] [0] [0] f(h(a(),a())) = [0] >= [0] = f(g(g(a()))) [0] [0] [2 1 0] [2 0 0] f(g(x)) = [0 0 0]x >= [0 0 0]x = f(h(x,x)) [1 0 0] [0 0 0] [0] [0] g(a()) = [0] >= [0] = g(g(a())) [1] [0] [0] [0] h(a(),a()) = [0] >= [0] = g(g(a())) [0] [0] problem: strict: f(h(a(),a())) -> f(g(g(a()))) weak: f(g(x)) -> f(h(x,x)) g(a()) -> g(g(a())) h(a(),a()) -> g(g(a())) Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [f](x0) = [0 0 0]x0 [0 0 1] , [0] [a] = [1] [0], [1 0 0] [g](x0) = [0 0 0]x0 [1 1 0] , [1 0 0] [1 0 0] [h](x0, x1) = [0 0 1]x0 + [0 0 0]x1 [0 0 0] [0 1 0] orientation: [1] [0] f(h(a(),a())) = [0] >= [0] = f(g(g(a()))) [1] [0] [2 1 0] [2 1 0] f(g(x)) = [0 0 0]x >= [0 0 0]x = f(h(x,x)) [1 1 0] [0 1 0] [0] [0] g(a()) = [0] >= [0] = g(g(a())) [1] [0] [0] [0] h(a(),a()) = [0] >= [0] = g(g(a())) [1] [0] problem: strict: weak: f(g(x)) -> f(h(x,x)) g(a()) -> g(g(a())) h(a(),a()) -> g(g(a())) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): f(g(x)) -> f(h(x,x)): 0 g(a()) -> g(g(a())): 0 h(a(),a()) -> g(g(a())): 0 Rule Labeling Processor: strict: weak: rule labeling (left): f(g(x)) -> f(h(x,x)): 2 g(a()) -> g(g(a())): 0 h(a(),a()) -> g(g(a())): 0 Decreasing Processor: The following diagrams are decreasing: peak: f(g(g(a()))) <-1|0[=>0,==1,==0]- f(g(a())) -0|[?=2,==1,==0]-> f(h(a(),a())) joins (1): f(h(a(),a())) -2|0[=>0,>>0,==0]-> f(g(g(a()))) Qed