YES Time: 1.026 Problem: Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) Proof: DP Processor: Equations#: union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7)) union{AC,#}(x5,x6) -> union{AC,#}(x6,x5) union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7) union{AC,#}(x6,x5) -> union{AC,#}(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> union{AC,#}(singl(x),singl(y)) max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(Y,Z)) max#(unionAC(singl(x),unionAC(Y,Z))) -> union{AC,#}(singl(x),singl(max(unionAC(Y,Z)))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(singl(x),singl(max(unionAC(Y,Z))))) union{AC,#}(x8,unionAC(empty(),X)) -> union{AC,#}(x8,X) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: union{AC,#}(unionAC(x9,x10),x11) -> union{AC,#}(x9,x10) union{AC,#}(x9,unionAC(x10,x11)) -> union{AC,#}(x10,x11) AC-EDG Processor: Equations#: union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7)) union{AC,#}(x5,x6) -> union{AC,#}(x6,x5) union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7) union{AC,#}(x6,x5) -> union{AC,#}(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> union{AC,#}(singl(x),singl(y)) max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(Y,Z)) max#(unionAC(singl(x),unionAC(Y,Z))) -> union{AC,#}(singl(x),singl(max(unionAC(Y,Z)))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(singl(x),singl(max(unionAC(Y,Z))))) union{AC,#}(x8,unionAC(empty(),X)) -> union{AC,#}(x8,X) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: union{AC,#}(unionAC(x9,x10),x11) -> union{AC,#}(x9,x10) union{AC,#}(x9,unionAC(x10,x11)) -> union{AC,#}(x10,x11) SCC Processor: #sccs: 2 #rules: 4 #arcs: 16/36 Equations#: union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7)) union{AC,#}(x5,x6) -> union{AC,#}(x6,x5) union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7) union{AC,#}(x6,x5) -> union{AC,#}(x5,x6) DPs: union{AC,#}(x8,unionAC(empty(),X)) -> union{AC,#}(x8,X) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: union{AC,#}(unionAC(x9,x10),x11) -> union{AC,#}(x9,x10) union{AC,#}(x9,unionAC(x10,x11)) -> union{AC,#}(x10,x11) AC-DP unlabeling: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: unionAC(x8,unionAC(empty(),X)) -> unionAC(x8,X) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) Usable Rule Processor: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: unionAC(x8,unionAC(empty(),X)) -> unionAC(x8,X) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) AC-KBO Processor: argument filtering: pi(unionAC) = [0,1] pi(empty) = [] precedence: unionAC > empty weight function: [empty] = 2, [unionAC](x0, x1) = x0 + x1 usable rules: unionAC(empty(),X) -> X problem: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) Qed Equations#: union{AC,#}(unionAC(x5,x6),x7) -> union{AC,#}(x5,unionAC(x6,x7)) union{AC,#}(x5,x6) -> union{AC,#}(x6,x5) union{AC,#}(x5,unionAC(x6,x7)) -> union{AC,#}(unionAC(x5,x6),x7) union{AC,#}(x6,x5) -> union{AC,#}(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(singl(x),singl(max(unionAC(Y,Z))))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(Y,Z)) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: union{AC,#}(unionAC(x9,x10),x11) -> union{AC,#}(x9,x10) union{AC,#}(x9,unionAC(x10,x11)) -> union{AC,#}(x10,x11) AC-DP unlabeling: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(singl(x),singl(max(unionAC(Y,Z))))) max#(unionAC(singl(x),unionAC(Y,Z))) -> max#(unionAC(Y,Z)) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) AC-KBO Processor: argument filtering: pi(unionAC) = [0,1] pi(empty) = [] pi(singl) = [] pi(max) = [] pi(0) = [] pi(s) = [0] pi(max#) = [0] precedence: max# > s ~ max ~ unionAC > 0 ~ singl ~ empty weight function: [max#](x0) = 4x0, [s](x0) = 3x0 + 6, [0] = 2, [max](x0) = 7, [singl](x0) = 1, [empty] = 4, [unionAC](x0, x1) = x0 + x1 + 1 usable rules: unionAC(empty(),X) -> X problem: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) Restore Modifier: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) AC-DP unlabeling: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: unionAC(empty(),X) -> X max(singl(x)) -> x max(unionAC(singl(x),singl(0()))) -> x max(unionAC(singl(s(x)),singl(s(y)))) -> s(max(unionAC(singl(x),singl(y)))) max(unionAC(singl(x),unionAC(Y,Z))) -> max(unionAC(singl(x),singl(max(unionAC(Y,Z))))) S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) Usable Rule Processor: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: max#(unionAC(singl(s(x)),singl(s(y)))) -> max#(unionAC(singl(x),singl(y))) Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) AC-KBO Processor: argument filtering: pi(unionAC) = [0,1] pi(singl) = [0] pi(s) = [0] pi(max#) = 0 precedence: s > unionAC > max# ~ singl weight function: [max#](x0) = x0, [s](x0) = x0, [singl](x0) = x0 + 1, [unionAC](x0, x1) = x0 + x1 usable rules: problem: Equations#: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) DPs: Equations: unionAC(unionAC(x5,x6),x7) -> unionAC(x5,unionAC(x6,x7)) unionAC(x5,x6) -> unionAC(x6,x5) unionAC(x5,unionAC(x6,x7)) -> unionAC(unionAC(x5,x6),x7) unionAC(x6,x5) -> unionAC(x5,x6) TRS: S: unionAC(unionAC(x9,x10),x11) -> unionAC(x9,x10) unionAC(x9,unionAC(x10,x11)) -> unionAC(x10,x11) Qed