YES Problem: f(f(f(f(x)))) -> f(f(f(g(x,f(x))))) f(x) -> g(x,f(x)) Proof: Church Rosser Transformation Processor (star): strict: f(0)(x19) -> g(0)(x19) f(0)(x19) -> g(1)(f(0)(x19)) f(0)(f(0)(f(0)(f(0)(x20)))) -> f(0)(f(0)(f(0)(g(0)(x20)))) f(0)(f(0)(f(0)(f(0)(x20)))) -> f(0)(f(0)(f(0)(g(1)(f(0)(x20))))) weak: critical peaks: 8 f(f(f(f(g(x11,f(x11)))))) <-0|0[]- f(f(f(f(f(x11))))) -0|[]-> f(f(f(g(f(x11),f(f(x11)))))) f(f(f(f(f(g(x12,f(x12))))))) <-0|0,0[]- f(f(f(f(f(f(x12)))))) -0|[ ]-> f(f(f(g(f(f(x12)),f(f(f(x12))))))) f(f(f(f(f(f(g(x13,f(x13)))))))) <-0|0,0,0[]- f(f(f(f(f(f(f(x13))))))) -0| []-> f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) f(f(f(g(x14,f(x14))))) <-0|[]- f(f(f(f(x14)))) -1|[]-> g(f(f(f(x14))),f(f(f(f(x14))))) g(f(f(f(x))),f(f(f(f(x))))) <-1|[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x))))) f(g(f(f(x)),f(f(f(x))))) <-1|0[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x))))) f(f(g(f(x),f(f(x))))) <-1|0,0[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x))))) f(f(f(g(x,f(x))))) <-1|0,0,0[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x))))) Matrix Interpretation Processor: dim=2, star lab=right interpretation: [1 0] [g(1)](x0) = [0 0]x0, [1 0] [0] [g(0)](x0) = [0 0]x0 + [1], [1 1] [0] [f(0)](x0) = [0 0]x0 + [1] orientation: [1 1] [0] [1 0] [0] f(0)(x19) = [0 0]x19 + [1] >= [0 0]x19 + [1] = g(0)(x19) [1 1] [0] [1 1] f(0)(x19) = [0 0]x19 + [1] >= [0 0]x19 = g(1)(f(0)(x19)) [1 1] [3] [1 0] [3] f(0)(f(0)(f(0)(f(0)(x20)))) = [0 0]x20 + [1] >= [0 0]x20 + [1] = f(0)(f(0)(f(0)(g(0)(x20)))) [1 1] [3] [1 1] [2] f(0)(f(0)(f(0)(f(0)(x20)))) = [0 0]x20 + [1] >= [0 0]x20 + [1] = f(0)(f(0)(f(0)(g(1)(f(0)(x20))))) problem: strict: f(0)(x19) -> g(0)(x19) f(0)(x19) -> g(1)(f(0)(x19)) f(0)(f(0)(f(0)(f(0)(x20)))) -> f(0)(f(0)(f(0)(g(0)(x20)))) weak: Matrix Interpretation Processor: dim=2, star lab=right interpretation: [1 0] [g(1)](x0) = [0 0]x0, [1 0] [g(0)](x0) = [0 0]x0, [1 1] [0] [f(0)](x0) = [0 0]x0 + [1] orientation: [1 1] [0] [1 0] f(0)(x19) = [0 0]x19 + [1] >= [0 0]x19 = g(0)(x19) [1 1] [0] [1 1] f(0)(x19) = [0 0]x19 + [1] >= [0 0]x19 = g(1)(f(0)(x19)) [1 1] [3] [1 0] [2] f(0)(f(0)(f(0)(f(0)(x20)))) = [0 0]x20 + [1] >= [0 0]x20 + [1] = f(0)(f(0)(f(0)(g(0)(x20)))) problem: strict: f(0)(x19) -> g(0)(x19) f(0)(x19) -> g(1)(f(0)(x19)) weak: Matrix Interpretation Processor: dim=1, star lab=right interpretation: [g(1)](x0) = x0, [g(0)](x0) = x0, [f(0)](x0) = 2x0 + 2 orientation: f(0)(x19) = 2x19 + 2 >= x19 = g(0)(x19) f(0)(x19) = 2x19 + 2 >= 2x19 + 2 = g(1)(f(0)(x19)) problem: strict: f(0)(x19) -> g(1)(f(0)(x19)) weak: Shift Processor (**) lab=left: strict: weak: Shift Processor lab=left (dd): strict: f(f(f(f(f(x11))))) -> f(f(f(f(g(x11,f(x11)))))) f(f(f(f(f(x11))))) -> f(f(f(g(f(x11),f(f(x11)))))) f(f(f(f(g(x11,f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11))))))) f(f(f(g(f(x11),f(f(x11)))))) -> f(f(f(g(f(x11),f(g(x11,f(x11))))))) f(f(f(g(f(x11),f(g(x11,f(x11))))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11))))))) f(f(f(f(g(x11,f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11))))))) f(f(f(g(f(x11),f(f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(f(x11)))))) f(f(f(g(g(x11,f(x11)),f(f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11))))))) f(f(f(f(f(f(x12)))))) -> f(f(f(f(f(g(x12,f(x12))))))) f(f(f(f(f(f(x12)))))) -> f(f(f(g(f(f(x12)),f(f(f(x12))))))) f(f(f(f(f(g(x12,f(x12))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12)))))))) f(f(f(g(f(f(x12)),f(f(f(x12))))))) -> f(f(f(g(f(f(x12)),f(f(g(x12,f(x12)))))))) f(f(f(g(f(f(x12)),f(f(g(x12,f(x12)))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12)))))))) f(f(f(f(f(g(x12,f(x12))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12)))))))) f(f(f(g(f(f(x12)),f(f(f(x12))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(f(x12))))))) f(f(f(g(f(g(x12,f(x12))),f(f(f(x12))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12)))))))) f(f(f(f(f(f(f(x13))))))) -> f(f(f(f(f(f(g(x13,f(x13)))))))) f(f(f(f(f(f(f(x13))))))) -> f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) f(f(f(f(f(f(g(x13,f(x13)))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13))))))))) f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) -> f(f(f(g(f(f(f(x13))),f(f(f(g(x13,f(x13))))))))) f(f(f(g(f(f(f(x13))),f(f(f(g(x13,f(x13))))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13))))))))) f(f(f(f(f(f(g(x13,f(x13)))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13))))))))) f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(f(x13)))))))) f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(f(x13)))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13))))))))) f(f(f(f(x14)))) -> f(f(f(g(x14,f(x14))))) f(f(f(f(x14)))) -> g(f(f(f(x14))),f(f(f(f(x14))))) f(f(f(g(x14,f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14)))))) g(f(f(f(x14))),f(f(f(f(x14))))) -> g(f(f(f(x14))),f(f(f(g(x14,f(x14)))))) g(f(f(f(x14))),f(f(f(g(x14,f(x14)))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14)))))) f(f(f(g(x14,f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14)))))) g(f(f(f(x14))),f(f(f(f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(f(x14))))) g(f(f(g(x14,f(x14)))),f(f(f(f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14)))))) f(f(f(f(x)))) -> g(f(f(f(x))),f(f(f(f(x))))) f(f(f(f(x)))) -> f(f(f(g(x,f(x))))) g(f(f(f(x))),f(f(f(f(x))))) -> g(f(f(f(x))),f(f(f(g(x,f(x)))))) g(f(f(f(x))),f(f(f(g(x,f(x)))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x)))))) g(f(f(f(x))),f(f(f(f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(f(x))))) g(f(f(g(x,f(x)))),f(f(f(f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x)))))) f(f(f(f(x)))) -> f(g(f(f(x)),f(f(f(x))))) f(f(f(f(x)))) -> f(f(f(g(x,f(x))))) f(g(f(f(x)),f(f(f(x))))) -> f(g(f(f(x)),f(f(g(x,f(x)))))) f(g(f(f(x)),f(f(g(x,f(x)))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x)))))) f(g(f(f(x)),f(f(f(x))))) -> f(g(f(g(x,f(x))),f(f(f(x))))) f(g(f(g(x,f(x))),f(f(f(x))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x)))))) f(f(f(f(x)))) -> f(f(g(f(x),f(f(x))))) f(f(f(f(x)))) -> f(f(f(g(x,f(x))))) f(f(g(f(x),f(f(x))))) -> f(f(g(f(x),f(g(x,f(x)))))) f(f(g(f(x),f(g(x,f(x)))))) -> f(f(g(g(x,f(x)),f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -> f(f(g(g(x,f(x)),f(g(x,f(x)))))) f(f(g(f(x),f(f(x))))) -> f(f(g(g(x,f(x)),f(f(x))))) f(f(g(g(x,f(x)),f(f(x))))) -> f(f(g(g(x,f(x)),f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -> f(f(g(g(x,f(x)),f(g(x,f(x)))))) f(f(f(f(x)))) -> f(f(f(g(x,f(x))))) f(f(f(f(x)))) -> f(f(f(g(x,f(x))))) weak: f(f(f(f(x)))) -> f(f(f(g(x,f(x))))) f(x) -> g(x,f(x)) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (left): f(f(f(f(x)))) -> f(f(f(g(x,f(x))))): 1 f(x) -> g(x,f(x)): 0 Decreasing Processor: The following diagrams are decreasing: peak: f(f(f(f(g(x11,f(x11)))))) <-0|0[==1,==1,=?0,=?0,=?2]- f(f(f(f(f(x11))))) -0| [==1,==1,==0,==0,>=0]-> f(f(f(g(f(x11),f(f(x11)))))) joins (1): f(f(f(f(g(x11,f(x11)))))) -0|[==1,==1,==0,==0,>=0]-> f(f(f ( g ( g(x11,f(x11)),f(g(x11,f(x11))))))) f(f(f(g(f(x11),f(f(x11)))))) -1|0,0,0,1,0[>>0,==1,??2,??2,??30]-> f(f(f(g(f(x11),f(g(x11,f(x11))))))) -1|0,0,0,0[>>0,==1,??3,??2,??14]-> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11))))))) peak: f(f(f(f(f(g(x12,f(x12))))))) <-0|0,0[==1,==1,=?1,=?1,=?6]- f(f(f(f(f(f(x12)))))) -0|[==1,==1,>=0,>=0,>=0]-> f(f(f(g(f(f(x12)),f(f(f(x12))))))) joins (1): f(f(f(f(f(g(x12,f(x12))))))) -0|[==1,==1,>=0,>=0,>=0]-> f( f ( f ( g ( f(g(x12,f(x12))), f (f(g(x12,f(x12)))))))) f(f(f(g(f(f(x12)),f(f(f(x12))))))) -1|0,0,0,1,0,0[>>0,==1,??3,??3,??62]-> f(f(f(g(f(f(x12)),f(f(g(x12,f(x12)))))))) -1|0,0,0,0,0[>>0,==1,??3,??2,??30]-> f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12)))))))) peak: f(f(f(f(f(f(g(x13,f(x13)))))))) <-0|0,0,0[==1,==1,=?2,=?2,=?14]- f(f(f(f(f(f(f(x13))))))) -0|[==1,==1,>=0,>=0,>=0]-> f(f(f( g(f(f(f(x13))),f(f(f(f(x13)))))))) joins (1): f(f(f(f(f(f(g(x13,f(x13)))))))) -0|[==1,==1,>=0,>=0,>=0]-> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13))))))))) f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) -0|0,0,0,1[==1,==1,=?2,=?2,=?14]-> f(f(f(g(f(f(f(x13))),f(f(f(g(x13,f(x13))))))))) -1|0,0,0,0,0,0[ >>0,==1,??4,??3,??62]-> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13))))))))) peak: f(f(f(g(x14,f(x14))))) <-0|[=?1,==1,==0,==0,==0]- f(f(f(f(x14)))) -1| [>=0,==1,==0,==0,==0]-> g(f(f(f(x14))),f(f(f(f(x14))))) joins (1): f(f(f(g(x14,f(x14))))) -1|[>=0,==1,==0,==0,==0]-> g(f(f(g(x14,f(x14)))), f(f(f(g(x14,f(x14)))))) g(f(f(f(x14))),f(f(f(f(x14))))) -0|1[=?1,==1,==0,==0,==0]-> g(f(f(f(x14))),f(f(f(g(x14,f(x14)))))) -1|0,0,0[>=0,==1,??1,??1,??6]-> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14)))))) peak: g(f(f(f(x))),f(f(f(f(x))))) <-1|[=>0,==1,==0,==0,==0]- f(f(f(f(x)))) -0| [?=1,==1,==0,==0,==0]-> f(f(f(g(x,f(x))))) joins (1): g(f(f(f(x))),f(f(f(f(x))))) -0|1[?=1,==1,==0,==0,==0]-> g(f(f(f(x))),f(f(f(g(x,f(x)))))) -1| 0, 0, 0[ =>0,==1,??1,??1,??6]-> g( f(f(g(x,f(x)))), f (f(f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -1|[=>0,==1,==0,==0,==0]-> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x)))))) peak: f(g(f(f(x)),f(f(f(x))))) <-1|0[=>0,==1,=?0,=?0,=?2]- f(f(f(f(x)))) -0| [?=1,==1,==0,==0,>=0]-> f(f(f(g(x,f(x))))) joins (1): f(g(f(f(x)),f(f(f(x))))) -1|0,1,0,0[=>0,==1,??1,??1,??14]-> f(g(f(f(x)),f(f(g(x,f(x)))))) -1|0,0,0[=>0,==1,??1,=?0,??6]-> f(g(f(g(x,f(x))),f(f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -1|0[=>0,==1,=?0,=?0,=?2]-> f(g(f(g(x,f(x))),f(f(g(x,f(x)))))) peak: f(f(g(f(x),f(f(x))))) <-1|0,0[=>0,==1,=?1,=?1,=?6]- f(f(f(f(x)))) -0| [?=1,==1,>=0,>=0,>=0]-> f(f(f(g(x,f(x))))) joins (1): f(f(g(f(x),f(f(x))))) -1|0,0,1,0[=>0,==1,=?1,=?1,??14]-> f(f(g(f(x),f(g(x,f(x)))))) -1| 0, 0, 0[ =>0,==1,??2,=?1,=?6]-> f (f(g(g(x,f(x)),f(g(x,f(x)))))) f(f(f(g(x,f(x))))) -1|0,0[=>0,==1,=?1,=?1,=?6]-> f(f(g(g(x,f(x)),f(g(x,f(x)))))) peak: f(f(f(g(x,f(x))))) <-1|0,0,0[=>0,==1,=?2,=?2,=?14]- f(f(f(f(x)))) -0| [?=1,==1,>=0,>=0,>=0]-> f(f(f(g(x,f(x))))) joins (1): Qed