MAYBE Problem: f(x,y,z) -> g(x,y,z) g(0(),1(),x) -> f(x,x,x) a() -> b() a() -> c() Proof: DP Processor: DPs: f#(x,y,z) -> g#(x,y,z) g#(0(),1(),x) -> f#(x,x,x) TRS: f(x,y,z) -> g(x,y,z) g(0(),1(),x) -> f(x,x,x) a() -> b() a() -> c() Usable Rule Processor: DPs: f#(x,y,z) -> g#(x,y,z) g#(0(),1(),x) -> f#(x,x,x) TRS: f10(x,y) -> x f10(x,y) -> y CDG Processor: DPs: f#(x,y,z) -> g#(x,y,z) g#(0(),1(),x) -> f#(x,x,x) TRS: f10(x,y) -> x f10(x,y) -> y graph: g#(0(),1(),x) -> f#(x,x,x) -> f#(x,y,z) -> g#(x,y,z) f#(x,y,z) -> g#(x,y,z) -> g#(0(),1(),x) -> f#(x,x,x) Restore Modifier: DPs: f#(x,y,z) -> g#(x,y,z) g#(0(),1(),x) -> f#(x,x,x) TRS: f(x,y,z) -> g(x,y,z) g(0(),1(),x) -> f(x,x,x) a() -> b() a() -> c() SCC Processor: #sccs: 1 #rules: 2 #arcs: 2/4 DPs: g#(0(),1(),x) -> f#(x,x,x) f#(x,y,z) -> g#(x,y,z) TRS: f(x,y,z) -> g(x,y,z) g(0(),1(),x) -> f(x,x,x) a() -> b() a() -> c() Open