Problem: a() -> b() a() -> f(a()) b() -> f(f(b())) f(f(f(b()))) -> b() Proof: Commute Transformation Processor: a() -> b() a() -> f(a()) b() -> f(f(b())) f(f(b())) -> b() f(f(f(b()))) -> b() b() -> f(f(f(b()))) Church Rosser Transformation Processor (star): strict: weak: critical peaks: 9 b() <-0|[]- a() -1|[]-> f(a()) f(a()) <-1|[]- a() -0|[]-> b() f(f(f(f(b())))) <-2|0,0[]- f(f(b())) -3|[]-> b() f(f(f(f(f(b()))))) <-2|0,0,0[]- f(f(f(b()))) -4|[]-> b() f(f(b())) <-2|[]- b() -5|[]-> f(f(f(b()))) f(b()) <-3|0[]- f(f(f(b()))) -4|[]-> b() f(f(f(b()))) <-5|[]- b() -2|[]-> f(f(b())) f(f(f(f(f(b()))))) <-5|0,0[]- f(f(b())) -3|[]-> b() f(f(f(f(f(f(b())))))) <-5|0,0,0[]- f(f(f(b()))) -4|[]-> b() Shift Processor lab=left (dd): strict: a() -> b() a() -> f(a()) b() -> f(f(b())) f(a()) -> f(f(a())) f(f(a())) -> f(f(b())) b() -> f(f(f(b()))) f(a()) -> f(b()) f(b()) -> f(f(f(b()))) b() -> f(f(b())) f(f(b())) -> f(f(f(f(b())))) f(a()) -> f(b()) f(b()) -> f(f(f(f(b())))) b() -> f(f(f(b()))) f(f(f(b()))) -> f(b()) f(a()) -> f(b()) a() -> f(a()) a() -> b() f(a()) -> f(b()) b() -> f(f(f(b()))) f(f(f(b()))) -> f(b()) f(a()) -> f(b()) f(b()) -> f(f(f(b()))) b() -> f(f(f(b()))) f(a()) -> f(b()) f(b()) -> f(f(f(f(b())))) b() -> f(f(b())) f(f(b())) -> f(f(f(f(b())))) f(a()) -> f(f(a())) f(f(a())) -> f(f(b())) b() -> f(f(b())) f(f(b())) -> f(f(f(f(b())))) f(f(b())) -> b() f(f(f(f(b())))) -> f(f(b())) b() -> f(f(b())) f(f(f(b()))) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> b() f(f(f(f(f(b()))))) -> f(f(f(b()))) b() -> f(f(f(b()))) f(f(f(f(f(b()))))) -> f(f(b())) b() -> f(f(b())) b() -> f(f(b())) b() -> f(f(f(b()))) f(f(b())) -> b() f(f(f(b()))) -> b() f(f(b())) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> f(b()) f(f(f(b()))) -> b() f(b()) -> f(f(f(b()))) b() -> f(f(f(b()))) b() -> f(f(f(b()))) b() -> f(f(b())) f(f(f(b()))) -> f(f(f(f(f(b()))))) f(f(b())) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> b() f(f(b())) -> b() f(f(b())) -> f(f(f(f(f(b()))))) f(f(b())) -> b() f(f(f(f(f(b()))))) -> f(f(f(b()))) b() -> f(f(f(b()))) f(f(f(f(f(b()))))) -> f(f(b())) b() -> f(f(b())) f(f(f(b()))) -> f(f(f(f(f(f(b())))))) f(f(f(b()))) -> b() f(f(f(f(f(f(b())))))) -> f(f(f(b()))) b() -> f(f(f(b()))) weak: a() -> b() a() -> f(a()) b() -> f(f(b())) f(f(b())) -> b() f(f(f(b()))) -> b() b() -> f(f(f(b()))) Polynomial Interpretation Processor: dimension: 1 interpretation: [f](x0) = x0, [b] = 0, [a] = 2 orientation: a() = 2 >= 0 = b() a() = 2 >= 2 = f(a()) b() = 0 >= 0 = f(f(b())) f(a()) = 2 >= 2 = f(f(a())) f(f(a())) = 2 >= 0 = f(f(b())) b() = 0 >= 0 = f(f(f(b()))) f(a()) = 2 >= 0 = f(b()) f(b()) = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(b())) f(f(b())) = 0 >= 0 = f(f(f(f(b())))) f(a()) = 2 >= 0 = f(b()) f(b()) = 0 >= 0 = f(f(f(f(b())))) b() = 0 >= 0 = f(f(f(b()))) f(f(f(b()))) = 0 >= 0 = f(b()) f(a()) = 2 >= 0 = f(b()) a() = 2 >= 2 = f(a()) a() = 2 >= 0 = b() f(a()) = 2 >= 0 = f(b()) b() = 0 >= 0 = f(f(f(b()))) f(f(f(b()))) = 0 >= 0 = f(b()) f(a()) = 2 >= 0 = f(b()) f(b()) = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(f(b()))) f(a()) = 2 >= 0 = f(b()) f(b()) = 0 >= 0 = f(f(f(f(b())))) b() = 0 >= 0 = f(f(b())) f(f(b())) = 0 >= 0 = f(f(f(f(b())))) f(a()) = 2 >= 2 = f(f(a())) f(f(a())) = 2 >= 0 = f(f(b())) b() = 0 >= 0 = f(f(b())) f(f(b())) = 0 >= 0 = f(f(f(f(b())))) f(f(b())) = 0 >= 0 = b() f(f(f(f(b())))) = 0 >= 0 = f(f(b())) b() = 0 >= 0 = f(f(b())) f(f(f(b()))) = 0 >= 0 = f(f(f(f(f(b()))))) f(f(f(b()))) = 0 >= 0 = b() f(f(f(f(f(b()))))) = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(f(b()))) f(f(f(f(f(b()))))) = 0 >= 0 = f(f(b())) b() = 0 >= 0 = f(f(b())) b() = 0 >= 0 = f(f(b())) b() = 0 >= 0 = f(f(f(b()))) f(f(b())) = 0 >= 0 = b() f(f(f(b()))) = 0 >= 0 = b() f(f(b())) = 0 >= 0 = f(f(f(f(f(b()))))) f(f(f(b()))) = 0 >= 0 = f(f(f(f(f(b()))))) f(f(f(b()))) = 0 >= 0 = f(b()) f(f(f(b()))) = 0 >= 0 = b() f(b()) = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(b())) f(f(f(b()))) = 0 >= 0 = f(f(f(f(f(b()))))) f(f(b())) = 0 >= 0 = f(f(f(f(f(b()))))) f(f(f(b()))) = 0 >= 0 = b() f(f(b())) = 0 >= 0 = b() f(f(b())) = 0 >= 0 = f(f(f(f(f(b()))))) f(f(b())) = 0 >= 0 = b() f(f(f(f(f(b()))))) = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(f(b()))) f(f(f(f(f(b()))))) = 0 >= 0 = f(f(b())) b() = 0 >= 0 = f(f(b())) f(f(f(b()))) = 0 >= 0 = f(f(f(f(f(f(b())))))) f(f(f(b()))) = 0 >= 0 = b() f(f(f(f(f(f(b())))))) = 0 >= 0 = f(f(f(b()))) b() = 0 >= 0 = f(f(f(b()))) problem: strict: a() -> f(a()) b() -> f(f(b())) f(a()) -> f(f(a())) b() -> f(f(f(b()))) f(b()) -> f(f(f(b()))) b() -> f(f(b())) f(f(b())) -> f(f(f(f(b())))) f(b()) -> f(f(f(f(b())))) b() -> f(f(f(b()))) f(f(f(b()))) -> f(b()) a() -> f(a()) b() -> f(f(f(b()))) f(f(f(b()))) -> f(b()) f(b()) -> f(f(f(b()))) b() -> f(f(f(b()))) f(b()) -> f(f(f(f(b())))) b() -> f(f(b())) f(f(b())) -> f(f(f(f(b())))) f(a()) -> f(f(a())) b() -> f(f(b())) f(f(b())) -> f(f(f(f(b())))) f(f(b())) -> b() f(f(f(f(b())))) -> f(f(b())) b() -> f(f(b())) f(f(f(b()))) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> b() f(f(f(f(f(b()))))) -> f(f(f(b()))) b() -> f(f(f(b()))) f(f(f(f(f(b()))))) -> f(f(b())) b() -> f(f(b())) b() -> f(f(b())) b() -> f(f(f(b()))) f(f(b())) -> b() f(f(f(b()))) -> b() f(f(b())) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> f(b()) f(f(f(b()))) -> b() f(b()) -> f(f(f(b()))) b() -> f(f(f(b()))) b() -> f(f(f(b()))) b() -> f(f(b())) f(f(f(b()))) -> f(f(f(f(f(b()))))) f(f(b())) -> f(f(f(f(f(b()))))) f(f(f(b()))) -> b() f(f(b())) -> b() f(f(b())) -> f(f(f(f(f(b()))))) f(f(b())) -> b() f(f(f(f(f(b()))))) -> f(f(f(b()))) b() -> f(f(f(b()))) f(f(f(f(f(b()))))) -> f(f(b())) b() -> f(f(b())) f(f(f(b()))) -> f(f(f(f(f(f(b())))))) f(f(f(b()))) -> b() f(f(f(f(f(f(b())))))) -> f(f(f(b()))) b() -> f(f(f(b()))) weak: a() -> f(a()) b() -> f(f(b())) f(f(b())) -> b() f(f(f(b()))) -> b() b() -> f(f(f(b()))) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: b() <-0|[1]- a() -1|[1]-> f(a()) joins: b() -5|[0]-> f(f(f(b()))) f(a()) -0|0[1]-> f(b()) -2|0[0]-> f(f(f(b()))) peak: f(a()) <-1|[1]- a() -0|[1]-> b() joins: f(a()) -0|0[1]-> f(b()) b() -5|[0]-> f(f(f(b()))) -3|0[0]-> f(b()) peak: f(f(f(f(b())))) <-2|0,0[1]- f(f(b())) -3|[1]-> b() joins: f(f(f(f(b())))) -3|0,0[1]-> f(f(b())) b() -2|[1]-> f(f(b())) peak: f(f(f(f(f(b()))))) <-2|0,0,0[1]- f(f(f(b()))) -4|[1]-> b() joins: f(f(f(f(f(b()))))) -3|0,0,0[1]-> f(f(f(b()))) b() -5|[1]-> f(f(f(b()))) peak: f(f(b())) <-2|[1]- b() -5|[1]-> f(f(f(b()))) joins: f(f(b())) -3|[1]-> b() f(f(f(b()))) -4|[1]-> b() peak: f(b()) <-3|0[1]- f(f(f(b()))) -4|[1]-> b() joins: f(b()) -2|0[1]-> f(f(f(b()))) b() -5|[1]-> f(f(f(b()))) peak: f(f(f(b()))) <-5|[1]- b() -2|[1]-> f(f(b())) joins: f(f(f(b()))) -2|0,0,0[1]-> f(f(f(f(f(b()))))) f(f(b())) -5|0,0[1]-> f(f(f(f(f(b()))))) peak: f(f(f(f(f(b()))))) <-5|0,0[1]- f(f(b())) -3|[1]-> b() joins: f(f(f(f(f(b()))))) -3|0,0,0[1]-> f(f(f(b()))) b() -5|[1]-> f(f(f(b()))) peak: f(f(f(f(f(f(b())))))) <-5|0,0,0[1]- f(f(f(b()))) -4|[1]-> b() joins: f(f(f(f(f(f(b())))))) -4|0,0,0[1]-> f(f(f(b()))) b() -5|[1]-> f(f(f(b()))) Qed