0.002/0.002 NO 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (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.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U102 1) 0.002/0.002 (U11 1) 0.002/0.002 (U111 1) 0.002/0.002 (U12 1) 0.002/0.002 (U121 1) 0.002/0.002 (U131 1) 0.002/0.002 (U132 1) 0.002/0.002 (U141 1) 0.002/0.002 (U142 1) 0.002/0.002 (U151 1) 0.002/0.002 (U152 1) 0.002/0.002 (U161 1) 0.002/0.002 (U171 1) 0.002/0.002 (U172 1) 0.002/0.002 (U181 1) 0.002/0.002 (U182 1) 0.002/0.002 (U191 1) 0.002/0.002 (U201 1) 0.002/0.002 (U202 1) 0.002/0.002 (U203 1) 0.002/0.002 (U204 1) 0.002/0.002 (U21 1) 0.002/0.002 (U211 1) 0.002/0.002 (U212 1) 0.002/0.002 (U22 1) 0.002/0.002 (U221 1) 0.002/0.002 (U222 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U91 1) 0.002/0.002 (afterNth) 0.002/0.002 (fst 1) 0.002/0.002 (head 1) 0.002/0.002 (isLNat 1) 0.002/0.002 (isNatural 1) 0.002/0.002 (isPLNat 1) 0.002/0.002 (natsFrom) 0.002/0.002 (sel) 0.002/0.002 (snd 1) 0.002/0.002 (splitAt 1 2) 0.002/0.002 (tail 1) 0.002/0.002 (take) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (pair) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,V2:S:S) -> U102(isLNat(V2:S:S)) 0.002/0.002 U102(tt) -> tt 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> U12(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U111(tt) -> tt 0.002/0.002 U12(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U121(tt) -> tt 0.002/0.002 U131(tt,V2:S:S) -> U132(isLNat(V2:S:S)) 0.002/0.002 U132(tt) -> tt 0.002/0.002 U141(tt,V2:S:S) -> U142(isLNat(V2:S:S)) 0.002/0.002 U142(tt) -> tt 0.002/0.002 U151(tt,V2:S:S) -> U152(isLNat(V2:S:S)) 0.002/0.002 U152(tt) -> tt 0.002/0.002 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U171(tt,N:S:S,XS:S:S) -> U172(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U172(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U181(tt,Y:S:S) -> U182(isLNat(Y:S:S),Y:S:S) 0.002/0.002 U182(tt,Y:S:S) -> Y:S:S 0.002/0.002 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U202(tt,N:S:S,X:S:S,XS:S:S) -> U203(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U203(tt,N:S:S,X:S:S,XS:S:S) -> U204(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U204(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U21(tt,X:S:S,Y:S:S) -> U22(isLNat(Y:S:S),X:S:S) 0.002/0.002 U211(tt,XS:S:S) -> U212(isLNat(XS:S:S),XS:S:S) 0.002/0.002 U212(tt,XS:S:S) -> XS:S:S 0.002/0.002 U22(tt,X:S:S) -> X:S:S 0.002/0.002 U221(tt,N:S:S,XS:S:S) -> U222(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U222(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U31(tt,N:S:S,XS:S:S) -> U32(isLNat(XS:S:S),N:S:S) 0.002/0.002 U32(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,V2:S:S) -> U42(isLNat(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S:S) -> U52(isLNat(V2:S:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt) -> tt 0.002/0.002 U81(tt) -> tt 0.002/0.002 U91(tt) -> tt 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(fst(V1:S:S)) -> U61(isPLNat(V1:S:S)) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> U71(isNatural(V1:S:S)) 0.002/0.002 isLNat(snd(V1:S:S)) -> U81(isPLNat(V1:S:S)) 0.002/0.002 isLNat(tail(V1:S:S)) -> U91(isLNat(V1:S:S)) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> U111(isLNat(V1:S:S)) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> U131(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> U121(isNatural(V1:S:S)) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(isLNat(V1:S:S),V2:S:S) 0.002/0.002 natsFrom(N:S:S) -> U161(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U171(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U181(isLNat(X:S:S),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U191(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U211(isNatural(N:S:S),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U221(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 CleanTRS Processor: 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (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.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U102 1) 0.002/0.002 (U11 1) 0.002/0.002 (U111 1) 0.002/0.002 (U12 1) 0.002/0.002 (U121 1) 0.002/0.002 (U131 1) 0.002/0.002 (U132 1) 0.002/0.002 (U141 1) 0.002/0.002 (U142 1) 0.002/0.002 (U151 1) 0.002/0.002 (U152 1) 0.002/0.002 (U161 1) 0.002/0.002 (U171 1) 0.002/0.002 (U172 1) 0.002/0.002 (U181 1) 0.002/0.002 (U182 1) 0.002/0.002 (U191 1) 0.002/0.002 (U201 1) 0.002/0.002 (U202 1) 0.002/0.002 (U203 1) 0.002/0.002 (U204 1) 0.002/0.002 (U21 1) 0.002/0.002 (U211 1) 0.002/0.002 (U212 1) 0.002/0.002 (U22 1) 0.002/0.002 (U221 1) 0.002/0.002 (U222 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U91 1) 0.002/0.002 (afterNth) 0.002/0.002 (fst 1) 0.002/0.002 (head 1) 0.002/0.002 (isLNat 1) 0.002/0.002 (isNatural 1) 0.002/0.002 (isPLNat 1) 0.002/0.002 (natsFrom) 0.002/0.002 (sel) 0.002/0.002 (snd 1) 0.002/0.002 (splitAt 1 2) 0.002/0.002 (tail 1) 0.002/0.002 (take) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (pair) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,V2:S:S) -> U102(isLNat(V2:S:S)) 0.002/0.002 U102(tt) -> tt 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> U12(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U111(tt) -> tt 0.002/0.002 U12(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U121(tt) -> tt 0.002/0.002 U131(tt,V2:S:S) -> U132(isLNat(V2:S:S)) 0.002/0.002 U132(tt) -> tt 0.002/0.002 U141(tt,V2:S:S) -> U142(isLNat(V2:S:S)) 0.002/0.002 U142(tt) -> tt 0.002/0.002 U151(tt,V2:S:S) -> U152(isLNat(V2:S:S)) 0.002/0.002 U152(tt) -> tt 0.002/0.002 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U171(tt,N:S:S,XS:S:S) -> U172(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U172(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U181(tt,Y:S:S) -> U182(isLNat(Y:S:S),Y:S:S) 0.002/0.002 U182(tt,Y:S:S) -> Y:S:S 0.002/0.002 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U202(tt,N:S:S,X:S:S,XS:S:S) -> U203(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U203(tt,N:S:S,X:S:S,XS:S:S) -> U204(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U204(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U21(tt,X:S:S,Y:S:S) -> U22(isLNat(Y:S:S),X:S:S) 0.002/0.002 U211(tt,XS:S:S) -> U212(isLNat(XS:S:S),XS:S:S) 0.002/0.002 U212(tt,XS:S:S) -> XS:S:S 0.002/0.002 U22(tt,X:S:S) -> X:S:S 0.002/0.002 U221(tt,N:S:S,XS:S:S) -> U222(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U222(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U31(tt,N:S:S,XS:S:S) -> U32(isLNat(XS:S:S),N:S:S) 0.002/0.002 U32(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,V2:S:S) -> U42(isLNat(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S:S) -> U52(isLNat(V2:S:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt) -> tt 0.002/0.002 U81(tt) -> tt 0.002/0.002 U91(tt) -> tt 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(fst(V1:S:S)) -> U61(isPLNat(V1:S:S)) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> U71(isNatural(V1:S:S)) 0.002/0.002 isLNat(snd(V1:S:S)) -> U81(isPLNat(V1:S:S)) 0.002/0.002 isLNat(tail(V1:S:S)) -> U91(isLNat(V1:S:S)) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> U111(isLNat(V1:S:S)) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> U131(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> U121(isNatural(V1:S:S)) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(isLNat(V1:S:S),V2:S:S) 0.002/0.002 natsFrom(N:S:S) -> U161(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U171(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U181(isLNat(X:S:S),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U191(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U211(isNatural(N:S:S),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U221(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 Modular Confluence Combinations Decomposition Processor: 0.002/0.002 It is a CTRS -> No modular confluence 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 CS-TRS Processor: 0.002/0.002 R is a CS-TRS 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (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.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (U101 1) 0.002/0.002 (U102 1) 0.002/0.002 (U11 1) 0.002/0.002 (U111 1) 0.002/0.002 (U12 1) 0.002/0.002 (U121 1) 0.002/0.002 (U131 1) 0.002/0.002 (U132 1) 0.002/0.002 (U141 1) 0.002/0.002 (U142 1) 0.002/0.002 (U151 1) 0.002/0.002 (U152 1) 0.002/0.002 (U161 1) 0.002/0.002 (U171 1) 0.002/0.002 (U172 1) 0.002/0.002 (U181 1) 0.002/0.002 (U182 1) 0.002/0.002 (U191 1) 0.002/0.002 (U201 1) 0.002/0.002 (U202 1) 0.002/0.002 (U203 1) 0.002/0.002 (U204 1) 0.002/0.002 (U21 1) 0.002/0.002 (U211 1) 0.002/0.002 (U212 1) 0.002/0.002 (U22 1) 0.002/0.002 (U221 1) 0.002/0.002 (U222 1) 0.002/0.002 (U31 1) 0.002/0.002 (U32 1) 0.002/0.002 (U41 1) 0.002/0.002 (U42 1) 0.002/0.002 (U51 1) 0.002/0.002 (U52 1) 0.002/0.002 (U61 1) 0.002/0.002 (U71 1) 0.002/0.002 (U81 1) 0.002/0.002 (U91 1) 0.002/0.002 (afterNth) 0.002/0.002 (fst 1) 0.002/0.002 (head 1) 0.002/0.002 (isLNat 1) 0.002/0.002 (isNatural 1) 0.002/0.002 (isPLNat 1) 0.002/0.002 (natsFrom) 0.002/0.002 (sel) 0.002/0.002 (snd 1) 0.002/0.002 (splitAt 1 2) 0.002/0.002 (tail 1) 0.002/0.002 (take) 0.002/0.002 (cons) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (nil) 0.002/0.002 (num0) 0.002/0.002 (pair) 0.002/0.002 (s) 0.002/0.002 (tt) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 U101(tt,V2:S:S) -> U102(isLNat(V2:S:S)) 0.002/0.002 U102(tt) -> tt 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> U12(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U111(tt) -> tt 0.002/0.002 U12(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U121(tt) -> tt 0.002/0.002 U131(tt,V2:S:S) -> U132(isLNat(V2:S:S)) 0.002/0.002 U132(tt) -> tt 0.002/0.002 U141(tt,V2:S:S) -> U142(isLNat(V2:S:S)) 0.002/0.002 U142(tt) -> tt 0.002/0.002 U151(tt,V2:S:S) -> U152(isLNat(V2:S:S)) 0.002/0.002 U152(tt) -> tt 0.002/0.002 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U171(tt,N:S:S,XS:S:S) -> U172(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U172(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U181(tt,Y:S:S) -> U182(isLNat(Y:S:S),Y:S:S) 0.002/0.002 U182(tt,Y:S:S) -> Y:S:S 0.002/0.002 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U202(tt,N:S:S,X:S:S,XS:S:S) -> U203(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U203(tt,N:S:S,X:S:S,XS:S:S) -> U204(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U204(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U21(tt,X:S:S,Y:S:S) -> U22(isLNat(Y:S:S),X:S:S) 0.002/0.002 U211(tt,XS:S:S) -> U212(isLNat(XS:S:S),XS:S:S) 0.002/0.002 U212(tt,XS:S:S) -> XS:S:S 0.002/0.002 U22(tt,X:S:S) -> X:S:S 0.002/0.002 U221(tt,N:S:S,XS:S:S) -> U222(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U222(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U31(tt,N:S:S,XS:S:S) -> U32(isLNat(XS:S:S),N:S:S) 0.002/0.002 U32(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,V2:S:S) -> U42(isLNat(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S:S) -> U52(isLNat(V2:S:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt) -> tt 0.002/0.002 U81(tt) -> tt 0.002/0.002 U91(tt) -> tt 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(fst(V1:S:S)) -> U61(isPLNat(V1:S:S)) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> U71(isNatural(V1:S:S)) 0.002/0.002 isLNat(snd(V1:S:S)) -> U81(isPLNat(V1:S:S)) 0.002/0.002 isLNat(tail(V1:S:S)) -> U91(isLNat(V1:S:S)) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> U111(isLNat(V1:S:S)) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> U131(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> U121(isNatural(V1:S:S)) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(isLNat(V1:S:S),V2:S:S) 0.002/0.002 natsFrom(N:S:S) -> U161(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U171(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U181(isLNat(X:S:S),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U191(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U211(isNatural(N:S:S),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U221(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 U101(tt,V2:S:S) -> U102(isLNat(V2:S:S)) 0.002/0.002 U102(tt) -> tt 0.002/0.002 U11(tt,N:S:S,XS:S:S) -> U12(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U111(tt) -> tt 0.002/0.002 U12(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U121(tt) -> tt 0.002/0.002 U131(tt,V2:S:S) -> U132(isLNat(V2:S:S)) 0.002/0.002 U132(tt) -> tt 0.002/0.002 U141(tt,V2:S:S) -> U142(isLNat(V2:S:S)) 0.002/0.002 U142(tt) -> tt 0.002/0.002 U151(tt,V2:S:S) -> U152(isLNat(V2:S:S)) 0.002/0.002 U152(tt) -> tt 0.002/0.002 U161(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.002/0.002 U171(tt,N:S:S,XS:S:S) -> U172(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U172(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.002/0.002 U181(tt,Y:S:S) -> U182(isLNat(Y:S:S),Y:S:S) 0.002/0.002 U182(tt,Y:S:S) -> Y:S:S 0.002/0.002 U191(tt,XS:S:S) -> pair(nil,XS:S:S) 0.002/0.002 U201(tt,N:S:S,X:S:S,XS:S:S) -> U202(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U202(tt,N:S:S,X:S:S,XS:S:S) -> U203(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 U203(tt,N:S:S,X:S:S,XS:S:S) -> U204(splitAt(N:S:S,XS:S:S),X:S:S) 0.002/0.002 U204(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.002/0.002 U21(tt,X:S:S,Y:S:S) -> U22(isLNat(Y:S:S),X:S:S) 0.002/0.002 U211(tt,XS:S:S) -> U212(isLNat(XS:S:S),XS:S:S) 0.002/0.002 U212(tt,XS:S:S) -> XS:S:S 0.002/0.002 U22(tt,X:S:S) -> X:S:S 0.002/0.002 U221(tt,N:S:S,XS:S:S) -> U222(isLNat(XS:S:S),N:S:S,XS:S:S) 0.002/0.002 U222(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.002/0.002 U31(tt,N:S:S,XS:S:S) -> U32(isLNat(XS:S:S),N:S:S) 0.002/0.002 U32(tt,N:S:S) -> N:S:S 0.002/0.002 U41(tt,V2:S:S) -> U42(isLNat(V2:S:S)) 0.002/0.002 U42(tt) -> tt 0.002/0.002 U51(tt,V2:S:S) -> U52(isLNat(V2:S:S)) 0.002/0.002 U52(tt) -> tt 0.002/0.002 U61(tt) -> tt 0.002/0.002 U71(tt) -> tt 0.002/0.002 U81(tt) -> tt 0.002/0.002 U91(tt) -> tt 0.002/0.002 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.002/0.002 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(fst(V1:S:S)) -> U61(isPLNat(V1:S:S)) 0.002/0.002 isLNat(natsFrom(V1:S:S)) -> U71(isNatural(V1:S:S)) 0.002/0.002 isLNat(snd(V1:S:S)) -> U81(isPLNat(V1:S:S)) 0.002/0.002 isLNat(tail(V1:S:S)) -> U91(isLNat(V1:S:S)) 0.002/0.002 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isLNat(nil) -> tt 0.002/0.002 isNatural(head(V1:S:S)) -> U111(isLNat(V1:S:S)) 0.002/0.002 isNatural(sel(V1:S:S,V2:S:S)) -> U131(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isNatural(num0) -> tt 0.002/0.002 isNatural(s(V1:S:S)) -> U121(isNatural(V1:S:S)) 0.002/0.002 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U151(isNatural(V1:S:S),V2:S:S) 0.002/0.002 isPLNat(pair(V1:S:S,V2:S:S)) -> U141(isLNat(V1:S:S),V2:S:S) 0.002/0.002 natsFrom(N:S:S) -> U161(isNatural(N:S:S),N:S:S) 0.002/0.002 sel(N:S:S,XS:S:S) -> U171(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 snd(pair(X:S:S,Y:S:S)) -> U181(isLNat(X:S:S),Y:S:S) 0.002/0.002 splitAt(num0,XS:S:S) -> U191(isLNat(XS:S:S),XS:S:S) 0.002/0.002 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U201(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.002/0.002 tail(cons(N:S:S,XS:S:S)) -> U211(isNatural(N:S:S),XS:S:S) 0.002/0.002 take(N:S:S,XS:S:S) -> U221(isNatural(N:S:S),N:S:S,XS:S:S) 0.002/0.002 -> Vars: 0.002/0.002 V2:S, N:S, XS:S, N:S, XS:S, V2:S, V2:S, V2:S, N:S, N:S, XS:S, N:S, XS:S, Y:S, Y:S, XS:S, N:S, X:S, XS:S, N:S, X:S, XS:S, N:S, X:S, XS:S, X:S, YS:S, ZS:S, X:S, Y:S, XS:S, XS:S, X:S, N:S, XS:S, N:S, XS:S, N:S, XS:S, N:S, V2:S, V2:S, N:S, XS: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, V1:S, V2:S, V1: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.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [Y:S], UV-RFrozen: [Y:S]) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [Y:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.002/0.002 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [X:S]) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, YS:S, ZS:S], UV-RFrozen: [X:S, YS:S, ZS:S]) 0.002/0.002 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S]) 0.002/0.002 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.002/0.002 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.002/0.002 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 43, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 45, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 46, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 47, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 48, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 49, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 50, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 51, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 52, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 54, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 55, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.002/0.002 (UV-RuleId: 56, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.002/0.002 (UV-RuleId: 57, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 (UV-RuleId: 58, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [Y:S]) 0.002/0.002 (UV-RuleId: 59, UV-LActive: [XS:S], UV-RActive: [XS:S], UV-LFrozen: [], UV-RFrozen: [XS:S]) 0.002/0.002 (UV-RuleId: 60, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.002/0.002 (UV-RuleId: 61, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [XS:S]) 0.002/0.002 (UV-RuleId: 62, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.002/0.002 -> FVars: 0.002/0.002 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 0.002/0.002 -> PVars: 0.002/0.002 V2:S: [x10, x15, x16, x17, x50, x51, x59, x65, x67, x70, x73, x75], N:S: [x11, x13, x18, x19, x21, x26, x29, x32, x43, x45, x47, x49, x52, x56, x76, x77, x82, x85, x87], XS:S: [x12, x14, x20, x22, x25, x28, x31, x34, x40, x41, x44, x46, x48, x53, x57, x78, x81, x84, x86, x88], Y:S: [x23, x24, x39, x55, x80], X:S: [x27, x30, x33, x35, x38, x42, x54, x79, x83], YS:S: [x36], ZS:S: [x37], V1:S: [x58, x60, x61, x62, x63, x64, x66, x68, x69, x71, x72, x74] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: U101(tt,x10:S) -> U102(isLNat(x10:S)), id: 1, possubterms: U101(tt,x10:S)->[], tt->[1]) 0.002/0.002 (rule: U102(tt) -> tt, id: 2, possubterms: U102(tt)->[], tt->[1]) 0.002/0.002 (rule: U11(tt,x11:S,x12:S) -> U12(isLNat(x12:S),x11:S,x12:S), id: 3, possubterms: U11(tt,x11:S,x12:S)->[], tt->[1]) 0.002/0.002 (rule: U111(tt) -> tt, id: 4, possubterms: U111(tt)->[], tt->[1]) 0.002/0.002 (rule: U12(tt,x13:S,x14:S) -> snd(splitAt(x13:S,x14:S)), id: 5, possubterms: U12(tt,x13:S,x14:S)->[], tt->[1]) 0.002/0.002 (rule: U121(tt) -> tt, id: 6, possubterms: U121(tt)->[], tt->[1]) 0.002/0.002 (rule: U131(tt,x15:S) -> U132(isLNat(x15:S)), id: 7, possubterms: U131(tt,x15:S)->[], tt->[1]) 0.002/0.002 (rule: U132(tt) -> tt, id: 8, possubterms: U132(tt)->[], tt->[1]) 0.002/0.002 (rule: U141(tt,x16:S) -> U142(isLNat(x16:S)), id: 9, possubterms: U141(tt,x16:S)->[], tt->[1]) 0.002/0.002 (rule: U142(tt) -> tt, id: 10, possubterms: U142(tt)->[], tt->[1]) 0.002/0.002 (rule: U151(tt,x17:S) -> U152(isLNat(x17:S)), id: 11, possubterms: U151(tt,x17:S)->[], tt->[1]) 0.002/0.002 (rule: U152(tt) -> tt, id: 12, possubterms: U152(tt)->[], tt->[1]) 0.002/0.002 (rule: U161(tt,x18:S) -> cons(x18:S,natsFrom(s(x18:S))), id: 13, possubterms: U161(tt,x18:S)->[], tt->[1]) 0.002/0.002 (rule: U171(tt,x19:S,x20:S) -> U172(isLNat(x20:S),x19:S,x20:S), id: 14, possubterms: U171(tt,x19:S,x20:S)->[], tt->[1]) 0.002/0.002 (rule: U172(tt,x21:S,x22:S) -> head(afterNth(x21:S,x22:S)), id: 15, possubterms: U172(tt,x21:S,x22:S)->[], tt->[1]) 0.002/0.002 (rule: U181(tt,x23:S) -> U182(isLNat(x23:S),x23:S), id: 16, possubterms: U181(tt,x23:S)->[], tt->[1]) 0.002/0.002 (rule: U182(tt,x24:S) -> x24:S, id: 17, possubterms: U182(tt,x24:S)->[], tt->[1]) 0.002/0.002 (rule: U191(tt,x25:S) -> pair(nil,x25:S), id: 18, possubterms: U191(tt,x25:S)->[], tt->[1]) 0.002/0.002 (rule: U201(tt,x26:S,x27:S,x28:S) -> U202(isNatural(x27:S),x26:S,x27:S,x28:S), id: 19, possubterms: U201(tt,x26:S,x27:S,x28:S)->[], tt->[1]) 0.002/0.002 (rule: U202(tt,x29:S,x30:S,x31:S) -> U203(isLNat(x31:S),x29:S,x30:S,x31:S), id: 20, possubterms: U202(tt,x29:S,x30:S,x31:S)->[], tt->[1]) 0.002/0.002 (rule: U203(tt,x32:S,x33:S,x34:S) -> U204(splitAt(x32:S,x34:S),x33:S), id: 21, possubterms: U203(tt,x32:S,x33:S,x34:S)->[], tt->[1]) 0.002/0.002 (rule: U204(pair(x36:S,x37:S),x35:S) -> pair(cons(x35:S,x36:S),x37:S), id: 22, possubterms: U204(pair(x36:S,x37:S),x35:S)->[], pair(x36:S,x37:S)->[1]) 0.002/0.002 (rule: U21(tt,x38:S,x39:S) -> U22(isLNat(x39:S),x38:S), id: 23, possubterms: U21(tt,x38:S,x39:S)->[], tt->[1]) 0.002/0.002 (rule: U211(tt,x40:S) -> U212(isLNat(x40:S),x40:S), id: 24, possubterms: U211(tt,x40:S)->[], tt->[1]) 0.002/0.002 (rule: U212(tt,x41:S) -> x41:S, id: 25, possubterms: U212(tt,x41:S)->[], tt->[1]) 0.002/0.002 (rule: U22(tt,x42:S) -> x42:S, id: 26, possubterms: U22(tt,x42:S)->[], tt->[1]) 0.002/0.002 (rule: U221(tt,x43:S,x44:S) -> U222(isLNat(x44:S),x43:S,x44:S), id: 27, possubterms: U221(tt,x43:S,x44:S)->[], tt->[1]) 0.002/0.002 (rule: U222(tt,x45:S,x46:S) -> fst(splitAt(x45:S,x46:S)), id: 28, possubterms: U222(tt,x45:S,x46:S)->[], tt->[1]) 0.002/0.002 (rule: U31(tt,x47:S,x48:S) -> U32(isLNat(x48:S),x47:S), id: 29, possubterms: U31(tt,x47:S,x48:S)->[], tt->[1]) 0.002/0.002 (rule: U32(tt,x49:S) -> x49:S, id: 30, possubterms: U32(tt,x49:S)->[], tt->[1]) 0.002/0.002 (rule: U41(tt,x50:S) -> U42(isLNat(x50:S)), id: 31, possubterms: U41(tt,x50:S)->[], tt->[1]) 0.002/0.002 (rule: U42(tt) -> tt, id: 32, possubterms: U42(tt)->[], tt->[1]) 0.002/0.002 (rule: U51(tt,x51:S) -> U52(isLNat(x51:S)), id: 33, possubterms: U51(tt,x51:S)->[], tt->[1]) 0.002/0.002 (rule: U52(tt) -> tt, id: 34, possubterms: U52(tt)->[], tt->[1]) 0.002/0.002 (rule: U61(tt) -> tt, id: 35, possubterms: U61(tt)->[], tt->[1]) 0.002/0.002 (rule: U71(tt) -> tt, id: 36, possubterms: U71(tt)->[], tt->[1]) 0.002/0.002 (rule: U81(tt) -> tt, id: 37, possubterms: U81(tt)->[], tt->[1]) 0.002/0.002 (rule: U91(tt) -> tt, id: 38, possubterms: U91(tt)->[], tt->[1]) 0.002/0.002 (rule: afterNth(x52:S,x53:S) -> U11(isNatural(x52:S),x52:S,x53:S), id: 39, possubterms: afterNth(x52:S,x53:S)->[]) 0.002/0.002 (rule: fst(pair(x54:S,x55:S)) -> U21(isLNat(x54:S),x54:S,x55:S), id: 40, possubterms: fst(pair(x54:S,x55:S))->[], pair(x54:S,x55:S)->[1]) 0.002/0.002 (rule: head(cons(x56:S,x57:S)) -> U31(isNatural(x56:S),x56:S,x57:S), id: 41, possubterms: head(cons(x56:S,x57:S))->[], cons(x56:S,x57:S)->[1]) 0.002/0.002 (rule: isLNat(afterNth(x58:S,x59:S)) -> U41(isNatural(x58:S),x59:S), id: 42, possubterms: isLNat(afterNth(x58:S,x59:S))->[], afterNth(x58:S,x59:S)->[1]) 0.002/0.002 (rule: isLNat(fst(x60:S)) -> U61(isPLNat(x60:S)), id: 43, possubterms: isLNat(fst(x60:S))->[], fst(x60:S)->[1]) 0.002/0.002 (rule: isLNat(natsFrom(x61:S)) -> U71(isNatural(x61:S)), id: 44, possubterms: isLNat(natsFrom(x61:S))->[], natsFrom(x61:S)->[1]) 0.002/0.002 (rule: isLNat(snd(x62:S)) -> U81(isPLNat(x62:S)), id: 45, possubterms: isLNat(snd(x62:S))->[], snd(x62:S)->[1]) 0.002/0.002 (rule: isLNat(tail(x63:S)) -> U91(isLNat(x63:S)), id: 46, possubterms: isLNat(tail(x63:S))->[], tail(x63:S)->[1]) 0.002/0.002 (rule: isLNat(take(x64:S,x65:S)) -> U101(isNatural(x64:S),x65:S), id: 47, possubterms: isLNat(take(x64:S,x65:S))->[], take(x64:S,x65:S)->[1]) 0.002/0.002 (rule: isLNat(cons(x66:S,x67:S)) -> U51(isNatural(x66:S),x67:S), id: 48, possubterms: isLNat(cons(x66:S,x67:S))->[], cons(x66:S,x67:S)->[1]) 0.002/0.002 (rule: isLNat(nil) -> tt, id: 49, possubterms: isLNat(nil)->[], nil->[1]) 0.002/0.002 (rule: isNatural(head(x68:S)) -> U111(isLNat(x68:S)), id: 50, possubterms: isNatural(head(x68:S))->[], head(x68:S)->[1]) 0.002/0.002 (rule: isNatural(sel(x69:S,x70:S)) -> U131(isNatural(x69:S),x70:S), id: 51, possubterms: isNatural(sel(x69:S,x70:S))->[], sel(x69:S,x70:S)->[1]) 0.002/0.002 (rule: isNatural(num0) -> tt, id: 52, possubterms: isNatural(num0)->[], num0->[1]) 0.002/0.002 (rule: isNatural(s(x71:S)) -> U121(isNatural(x71:S)), id: 53, possubterms: isNatural(s(x71:S))->[], s(x71:S)->[1]) 0.002/0.002 (rule: isPLNat(splitAt(x72:S,x73:S)) -> U151(isNatural(x72:S),x73:S), id: 54, possubterms: isPLNat(splitAt(x72:S,x73:S))->[], splitAt(x72:S,x73:S)->[1]) 0.002/0.002 (rule: isPLNat(pair(x74:S,x75:S)) -> U141(isLNat(x74:S),x75:S), id: 55, possubterms: isPLNat(pair(x74:S,x75:S))->[], pair(x74:S,x75:S)->[1]) 0.002/0.002 (rule: natsFrom(x76:S) -> U161(isNatural(x76:S),x76:S), id: 56, possubterms: natsFrom(x76:S)->[]) 0.002/0.002 (rule: sel(x77:S,x78:S) -> U171(isNatural(x77:S),x77:S,x78:S), id: 57, possubterms: sel(x77:S,x78:S)->[]) 0.002/0.002 (rule: snd(pair(x79:S,x80:S)) -> U181(isLNat(x79:S),x80:S), id: 58, possubterms: snd(pair(x79:S,x80:S))->[], pair(x79:S,x80:S)->[1]) 0.002/0.002 (rule: splitAt(num0,x81:S) -> U191(isLNat(x81:S),x81:S), id: 59, possubterms: splitAt(num0,x81:S)->[], num0->[1]) 0.002/0.002 (rule: splitAt(s(x82:S),cons(x83:S,x84:S)) -> U201(isNatural(x82:S),x82:S,x83:S,x84:S), id: 60, possubterms: splitAt(s(x82:S),cons(x83:S,x84:S))->[], s(x82:S)->[1], cons(x83:S,x84:S)->[2]) 0.002/0.002 (rule: tail(cons(x85:S,x86:S)) -> U211(isNatural(x85:S),x86:S), id: 61, possubterms: tail(cons(x85:S,x86:S))->[], cons(x85:S,x86:S)->[1]) 0.002/0.002 (rule: take(x87:S,x88:S) -> U221(isNatural(x87:S),x87:S,x88:S), id: 62, possubterms: take(x87:S,x88:S)->[]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R42 unifies with R39 at p: [1], l: isLNat(afterNth(x58:S,x59:S)), lp: afterNth(x58:S,x59:S), sig: {x58:S -> N:S:S,x59:S -> XS:S:S}, l': afterNth(N:S:S,XS:S:S), r: U41(isNatural(x58:S),x59:S), r': U11(isNatural(N:S:S),N:S:S,XS:S:S)) 0.002/0.002 (R43 unifies with R40 at p: [1], l: isLNat(fst(x60:S)), lp: fst(x60:S), sig: {x60:S -> pair(X:S:S,Y:S:S)}, l': fst(pair(X:S:S,Y:S:S)), r: U61(isPLNat(x60:S)), r': U21(isLNat(X:S:S),X:S:S,Y:S:S)) 0.002/0.002 (R44 unifies with R56 at p: [1], l: isLNat(natsFrom(x61:S)), lp: natsFrom(x61:S), sig: {x61:S -> N:S:S}, l': natsFrom(N:S:S), r: U71(isNatural(x61:S)), r': U161(isNatural(N:S:S),N:S:S)) 0.002/0.002 (R45 unifies with R58 at p: [1], l: isLNat(snd(x62:S)), lp: snd(x62:S), sig: {x62:S -> pair(X:S:S,Y:S:S)}, l': snd(pair(X:S:S,Y:S:S)), r: U81(isPLNat(x62:S)), r': U181(isLNat(X:S:S),Y:S:S)) 0.002/0.002 (R46 unifies with R61 at p: [1], l: isLNat(tail(x63:S)), lp: tail(x63:S), sig: {x63:S -> cons(N:S:S,XS:S:S)}, l': tail(cons(N:S:S,XS:S:S)), r: U91(isLNat(x63:S)), r': U211(isNatural(N:S:S),XS:S:S)) 0.002/0.002 (R47 unifies with R62 at p: [1], l: isLNat(take(x64:S,x65:S)), lp: take(x64:S,x65:S), sig: {x64:S -> N:S:S,x65:S -> XS:S:S}, l': take(N:S:S,XS:S:S), r: U101(isNatural(x64:S),x65:S), r': U221(isNatural(N:S:S),N:S:S,XS:S:S)) 0.002/0.002 (R50 unifies with R41 at p: [1], l: isNatural(head(x68:S)), lp: head(x68:S), sig: {x68:S -> cons(N:S:S,XS:S:S)}, l': head(cons(N:S:S,XS:S:S)), r: U111(isLNat(x68:S)), r': U31(isNatural(N:S:S),N:S:S,XS:S:S)) 0.002/0.002 (R51 unifies with R57 at p: [1], l: isNatural(sel(x69:S,x70:S)), lp: sel(x69:S,x70:S), sig: {x69:S -> N:S:S,x70:S -> XS:S:S}, l': sel(N:S:S,XS:S:S), r: U131(isNatural(x69:S),x70:S), r': U171(isNatural(N:S:S),N:S:S,XS:S:S)) 0.002/0.002 (R54 unifies with R59 at p: [1], l: isPLNat(splitAt(x72:S,x73:S)), lp: splitAt(x72:S,x73:S), sig: {x72:S -> num0,x73:S -> XS:S:S}, l': splitAt(num0,XS:S:S), r: U151(isNatural(x72:S),x73:S), r': U191(isLNat(XS:S:S),XS:S:S)) 0.002/0.002 (R54 unifies with R60 at p: [1], l: isPLNat(splitAt(x72:S,x73:S)), lp: splitAt(x72:S,x73:S), sig: {x72:S -> s(N:S:S),x73:S -> cons(X:S:S,XS:S:S)}, l': splitAt(s(N:S:S),cons(X:S:S,XS:S:S)), r: U151(isNatural(x72:S),x73:S), r': U201(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S)) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Not overlay, NW0, N1 0.002/0.002 => Not trivial, Not overlay, NW0, N2 0.002/0.002 => Not trivial, Not overlay, NW0, N3 0.002/0.002 => Not trivial, Not overlay, NW0, N4 0.002/0.002 => Not trivial, Not overlay, NW0, N5 0.002/0.002 => Not trivial, Not overlay, NW0, N6 0.002/0.002 => Not trivial, Not overlay, NW0, N7 0.002/0.002 => Not trivial, Not overlay, NW0, N8 0.002/0.002 => Not trivial, Not overlay, NW0, N9 0.002/0.002 => Not trivial, Not overlay, NW0, N10 0.002/0.002 0.002/0.002 -> Problem conclusions: 0.002/0.002 Left linear, Not right linear, Not linear 0.002/0.002 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.002/0.002 Not Huet-Levy confluent, Not Newman confluent 0.002/0.002 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 No Convergence Brute Force Processor: 0.002/0.002 -> Rewritings: 0.002/0.002 s: isPLNat(U191(isLNat(XS:S:S),XS:S:S)) 0.002/0.002 Nodes: [0] 0.002/0.002 Edges: [] 0.002/0.002 ID: 0 => ('isPLNat(U191(isLNat(XS:S:S),XS:S:S))', D0) 0.002/0.002 t: U151(isNatural(num0),XS:S:S) 0.002/0.002 Nodes: [0,1,2] 0.002/0.002 Edges: [(0,1),(1,2)] 0.002/0.002 ID: 0 => ('U151(isNatural(num0),XS:S:S)', D0) 0.002/0.002 ID: 1 => ('U151(tt,XS:S:S)', D1, R52, P[1], S{}), NR: 'tt' 0.002/0.002 ID: 2 => ('U152(isLNat(XS:S:S))', D2, R11, P[], S{x17:S -> XS:S:S}), NR: 'U152(isLNat(XS:S:S))' 0.002/0.002 isPLNat(U191(isLNat(XS:S:S),XS:S:S)) ->* no union *<- U151(isNatural(num0),XS:S:S) 0.002/0.002 "Not joinable" 0.002/0.002 0.002/0.002 The problem is not joinable. 0.002/0.002 0.02user 0.00system 0:00.02elapsed 90%CPU (0avgtext+0avgdata 12156maxresident)k 0.002/0.002 8inputs+0outputs (0major+1221minor)pagefaults 0swaps