Problem: h(f(),a(),a()) -> h(g(),a(),a()) h(g(),a(),a()) -> h(f(),a(),a()) a() -> a'() h(x,a'(),y) -> h(x,y,y) g() -> f() f() -> g() Proof: Church Rosser Transformation Processor (star): strict: h(2)(y) -> h(1)(y) h(2)(y) -> h(2)(y) weak: h(0)(x) -> h(0)(x) critical peaks: 6 h(f(),a'(),a()) <-2|1[]- h(f(),a(),a()) -0|[]-> h(g(),a(),a()) h(f(),a(),a'()) <-2|2[]- h(f(),a(),a()) -0|[]-> h(g(),a(),a()) h(g(),a'(),a()) <-2|1[]- h(g(),a(),a()) -1|[]-> h(f(),a(),a()) h(g(),a(),a'()) <-2|2[]- h(g(),a(),a()) -1|[]-> h(f(),a(),a()) h(f(),a(),a()) <-4|0[]- h(g(),a(),a()) -1|[]-> h(f(),a(),a()) h(g(),a(),a()) <-5|0[]- h(f(),a(),a()) -0|[]-> h(g(),a(),a()) Matrix Interpretation Processor: dim=1, lab=right interpretation: [h(1)](x0) = x0, [h(2)](x0) = x0 + 1, [h(0)](x0) = 2x0 orientation: h(2)(y) = y + 1 >= y = h(1)(y) h(2)(y) = y + 1 >= y + 1 = h(2)(y) h(0)(x) = 2x >= 2x = h(0)(x) problem: strict: h(2)(y) -> h(2)(y) weak: h(0)(x) -> h(0)(x) Shift Processor (**) lab=left: strict: weak: Shift Processor lab=left (dd): strict: h(f(),a(),a()) -> h(f(),a'(),a()) h(f(),a(),a()) -> h(g(),a(),a()) h(f(),a'(),a()) -> h(f(),a(),a()) h(g(),a(),a()) -> h(f(),a(),a()) h(f(),a'(),a()) -> h(g(),a'(),a()) h(g(),a(),a()) -> h(g(),a'(),a()) h(f(),a(),a()) -> h(f(),a(),a'()) h(f(),a(),a()) -> h(g(),a(),a()) h(f(),a(),a'()) -> h(g(),a(),a'()) h(g(),a(),a()) -> h(g(),a(),a'()) h(g(),a(),a()) -> h(g(),a'(),a()) h(g(),a(),a()) -> h(f(),a(),a()) h(g(),a'(),a()) -> h(g(),a(),a()) h(f(),a(),a()) -> h(g(),a(),a()) h(g(),a'(),a()) -> h(f(),a'(),a()) h(f(),a(),a()) -> h(f(),a'(),a()) h(g(),a(),a()) -> h(g(),a(),a'()) h(g(),a(),a()) -> h(f(),a(),a()) h(g(),a(),a'()) -> h(f(),a(),a'()) h(f(),a(),a()) -> h(f(),a(),a'()) h(g(),a(),a()) -> h(f(),a(),a()) h(g(),a(),a()) -> h(f(),a(),a()) h(f(),a(),a()) -> h(g(),a(),a()) h(f(),a(),a()) -> h(g(),a(),a()) weak: h(f(),a(),a()) -> h(g(),a(),a()) h(g(),a(),a()) -> h(f(),a(),a()) a() -> a'() h(x,a'(),y) -> h(x,y,y) g() -> f() f() -> g() Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: h(f(),a'(),a()) <-2|1[1,0]- h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a()) joins: h(f(),a'(),a()) -3|[1,0]-> h(f(),a(),a()) h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a()) peak: h(f(),a(),a'()) <-2|2[1,1]- h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a()) joins: h(f(),a(),a'()) -5|0[1,0]-> h(g(),a(),a'()) h(g(),a(),a()) -2|2[1,1]-> h(g(),a(),a'()) peak: h(g(),a'(),a()) <-2|1[1,0]- h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a()) joins: h(g(),a'(),a()) -3|[1,0]-> h(g(),a(),a()) h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a()) peak: h(g(),a(),a'()) <-2|2[1,1]- h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a()) joins: h(g(),a(),a'()) -4|0[1,0]-> h(f(),a(),a'()) h(f(),a(),a()) -2|2[1,1]-> h(f(),a(),a'()) peak: h(f(),a(),a()) <-4|0[1,0]- h(g(),a(),a()) -1|[1,0]-> h(f(),a(),a()) joins: peak: h(g(),a(),a()) <-5|0[1,0]- h(f(),a(),a()) -0|[1,0]-> h(g(),a(),a()) joins: Qed