YES Time: 0.453 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: empty ~ unionAC weight function: w0 = 1 w(empty) = 7 w(unionAC) = 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: 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# ~ 0 ~ empty > s > max ~ singl ~ unionAC weight function: w0 = 2 w(max) = w(singl) = 4 w(max#) = w(0) = w(empty) = w(unionAC) = 2 w(s) = 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: singl > max# ~ s ~ unionAC weight function: w0 = 2 w(unionAC) = 6 w(s) = 3 w(max#) = w(singl) = 2 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