MAYBE Problem: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) Proof: DP Processor: DPs: nthtail#(n,l) -> length#(l) nthtail#(n,l) -> ge#(n,length(l)) nthtail#(n,l) -> cond#(ge(n,length(l)),n,l) cond#(false(),n,l) -> nthtail#(s(n),l) cond#(false(),n,l) -> tail#(nthtail(s(n),l)) length#(cons(x,l)) -> length#(l) ge#(s(u),s(v)) -> ge#(u,v) TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) TDG Processor: DPs: nthtail#(n,l) -> length#(l) nthtail#(n,l) -> ge#(n,length(l)) nthtail#(n,l) -> cond#(ge(n,length(l)),n,l) cond#(false(),n,l) -> nthtail#(s(n),l) cond#(false(),n,l) -> tail#(nthtail(s(n),l)) length#(cons(x,l)) -> length#(l) ge#(s(u),s(v)) -> ge#(u,v) TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) graph: cond#(false(),n,l) -> nthtail#(s(n),l) -> nthtail#(n,l) -> cond#(ge(n,length(l)),n,l) cond#(false(),n,l) -> nthtail#(s(n),l) -> nthtail#(n,l) -> ge#(n,length(l)) cond#(false(),n,l) -> nthtail#(s(n),l) -> nthtail#(n,l) -> length#(l) ge#(s(u),s(v)) -> ge#(u,v) -> ge#(s(u),s(v)) -> ge#(u,v) length#(cons(x,l)) -> length#(l) -> length#(cons(x,l)) -> length#(l) nthtail#(n,l) -> cond#(ge(n,length(l)),n,l) -> cond#(false(),n,l) -> tail#(nthtail(s(n),l)) nthtail#(n,l) -> cond#(ge(n,length(l)),n,l) -> cond#(false(),n,l) -> nthtail#(s(n),l) nthtail#(n,l) -> ge#(n,length(l)) -> ge#(s(u),s(v)) -> ge#(u,v) nthtail#(n,l) -> length#(l) -> length#(cons(x,l)) -> length#(l) Restore Modifier: DPs: nthtail#(n,l) -> length#(l) nthtail#(n,l) -> ge#(n,length(l)) nthtail#(n,l) -> cond#(ge(n,length(l)),n,l) cond#(false(),n,l) -> nthtail#(s(n),l) cond#(false(),n,l) -> tail#(nthtail(s(n),l)) length#(cons(x,l)) -> length#(l) ge#(s(u),s(v)) -> ge#(u,v) TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) SCC Processor: #sccs: 3 #rules: 4 #arcs: 9/49 DPs: cond#(false(),n,l) -> nthtail#(s(n),l) nthtail#(n,l) -> cond#(ge(n,length(l)),n,l) TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) Open DPs: ge#(s(u),s(v)) -> ge#(u,v) TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) Matrix Interpretation Processor: dimension: 1 interpretation: [ge#](x0, x1) = x1 + 1, [0] = 0, [cons](x0, x1) = x1 + 1, [nil] = 0, [tail](x0) = x0, [s](x0) = x0 + 1, [false] = 0, [true] = 0, [cond](x0, x1, x2) = x2, [ge](x0, x1) = 0, [length](x0) = x0, [nthtail](x0, x1) = x1 orientation: ge#(s(u),s(v)) = v + 2 >= v + 1 = ge#(u,v) nthtail(n,l) = l >= l = cond(ge(n,length(l)),n,l) cond(true(),n,l) = l >= l = l cond(false(),n,l) = l >= l = tail(nthtail(s(n),l)) tail(nil()) = 0 >= 0 = nil() tail(cons(x,l)) = l + 1 >= l = l length(nil()) = 0 >= 0 = 0() length(cons(x,l)) = l + 1 >= l + 1 = s(length(l)) ge(u,0()) = 0 >= 0 = true() ge(0(),s(v)) = 0 >= 0 = false() ge(s(u),s(v)) = 0 >= 0 = ge(u,v) problem: DPs: TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) Qed DPs: length#(cons(x,l)) -> length#(l) TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) Matrix Interpretation Processor: dimension: 1 interpretation: [length#](x0) = x0, [0] = 0, [cons](x0, x1) = x1 + 1, [nil] = 0, [tail](x0) = x0, [s](x0) = 0, [false] = 0, [true] = 0, [cond](x0, x1, x2) = x2, [ge](x0, x1) = 0, [length](x0) = 0, [nthtail](x0, x1) = x1 orientation: length#(cons(x,l)) = l + 1 >= l = length#(l) nthtail(n,l) = l >= l = cond(ge(n,length(l)),n,l) cond(true(),n,l) = l >= l = l cond(false(),n,l) = l >= l = tail(nthtail(s(n),l)) tail(nil()) = 0 >= 0 = nil() tail(cons(x,l)) = l + 1 >= l = l length(nil()) = 0 >= 0 = 0() length(cons(x,l)) = 0 >= 0 = s(length(l)) ge(u,0()) = 0 >= 0 = true() ge(0(),s(v)) = 0 >= 0 = false() ge(s(u),s(v)) = 0 >= 0 = ge(u,v) problem: DPs: TRS: nthtail(n,l) -> cond(ge(n,length(l)),n,l) cond(true(),n,l) -> l cond(false(),n,l) -> tail(nthtail(s(n),l)) tail(nil()) -> nil() tail(cons(x,l)) -> l length(nil()) -> 0() length(cons(x,l)) -> s(length(l)) ge(u,0()) -> true() ge(0(),s(v)) -> false() ge(s(u),s(v)) -> ge(u,v) Qed