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