MAYBE Problem: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Proof: DP Processor: DPs: eq#(s(n),s(m)) -> eq#(n,m) le#(s(n),s(m)) -> le#(n,m) min#(cons(n,cons(m,x))) -> le#(n,m) min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) replace#(n,m,cons(k,x)) -> eq#(n,k) replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) sort#(x) -> sortIter#(x,nil()) sortIter#(x,y) -> min#(x) sortIter#(x,y) -> empty#(x) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) if#(false(),x,y,z) -> tail#(x) if#(false(),x,y,z) -> head#(x) if#(false(),x,y,z) -> min#(x) if#(false(),x,y,z) -> replace#(min(x),head(x),tail(x)) if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Usable Rule Processor: DPs: eq#(s(n),s(m)) -> eq#(n,m) le#(s(n),s(m)) -> le#(n,m) min#(cons(n,cons(m,x))) -> le#(n,m) min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) replace#(n,m,cons(k,x)) -> eq#(n,k) replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) sort#(x) -> sortIter#(x,nil()) sortIter#(x,y) -> min#(x) sortIter#(x,y) -> empty#(x) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) if#(false(),x,y,z) -> tail#(x) if#(false(),x,y,z) -> head#(x) if#(false(),x,y,z) -> min#(x) if#(false(),x,y,z) -> replace#(min(x),head(x),tail(x)) if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) TRS: f31(x,y) -> x f31(x,y) -> y le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() tail(nil()) -> nil() tail(cons(n,x)) -> x head(cons(n,x)) -> n replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) ADG Processor: DPs: eq#(s(n),s(m)) -> eq#(n,m) le#(s(n),s(m)) -> le#(n,m) min#(cons(n,cons(m,x))) -> le#(n,m) min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) replace#(n,m,cons(k,x)) -> eq#(n,k) replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) sort#(x) -> sortIter#(x,nil()) sortIter#(x,y) -> min#(x) sortIter#(x,y) -> empty#(x) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) if#(false(),x,y,z) -> tail#(x) if#(false(),x,y,z) -> head#(x) if#(false(),x,y,z) -> min#(x) if#(false(),x,y,z) -> replace#(min(x),head(x),tail(x)) if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) TRS: f31(x,y) -> x f31(x,y) -> y le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() tail(nil()) -> nil() tail(cons(n,x)) -> x head(cons(n,x)) -> n replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) graph: if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) -> sortIter#(x,y) -> min#(x) if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) -> sortIter#(x,y) -> empty#(x) if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) -> sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) if#(false(),x,y,z) -> replace#(min(x),head(x),tail(x)) -> replace#(n,m,cons(k,x)) -> eq#(n,k) if#(false(),x,y,z) -> replace#(min(x),head(x),tail(x)) -> replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) if#(false(),x,y,z) -> min#(x) -> min#(cons(n,cons(m,x))) -> le#(n,m) if#(false(),x,y,z) -> min#(x) -> min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) -> if#(false(),x,y,z) -> tail#(x) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) -> if#(false(),x,y,z) -> head#(x) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) -> if#(false(),x,y,z) -> min#(x) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) -> if#(false(),x,y,z) -> replace#(min(x),head(x),tail(x)) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) -> if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) sortIter#(x,y) -> min#(x) -> min#(cons(n,cons(m,x))) -> le#(n,m) sortIter#(x,y) -> min#(x) -> min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) sort#(x) -> sortIter#(x,nil()) -> sortIter#(x,y) -> min#(x) sort#(x) -> sortIter#(x,nil()) -> sortIter#(x,y) -> empty#(x) sort#(x) -> sortIter#(x,nil()) -> sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) -> replace#(n,m,cons(k,x)) -> eq#(n,k) if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) -> replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) -> if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) replace#(n,m,cons(k,x)) -> eq#(n,k) -> eq#(s(n),s(m)) -> eq#(n,m) if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) -> min#(cons(n,cons(m,x))) -> le#(n,m) if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) -> min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) -> min#(cons(n,cons(m,x))) -> le#(n,m) if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) -> min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) -> if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) -> if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) min#(cons(n,cons(m,x))) -> le#(n,m) -> le#(s(n),s(m)) -> le#(n,m) le#(s(n),s(m)) -> le#(n,m) -> le#(s(n),s(m)) -> le#(n,m) eq#(s(n),s(m)) -> eq#(n,m) -> eq#(s(n),s(m)) -> eq#(n,m) Restore Modifier: DPs: eq#(s(n),s(m)) -> eq#(n,m) le#(s(n),s(m)) -> le#(n,m) min#(cons(n,cons(m,x))) -> le#(n,m) min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) replace#(n,m,cons(k,x)) -> eq#(n,k) replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) sort#(x) -> sortIter#(x,nil()) sortIter#(x,y) -> min#(x) sortIter#(x,y) -> empty#(x) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) if#(false(),x,y,z) -> tail#(x) if#(false(),x,y,z) -> head#(x) if#(false(),x,y,z) -> min#(x) if#(false(),x,y,z) -> replace#(min(x),head(x),tail(x)) if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) SCC Processor: #sccs: 5 #rules: 9 #arcs: 30/324 DPs: if#(false(),x,y,z) -> sortIter#(replace(min(x),head(x),tail(x)),z) sortIter#(x,y) -> if#(empty(x),x,y,append(y,cons(min(x),nil()))) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Open DPs: min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Matrix Interpretation Processor: dimension: 1 interpretation: [if_min#](x0, x1) = x1, [min#](x0) = x0, [if](x0, x1, x2, x3) = x2 + x3, [append](x0, x1) = 0, [sortIter](x0, x1) = x1, [sort](x0) = 1, [tail](x0) = x0, [head](x0) = x0, [empty](x0) = 0, [if_replace](x0, x1, x2, x3) = x2 + x3, [replace](x0, x1, x2) = x1 + x2, [if_min](x0, x1) = x1, [min](x0) = x0, [cons](x0, x1) = x0 + x1 + 1, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = x0 + 1, [true] = 0, [eq](x0, x1) = x1 + 1, [0] = 0 orientation: min#(cons(n,cons(m,x))) = m + n + x + 2 >= m + n + x + 2 = if_min#(le(n,m),cons(n,cons(m,x))) if_min#(false(),cons(n,cons(m,x))) = m + n + x + 2 >= m + x + 1 = min#(cons(m,x)) if_min#(true(),cons(n,cons(m,x))) = m + n + x + 2 >= n + x + 1 = min#(cons(n,x)) eq(0(),0()) = 1 >= 0 = true() eq(0(),s(m)) = m + 2 >= 0 = false() eq(s(n),0()) = 1 >= 0 = false() eq(s(n),s(m)) = m + 2 >= m + 1 = eq(n,m) le(0(),m) = 0 >= 0 = true() le(s(n),0()) = 0 >= 0 = false() le(s(n),s(m)) = 0 >= 0 = le(n,m) min(cons(x,nil())) = x + 1 >= x = x min(cons(n,cons(m,x))) = m + n + x + 2 >= m + n + x + 2 = if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) = m + n + x + 2 >= n + x + 1 = min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) = m + n + x + 2 >= m + x + 1 = min(cons(m,x)) replace(n,m,nil()) = m >= 0 = nil() replace(n,m,cons(k,x)) = k + m + x + 1 >= k + m + x + 1 = if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) = k + m + x + 1 >= m + x + 1 = cons(m,x) if_replace(false(),n,m,cons(k,x)) = k + m + x + 1 >= k + m + x + 1 = cons(k,replace(n,m,x)) empty(nil()) = 0 >= 0 = true() empty(cons(n,x)) = 0 >= 0 = false() head(cons(n,x)) = n + x + 1 >= n = n tail(nil()) = 0 >= 0 = nil() tail(cons(n,x)) = n + x + 1 >= x = x sort(x) = 1 >= 0 = sortIter(x,nil()) sortIter(x,y) = y >= y = if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) = y + z >= y = y if(false(),x,y,z) = y + z >= z = sortIter(replace(min(x),head(x),tail(x)),z) problem: DPs: min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Matrix Interpretation Processor: dimension: 1 interpretation: [if_min#](x0, x1) = 0, [min#](x0) = 1, [if](x0, x1, x2, x3) = x2 + x3, [append](x0, x1) = 0, [sortIter](x0, x1) = x1, [sort](x0) = 0, [tail](x0) = x0, [head](x0) = x0, [empty](x0) = 0, [if_replace](x0, x1, x2, x3) = x2 + x3, [replace](x0, x1, x2) = x1 + x2, [if_min](x0, x1) = x1, [min](x0) = x0, [cons](x0, x1) = x0 + x1, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: min#(cons(n,cons(m,x))) = 1 >= 0 = if_min#(le(n,m),cons(n,cons(m,x))) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(m)) = 0 >= 0 = false() eq(s(n),0()) = 0 >= 0 = false() eq(s(n),s(m)) = 0 >= 0 = eq(n,m) le(0(),m) = 0 >= 0 = true() le(s(n),0()) = 0 >= 0 = false() le(s(n),s(m)) = 0 >= 0 = le(n,m) min(cons(x,nil())) = x >= x = x min(cons(n,cons(m,x))) = m + n + x >= m + n + x = if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) = m + n + x >= n + x = min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) = m + n + x >= m + x = min(cons(m,x)) replace(n,m,nil()) = m >= 0 = nil() replace(n,m,cons(k,x)) = k + m + x >= k + m + x = if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) = k + m + x >= m + x = cons(m,x) if_replace(false(),n,m,cons(k,x)) = k + m + x >= k + m + x = cons(k,replace(n,m,x)) empty(nil()) = 0 >= 0 = true() empty(cons(n,x)) = 0 >= 0 = false() head(cons(n,x)) = n + x >= n = n tail(nil()) = 0 >= 0 = nil() tail(cons(n,x)) = n + x >= x = x sort(x) = 0 >= 0 = sortIter(x,nil()) sortIter(x,y) = y >= y = if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) = y + z >= y = y if(false(),x,y,z) = y + z >= z = sortIter(replace(min(x),head(x),tail(x)),z) problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Qed DPs: le#(s(n),s(m)) -> le#(n,m) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Matrix Interpretation Processor: dimension: 1 interpretation: [le#](x0, x1) = x0 + 1, [if](x0, x1, x2, x3) = x2 + x3, [append](x0, x1) = 0, [sortIter](x0, x1) = x1, [sort](x0) = 0, [tail](x0) = x0, [head](x0) = x0, [empty](x0) = 0, [if_replace](x0, x1, x2, x3) = x2 + x3, [replace](x0, x1, x2) = x1 + x2, [if_min](x0, x1) = x1, [min](x0) = x0, [cons](x0, x1) = x0 + x1, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = x0 + 1, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: le#(s(n),s(m)) = n + 2 >= n + 1 = le#(n,m) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(m)) = 0 >= 0 = false() eq(s(n),0()) = 0 >= 0 = false() eq(s(n),s(m)) = 0 >= 0 = eq(n,m) le(0(),m) = 0 >= 0 = true() le(s(n),0()) = 0 >= 0 = false() le(s(n),s(m)) = 0 >= 0 = le(n,m) min(cons(x,nil())) = x >= x = x min(cons(n,cons(m,x))) = m + n + x >= m + n + x = if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) = m + n + x >= n + x = min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) = m + n + x >= m + x = min(cons(m,x)) replace(n,m,nil()) = m >= 0 = nil() replace(n,m,cons(k,x)) = k + m + x >= k + m + x = if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) = k + m + x >= m + x = cons(m,x) if_replace(false(),n,m,cons(k,x)) = k + m + x >= k + m + x = cons(k,replace(n,m,x)) empty(nil()) = 0 >= 0 = true() empty(cons(n,x)) = 0 >= 0 = false() head(cons(n,x)) = n + x >= n = n tail(nil()) = 0 >= 0 = nil() tail(cons(n,x)) = n + x >= x = x sort(x) = 0 >= 0 = sortIter(x,nil()) sortIter(x,y) = y >= y = if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) = y + z >= y = y if(false(),x,y,z) = y + z >= z = sortIter(replace(min(x),head(x),tail(x)),z) problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Qed DPs: replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Matrix Interpretation Processor: dimension: 1 interpretation: [if_replace#](x0, x1, x2, x3) = x3, [replace#](x0, x1, x2) = x2, [if](x0, x1, x2, x3) = x2 + x3, [append](x0, x1) = 0, [sortIter](x0, x1) = x1, [sort](x0) = 0, [tail](x0) = x0, [head](x0) = x0, [empty](x0) = 0, [if_replace](x0, x1, x2, x3) = x2 + x3, [replace](x0, x1, x2) = x1 + x2, [if_min](x0, x1) = x1 + 1, [min](x0) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 1, [0] = 0 orientation: replace#(n,m,cons(k,x)) = k + x + 1 >= k + x + 1 = if_replace#(eq(n,k),n,m,cons(k,x)) if_replace#(false(),n,m,cons(k,x)) = k + x + 1 >= x = replace#(n,m,x) eq(0(),0()) = 1 >= 0 = true() eq(0(),s(m)) = 1 >= 0 = false() eq(s(n),0()) = 1 >= 0 = false() eq(s(n),s(m)) = 1 >= 1 = eq(n,m) le(0(),m) = 0 >= 0 = true() le(s(n),0()) = 0 >= 0 = false() le(s(n),s(m)) = 0 >= 0 = le(n,m) min(cons(x,nil())) = x + 2 >= x = x min(cons(n,cons(m,x))) = m + n + x + 3 >= m + n + x + 3 = if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) = m + n + x + 3 >= n + x + 2 = min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) = m + n + x + 3 >= m + x + 2 = min(cons(m,x)) replace(n,m,nil()) = m >= 0 = nil() replace(n,m,cons(k,x)) = k + m + x + 1 >= k + m + x + 1 = if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) = k + m + x + 1 >= m + x + 1 = cons(m,x) if_replace(false(),n,m,cons(k,x)) = k + m + x + 1 >= k + m + x + 1 = cons(k,replace(n,m,x)) empty(nil()) = 0 >= 0 = true() empty(cons(n,x)) = 0 >= 0 = false() head(cons(n,x)) = n + x + 1 >= n = n tail(nil()) = 0 >= 0 = nil() tail(cons(n,x)) = n + x + 1 >= x = x sort(x) = 0 >= 0 = sortIter(x,nil()) sortIter(x,y) = y >= y = if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) = y + z >= y = y if(false(),x,y,z) = y + z >= z = sortIter(replace(min(x),head(x),tail(x)),z) problem: DPs: replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Matrix Interpretation Processor: dimension: 1 interpretation: [if_replace#](x0, x1, x2, x3) = 0, [replace#](x0, x1, x2) = 1, [if](x0, x1, x2, x3) = x2 + x3, [append](x0, x1) = 0, [sortIter](x0, x1) = x1, [sort](x0) = 0, [tail](x0) = x0, [head](x0) = x0, [empty](x0) = 0, [if_replace](x0, x1, x2, x3) = x2 + x3, [replace](x0, x1, x2) = x1 + x2, [if_min](x0, x1) = x1, [min](x0) = x0, [cons](x0, x1) = x0 + x1, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: replace#(n,m,cons(k,x)) = 1 >= 0 = if_replace#(eq(n,k),n,m,cons(k,x)) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(m)) = 0 >= 0 = false() eq(s(n),0()) = 0 >= 0 = false() eq(s(n),s(m)) = 0 >= 0 = eq(n,m) le(0(),m) = 0 >= 0 = true() le(s(n),0()) = 0 >= 0 = false() le(s(n),s(m)) = 0 >= 0 = le(n,m) min(cons(x,nil())) = x >= x = x min(cons(n,cons(m,x))) = m + n + x >= m + n + x = if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) = m + n + x >= n + x = min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) = m + n + x >= m + x = min(cons(m,x)) replace(n,m,nil()) = m >= 0 = nil() replace(n,m,cons(k,x)) = k + m + x >= k + m + x = if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) = k + m + x >= m + x = cons(m,x) if_replace(false(),n,m,cons(k,x)) = k + m + x >= k + m + x = cons(k,replace(n,m,x)) empty(nil()) = 0 >= 0 = true() empty(cons(n,x)) = 0 >= 0 = false() head(cons(n,x)) = n + x >= n = n tail(nil()) = 0 >= 0 = nil() tail(cons(n,x)) = n + x >= x = x sort(x) = 0 >= 0 = sortIter(x,nil()) sortIter(x,y) = y >= y = if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) = y + z >= y = y if(false(),x,y,z) = y + z >= z = sortIter(replace(min(x),head(x),tail(x)),z) problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Qed DPs: eq#(s(n),s(m)) -> eq#(n,m) TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Matrix Interpretation Processor: dimension: 1 interpretation: [eq#](x0, x1) = x0 + 1, [if](x0, x1, x2, x3) = x2 + x3, [append](x0, x1) = 0, [sortIter](x0, x1) = x1, [sort](x0) = 0, [tail](x0) = x0, [head](x0) = x0, [empty](x0) = 0, [if_replace](x0, x1, x2, x3) = x2 + x3, [replace](x0, x1, x2) = x1 + x2, [if_min](x0, x1) = x1, [min](x0) = x0, [cons](x0, x1) = x0 + x1, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = x0 + 1, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: eq#(s(n),s(m)) = n + 2 >= n + 1 = eq#(n,m) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(m)) = 0 >= 0 = false() eq(s(n),0()) = 0 >= 0 = false() eq(s(n),s(m)) = 0 >= 0 = eq(n,m) le(0(),m) = 0 >= 0 = true() le(s(n),0()) = 0 >= 0 = false() le(s(n),s(m)) = 0 >= 0 = le(n,m) min(cons(x,nil())) = x >= x = x min(cons(n,cons(m,x))) = m + n + x >= m + n + x = if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) = m + n + x >= n + x = min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) = m + n + x >= m + x = min(cons(m,x)) replace(n,m,nil()) = m >= 0 = nil() replace(n,m,cons(k,x)) = k + m + x >= k + m + x = if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) = k + m + x >= m + x = cons(m,x) if_replace(false(),n,m,cons(k,x)) = k + m + x >= k + m + x = cons(k,replace(n,m,x)) empty(nil()) = 0 >= 0 = true() empty(cons(n,x)) = 0 >= 0 = false() head(cons(n,x)) = n + x >= n = n tail(nil()) = 0 >= 0 = nil() tail(cons(n,x)) = n + x >= x = x sort(x) = 0 >= 0 = sortIter(x,nil()) sortIter(x,y) = y >= y = if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) = y + z >= y = y if(false(),x,y,z) = y + z >= z = sortIter(replace(min(x),head(x),tail(x)),z) problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(m)) -> false() eq(s(n),0()) -> false() eq(s(n),s(m)) -> eq(n,m) le(0(),m) -> true() le(s(n),0()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(x,nil())) -> x min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) empty(nil()) -> true() empty(cons(n,x)) -> false() head(cons(n,x)) -> n tail(nil()) -> nil() tail(cons(n,x)) -> x sort(x) -> sortIter(x,nil()) sortIter(x,y) -> if(empty(x),x,y,append(y,cons(min(x),nil()))) if(true(),x,y,z) -> y if(false(),x,y,z) -> sortIter(replace(min(x),head(x),tail(x)),z) Qed