MAYBE Problem: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Proof: DP Processor: DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) i#(*(x,y)) -> i#(x) i#(*(x,y)) -> i#(y) i#(*(x,y)) -> *#(i(y),i(x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() TDG Processor: DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) i#(*(x,y)) -> i#(x) i#(*(x,y)) -> i#(y) i#(*(x,y)) -> *#(i(y),i(x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() graph: i#(*(x,y)) -> i#(y) -> i#(*(x,y)) -> *#(i(y),i(x)) i#(*(x,y)) -> i#(y) -> i#(*(x,y)) -> i#(y) i#(*(x,y)) -> i#(y) -> i#(*(x,y)) -> i#(x) i#(*(x,y)) -> i#(x) -> i#(*(x,y)) -> *#(i(y),i(x)) i#(*(x,y)) -> i#(x) -> i#(*(x,y)) -> i#(y) i#(*(x,y)) -> i#(x) -> i#(*(x,y)) -> i#(x) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(x,*(y,z)) -> *#(*(x,y),z) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(x,*(y,z)) -> *#(x,y) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(x,*(y,z)) -> *#(x,y) -> *#(x,*(y,z)) -> *#(x,y) SCC Processor: #sccs: 2 #rules: 8 #arcs: 55/100 DPs: i#(*(x,y)) -> i#(y) i#(*(x,y)) -> i#(x) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Subterm Criterion Processor: simple projection: pi(i#) = 0 problem: DPs: TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Qed DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Open