0.003/0.003 NO 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S v_NonEmpty:S:S N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U11 1) 0.003/0.003 (U111 1) 0.003/0.003 (U112 1) 0.003/0.003 (U121 1) 0.003/0.003 (U122 1) 0.003/0.003 (U131 1) 0.003/0.003 (U132 1) 0.003/0.003 (U133 1) 0.003/0.003 (U141 1) 0.003/0.003 (U142 1) 0.003/0.003 (U143 1) 0.003/0.003 (U151 1) 0.003/0.003 (U152 1) 0.003/0.003 (U153 1) 0.003/0.003 (U161 1) 0.003/0.003 (U171 1) 0.003/0.003 (U181 1) 0.003/0.003 (U191 1) 0.003/0.003 (U201 1) 0.003/0.003 (U202 1) 0.003/0.003 (U21 1) 0.003/0.003 (U211 1) 0.003/0.003 (U221 1) 0.003/0.003 (U31 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U53 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (U81 1) 0.003/0.003 (U82 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (afterNth) 0.003/0.003 (and 1) 0.003/0.003 (fst 1) 0.003/0.003 (head 1) 0.003/0.003 (isLNat 1) 0.003/0.003 (isLNatKind 1) 0.003/0.003 (isNatural 1) 0.003/0.003 (isNaturalKind 1) 0.003/0.003 (isPLNat 1) 0.003/0.003 (isPLNatKind 1) 0.003/0.003 (natsFrom) 0.003/0.003 (sel) 0.003/0.003 (snd 1) 0.003/0.003 (splitAt 1 2) 0.003/0.003 (tail 1) 0.003/0.003 (take) 0.003/0.003 (cons) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (nil) 0.003/0.003 (num0) 0.003/0.003 (pair) 0.003/0.003 (s) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U102(tt,V2:S:S) -> U103(isLNat(V2:S:S)) 0.003/0.003 U103(tt) -> tt 0.003/0.003 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U111(tt,V1:S:S) -> U112(isLNat(V1:S:S)) 0.003/0.003 U112(tt) -> tt 0.003/0.003 U121(tt,V1:S:S) -> U122(isNatural(V1:S:S)) 0.003/0.003 U122(tt) -> tt 0.003/0.003 U131(tt,V1:S:S,V2:S:S) -> U132(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U132(tt,V2:S:S) -> U133(isLNat(V2:S:S)) 0.003/0.003 U133(tt) -> tt 0.003/0.003 U141(tt,V1:S:S,V2:S:S) -> U142(isLNat(V1:S:S),V2:S:S) 0.003/0.003 U142(tt,V2:S:S) -> U143(isLNat(V2:S:S)) 0.003/0.003 U143(tt) -> tt 0.003/0.003 U151(tt,V1:S:S,V2:S:S) -> U152(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U152(tt,V2:S:S) -> U153(isLNat(V2:S:S)) 0.003/0.003 U153(tt) -> tt 0.003/0.003 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.003/0.003 U171(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.003/0.003 U181(tt,Y:S:S) -> Y:S:S 0.003/0.003 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.003/0.003 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(splitAt(N:S:S,XS:S:S),X:S:S) 0.003/0.003 U202(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.003/0.003 U21(tt,X:S:S) -> X:S:S 0.003/0.003 U211(tt,XS:S:S) -> XS:S:S 0.003/0.003 U221(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U31(tt,N:S:S) -> N:S:S 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isLNat(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isLNat(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V1:S:S) -> U62(isPLNat(V1:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V1:S:S) -> U72(isNatural(V1:S:S)) 0.003/0.003 U72(tt) -> tt 0.003/0.003 U81(tt,V1:S:S) -> U82(isPLNat(V1:S:S)) 0.003/0.003 U82(tt) -> tt 0.003/0.003 U91(tt,V1:S:S) -> U92(isLNat(V1:S:S)) 0.003/0.003 U92(tt) -> tt 0.003/0.003 afterNth(N:S:S,XS:S:S) -> U11(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 and(tt,X:S:S) -> X:S:S 0.003/0.003 fst(pair(X:S:S,Y:S:S)) -> U21(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),X:S:S) 0.003/0.003 head(cons(N:S:S,XS:S:S)) -> U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S) 0.003/0.003 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(take(V1:S:S,V2:S:S)) -> U101(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(cons(V1:S:S,V2:S:S)) -> U51(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(nil) -> tt 0.003/0.003 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(fst(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(natsFrom(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isLNatKind(snd(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(tail(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isLNatKind(take(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(cons(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(nil) -> tt 0.003/0.003 isNatural(head(V1:S:S)) -> U111(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatural(sel(V1:S:S,V2:S:S)) -> U131(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNatural(num0) -> tt 0.003/0.003 isNatural(s(V1:S:S)) -> U121(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isNaturalKind(head(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isNaturalKind(sel(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isNaturalKind(num0) -> tt 0.003/0.003 isNaturalKind(s(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isPLNatKind(pair(V1:S:S,V2:S:S)) -> and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 natsFrom(N:S:S) -> U161(and(isNatural(N:S:S),isNaturalKind(N:S:S)),N:S:S) 0.003/0.003 sel(N:S:S,XS:S:S) -> U171(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 snd(pair(X:S:S,Y:S:S)) -> U181(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),Y:S:S) 0.003/0.003 splitAt(num0,XS:S:S) -> U191(and(isLNat(XS:S:S),isLNatKind(XS:S:S)),XS:S:S) 0.003/0.003 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(and(isNatural(X:S:S),isNaturalKind(X:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S)))),N:S:S,X:S:S,XS:S:S) 0.003/0.003 tail(cons(N:S:S,XS:S:S)) -> U211(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),XS:S:S) 0.003/0.003 take(N:S:S,XS:S:S) -> U221(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 CleanTRS Processor: 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S v_NonEmpty:S:S N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U11 1) 0.003/0.003 (U111 1) 0.003/0.003 (U112 1) 0.003/0.003 (U121 1) 0.003/0.003 (U122 1) 0.003/0.003 (U131 1) 0.003/0.003 (U132 1) 0.003/0.003 (U133 1) 0.003/0.003 (U141 1) 0.003/0.003 (U142 1) 0.003/0.003 (U143 1) 0.003/0.003 (U151 1) 0.003/0.003 (U152 1) 0.003/0.003 (U153 1) 0.003/0.003 (U161 1) 0.003/0.003 (U171 1) 0.003/0.003 (U181 1) 0.003/0.003 (U191 1) 0.003/0.003 (U201 1) 0.003/0.003 (U202 1) 0.003/0.003 (U21 1) 0.003/0.003 (U211 1) 0.003/0.003 (U221 1) 0.003/0.003 (U31 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U53 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (U81 1) 0.003/0.003 (U82 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (afterNth) 0.003/0.003 (and 1) 0.003/0.003 (fst 1) 0.003/0.003 (head 1) 0.003/0.003 (isLNat 1) 0.003/0.003 (isLNatKind 1) 0.003/0.003 (isNatural 1) 0.003/0.003 (isNaturalKind 1) 0.003/0.003 (isPLNat 1) 0.003/0.003 (isPLNatKind 1) 0.003/0.003 (natsFrom) 0.003/0.003 (sel) 0.003/0.003 (snd 1) 0.003/0.003 (splitAt 1 2) 0.003/0.003 (tail 1) 0.003/0.003 (take) 0.003/0.003 (cons) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (nil) 0.003/0.003 (num0) 0.003/0.003 (pair) 0.003/0.003 (s) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U102(tt,V2:S:S) -> U103(isLNat(V2:S:S)) 0.003/0.003 U103(tt) -> tt 0.003/0.003 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U111(tt,V1:S:S) -> U112(isLNat(V1:S:S)) 0.003/0.003 U112(tt) -> tt 0.003/0.003 U121(tt,V1:S:S) -> U122(isNatural(V1:S:S)) 0.003/0.003 U122(tt) -> tt 0.003/0.003 U131(tt,V1:S:S,V2:S:S) -> U132(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U132(tt,V2:S:S) -> U133(isLNat(V2:S:S)) 0.003/0.003 U133(tt) -> tt 0.003/0.003 U141(tt,V1:S:S,V2:S:S) -> U142(isLNat(V1:S:S),V2:S:S) 0.003/0.003 U142(tt,V2:S:S) -> U143(isLNat(V2:S:S)) 0.003/0.003 U143(tt) -> tt 0.003/0.003 U151(tt,V1:S:S,V2:S:S) -> U152(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U152(tt,V2:S:S) -> U153(isLNat(V2:S:S)) 0.003/0.003 U153(tt) -> tt 0.003/0.003 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.003/0.003 U171(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.003/0.003 U181(tt,Y:S:S) -> Y:S:S 0.003/0.003 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.003/0.003 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(splitAt(N:S:S,XS:S:S),X:S:S) 0.003/0.003 U202(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.003/0.003 U21(tt,X:S:S) -> X:S:S 0.003/0.003 U211(tt,XS:S:S) -> XS:S:S 0.003/0.003 U221(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U31(tt,N:S:S) -> N:S:S 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isLNat(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isLNat(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V1:S:S) -> U62(isPLNat(V1:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V1:S:S) -> U72(isNatural(V1:S:S)) 0.003/0.003 U72(tt) -> tt 0.003/0.003 U81(tt,V1:S:S) -> U82(isPLNat(V1:S:S)) 0.003/0.003 U82(tt) -> tt 0.003/0.003 U91(tt,V1:S:S) -> U92(isLNat(V1:S:S)) 0.003/0.003 U92(tt) -> tt 0.003/0.003 afterNth(N:S:S,XS:S:S) -> U11(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 and(tt,X:S:S) -> X:S:S 0.003/0.003 fst(pair(X:S:S,Y:S:S)) -> U21(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),X:S:S) 0.003/0.003 head(cons(N:S:S,XS:S:S)) -> U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S) 0.003/0.003 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(take(V1:S:S,V2:S:S)) -> U101(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(cons(V1:S:S,V2:S:S)) -> U51(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(nil) -> tt 0.003/0.003 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(fst(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(natsFrom(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isLNatKind(snd(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(tail(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isLNatKind(take(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(cons(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(nil) -> tt 0.003/0.003 isNatural(head(V1:S:S)) -> U111(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatural(sel(V1:S:S,V2:S:S)) -> U131(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNatural(num0) -> tt 0.003/0.003 isNatural(s(V1:S:S)) -> U121(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isNaturalKind(head(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isNaturalKind(sel(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isNaturalKind(num0) -> tt 0.003/0.003 isNaturalKind(s(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isPLNatKind(pair(V1:S:S,V2:S:S)) -> and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 natsFrom(N:S:S) -> U161(and(isNatural(N:S:S),isNaturalKind(N:S:S)),N:S:S) 0.003/0.003 sel(N:S:S,XS:S:S) -> U171(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 snd(pair(X:S:S,Y:S:S)) -> U181(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),Y:S:S) 0.003/0.003 splitAt(num0,XS:S:S) -> U191(and(isLNat(XS:S:S),isLNatKind(XS:S:S)),XS:S:S) 0.003/0.003 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(and(isNatural(X:S:S),isNaturalKind(X:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S)))),N:S:S,X:S:S,XS:S:S) 0.003/0.003 tail(cons(N:S:S,XS:S:S)) -> U211(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),XS:S:S) 0.003/0.003 take(N:S:S,XS:S:S) -> U221(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 Modular Confluence Combinations Decomposition Processor: 0.003/0.003 It is a CTRS -> No modular confluence 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 CS-TRS Processor: 0.003/0.003 R is a CS-TRS 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S v_NonEmpty:S:S N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (U101 1) 0.003/0.003 (U102 1) 0.003/0.003 (U103 1) 0.003/0.003 (U11 1) 0.003/0.003 (U111 1) 0.003/0.003 (U112 1) 0.003/0.003 (U121 1) 0.003/0.003 (U122 1) 0.003/0.003 (U131 1) 0.003/0.003 (U132 1) 0.003/0.003 (U133 1) 0.003/0.003 (U141 1) 0.003/0.003 (U142 1) 0.003/0.003 (U143 1) 0.003/0.003 (U151 1) 0.003/0.003 (U152 1) 0.003/0.003 (U153 1) 0.003/0.003 (U161 1) 0.003/0.003 (U171 1) 0.003/0.003 (U181 1) 0.003/0.003 (U191 1) 0.003/0.003 (U201 1) 0.003/0.003 (U202 1) 0.003/0.003 (U21 1) 0.003/0.003 (U211 1) 0.003/0.003 (U221 1) 0.003/0.003 (U31 1) 0.003/0.003 (U41 1) 0.003/0.003 (U42 1) 0.003/0.003 (U43 1) 0.003/0.003 (U51 1) 0.003/0.003 (U52 1) 0.003/0.003 (U53 1) 0.003/0.003 (U61 1) 0.003/0.003 (U62 1) 0.003/0.003 (U71 1) 0.003/0.003 (U72 1) 0.003/0.003 (U81 1) 0.003/0.003 (U82 1) 0.003/0.003 (U91 1) 0.003/0.003 (U92 1) 0.003/0.003 (afterNth) 0.003/0.003 (and 1) 0.003/0.003 (fst 1) 0.003/0.003 (head 1) 0.003/0.003 (isLNat 1) 0.003/0.003 (isLNatKind 1) 0.003/0.003 (isNatural 1) 0.003/0.003 (isNaturalKind 1) 0.003/0.003 (isPLNat 1) 0.003/0.003 (isPLNatKind 1) 0.003/0.003 (natsFrom) 0.003/0.003 (sel) 0.003/0.003 (snd 1) 0.003/0.003 (splitAt 1 2) 0.003/0.003 (tail 1) 0.003/0.003 (take) 0.003/0.003 (cons) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (nil) 0.003/0.003 (num0) 0.003/0.003 (pair) 0.003/0.003 (s) 0.003/0.003 (tt) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U102(tt,V2:S:S) -> U103(isLNat(V2:S:S)) 0.003/0.003 U103(tt) -> tt 0.003/0.003 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U111(tt,V1:S:S) -> U112(isLNat(V1:S:S)) 0.003/0.003 U112(tt) -> tt 0.003/0.003 U121(tt,V1:S:S) -> U122(isNatural(V1:S:S)) 0.003/0.003 U122(tt) -> tt 0.003/0.003 U131(tt,V1:S:S,V2:S:S) -> U132(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U132(tt,V2:S:S) -> U133(isLNat(V2:S:S)) 0.003/0.003 U133(tt) -> tt 0.003/0.003 U141(tt,V1:S:S,V2:S:S) -> U142(isLNat(V1:S:S),V2:S:S) 0.003/0.003 U142(tt,V2:S:S) -> U143(isLNat(V2:S:S)) 0.003/0.003 U143(tt) -> tt 0.003/0.003 U151(tt,V1:S:S,V2:S:S) -> U152(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U152(tt,V2:S:S) -> U153(isLNat(V2:S:S)) 0.003/0.003 U153(tt) -> tt 0.003/0.003 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.003/0.003 U171(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.003/0.003 U181(tt,Y:S:S) -> Y:S:S 0.003/0.003 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.003/0.003 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(splitAt(N:S:S,XS:S:S),X:S:S) 0.003/0.003 U202(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.003/0.003 U21(tt,X:S:S) -> X:S:S 0.003/0.003 U211(tt,XS:S:S) -> XS:S:S 0.003/0.003 U221(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U31(tt,N:S:S) -> N:S:S 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isLNat(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isLNat(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V1:S:S) -> U62(isPLNat(V1:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V1:S:S) -> U72(isNatural(V1:S:S)) 0.003/0.003 U72(tt) -> tt 0.003/0.003 U81(tt,V1:S:S) -> U82(isPLNat(V1:S:S)) 0.003/0.003 U82(tt) -> tt 0.003/0.003 U91(tt,V1:S:S) -> U92(isLNat(V1:S:S)) 0.003/0.003 U92(tt) -> tt 0.003/0.003 afterNth(N:S:S,XS:S:S) -> U11(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 and(tt,X:S:S) -> X:S:S 0.003/0.003 fst(pair(X:S:S,Y:S:S)) -> U21(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),X:S:S) 0.003/0.003 head(cons(N:S:S,XS:S:S)) -> U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S) 0.003/0.003 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(take(V1:S:S,V2:S:S)) -> U101(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(cons(V1:S:S,V2:S:S)) -> U51(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(nil) -> tt 0.003/0.003 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(fst(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(natsFrom(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isLNatKind(snd(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(tail(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isLNatKind(take(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(cons(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(nil) -> tt 0.003/0.003 isNatural(head(V1:S:S)) -> U111(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatural(sel(V1:S:S,V2:S:S)) -> U131(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNatural(num0) -> tt 0.003/0.003 isNatural(s(V1:S:S)) -> U121(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isNaturalKind(head(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isNaturalKind(sel(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isNaturalKind(num0) -> tt 0.003/0.003 isNaturalKind(s(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isPLNatKind(pair(V1:S:S,V2:S:S)) -> and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 natsFrom(N:S:S) -> U161(and(isNatural(N:S:S),isNaturalKind(N:S:S)),N:S:S) 0.003/0.003 sel(N:S:S,XS:S:S) -> U171(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 snd(pair(X:S:S,Y:S:S)) -> U181(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),Y:S:S) 0.003/0.003 splitAt(num0,XS:S:S) -> U191(and(isLNat(XS:S:S),isLNatKind(XS:S:S)),XS:S:S) 0.003/0.003 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(and(isNatural(X:S:S),isNaturalKind(X:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S)))),N:S:S,X:S:S,XS:S:S) 0.003/0.003 tail(cons(N:S:S,XS:S:S)) -> U211(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),XS:S:S) 0.003/0.003 take(N:S:S,XS:S:S) -> U221(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 Huet Levy Processor: 0.003/0.003 -> Rules: 0.003/0.003 U101(tt,V1:S:S,V2:S:S) -> U102(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U102(tt,V2:S:S) -> U103(isLNat(V2:S:S)) 0.003/0.003 U103(tt) -> tt 0.003/0.003 U11(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U111(tt,V1:S:S) -> U112(isLNat(V1:S:S)) 0.003/0.003 U112(tt) -> tt 0.003/0.003 U121(tt,V1:S:S) -> U122(isNatural(V1:S:S)) 0.003/0.003 U122(tt) -> tt 0.003/0.003 U131(tt,V1:S:S,V2:S:S) -> U132(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U132(tt,V2:S:S) -> U133(isLNat(V2:S:S)) 0.003/0.003 U133(tt) -> tt 0.003/0.003 U141(tt,V1:S:S,V2:S:S) -> U142(isLNat(V1:S:S),V2:S:S) 0.003/0.003 U142(tt,V2:S:S) -> U143(isLNat(V2:S:S)) 0.003/0.003 U143(tt) -> tt 0.003/0.003 U151(tt,V1:S:S,V2:S:S) -> U152(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U152(tt,V2:S:S) -> U153(isLNat(V2:S:S)) 0.003/0.003 U153(tt) -> tt 0.003/0.003 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.003/0.003 U171(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.003/0.003 U181(tt,Y:S:S) -> Y:S:S 0.003/0.003 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.003/0.003 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(splitAt(N:S:S,XS:S:S),X:S:S) 0.003/0.003 U202(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.003/0.003 U21(tt,X:S:S) -> X:S:S 0.003/0.003 U211(tt,XS:S:S) -> XS:S:S 0.003/0.003 U221(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.003/0.003 U31(tt,N:S:S) -> N:S:S 0.003/0.003 U41(tt,V1:S:S,V2:S:S) -> U42(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U42(tt,V2:S:S) -> U43(isLNat(V2:S:S)) 0.003/0.003 U43(tt) -> tt 0.003/0.003 U51(tt,V1:S:S,V2:S:S) -> U52(isNatural(V1:S:S),V2:S:S) 0.003/0.003 U52(tt,V2:S:S) -> U53(isLNat(V2:S:S)) 0.003/0.003 U53(tt) -> tt 0.003/0.003 U61(tt,V1:S:S) -> U62(isPLNat(V1:S:S)) 0.003/0.003 U62(tt) -> tt 0.003/0.003 U71(tt,V1:S:S) -> U72(isNatural(V1:S:S)) 0.003/0.003 U72(tt) -> tt 0.003/0.003 U81(tt,V1:S:S) -> U82(isPLNat(V1:S:S)) 0.003/0.003 U82(tt) -> tt 0.003/0.003 U91(tt,V1:S:S) -> U92(isLNat(V1:S:S)) 0.003/0.003 U92(tt) -> tt 0.003/0.003 afterNth(N:S:S,XS:S:S) -> U11(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 and(tt,X:S:S) -> X:S:S 0.003/0.003 fst(pair(X:S:S,Y:S:S)) -> U21(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),X:S:S) 0.003/0.003 head(cons(N:S:S,XS:S:S)) -> U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S) 0.003/0.003 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isLNat(take(V1:S:S,V2:S:S)) -> U101(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(cons(V1:S:S,V2:S:S)) -> U51(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isLNat(nil) -> tt 0.003/0.003 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(fst(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(natsFrom(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isLNatKind(snd(V1:S:S)) -> isPLNatKind(V1:S:S) 0.003/0.003 isLNatKind(tail(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isLNatKind(take(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(cons(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isLNatKind(nil) -> tt 0.003/0.003 isNatural(head(V1:S:S)) -> U111(isLNatKind(V1:S:S),V1:S:S) 0.003/0.003 isNatural(sel(V1:S:S,V2:S:S)) -> U131(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isNatural(num0) -> tt 0.003/0.003 isNatural(s(V1:S:S)) -> U121(isNaturalKind(V1:S:S),V1:S:S) 0.003/0.003 isNaturalKind(head(V1:S:S)) -> isLNatKind(V1:S:S) 0.003/0.003 isNaturalKind(sel(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isNaturalKind(num0) -> tt 0.003/0.003 isNaturalKind(s(V1:S:S)) -> isNaturalKind(V1:S:S) 0.003/0.003 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)),V1:S:S,V2:S:S) 0.003/0.003 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> and(isNaturalKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 isPLNatKind(pair(V1:S:S,V2:S:S)) -> and(isLNatKind(V1:S:S),isLNatKind(V2:S:S)) 0.003/0.003 natsFrom(N:S:S) -> U161(and(isNatural(N:S:S),isNaturalKind(N:S:S)),N:S:S) 0.003/0.003 sel(N:S:S,XS:S:S) -> U171(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 snd(pair(X:S:S,Y:S:S)) -> U181(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),Y:S:S) 0.003/0.003 splitAt(num0,XS:S:S) -> U191(and(isLNat(XS:S:S),isLNatKind(XS:S:S)),XS:S:S) 0.003/0.003 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(and(isNatural(X:S:S),isNaturalKind(X:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S)))),N:S:S,X:S:S,XS:S:S) 0.003/0.003 tail(cons(N:S:S,XS:S:S)) -> U211(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),XS:S:S) 0.003/0.003 take(N:S:S,XS:S:S) -> U221(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S) 0.003/0.003 -> Vars: 0.003/0.003 V1:S, V2:S, V2:S, N:S, XS:S, V1:S, V1:S, V1:S, V2:S, V2:S, V1:S, V2:S, V2:S, V1:S, V2:S, V2:S, N:S, N:S, XS:S, Y:S, XS:S, N:S, X:S, XS:S, X:S, YS:S, ZS:S, X:S, XS:S, N:S, XS:S, N:S, V1:S, V2:S, V2:S, V1:S, V2:S, V2:S, V1:S, V1:S, V1:S, V1:S, N:S, XS:S, X:S, X:S, Y:S, N:S, XS:S, V1:S, V2:S, V1:S, V1:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V1:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, N:S, N:S, XS:S, X:S, Y:S, XS:S, N:S, X:S, XS:S, N:S, XS:S, N:S, XS:S 0.003/0.003 -> UVars: 0.003/0.003 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.003/0.003 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.003/0.003 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [Y:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.003/0.003 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [X:S]) 0.003/0.003 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, YS:S, ZS:S], UV-RFrozen: [X:S, YS:S, ZS:S]) 0.003/0.003 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.003/0.003 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.003/0.003 (UV-RuleId: 45, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.003/0.003 (UV-RuleId: 46, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 47, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 48, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 49, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 50, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 51, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 52, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 54, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 55, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 56, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 57, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 58, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 59, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 60, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 61, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 62, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 63, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 64, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 65, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.003/0.003 (UV-RuleId: 66, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 67, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 68, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 69, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 70, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 71, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.003/0.003 (UV-RuleId: 72, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 73, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.003/0.003 (UV-RuleId: 74, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.003/0.003 (UV-RuleId: 75, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.003/0.003 (UV-RuleId: 76, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.003/0.003 (UV-RuleId: 77, UV-LActive: [XS:S], UV-RActive: [XS:S], UV-LFrozen: [], UV-RFrozen: [XS:S]) 0.003/0.003 (UV-RuleId: 78, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.003/0.003 (UV-RuleId: 79, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.003/0.003 (UV-RuleId: 80, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.003/0.003 -> FVars: 0.003/0.003 x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64, x65, x66, x67, x68, x69, x70, x71, x72, x73, x74, x75, x76, x77, x78, x79, x80, x81, x82, x83, x84, x85, x86, x87, x88, x89, x90, x91, x92, x93, x94, x95, x96, x97, x98, x99, x100, x101, x102, x103, x104, x105, x106, x107 0.003/0.003 -> PVars: 0.003/0.003 V1:S: [x10, x15, x16, x17, x20, x23, x42, x45, x48, x49, x50, x51, x59, x61, x62, x63, x64, x65, x67, x69, x71, x72, x73, x74, x75, x77, x79, x80, x82, x83, x84, x86, x87, x89, x91, x93], V2:S: [x11, x12, x18, x19, x21, x22, x24, x25, x43, x44, x46, x47, x60, x66, x68, x70, x76, x78, x81, x85, x88, x90, x92, x94], N:S: [x13, x26, x27, x31, x39, x41, x52, x57, x95, x96, x101, x104, x106], XS:S: [x14, x28, x30, x33, x38, x40, x53, x58, x97, x100, x103, x105, x107], Y:S: [x29, x56, x99], X:S: [x32, x34, x37, x54, x55, x98, x102], YS:S: [x35], ZS:S: [x36] 0.003/0.003 0.003/0.003 -> Rlps: 0.003/0.003 (rule: U101(tt,x10:S,x11:S) -> U102(isNatural(x10:S),x11:S), id: 1, possubterms: U101(tt,x10:S,x11:S)->[], tt->[1]) 0.003/0.003 (rule: U102(tt,x12:S) -> U103(isLNat(x12:S)), id: 2, possubterms: U102(tt,x12:S)->[], tt->[1]) 0.003/0.003 (rule: U103(tt) -> tt, id: 3, possubterms: U103(tt)->[], tt->[1]) 0.003/0.003 (rule: U11(tt,x13:S,x14:S) -> snd(splitAt(x13:S,x14:S)), id: 4, possubterms: U11(tt,x13:S,x14:S)->[], tt->[1]) 0.003/0.003 (rule: U111(tt,x15:S) -> U112(isLNat(x15:S)), id: 5, possubterms: U111(tt,x15:S)->[], tt->[1]) 0.003/0.003 (rule: U112(tt) -> tt, id: 6, possubterms: U112(tt)->[], tt->[1]) 0.003/0.003 (rule: U121(tt,x16:S) -> U122(isNatural(x16:S)), id: 7, possubterms: U121(tt,x16:S)->[], tt->[1]) 0.003/0.003 (rule: U122(tt) -> tt, id: 8, possubterms: U122(tt)->[], tt->[1]) 0.003/0.003 (rule: U131(tt,x17:S,x18:S) -> U132(isNatural(x17:S),x18:S), id: 9, possubterms: U131(tt,x17:S,x18:S)->[], tt->[1]) 0.003/0.003 (rule: U132(tt,x19:S) -> U133(isLNat(x19:S)), id: 10, possubterms: U132(tt,x19:S)->[], tt->[1]) 0.003/0.003 (rule: U133(tt) -> tt, id: 11, possubterms: U133(tt)->[], tt->[1]) 0.003/0.003 (rule: U141(tt,x20:S,x21:S) -> U142(isLNat(x20:S),x21:S), id: 12, possubterms: U141(tt,x20:S,x21:S)->[], tt->[1]) 0.003/0.003 (rule: U142(tt,x22:S) -> U143(isLNat(x22:S)), id: 13, possubterms: U142(tt,x22:S)->[], tt->[1]) 0.003/0.003 (rule: U143(tt) -> tt, id: 14, possubterms: U143(tt)->[], tt->[1]) 0.003/0.003 (rule: U151(tt,x23:S,x24:S) -> U152(isNatural(x23:S),x24:S), id: 15, possubterms: U151(tt,x23:S,x24:S)->[], tt->[1]) 0.003/0.003 (rule: U152(tt,x25:S) -> U153(isLNat(x25:S)), id: 16, possubterms: U152(tt,x25:S)->[], tt->[1]) 0.003/0.003 (rule: U153(tt) -> tt, id: 17, possubterms: U153(tt)->[], tt->[1]) 0.003/0.003 (rule: U161(tt,x26:S) -> cons(x26:S,natsFrom(s(x26:S))), id: 18, possubterms: U161(tt,x26:S)->[], tt->[1]) 0.003/0.003 (rule: U171(tt,x27:S,x28:S) -> head(afterNth(x27:S,x28:S)), id: 19, possubterms: U171(tt,x27:S,x28:S)->[], tt->[1]) 0.003/0.003 (rule: U181(tt,x29:S) -> x29:S, id: 20, possubterms: U181(tt,x29:S)->[], tt->[1]) 0.003/0.003 (rule: U191(tt,x30:S) -> pair(nil,x30:S), id: 21, possubterms: U191(tt,x30:S)->[], tt->[1]) 0.003/0.003 (rule: U201(tt,x31:S,x32:S,x33:S) -> U202(splitAt(x31:S,x33:S),x32:S), id: 22, possubterms: U201(tt,x31:S,x32:S,x33:S)->[], tt->[1]) 0.003/0.003 (rule: U202(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S), id: 23, possubterms: U202(pair(x35:S,x36:S),x34:S)->[], pair(x35:S,x36:S)->[1]) 0.003/0.003 (rule: U21(tt,x37:S) -> x37:S, id: 24, possubterms: U21(tt,x37:S)->[], tt->[1]) 0.003/0.003 (rule: U211(tt,x38:S) -> x38:S, id: 25, possubterms: U211(tt,x38:S)->[], tt->[1]) 0.003/0.003 (rule: U221(tt,x39:S,x40:S) -> fst(splitAt(x39:S,x40:S)), id: 26, possubterms: U221(tt,x39:S,x40:S)->[], tt->[1]) 0.003/0.003 (rule: U31(tt,x41:S) -> x41:S, id: 27, possubterms: U31(tt,x41:S)->[], tt->[1]) 0.003/0.003 (rule: U41(tt,x42:S,x43:S) -> U42(isNatural(x42:S),x43:S), id: 28, possubterms: U41(tt,x42:S,x43:S)->[], tt->[1]) 0.003/0.003 (rule: U42(tt,x44:S) -> U43(isLNat(x44:S)), id: 29, possubterms: U42(tt,x44:S)->[], tt->[1]) 0.003/0.003 (rule: U43(tt) -> tt, id: 30, possubterms: U43(tt)->[], tt->[1]) 0.003/0.003 (rule: U51(tt,x45:S,x46:S) -> U52(isNatural(x45:S),x46:S), id: 31, possubterms: U51(tt,x45:S,x46:S)->[], tt->[1]) 0.003/0.003 (rule: U52(tt,x47:S) -> U53(isLNat(x47:S)), id: 32, possubterms: U52(tt,x47:S)->[], tt->[1]) 0.003/0.003 (rule: U53(tt) -> tt, id: 33, possubterms: U53(tt)->[], tt->[1]) 0.003/0.003 (rule: U61(tt,x48:S) -> U62(isPLNat(x48:S)), id: 34, possubterms: U61(tt,x48:S)->[], tt->[1]) 0.003/0.003 (rule: U62(tt) -> tt, id: 35, possubterms: U62(tt)->[], tt->[1]) 0.003/0.003 (rule: U71(tt,x49:S) -> U72(isNatural(x49:S)), id: 36, possubterms: U71(tt,x49:S)->[], tt->[1]) 0.003/0.003 (rule: U72(tt) -> tt, id: 37, possubterms: U72(tt)->[], tt->[1]) 0.003/0.003 (rule: U81(tt,x50:S) -> U82(isPLNat(x50:S)), id: 38, possubterms: U81(tt,x50:S)->[], tt->[1]) 0.003/0.003 (rule: U82(tt) -> tt, id: 39, possubterms: U82(tt)->[], tt->[1]) 0.003/0.003 (rule: U91(tt,x51:S) -> U92(isLNat(x51:S)), id: 40, possubterms: U91(tt,x51:S)->[], tt->[1]) 0.003/0.003 (rule: U92(tt) -> tt, id: 41, possubterms: U92(tt)->[], tt->[1]) 0.003/0.003 (rule: afterNth(x52:S,x53:S) -> U11(and(and(isNatural(x52:S),isNaturalKind(x52:S)),and(isLNat(x53:S),isLNatKind(x53:S))),x52:S,x53:S), id: 42, possubterms: afterNth(x52:S,x53:S)->[]) 0.003/0.003 (rule: and(tt,x54:S) -> x54:S, id: 43, possubterms: and(tt,x54:S)->[], tt->[1]) 0.003/0.003 (rule: fst(pair(x55:S,x56:S)) -> U21(and(and(isLNat(x55:S),isLNatKind(x55:S)),and(isLNat(x56:S),isLNatKind(x56:S))),x55:S), id: 44, possubterms: fst(pair(x55:S,x56:S))->[], pair(x55:S,x56:S)->[1]) 0.003/0.003 (rule: head(cons(x57:S,x58:S)) -> U31(and(and(isNatural(x57:S),isNaturalKind(x57:S)),and(isLNat(x58:S),isLNatKind(x58:S))),x57:S), id: 45, possubterms: head(cons(x57:S,x58:S))->[], cons(x57:S,x58:S)->[1]) 0.003/0.003 (rule: isLNat(afterNth(x59:S,x60:S)) -> U41(and(isNaturalKind(x59:S),isLNatKind(x60:S)),x59:S,x60:S), id: 46, possubterms: isLNat(afterNth(x59:S,x60:S))->[], afterNth(x59:S,x60:S)->[1]) 0.003/0.003 (rule: isLNat(fst(x61:S)) -> U61(isPLNatKind(x61:S),x61:S), id: 47, possubterms: isLNat(fst(x61:S))->[], fst(x61:S)->[1]) 0.003/0.003 (rule: isLNat(natsFrom(x62:S)) -> U71(isNaturalKind(x62:S),x62:S), id: 48, possubterms: isLNat(natsFrom(x62:S))->[], natsFrom(x62:S)->[1]) 0.003/0.003 (rule: isLNat(snd(x63:S)) -> U81(isPLNatKind(x63:S),x63:S), id: 49, possubterms: isLNat(snd(x63:S))->[], snd(x63:S)->[1]) 0.003/0.003 (rule: isLNat(tail(x64:S)) -> U91(isLNatKind(x64:S),x64:S), id: 50, possubterms: isLNat(tail(x64:S))->[], tail(x64:S)->[1]) 0.003/0.003 (rule: isLNat(take(x65:S,x66:S)) -> U101(and(isNaturalKind(x65:S),isLNatKind(x66:S)),x65:S,x66:S), id: 51, possubterms: isLNat(take(x65:S,x66:S))->[], take(x65:S,x66:S)->[1]) 0.003/0.003 (rule: isLNat(cons(x67:S,x68:S)) -> U51(and(isNaturalKind(x67:S),isLNatKind(x68:S)),x67:S,x68:S), id: 52, possubterms: isLNat(cons(x67:S,x68:S))->[], cons(x67:S,x68:S)->[1]) 0.003/0.003 (rule: isLNat(nil) -> tt, id: 53, possubterms: isLNat(nil)->[], nil->[1]) 0.003/0.003 (rule: isLNatKind(afterNth(x69:S,x70:S)) -> and(isNaturalKind(x69:S),isLNatKind(x70:S)), id: 54, possubterms: isLNatKind(afterNth(x69:S,x70:S))->[], afterNth(x69:S,x70:S)->[1]) 0.003/0.003 (rule: isLNatKind(fst(x71:S)) -> isPLNatKind(x71:S), id: 55, possubterms: isLNatKind(fst(x71:S))->[], fst(x71:S)->[1]) 0.003/0.003 (rule: isLNatKind(natsFrom(x72:S)) -> isNaturalKind(x72:S), id: 56, possubterms: isLNatKind(natsFrom(x72:S))->[], natsFrom(x72:S)->[1]) 0.003/0.003 (rule: isLNatKind(snd(x73:S)) -> isPLNatKind(x73:S), id: 57, possubterms: isLNatKind(snd(x73:S))->[], snd(x73:S)->[1]) 0.003/0.003 (rule: isLNatKind(tail(x74:S)) -> isLNatKind(x74:S), id: 58, possubterms: isLNatKind(tail(x74:S))->[], tail(x74:S)->[1]) 0.003/0.003 (rule: isLNatKind(take(x75:S,x76:S)) -> and(isNaturalKind(x75:S),isLNatKind(x76:S)), id: 59, possubterms: isLNatKind(take(x75:S,x76:S))->[], take(x75:S,x76:S)->[1]) 0.003/0.003 (rule: isLNatKind(cons(x77:S,x78:S)) -> and(isNaturalKind(x77:S),isLNatKind(x78:S)), id: 60, possubterms: isLNatKind(cons(x77:S,x78:S))->[], cons(x77:S,x78:S)->[1]) 0.003/0.003 (rule: isLNatKind(nil) -> tt, id: 61, possubterms: isLNatKind(nil)->[], nil->[1]) 0.003/0.003 (rule: isNatural(head(x79:S)) -> U111(isLNatKind(x79:S),x79:S), id: 62, possubterms: isNatural(head(x79:S))->[], head(x79:S)->[1]) 0.003/0.003 (rule: isNatural(sel(x80:S,x81:S)) -> U131(and(isNaturalKind(x80:S),isLNatKind(x81:S)),x80:S,x81:S), id: 63, possubterms: isNatural(sel(x80:S,x81:S))->[], sel(x80:S,x81:S)->[1]) 0.003/0.003 (rule: isNatural(num0) -> tt, id: 64, possubterms: isNatural(num0)->[], num0->[1]) 0.003/0.003 (rule: isNatural(s(x82:S)) -> U121(isNaturalKind(x82:S),x82:S), id: 65, possubterms: isNatural(s(x82:S))->[], s(x82:S)->[1]) 0.003/0.003 (rule: isNaturalKind(head(x83:S)) -> isLNatKind(x83:S), id: 66, possubterms: isNaturalKind(head(x83:S))->[], head(x83:S)->[1]) 0.003/0.003 (rule: isNaturalKind(sel(x84:S,x85:S)) -> and(isNaturalKind(x84:S),isLNatKind(x85:S)), id: 67, possubterms: isNaturalKind(sel(x84:S,x85:S))->[], sel(x84:S,x85:S)->[1]) 0.003/0.003 (rule: isNaturalKind(num0) -> tt, id: 68, possubterms: isNaturalKind(num0)->[], num0->[1]) 0.003/0.003 (rule: isNaturalKind(s(x86:S)) -> isNaturalKind(x86:S), id: 69, possubterms: isNaturalKind(s(x86:S))->[], s(x86:S)->[1]) 0.003/0.003 (rule: isPLNat(splitAt(x87:S,x88:S)) -> U151(and(isNaturalKind(x87:S),isLNatKind(x88:S)),x87:S,x88:S), id: 70, possubterms: isPLNat(splitAt(x87:S,x88:S))->[], splitAt(x87:S,x88:S)->[1]) 0.003/0.003 (rule: isPLNat(pair(x89:S,x90:S)) -> U141(and(isLNatKind(x89:S),isLNatKind(x90:S)),x89:S,x90:S), id: 71, possubterms: isPLNat(pair(x89:S,x90:S))->[], pair(x89:S,x90:S)->[1]) 0.003/0.003 (rule: isPLNatKind(splitAt(x91:S,x92:S)) -> and(isNaturalKind(x91:S),isLNatKind(x92:S)), id: 72, possubterms: isPLNatKind(splitAt(x91:S,x92:S))->[], splitAt(x91:S,x92:S)->[1]) 0.003/0.003 (rule: isPLNatKind(pair(x93:S,x94:S)) -> and(isLNatKind(x93:S),isLNatKind(x94:S)), id: 73, possubterms: isPLNatKind(pair(x93:S,x94:S))->[], pair(x93:S,x94:S)->[1]) 0.003/0.003 (rule: natsFrom(x95:S) -> U161(and(isNatural(x95:S),isNaturalKind(x95:S)),x95:S), id: 74, possubterms: natsFrom(x95:S)->[]) 0.003/0.003 (rule: sel(x96:S,x97:S) -> U171(and(and(isNatural(x96:S),isNaturalKind(x96:S)),and(isLNat(x97:S),isLNatKind(x97:S))),x96:S,x97:S), id: 75, possubterms: sel(x96:S,x97:S)->[]) 0.003/0.003 (rule: snd(pair(x98:S,x99:S)) -> U181(and(and(isLNat(x98:S),isLNatKind(x98:S)),and(isLNat(x99:S),isLNatKind(x99:S))),x99:S), id: 76, possubterms: snd(pair(x98:S,x99:S))->[], pair(x98:S,x99:S)->[1]) 0.003/0.003 (rule: splitAt(num0,x100:S) -> U191(and(isLNat(x100:S),isLNatKind(x100:S)),x100:S), id: 77, possubterms: splitAt(num0,x100:S)->[], num0->[1]) 0.003/0.003 (rule: splitAt(s(x101:S),cons(x102:S,x103:S)) -> U201(and(and(isNatural(x101:S),isNaturalKind(x101:S)),and(and(isNatural(x102:S),isNaturalKind(x102:S)),and(isLNat(x103:S),isLNatKind(x103:S)))),x101:S,x102:S,x103:S), id: 78, possubterms: splitAt(s(x101:S),cons(x102:S,x103:S))->[], s(x101:S)->[1], cons(x102:S,x103:S)->[2]) 0.003/0.003 (rule: tail(cons(x104:S,x105:S)) -> U211(and(and(isNatural(x104:S),isNaturalKind(x104:S)),and(isLNat(x105:S),isLNatKind(x105:S))),x105:S), id: 79, possubterms: tail(cons(x104:S,x105:S))->[], cons(x104:S,x105:S)->[1]) 0.003/0.003 (rule: take(x106:S,x107:S) -> U221(and(and(isNatural(x106:S),isNaturalKind(x106:S)),and(isLNat(x107:S),isLNatKind(x107:S))),x106:S,x107:S), id: 80, possubterms: take(x106:S,x107:S)->[]) 0.003/0.003 0.003/0.003 -> Unifications: 0.003/0.003 (R46 unifies with R42 at p: [1], l: isLNat(afterNth(x59:S,x60:S)), lp: afterNth(x59:S,x60:S), sig: {x59:S -> N:S:S,x60:S -> XS:S:S}, l': afterNth(N:S:S,XS:S:S), r: U41(and(isNaturalKind(x59:S),isLNatKind(x60:S)),x59:S,x60:S), r': U11(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S)) 0.003/0.003 (R47 unifies with R44 at p: [1], l: isLNat(fst(x61:S)), lp: fst(x61:S), sig: {x61:S -> pair(X:S:S,Y:S:S)}, l': fst(pair(X:S:S,Y:S:S)), r: U61(isPLNatKind(x61:S),x61:S), r': U21(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),X:S:S)) 0.003/0.003 (R48 unifies with R74 at p: [1], l: isLNat(natsFrom(x62:S)), lp: natsFrom(x62:S), sig: {x62:S -> N:S:S}, l': natsFrom(N:S:S), r: U71(isNaturalKind(x62:S),x62:S), r': U161(and(isNatural(N:S:S),isNaturalKind(N:S:S)),N:S:S)) 0.003/0.003 (R49 unifies with R76 at p: [1], l: isLNat(snd(x63:S)), lp: snd(x63:S), sig: {x63:S -> pair(X:S:S,Y:S:S)}, l': snd(pair(X:S:S,Y:S:S)), r: U81(isPLNatKind(x63:S),x63:S), r': U181(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),Y:S:S)) 0.003/0.003 (R50 unifies with R79 at p: [1], l: isLNat(tail(x64:S)), lp: tail(x64:S), sig: {x64:S -> cons(N:S:S,XS:S:S)}, l': tail(cons(N:S:S,XS:S:S)), r: U91(isLNatKind(x64:S),x64:S), r': U211(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),XS:S:S)) 0.003/0.003 (R51 unifies with R80 at p: [1], l: isLNat(take(x65:S,x66:S)), lp: take(x65:S,x66:S), sig: {x65:S -> N:S:S,x66:S -> XS:S:S}, l': take(N:S:S,XS:S:S), r: U101(and(isNaturalKind(x65:S),isLNatKind(x66:S)),x65:S,x66:S), r': U221(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S)) 0.003/0.003 (R54 unifies with R42 at p: [1], l: isLNatKind(afterNth(x69:S,x70:S)), lp: afterNth(x69:S,x70:S), sig: {x69:S -> N:S:S,x70:S -> XS:S:S}, l': afterNth(N:S:S,XS:S:S), r: and(isNaturalKind(x69:S),isLNatKind(x70:S)), r': U11(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S)) 0.003/0.003 (R55 unifies with R44 at p: [1], l: isLNatKind(fst(x71:S)), lp: fst(x71:S), sig: {x71:S -> pair(X:S:S,Y:S:S)}, l': fst(pair(X:S:S,Y:S:S)), r: isPLNatKind(x71:S), r': U21(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),X:S:S)) 0.003/0.003 (R56 unifies with R74 at p: [1], l: isLNatKind(natsFrom(x72:S)), lp: natsFrom(x72:S), sig: {x72:S -> N:S:S}, l': natsFrom(N:S:S), r: isNaturalKind(x72:S), r': U161(and(isNatural(N:S:S),isNaturalKind(N:S:S)),N:S:S)) 0.003/0.003 (R57 unifies with R76 at p: [1], l: isLNatKind(snd(x73:S)), lp: snd(x73:S), sig: {x73:S -> pair(X:S:S,Y:S:S)}, l': snd(pair(X:S:S,Y:S:S)), r: isPLNatKind(x73:S), r': U181(and(and(isLNat(X:S:S),isLNatKind(X:S:S)),and(isLNat(Y:S:S),isLNatKind(Y:S:S))),Y:S:S)) 0.003/0.003 (R58 unifies with R79 at p: [1], l: isLNatKind(tail(x74:S)), lp: tail(x74:S), sig: {x74:S -> cons(N:S:S,XS:S:S)}, l': tail(cons(N:S:S,XS:S:S)), r: isLNatKind(x74:S), r': U211(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),XS:S:S)) 0.003/0.003 (R59 unifies with R80 at p: [1], l: isLNatKind(take(x75:S,x76:S)), lp: take(x75:S,x76:S), sig: {x75:S -> N:S:S,x76:S -> XS:S:S}, l': take(N:S:S,XS:S:S), r: and(isNaturalKind(x75:S),isLNatKind(x76:S)), r': U221(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S)) 0.003/0.003 (R62 unifies with R45 at p: [1], l: isNatural(head(x79:S)), lp: head(x79:S), sig: {x79:S -> cons(N:S:S,XS:S:S)}, l': head(cons(N:S:S,XS:S:S)), r: U111(isLNatKind(x79:S),x79:S), r': U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S)) 0.003/0.003 (R63 unifies with R75 at p: [1], l: isNatural(sel(x80:S,x81:S)), lp: sel(x80:S,x81:S), sig: {x80:S -> N:S:S,x81:S -> XS:S:S}, l': sel(N:S:S,XS:S:S), r: U131(and(isNaturalKind(x80:S),isLNatKind(x81:S)),x80:S,x81:S), r': U171(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S)) 0.003/0.003 (R66 unifies with R45 at p: [1], l: isNaturalKind(head(x83:S)), lp: head(x83:S), sig: {x83:S -> cons(N:S:S,XS:S:S)}, l': head(cons(N:S:S,XS:S:S)), r: isLNatKind(x83:S), r': U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S)) 0.003/0.003 (R67 unifies with R75 at p: [1], l: isNaturalKind(sel(x84:S,x85:S)), lp: sel(x84:S,x85:S), sig: {x84:S -> N:S:S,x85:S -> XS:S:S}, l': sel(N:S:S,XS:S:S), r: and(isNaturalKind(x84:S),isLNatKind(x85:S)), r': U171(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S,XS:S:S)) 0.003/0.003 (R70 unifies with R77 at p: [1], l: isPLNat(splitAt(x87:S,x88:S)), lp: splitAt(x87:S,x88:S), sig: {x87:S -> num0,x88:S -> XS:S:S}, l': splitAt(num0,XS:S:S), r: U151(and(isNaturalKind(x87:S),isLNatKind(x88:S)),x87:S,x88:S), r': U191(and(isLNat(XS:S:S),isLNatKind(XS:S:S)),XS:S:S)) 0.003/0.003 (R70 unifies with R78 at p: [1], l: isPLNat(splitAt(x87:S,x88:S)), lp: splitAt(x87:S,x88:S), sig: {x87:S -> s(N:S:S),x88:S -> cons(X:S:S,XS:S:S)}, l': splitAt(s(N:S:S),cons(X:S:S,XS:S:S)), r: U151(and(isNaturalKind(x87:S),isLNatKind(x88:S)),x87:S,x88:S), r': U201(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(and(isNatural(X:S:S),isNaturalKind(X:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S)))),N:S:S,X:S:S,XS:S:S)) 0.003/0.003 (R72 unifies with R77 at p: [1], l: isPLNatKind(splitAt(x91:S,x92:S)), lp: splitAt(x91:S,x92:S), sig: {x91:S -> num0,x92:S -> XS:S:S}, l': splitAt(num0,XS:S:S), r: and(isNaturalKind(x91:S),isLNatKind(x92:S)), r': U191(and(isLNat(XS:S:S),isLNatKind(XS:S:S)),XS:S:S)) 0.003/0.003 (R72 unifies with R78 at p: [1], l: isPLNatKind(splitAt(x91:S,x92:S)), lp: splitAt(x91:S,x92:S), sig: {x91:S -> s(N:S:S),x92:S -> cons(X:S:S,XS:S:S)}, l': splitAt(s(N:S:S),cons(X:S:S,XS:S:S)), r: and(isNaturalKind(x91:S),isLNatKind(x92:S)), r': U201(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(and(isNatural(X:S:S),isNaturalKind(X:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S)))),N:S:S,X:S:S,XS:S:S)) 0.003/0.003 0.003/0.003 -> Critical pairs info: 0.003/0.003 => Not trivial, Not overlay, NW0, N1 0.003/0.003 => Not trivial, Not overlay, NW0, N2 0.003/0.003 => Not trivial, Not overlay, NW0, N3 0.003/0.003 => Not trivial, Not overlay, NW0, N4 0.003/0.003 => Not trivial, Not overlay, NW0, N5 0.003/0.003 => Not trivial, Not overlay, NW0, N6 0.003/0.003 => Not trivial, Not overlay, NW0, N7 0.003/0.003 => Not trivial, Not overlay, NW0, N8 0.003/0.003 => Not trivial, Not overlay, NW0, N9 0.003/0.003 => Not trivial, Not overlay, NW0, N10 0.003/0.003 => Not trivial, Not overlay, NW0, N11 0.003/0.003 => Not trivial, Not overlay, NW0, N12 0.003/0.003 => Not trivial, Not overlay, NW0, N13 0.003/0.003 => Not trivial, Not overlay, NW0, N14 0.003/0.003 => Not trivial, Not overlay, NW0, N15 0.003/0.003 => Not trivial, Not overlay, NW0, N16 0.003/0.003 => Not trivial, Not overlay, NW0, N17 0.003/0.003 => Not trivial, Not overlay, NW0, N18 0.003/0.003 => Not trivial, Not overlay, NW0, N19 0.003/0.003 => Not trivial, Not overlay, NW0, N20 0.003/0.003 0.003/0.003 -> Problem conclusions: 0.003/0.003 Left linear, Not right linear, Not linear 0.003/0.003 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.003/0.003 Not Huet-Levy confluent, Not Newman confluent 0.003/0.003 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 No Convergence Brute Force Processor: 0.003/0.003 -> Rewritings: 0.003/0.003 s: isNatural(U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S)) 0.003/0.003 Nodes: [0] 0.003/0.003 Edges: [] 0.003/0.003 ID: 0 => ('isNatural(U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S))', D0) 0.003/0.003 t: U111(isLNatKind(cons(N:S:S,XS:S:S)),cons(N:S:S,XS:S:S)) 0.003/0.003 Nodes: [0,1] 0.003/0.003 Edges: [(0,1)] 0.003/0.003 ID: 0 => ('U111(isLNatKind(cons(N:S:S,XS:S:S)),cons(N:S:S,XS:S:S))', D0) 0.003/0.003 ID: 1 => ('U111(and(isNaturalKind(N:S:S),isLNatKind(XS:S:S)),cons(N:S:S,XS:S:S))', D1, R60, P[1], S{x77:S -> N:S:S, x78:S -> XS:S:S}), NR: 'and(isNaturalKind(N:S:S),isLNatKind(XS:S:S))' 0.003/0.003 isNatural(U31(and(and(isNatural(N:S:S),isNaturalKind(N:S:S)),and(isLNat(XS:S:S),isLNatKind(XS:S:S))),N:S:S)) ->* no union *<- U111(isLNatKind(cons(N:S:S,XS:S:S)),cons(N:S:S,XS:S:S)) 0.003/0.003 "Not joinable" 0.003/0.003 0.003/0.003 The problem is not joinable. 0.003/0.003 0.02user 0.00system 0:00.03elapsed 84%CPU (0avgtext+0avgdata 13128maxresident)k 0.003/0.003 16inputs+0outputs (0major+1497minor)pagefaults 0swaps