MAYBE Problem: a(b(a(x1))) -> b(x1) b(a(b(x1))) -> b(b(b(x1))) b(b(x1)) -> a(a(a(x1))) Proof: DP Processor: DPs: a#(b(a(x1))) -> b#(x1) b#(a(b(x1))) -> b#(b(x1)) b#(a(b(x1))) -> b#(b(b(x1))) b#(b(x1)) -> a#(x1) b#(b(x1)) -> a#(a(x1)) b#(b(x1)) -> a#(a(a(x1))) TRS: a(b(a(x1))) -> b(x1) b(a(b(x1))) -> b(b(b(x1))) b(b(x1)) -> a(a(a(x1))) TDG Processor: DPs: a#(b(a(x1))) -> b#(x1) b#(a(b(x1))) -> b#(b(x1)) b#(a(b(x1))) -> b#(b(b(x1))) b#(b(x1)) -> a#(x1) b#(b(x1)) -> a#(a(x1)) b#(b(x1)) -> a#(a(a(x1))) TRS: a(b(a(x1))) -> b(x1) b(a(b(x1))) -> b(b(b(x1))) b(b(x1)) -> a(a(a(x1))) graph: b#(b(x1)) -> a#(a(a(x1))) -> a#(b(a(x1))) -> b#(x1) b#(b(x1)) -> a#(a(x1)) -> a#(b(a(x1))) -> b#(x1) b#(b(x1)) -> a#(x1) -> a#(b(a(x1))) -> b#(x1) b#(a(b(x1))) -> b#(b(b(x1))) -> b#(b(x1)) -> a#(a(a(x1))) b#(a(b(x1))) -> b#(b(b(x1))) -> b#(b(x1)) -> a#(a(x1)) b#(a(b(x1))) -> b#(b(b(x1))) -> b#(b(x1)) -> a#(x1) b#(a(b(x1))) -> b#(b(b(x1))) -> b#(a(b(x1))) -> b#(b(b(x1))) b#(a(b(x1))) -> b#(b(b(x1))) -> b#(a(b(x1))) -> b#(b(x1)) b#(a(b(x1))) -> b#(b(x1)) -> b#(b(x1)) -> a#(a(a(x1))) b#(a(b(x1))) -> b#(b(x1)) -> b#(b(x1)) -> a#(a(x1)) b#(a(b(x1))) -> b#(b(x1)) -> b#(b(x1)) -> a#(x1) b#(a(b(x1))) -> b#(b(x1)) -> b#(a(b(x1))) -> b#(b(b(x1))) b#(a(b(x1))) -> b#(b(x1)) -> b#(a(b(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(b(x1)) -> a#(a(a(x1))) a#(b(a(x1))) -> b#(x1) -> b#(b(x1)) -> a#(a(x1)) a#(b(a(x1))) -> b#(x1) -> b#(b(x1)) -> a#(x1) a#(b(a(x1))) -> b#(x1) -> b#(a(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(b(x1))) -> b#(b(x1)) SCC Processor: #sccs: 1 #rules: 6 #arcs: 18/36 DPs: b#(b(x1)) -> a#(a(a(x1))) a#(b(a(x1))) -> b#(x1) b#(a(b(x1))) -> b#(b(x1)) b#(a(b(x1))) -> b#(b(b(x1))) b#(b(x1)) -> a#(x1) b#(b(x1)) -> a#(a(x1)) TRS: a(b(a(x1))) -> b(x1) b(a(b(x1))) -> b(b(b(x1))) b(b(x1)) -> a(a(a(x1))) Open