0.008/0.008 NO 0.008/0.008 0.008/0.008 Problem 1: 0.008/0.008 0.008/0.008 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 Confluence Problem: 0.008/0.008 (VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S) 0.008/0.008 (STRATEGY CONTEXTSENSITIVE 0.008/0.008 (U101 1) 0.008/0.008 (U102 1) 0.008/0.008 (U11 1) 0.008/0.008 (U111 1) 0.008/0.008 (U12 1) 0.008/0.008 (U121 1) 0.008/0.008 (U131 1) 0.008/0.008 (U132 1) 0.008/0.008 (U141 1) 0.008/0.008 (U142 1) 0.008/0.008 (U151 1) 0.008/0.008 (U152 1) 0.008/0.008 (U161 1) 0.008/0.008 (U171 1) 0.008/0.008 (U172 1) 0.008/0.008 (U181 1) 0.008/0.008 (U182 1) 0.008/0.008 (U191 1) 0.008/0.008 (U201 1) 0.008/0.008 (U202 1) 0.008/0.008 (U203 1) 0.008/0.008 (U204 1) 0.008/0.008 (U21 1) 0.008/0.008 (U211 1) 0.008/0.008 (U212 1) 0.008/0.008 (U22 1) 0.008/0.008 (U221 1) 0.008/0.008 (U222 1) 0.008/0.008 (U31 1) 0.008/0.008 (U32 1) 0.008/0.008 (U41 1) 0.008/0.008 (U42 1) 0.008/0.008 (U51 1) 0.008/0.008 (U52 1) 0.008/0.008 (U61 1) 0.008/0.008 (U71 1) 0.008/0.008 (U81 1) 0.008/0.008 (U91 1) 0.008/0.008 (afterNth 1 2) 0.008/0.008 (fst 1) 0.008/0.008 (head 1) 0.008/0.008 (isLNat) 0.008/0.008 (isNatural) 0.008/0.008 (isPLNat) 0.008/0.008 (natsFrom 1) 0.008/0.008 (sel 1 2) 0.008/0.008 (snd 1) 0.008/0.008 (splitAt 1 2) 0.008/0.008 (tail 1) 0.008/0.008 (take 1 2) 0.008/0.008 (0) 0.008/0.008 (cons 1) 0.008/0.008 (fSNonEmpty) 0.008/0.008 (nil) 0.008/0.008 (pair 1 2) 0.008/0.008 (s 1) 0.008/0.008 (tt) 0.008/0.008 ) 0.008/0.008 (RULES 0.008/0.008 U101(tt,V2:S) -> U102(isLNat(V2:S)) 0.008/0.008 U102(tt) -> tt 0.008/0.008 U11(tt,N:S,XS:S) -> U12(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U111(tt) -> tt 0.008/0.008 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.008/0.008 U121(tt) -> tt 0.008/0.008 U131(tt,V2:S) -> U132(isLNat(V2:S)) 0.008/0.008 U132(tt) -> tt 0.008/0.008 U141(tt,V2:S) -> U142(isLNat(V2:S)) 0.008/0.008 U142(tt) -> tt 0.008/0.008 U151(tt,V2:S) -> U152(isLNat(V2:S)) 0.008/0.008 U152(tt) -> tt 0.008/0.008 U161(tt,N:S) -> cons(N:S,natsFrom(s(N:S))) 0.008/0.008 U171(tt,N:S,XS:S) -> U172(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U172(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.008/0.008 U181(tt,Y:S) -> U182(isLNat(Y:S),Y:S) 0.008/0.008 U182(tt,Y:S) -> Y:S 0.008/0.008 U191(tt,XS:S) -> pair(nil,XS:S) 0.008/0.008 U201(tt,N:S,X:S,XS:S) -> U202(isNatural(X:S),N:S,X:S,XS:S) 0.008/0.008 U202(tt,N:S,X:S,XS:S) -> U203(isLNat(XS:S),N:S,X:S,XS:S) 0.008/0.008 U203(tt,N:S,X:S,XS:S) -> U204(splitAt(N:S,XS:S),X:S) 0.008/0.008 U204(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.008/0.008 U21(tt,X:S,Y:S) -> U22(isLNat(Y:S),X:S) 0.008/0.008 U211(tt,XS:S) -> U212(isLNat(XS:S),XS:S) 0.008/0.008 U212(tt,XS:S) -> XS:S 0.008/0.008 U22(tt,X:S) -> X:S 0.008/0.008 U221(tt,N:S,XS:S) -> U222(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U222(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.008/0.008 U31(tt,N:S,XS:S) -> U32(isLNat(XS:S),N:S) 0.008/0.008 U32(tt,N:S) -> N:S 0.008/0.008 U41(tt,V2:S) -> U42(isLNat(V2:S)) 0.008/0.008 U42(tt) -> tt 0.008/0.008 U51(tt,V2:S) -> U52(isLNat(V2:S)) 0.008/0.008 U52(tt) -> tt 0.008/0.008 U61(tt) -> tt 0.008/0.008 U71(tt) -> tt 0.008/0.008 U81(tt) -> tt 0.008/0.008 U91(tt) -> tt 0.008/0.008 afterNth(N:S,XS:S) -> U11(isNatural(N:S),N:S,XS:S) 0.008/0.008 fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 isNatural(0) -> tt 0.008/0.008 isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 ) 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 0.008/0.008 0.008/0.008 Problem 1: 0.008/0.008 0.008/0.008 CleanTRS Processor: 0.008/0.008 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 Confluence Problem: 0.008/0.008 (VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S) 0.008/0.008 (STRATEGY CONTEXTSENSITIVE 0.008/0.008 (U101 1) 0.008/0.008 (U102 1) 0.008/0.008 (U11 1) 0.008/0.008 (U111 1) 0.008/0.008 (U12 1) 0.008/0.008 (U121 1) 0.008/0.008 (U131 1) 0.008/0.008 (U132 1) 0.008/0.008 (U141 1) 0.008/0.008 (U142 1) 0.008/0.008 (U151 1) 0.008/0.008 (U152 1) 0.008/0.008 (U161 1) 0.008/0.008 (U171 1) 0.008/0.008 (U172 1) 0.008/0.008 (U181 1) 0.008/0.008 (U182 1) 0.008/0.008 (U191 1) 0.008/0.008 (U201 1) 0.008/0.008 (U202 1) 0.008/0.008 (U203 1) 0.008/0.008 (U204 1) 0.008/0.008 (U21 1) 0.008/0.008 (U211 1) 0.008/0.008 (U212 1) 0.008/0.008 (U22 1) 0.008/0.008 (U221 1) 0.008/0.008 (U222 1) 0.008/0.008 (U31 1) 0.008/0.008 (U32 1) 0.008/0.008 (U41 1) 0.008/0.008 (U42 1) 0.008/0.008 (U51 1) 0.008/0.008 (U52 1) 0.008/0.008 (U61 1) 0.008/0.008 (U71 1) 0.008/0.008 (U81 1) 0.008/0.008 (U91 1) 0.008/0.008 (afterNth 1 2) 0.008/0.008 (fst 1) 0.008/0.008 (head 1) 0.008/0.008 (isLNat) 0.008/0.008 (isNatural) 0.008/0.008 (isPLNat) 0.008/0.008 (natsFrom 1) 0.008/0.008 (sel 1 2) 0.008/0.008 (snd 1) 0.008/0.008 (splitAt 1 2) 0.008/0.008 (tail 1) 0.008/0.008 (take 1 2) 0.008/0.008 (0) 0.008/0.008 (cons 1) 0.008/0.008 (fSNonEmpty) 0.008/0.008 (nil) 0.008/0.008 (pair 1 2) 0.008/0.008 (s 1) 0.008/0.008 (tt) 0.008/0.008 ) 0.008/0.008 (RULES 0.008/0.008 U101(tt,V2:S) -> U102(isLNat(V2:S)) 0.008/0.008 U102(tt) -> tt 0.008/0.008 U11(tt,N:S,XS:S) -> U12(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U111(tt) -> tt 0.008/0.008 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.008/0.008 U121(tt) -> tt 0.008/0.008 U131(tt,V2:S) -> U132(isLNat(V2:S)) 0.008/0.008 U132(tt) -> tt 0.008/0.008 U141(tt,V2:S) -> U142(isLNat(V2:S)) 0.008/0.008 U142(tt) -> tt 0.008/0.008 U151(tt,V2:S) -> U152(isLNat(V2:S)) 0.008/0.008 U152(tt) -> tt 0.008/0.008 U161(tt,N:S) -> cons(N:S,natsFrom(s(N:S))) 0.008/0.008 U171(tt,N:S,XS:S) -> U172(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U172(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.008/0.008 U181(tt,Y:S) -> U182(isLNat(Y:S),Y:S) 0.008/0.008 U182(tt,Y:S) -> Y:S 0.008/0.008 U191(tt,XS:S) -> pair(nil,XS:S) 0.008/0.008 U201(tt,N:S,X:S,XS:S) -> U202(isNatural(X:S),N:S,X:S,XS:S) 0.008/0.008 U202(tt,N:S,X:S,XS:S) -> U203(isLNat(XS:S),N:S,X:S,XS:S) 0.008/0.008 U203(tt,N:S,X:S,XS:S) -> U204(splitAt(N:S,XS:S),X:S) 0.008/0.008 U204(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.008/0.008 U21(tt,X:S,Y:S) -> U22(isLNat(Y:S),X:S) 0.008/0.008 U211(tt,XS:S) -> U212(isLNat(XS:S),XS:S) 0.008/0.008 U212(tt,XS:S) -> XS:S 0.008/0.008 U22(tt,X:S) -> X:S 0.008/0.008 U221(tt,N:S,XS:S) -> U222(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U222(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.008/0.008 U31(tt,N:S,XS:S) -> U32(isLNat(XS:S),N:S) 0.008/0.008 U32(tt,N:S) -> N:S 0.008/0.008 U41(tt,V2:S) -> U42(isLNat(V2:S)) 0.008/0.008 U42(tt) -> tt 0.008/0.008 U51(tt,V2:S) -> U52(isLNat(V2:S)) 0.008/0.008 U52(tt) -> tt 0.008/0.008 U61(tt) -> tt 0.008/0.008 U71(tt) -> tt 0.008/0.008 U81(tt) -> tt 0.008/0.008 U91(tt) -> tt 0.008/0.008 afterNth(N:S,XS:S) -> U11(isNatural(N:S),N:S,XS:S) 0.008/0.008 fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 isNatural(0) -> tt 0.008/0.008 isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 ) 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 0.008/0.008 0.008/0.008 Problem 1: 0.008/0.008 0.008/0.008 Modular Confluence Combinations Decomposition Processor: 0.008/0.008 It is a CTRS -> No modular confluence 0.008/0.008 0.008/0.008 Problem 1: 0.008/0.008 CS-TRS Processor: 0.008/0.008 R is a CS-TRS 0.008/0.008 0.008/0.008 Problem 1: 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 Confluence Problem: 0.008/0.008 (VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S) 0.008/0.008 (STRATEGY CONTEXTSENSITIVE 0.008/0.008 (U101 1) 0.008/0.008 (U102 1) 0.008/0.008 (U11 1) 0.008/0.008 (U111 1) 0.008/0.008 (U12 1) 0.008/0.008 (U121 1) 0.008/0.008 (U131 1) 0.008/0.008 (U132 1) 0.008/0.008 (U141 1) 0.008/0.008 (U142 1) 0.008/0.008 (U151 1) 0.008/0.008 (U152 1) 0.008/0.008 (U161 1) 0.008/0.008 (U171 1) 0.008/0.008 (U172 1) 0.008/0.008 (U181 1) 0.008/0.008 (U182 1) 0.008/0.008 (U191 1) 0.008/0.008 (U201 1) 0.008/0.008 (U202 1) 0.008/0.008 (U203 1) 0.008/0.008 (U204 1) 0.008/0.008 (U21 1) 0.008/0.008 (U211 1) 0.008/0.008 (U212 1) 0.008/0.008 (U22 1) 0.008/0.008 (U221 1) 0.008/0.008 (U222 1) 0.008/0.008 (U31 1) 0.008/0.008 (U32 1) 0.008/0.008 (U41 1) 0.008/0.008 (U42 1) 0.008/0.008 (U51 1) 0.008/0.008 (U52 1) 0.008/0.008 (U61 1) 0.008/0.008 (U71 1) 0.008/0.008 (U81 1) 0.008/0.008 (U91 1) 0.008/0.008 (afterNth 1 2) 0.008/0.008 (fst 1) 0.008/0.008 (head 1) 0.008/0.008 (isLNat) 0.008/0.008 (isNatural) 0.008/0.008 (isPLNat) 0.008/0.008 (natsFrom 1) 0.008/0.008 (sel 1 2) 0.008/0.008 (snd 1) 0.008/0.008 (splitAt 1 2) 0.008/0.008 (tail 1) 0.008/0.008 (take 1 2) 0.008/0.008 (0) 0.008/0.008 (cons 1) 0.008/0.008 (fSNonEmpty) 0.008/0.008 (nil) 0.008/0.008 (pair 1 2) 0.008/0.008 (s 1) 0.008/0.008 (tt) 0.008/0.008 ) 0.008/0.008 (RULES 0.008/0.008 U101(tt,V2:S) -> U102(isLNat(V2:S)) 0.008/0.008 U102(tt) -> tt 0.008/0.008 U11(tt,N:S,XS:S) -> U12(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U111(tt) -> tt 0.008/0.008 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.008/0.008 U121(tt) -> tt 0.008/0.008 U131(tt,V2:S) -> U132(isLNat(V2:S)) 0.008/0.008 U132(tt) -> tt 0.008/0.008 U141(tt,V2:S) -> U142(isLNat(V2:S)) 0.008/0.008 U142(tt) -> tt 0.008/0.008 U151(tt,V2:S) -> U152(isLNat(V2:S)) 0.008/0.008 U152(tt) -> tt 0.008/0.008 U161(tt,N:S) -> cons(N:S,natsFrom(s(N:S))) 0.008/0.008 U171(tt,N:S,XS:S) -> U172(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U172(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.008/0.008 U181(tt,Y:S) -> U182(isLNat(Y:S),Y:S) 0.008/0.008 U182(tt,Y:S) -> Y:S 0.008/0.008 U191(tt,XS:S) -> pair(nil,XS:S) 0.008/0.008 U201(tt,N:S,X:S,XS:S) -> U202(isNatural(X:S),N:S,X:S,XS:S) 0.008/0.008 U202(tt,N:S,X:S,XS:S) -> U203(isLNat(XS:S),N:S,X:S,XS:S) 0.008/0.008 U203(tt,N:S,X:S,XS:S) -> U204(splitAt(N:S,XS:S),X:S) 0.008/0.008 U204(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.008/0.008 U21(tt,X:S,Y:S) -> U22(isLNat(Y:S),X:S) 0.008/0.008 U211(tt,XS:S) -> U212(isLNat(XS:S),XS:S) 0.008/0.008 U212(tt,XS:S) -> XS:S 0.008/0.008 U22(tt,X:S) -> X:S 0.008/0.008 U221(tt,N:S,XS:S) -> U222(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U222(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.008/0.008 U31(tt,N:S,XS:S) -> U32(isLNat(XS:S),N:S) 0.008/0.008 U32(tt,N:S) -> N:S 0.008/0.008 U41(tt,V2:S) -> U42(isLNat(V2:S)) 0.008/0.008 U42(tt) -> tt 0.008/0.008 U51(tt,V2:S) -> U52(isLNat(V2:S)) 0.008/0.008 U52(tt) -> tt 0.008/0.008 U61(tt) -> tt 0.008/0.008 U71(tt) -> tt 0.008/0.008 U81(tt) -> tt 0.008/0.008 U91(tt) -> tt 0.008/0.008 afterNth(N:S,XS:S) -> U11(isNatural(N:S),N:S,XS:S) 0.008/0.008 fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 isNatural(0) -> tt 0.008/0.008 isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 ) 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 0.008/0.008 Extended u-Critical Pairs NonLHRV Processor [JLAMP21]: 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 22 (l' :-> r') => U204(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U204(pair(YS:S,ZS:S),X:S)} 0.008/0.008 s => pair(cons(x34:S,U204(pair(YS:S,ZS:S),X:S)),x36:S) 0.008/0.008 t => U204(pair(pair(cons(X:S,YS:S),ZS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 23 (l' :-> r') => U21(tt,X:S,Y:S) -> U22(isLNat(Y:S),X:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U21(tt,X:S,Y:S)} 0.008/0.008 s => pair(cons(x34:S,U21(tt,X:S,Y:S)),x36:S) 0.008/0.008 t => U204(pair(U22(isLNat(Y:S),X:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 24 (l' :-> r') => U211(tt,XS:S) -> U212(isLNat(XS:S),XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U211(tt,XS:S)} 0.008/0.008 s => pair(cons(x34:S,U211(tt,XS:S)),x36:S) 0.008/0.008 t => U204(pair(U212(isLNat(XS:S),XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 25 (l' :-> r') => U212(tt,XS:S) -> XS:S 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U212(tt,XS:S)} 0.008/0.008 s => pair(cons(x34:S,U212(tt,XS:S)),x36:S) 0.008/0.008 t => U204(pair(XS:S,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 26 (l' :-> r') => U22(tt,X:S) -> X:S 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U22(tt,X:S)} 0.008/0.008 s => pair(cons(x34:S,U22(tt,X:S)),x36:S) 0.008/0.008 t => U204(pair(X:S,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 27 (l' :-> r') => U221(tt,N:S,XS:S) -> U222(isLNat(XS:S),N:S,XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U221(tt,N:S,XS:S)} 0.008/0.008 s => pair(cons(x34:S,U221(tt,N:S,XS:S)),x36:S) 0.008/0.008 t => U204(pair(U222(isLNat(XS:S),N:S,XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 28 (l' :-> r') => U222(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U222(tt,N:S,XS:S)} 0.008/0.008 s => pair(cons(x34:S,U222(tt,N:S,XS:S)),x36:S) 0.008/0.008 t => U204(pair(fst(splitAt(N:S,XS:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 29 (l' :-> r') => U31(tt,N:S,XS:S) -> U32(isLNat(XS:S),N:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U31(tt,N:S,XS:S)} 0.008/0.008 s => pair(cons(x34:S,U31(tt,N:S,XS:S)),x36:S) 0.008/0.008 t => U204(pair(U32(isLNat(XS:S),N:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 30 (l' :-> r') => U32(tt,N:S) -> N:S 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U32(tt,N:S)} 0.008/0.008 s => pair(cons(x34:S,U32(tt,N:S)),x36:S) 0.008/0.008 t => U204(pair(N:S,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 31 (l' :-> r') => U41(tt,V2:S) -> U42(isLNat(V2:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U41(tt,V2:S)} 0.008/0.008 s => pair(cons(x34:S,U41(tt,V2:S)),x36:S) 0.008/0.008 t => U204(pair(U42(isLNat(V2:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 32 (l' :-> r') => U42(tt) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U42(tt)} 0.008/0.008 s => pair(cons(x34:S,U42(tt)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 33 (l' :-> r') => U51(tt,V2:S) -> U52(isLNat(V2:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U51(tt,V2:S)} 0.008/0.008 s => pair(cons(x34:S,U51(tt,V2:S)),x36:S) 0.008/0.008 t => U204(pair(U52(isLNat(V2:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 34 (l' :-> r') => U52(tt) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U52(tt)} 0.008/0.008 s => pair(cons(x34:S,U52(tt)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 35 (l' :-> r') => U61(tt) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U61(tt)} 0.008/0.008 s => pair(cons(x34:S,U61(tt)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 36 (l' :-> r') => U71(tt) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U71(tt)} 0.008/0.008 s => pair(cons(x34:S,U71(tt)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 37 (l' :-> r') => U81(tt) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U81(tt)} 0.008/0.008 s => pair(cons(x34:S,U81(tt)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 38 (l' :-> r') => U91(tt) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> U91(tt)} 0.008/0.008 s => pair(cons(x34:S,U91(tt)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 39 (l' :-> r') => afterNth(N:S,XS:S) -> U11(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> afterNth(N:S,XS:S)} 0.008/0.008 s => pair(cons(x34:S,afterNth(N:S,XS:S)),x36:S) 0.008/0.008 t => U204(pair(U11(isNatural(N:S),N:S,XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 40 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> fst(pair(X:S,Y:S))} 0.008/0.008 s => pair(cons(x34:S,fst(pair(X:S,Y:S))),x36:S) 0.008/0.008 t => U204(pair(U21(isLNat(X:S),X:S,Y:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 41 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> head(cons(N:S,XS:S))} 0.008/0.008 s => pair(cons(x34:S,head(cons(N:S,XS:S))),x36:S) 0.008/0.008 t => U204(pair(U31(isNatural(N:S),N:S,XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 42 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(afterNth(V1:S,V2:S))} 0.008/0.008 s => pair(cons(x34:S,isLNat(afterNth(V1:S,V2:S))),x36:S) 0.008/0.008 t => U204(pair(U41(isNatural(V1:S),V2:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 43 (l' :-> r') => isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(fst(V1:S))} 0.008/0.008 s => pair(cons(x34:S,isLNat(fst(V1:S))),x36:S) 0.008/0.008 t => U204(pair(U61(isPLNat(V1:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 44 (l' :-> r') => isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(natsFrom(V1:S))} 0.008/0.008 s => pair(cons(x34:S,isLNat(natsFrom(V1:S))),x36:S) 0.008/0.008 t => U204(pair(U71(isNatural(V1:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 45 (l' :-> r') => isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(snd(V1:S))} 0.008/0.008 s => pair(cons(x34:S,isLNat(snd(V1:S))),x36:S) 0.008/0.008 t => U204(pair(U81(isPLNat(V1:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 46 (l' :-> r') => isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(tail(V1:S))} 0.008/0.008 s => pair(cons(x34:S,isLNat(tail(V1:S))),x36:S) 0.008/0.008 t => U204(pair(U91(isLNat(V1:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 47 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(take(V1:S,V2:S))} 0.008/0.008 s => pair(cons(x34:S,isLNat(take(V1:S,V2:S))),x36:S) 0.008/0.008 t => U204(pair(U101(isNatural(V1:S),V2:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 48 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(cons(V1:S,V2:S))} 0.008/0.008 s => pair(cons(x34:S,isLNat(cons(V1:S,V2:S))),x36:S) 0.008/0.008 t => U204(pair(U51(isNatural(V1:S),V2:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 49 (l' :-> r') => isLNat(nil) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isLNat(nil)} 0.008/0.008 s => pair(cons(x34:S,isLNat(nil)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 50 (l' :-> r') => isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isNatural(head(V1:S))} 0.008/0.008 s => pair(cons(x34:S,isNatural(head(V1:S))),x36:S) 0.008/0.008 t => U204(pair(U111(isLNat(V1:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 51 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isNatural(sel(V1:S,V2:S))} 0.008/0.008 s => pair(cons(x34:S,isNatural(sel(V1:S,V2:S))),x36:S) 0.008/0.008 t => U204(pair(U131(isNatural(V1:S),V2:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 52 (l' :-> r') => isNatural(0) -> tt 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isNatural(0)} 0.008/0.008 s => pair(cons(x34:S,isNatural(0)),x36:S) 0.008/0.008 t => U204(pair(tt,x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 53 (l' :-> r') => isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isNatural(s(V1:S))} 0.008/0.008 s => pair(cons(x34:S,isNatural(s(V1:S))),x36:S) 0.008/0.008 t => U204(pair(U121(isNatural(V1:S)),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 54 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isPLNat(splitAt(V1:S,V2:S))} 0.008/0.008 s => pair(cons(x34:S,isPLNat(splitAt(V1:S,V2:S))),x36:S) 0.008/0.008 t => U204(pair(U151(isNatural(V1:S),V2:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 55 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> isPLNat(pair(V1:S,V2:S))} 0.008/0.008 s => pair(cons(x34:S,isPLNat(pair(V1:S,V2:S))),x36:S) 0.008/0.008 t => U204(pair(U141(isLNat(V1:S),V2:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 56 (l' :-> r') => natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> natsFrom(N:S)} 0.008/0.008 s => pair(cons(x34:S,natsFrom(N:S)),x36:S) 0.008/0.008 t => U204(pair(U161(isNatural(N:S),N:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 57 (l' :-> r') => sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> sel(N:S,XS:S)} 0.008/0.008 s => pair(cons(x34:S,sel(N:S,XS:S)),x36:S) 0.008/0.008 t => U204(pair(U171(isNatural(N:S),N:S,XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 58 (l' :-> r') => snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> snd(pair(X:S,Y:S))} 0.008/0.008 s => pair(cons(x34:S,snd(pair(X:S,Y:S))),x36:S) 0.008/0.008 t => U204(pair(U181(isLNat(X:S),Y:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> splitAt(0,XS:S)} 0.008/0.008 s => pair(cons(x34:S,splitAt(0,XS:S)),x36:S) 0.008/0.008 t => U204(pair(U191(isLNat(XS:S),XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => pair(cons(x34:S,splitAt(s(N:S),cons(X:S,XS:S))),x36:S) 0.008/0.008 t => U204(pair(U201(isNatural(N:S),N:S,X:S,XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => pair(cons(x34:S,tail(cons(N:S,XS:S))),x36:S) 0.008/0.008 t => U204(pair(U211(isNatural(N:S),XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x35:S 0.008/0.008 Pos x35:S in l => [1,1] 0.008/0.008 Sigma => {x35:S -> take(N:S,XS:S)} 0.008/0.008 s => pair(cons(x34:S,take(N:S,XS:S)),x36:S) 0.008/0.008 t => U204(pair(U221(isNatural(N:S),N:S,XS:S),x36:S),x34:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 39 (l' :-> r') => afterNth(N:S,XS:S) -> U11(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> afterNth(N:S,XS:S)} 0.008/0.008 s => U11(isNatural(afterNth(N:S,XS:S)),afterNth(N:S,XS:S),x52:S) 0.008/0.008 t => afterNth(U11(isNatural(N:S),N:S,XS:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 40 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> fst(pair(X:S,Y:S))} 0.008/0.008 s => U11(isNatural(fst(pair(X:S,Y:S))),fst(pair(X:S,Y:S)),x52:S) 0.008/0.008 t => afterNth(U21(isLNat(X:S),X:S,Y:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 41 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> head(cons(N:S,XS:S))} 0.008/0.008 s => U11(isNatural(head(cons(N:S,XS:S))),head(cons(N:S,XS:S)),x52:S) 0.008/0.008 t => afterNth(U31(isNatural(N:S),N:S,XS:S),x52:S) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 42 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(afterNth(V1:S,V2:S))} 0.008/0.008 s => U11(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(afterNth(V1:S,V2:S)),x52:S) 0.008/0.008 t => afterNth(U41(isNatural(V1:S),V2:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 43 (l' :-> r') => isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(fst(V1:S))} 0.008/0.008 s => U11(isNatural(isLNat(fst(V1:S))),isLNat(fst(V1:S)),x52:S) 0.008/0.008 t => afterNth(U61(isPLNat(V1:S)),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 44 (l' :-> r') => isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(natsFrom(V1:S))} 0.008/0.008 s => U11(isNatural(isLNat(natsFrom(V1:S))),isLNat(natsFrom(V1:S)),x52:S) 0.008/0.008 t => afterNth(U71(isNatural(V1:S)),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 45 (l' :-> r') => isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(snd(V1:S))} 0.008/0.008 s => U11(isNatural(isLNat(snd(V1:S))),isLNat(snd(V1:S)),x52:S) 0.008/0.008 t => afterNth(U81(isPLNat(V1:S)),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 46 (l' :-> r') => isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(tail(V1:S))} 0.008/0.008 s => U11(isNatural(isLNat(tail(V1:S))),isLNat(tail(V1:S)),x52:S) 0.008/0.008 t => afterNth(U91(isLNat(V1:S)),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 47 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(take(V1:S,V2:S))} 0.008/0.008 s => U11(isNatural(isLNat(take(V1:S,V2:S))),isLNat(take(V1:S,V2:S)),x52:S) 0.008/0.008 t => afterNth(U101(isNatural(V1:S),V2:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 48 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(cons(V1:S,V2:S))} 0.008/0.008 s => U11(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(cons(V1:S,V2:S)),x52:S) 0.008/0.008 t => afterNth(U51(isNatural(V1:S),V2:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 49 (l' :-> r') => isLNat(nil) -> tt 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isLNat(nil)} 0.008/0.008 s => U11(isNatural(isLNat(nil)),isLNat(nil),x52:S) 0.008/0.008 t => afterNth(tt,x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 50 (l' :-> r') => isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isNatural(head(V1:S))} 0.008/0.008 s => U11(isNatural(isNatural(head(V1:S))),isNatural(head(V1:S)),x52:S) 0.008/0.008 t => afterNth(U111(isLNat(V1:S)),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 51 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isNatural(sel(V1:S,V2:S))} 0.008/0.008 s => U11(isNatural(isNatural(sel(V1:S,V2:S))),isNatural(sel(V1:S,V2:S)),x52:S) 0.008/0.008 t => afterNth(U131(isNatural(V1:S),V2:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 52 (l' :-> r') => isNatural(0) -> tt 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isNatural(0)} 0.008/0.008 s => U11(isNatural(isNatural(0)),isNatural(0),x52:S) 0.008/0.008 t => afterNth(tt,x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 53 (l' :-> r') => isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isNatural(s(V1:S))} 0.008/0.008 s => U11(isNatural(isNatural(s(V1:S))),isNatural(s(V1:S)),x52:S) 0.008/0.008 t => afterNth(U121(isNatural(V1:S)),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 54 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isPLNat(splitAt(V1:S,V2:S))} 0.008/0.008 s => U11(isNatural(isPLNat(splitAt(V1:S,V2:S))),isPLNat(splitAt(V1:S,V2:S)),x52:S) 0.008/0.008 t => afterNth(U151(isNatural(V1:S),V2:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 55 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> isPLNat(pair(V1:S,V2:S))} 0.008/0.008 s => U11(isNatural(isPLNat(pair(V1:S,V2:S))),isPLNat(pair(V1:S,V2:S)),x52:S) 0.008/0.008 t => afterNth(U141(isLNat(V1:S),V2:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 56 (l' :-> r') => natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> natsFrom(N:S)} 0.008/0.008 s => U11(isNatural(natsFrom(N:S)),natsFrom(N:S),x52:S) 0.008/0.008 t => afterNth(U161(isNatural(N:S),N:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 57 (l' :-> r') => sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> sel(N:S,XS:S)} 0.008/0.008 s => U11(isNatural(sel(N:S,XS:S)),sel(N:S,XS:S),x52:S) 0.008/0.008 t => afterNth(U171(isNatural(N:S),N:S,XS:S),x52:S) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 58 (l' :-> r') => snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> snd(pair(X:S,Y:S))} 0.008/0.008 s => U11(isNatural(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S)),x52:S) 0.008/0.008 t => afterNth(U181(isLNat(X:S),Y:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> splitAt(0,XS:S)} 0.008/0.008 s => U11(isNatural(splitAt(0,XS:S)),splitAt(0,XS:S),x52:S) 0.008/0.008 t => afterNth(U191(isLNat(XS:S),XS:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U11(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S)),x52:S) 0.008/0.008 t => afterNth(U201(isNatural(N:S),N:S,X:S,XS:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U11(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)),x52:S) 0.008/0.008 t => afterNth(U211(isNatural(N:S),XS:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x51:S 0.008/0.008 Pos x51:S in l => [1] 0.008/0.008 Sigma => {x51:S -> take(N:S,XS:S)} 0.008/0.008 s => U11(isNatural(take(N:S,XS:S)),take(N:S,XS:S),x52:S) 0.008/0.008 t => afterNth(U221(isNatural(N:S),N:S,XS:S),x52:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 40 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> fst(pair(X:S,Y:S))} 0.008/0.008 s => U21(isLNat(fst(pair(X:S,Y:S))),fst(pair(X:S,Y:S)),x54:S) 0.008/0.008 t => fst(pair(U21(isLNat(X:S),X:S,Y:S),x54:S)) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 41 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> head(cons(N:S,XS:S))} 0.008/0.008 s => U21(isLNat(head(cons(N:S,XS:S))),head(cons(N:S,XS:S)),x54:S) 0.008/0.008 t => fst(pair(U31(isNatural(N:S),N:S,XS:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 42 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(afterNth(V1:S,V2:S))} 0.008/0.008 s => U21(isLNat(isLNat(afterNth(V1:S,V2:S))),isLNat(afterNth(V1:S,V2:S)),x54:S) 0.008/0.008 t => fst(pair(U41(isNatural(V1:S),V2:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 43 (l' :-> r') => isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(fst(V1:S))} 0.008/0.008 s => U21(isLNat(isLNat(fst(V1:S))),isLNat(fst(V1:S)),x54:S) 0.008/0.008 t => fst(pair(U61(isPLNat(V1:S)),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 44 (l' :-> r') => isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(natsFrom(V1:S))} 0.008/0.008 s => U21(isLNat(isLNat(natsFrom(V1:S))),isLNat(natsFrom(V1:S)),x54:S) 0.008/0.008 t => fst(pair(U71(isNatural(V1:S)),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 45 (l' :-> r') => isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(snd(V1:S))} 0.008/0.008 s => U21(isLNat(isLNat(snd(V1:S))),isLNat(snd(V1:S)),x54:S) 0.008/0.008 t => fst(pair(U81(isPLNat(V1:S)),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 46 (l' :-> r') => isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(tail(V1:S))} 0.008/0.008 s => U21(isLNat(isLNat(tail(V1:S))),isLNat(tail(V1:S)),x54:S) 0.008/0.008 t => fst(pair(U91(isLNat(V1:S)),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 47 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(take(V1:S,V2:S))} 0.008/0.008 s => U21(isLNat(isLNat(take(V1:S,V2:S))),isLNat(take(V1:S,V2:S)),x54:S) 0.008/0.008 t => fst(pair(U101(isNatural(V1:S),V2:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 48 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(cons(V1:S,V2:S))} 0.008/0.008 s => U21(isLNat(isLNat(cons(V1:S,V2:S))),isLNat(cons(V1:S,V2:S)),x54:S) 0.008/0.008 t => fst(pair(U51(isNatural(V1:S),V2:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 49 (l' :-> r') => isLNat(nil) -> tt 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isLNat(nil)} 0.008/0.008 s => U21(isLNat(isLNat(nil)),isLNat(nil),x54:S) 0.008/0.008 t => fst(pair(tt,x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 50 (l' :-> r') => isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isNatural(head(V1:S))} 0.008/0.008 s => U21(isLNat(isNatural(head(V1:S))),isNatural(head(V1:S)),x54:S) 0.008/0.008 t => fst(pair(U111(isLNat(V1:S)),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 51 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isNatural(sel(V1:S,V2:S))} 0.008/0.008 s => U21(isLNat(isNatural(sel(V1:S,V2:S))),isNatural(sel(V1:S,V2:S)),x54:S) 0.008/0.008 t => fst(pair(U131(isNatural(V1:S),V2:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 52 (l' :-> r') => isNatural(0) -> tt 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isNatural(0)} 0.008/0.008 s => U21(isLNat(isNatural(0)),isNatural(0),x54:S) 0.008/0.008 t => fst(pair(tt,x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 53 (l' :-> r') => isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isNatural(s(V1:S))} 0.008/0.008 s => U21(isLNat(isNatural(s(V1:S))),isNatural(s(V1:S)),x54:S) 0.008/0.008 t => fst(pair(U121(isNatural(V1:S)),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 54 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isPLNat(splitAt(V1:S,V2:S))} 0.008/0.008 s => U21(isLNat(isPLNat(splitAt(V1:S,V2:S))),isPLNat(splitAt(V1:S,V2:S)),x54:S) 0.008/0.008 t => fst(pair(U151(isNatural(V1:S),V2:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 55 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> isPLNat(pair(V1:S,V2:S))} 0.008/0.008 s => U21(isLNat(isPLNat(pair(V1:S,V2:S))),isPLNat(pair(V1:S,V2:S)),x54:S) 0.008/0.008 t => fst(pair(U141(isLNat(V1:S),V2:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 56 (l' :-> r') => natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> natsFrom(N:S)} 0.008/0.008 s => U21(isLNat(natsFrom(N:S)),natsFrom(N:S),x54:S) 0.008/0.008 t => fst(pair(U161(isNatural(N:S),N:S),x54:S)) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 57 (l' :-> r') => sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> sel(N:S,XS:S)} 0.008/0.008 s => U21(isLNat(sel(N:S,XS:S)),sel(N:S,XS:S),x54:S) 0.008/0.008 t => fst(pair(U171(isNatural(N:S),N:S,XS:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 58 (l' :-> r') => snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> snd(pair(X:S,Y:S))} 0.008/0.008 s => U21(isLNat(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S)),x54:S) 0.008/0.008 t => fst(pair(U181(isLNat(X:S),Y:S),x54:S)) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> splitAt(0,XS:S)} 0.008/0.008 s => U21(isLNat(splitAt(0,XS:S)),splitAt(0,XS:S),x54:S) 0.008/0.008 t => fst(pair(U191(isLNat(XS:S),XS:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U21(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S)),x54:S) 0.008/0.008 t => fst(pair(U201(isNatural(N:S),N:S,X:S,XS:S),x54:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U21(isLNat(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)),x54:S) 0.008/0.008 t => fst(pair(U211(isNatural(N:S),XS:S),x54:S)) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x53:S 0.008/0.008 Pos x53:S in l => [1,1] 0.008/0.008 Sigma => {x53:S -> take(N:S,XS:S)} 0.008/0.008 s => U21(isLNat(take(N:S,XS:S)),take(N:S,XS:S),x54:S) 0.008/0.008 t => fst(pair(U221(isNatural(N:S),N:S,XS:S),x54:S)) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 41 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> head(cons(N:S,XS:S))} 0.008/0.008 s => U31(isNatural(head(cons(N:S,XS:S))),head(cons(N:S,XS:S)),x56:S) 0.008/0.008 t => head(cons(U31(isNatural(N:S),N:S,XS:S),x56:S)) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 42 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(afterNth(V1:S,V2:S))} 0.008/0.008 s => U31(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(afterNth(V1:S,V2:S)),x56:S) 0.008/0.008 t => head(cons(U41(isNatural(V1:S),V2:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 43 (l' :-> r') => isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(fst(V1:S))} 0.008/0.008 s => U31(isNatural(isLNat(fst(V1:S))),isLNat(fst(V1:S)),x56:S) 0.008/0.008 t => head(cons(U61(isPLNat(V1:S)),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 44 (l' :-> r') => isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(natsFrom(V1:S))} 0.008/0.008 s => U31(isNatural(isLNat(natsFrom(V1:S))),isLNat(natsFrom(V1:S)),x56:S) 0.008/0.008 t => head(cons(U71(isNatural(V1:S)),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 45 (l' :-> r') => isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(snd(V1:S))} 0.008/0.008 s => U31(isNatural(isLNat(snd(V1:S))),isLNat(snd(V1:S)),x56:S) 0.008/0.008 t => head(cons(U81(isPLNat(V1:S)),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 46 (l' :-> r') => isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(tail(V1:S))} 0.008/0.008 s => U31(isNatural(isLNat(tail(V1:S))),isLNat(tail(V1:S)),x56:S) 0.008/0.008 t => head(cons(U91(isLNat(V1:S)),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 47 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(take(V1:S,V2:S))} 0.008/0.008 s => U31(isNatural(isLNat(take(V1:S,V2:S))),isLNat(take(V1:S,V2:S)),x56:S) 0.008/0.008 t => head(cons(U101(isNatural(V1:S),V2:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 48 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(cons(V1:S,V2:S))} 0.008/0.008 s => U31(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(cons(V1:S,V2:S)),x56:S) 0.008/0.008 t => head(cons(U51(isNatural(V1:S),V2:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 49 (l' :-> r') => isLNat(nil) -> tt 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isLNat(nil)} 0.008/0.008 s => U31(isNatural(isLNat(nil)),isLNat(nil),x56:S) 0.008/0.008 t => head(cons(tt,x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 50 (l' :-> r') => isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isNatural(head(V1:S))} 0.008/0.008 s => U31(isNatural(isNatural(head(V1:S))),isNatural(head(V1:S)),x56:S) 0.008/0.008 t => head(cons(U111(isLNat(V1:S)),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 51 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isNatural(sel(V1:S,V2:S))} 0.008/0.008 s => U31(isNatural(isNatural(sel(V1:S,V2:S))),isNatural(sel(V1:S,V2:S)),x56:S) 0.008/0.008 t => head(cons(U131(isNatural(V1:S),V2:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 52 (l' :-> r') => isNatural(0) -> tt 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isNatural(0)} 0.008/0.008 s => U31(isNatural(isNatural(0)),isNatural(0),x56:S) 0.008/0.008 t => head(cons(tt,x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 53 (l' :-> r') => isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isNatural(s(V1:S))} 0.008/0.008 s => U31(isNatural(isNatural(s(V1:S))),isNatural(s(V1:S)),x56:S) 0.008/0.008 t => head(cons(U121(isNatural(V1:S)),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 54 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isPLNat(splitAt(V1:S,V2:S))} 0.008/0.008 s => U31(isNatural(isPLNat(splitAt(V1:S,V2:S))),isPLNat(splitAt(V1:S,V2:S)),x56:S) 0.008/0.008 t => head(cons(U151(isNatural(V1:S),V2:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 55 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> isPLNat(pair(V1:S,V2:S))} 0.008/0.008 s => U31(isNatural(isPLNat(pair(V1:S,V2:S))),isPLNat(pair(V1:S,V2:S)),x56:S) 0.008/0.008 t => head(cons(U141(isLNat(V1:S),V2:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 56 (l' :-> r') => natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> natsFrom(N:S)} 0.008/0.008 s => U31(isNatural(natsFrom(N:S)),natsFrom(N:S),x56:S) 0.008/0.008 t => head(cons(U161(isNatural(N:S),N:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 57 (l' :-> r') => sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> sel(N:S,XS:S)} 0.008/0.008 s => U31(isNatural(sel(N:S,XS:S)),sel(N:S,XS:S),x56:S) 0.008/0.008 t => head(cons(U171(isNatural(N:S),N:S,XS:S),x56:S)) 0.008/0.008 NW => 0 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 58 (l' :-> r') => snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> snd(pair(X:S,Y:S))} 0.008/0.008 s => U31(isNatural(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S)),x56:S) 0.008/0.008 t => head(cons(U181(isLNat(X:S),Y:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> splitAt(0,XS:S)} 0.008/0.008 s => U31(isNatural(splitAt(0,XS:S)),splitAt(0,XS:S),x56:S) 0.008/0.008 t => head(cons(U191(isLNat(XS:S),XS:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U31(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S)),x56:S) 0.008/0.008 t => head(cons(U201(isNatural(N:S),N:S,X:S,XS:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U31(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)),x56:S) 0.008/0.008 t => head(cons(U211(isNatural(N:S),XS:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x55:S 0.008/0.008 Pos x55:S in l => [1,1] 0.008/0.008 Sigma => {x55:S -> take(N:S,XS:S)} 0.008/0.008 s => U31(isNatural(take(N:S,XS:S)),take(N:S,XS:S),x56:S) 0.008/0.008 t => head(cons(U221(isNatural(N:S),N:S,XS:S),x56:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S) 0.008/0.008 Rule 56 (l' :-> r') => natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 Var => x75:S 0.008/0.008 Pos x75:S in l => [1] 0.008/0.008 Sigma => {x75:S -> natsFrom(N:S)} 0.008/0.008 s => U161(isNatural(natsFrom(N:S)),natsFrom(N:S)) 0.008/0.008 t => natsFrom(U161(isNatural(N:S),N:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S) 0.008/0.008 Rule 57 (l' :-> r') => sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x75:S 0.008/0.008 Pos x75:S in l => [1] 0.008/0.008 Sigma => {x75:S -> sel(N:S,XS:S)} 0.008/0.008 s => U161(isNatural(sel(N:S,XS:S)),sel(N:S,XS:S)) 0.008/0.008 t => natsFrom(U171(isNatural(N:S),N:S,XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S) 0.008/0.008 Rule 58 (l' :-> r') => snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 Var => x75:S 0.008/0.008 Pos x75:S in l => [1] 0.008/0.008 Sigma => {x75:S -> snd(pair(X:S,Y:S))} 0.008/0.008 s => U161(isNatural(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S))) 0.008/0.008 t => natsFrom(U181(isLNat(X:S),Y:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x75:S 0.008/0.008 Pos x75:S in l => [1] 0.008/0.008 Sigma => {x75:S -> splitAt(0,XS:S)} 0.008/0.008 s => U161(isNatural(splitAt(0,XS:S)),splitAt(0,XS:S)) 0.008/0.008 t => natsFrom(U191(isLNat(XS:S),XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x75:S 0.008/0.008 Pos x75:S in l => [1] 0.008/0.008 Sigma => {x75:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U161(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S))) 0.008/0.008 t => natsFrom(U201(isNatural(N:S),N:S,X:S,XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x75:S 0.008/0.008 Pos x75:S in l => [1] 0.008/0.008 Sigma => {x75:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U161(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))) 0.008/0.008 t => natsFrom(U211(isNatural(N:S),XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x75:S 0.008/0.008 Pos x75:S in l => [1] 0.008/0.008 Sigma => {x75:S -> take(N:S,XS:S)} 0.008/0.008 s => U161(isNatural(take(N:S,XS:S)),take(N:S,XS:S)) 0.008/0.008 t => natsFrom(U221(isNatural(N:S),N:S,XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => sel(x76:S,x77:S) -> U171(isNatural(x76:S),x76:S,x77:S) 0.008/0.008 Rule 57 (l' :-> r') => sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x76:S 0.008/0.008 Pos x76:S in l => [1] 0.008/0.008 Sigma => {x76:S -> sel(N:S,XS:S)} 0.008/0.008 s => U171(isNatural(sel(N:S,XS:S)),sel(N:S,XS:S),x77:S) 0.008/0.008 t => sel(U171(isNatural(N:S),N:S,XS:S),x77:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => sel(x76:S,x77:S) -> U171(isNatural(x76:S),x76:S,x77:S) 0.008/0.008 Rule 58 (l' :-> r') => snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 Var => x76:S 0.008/0.008 Pos x76:S in l => [1] 0.008/0.008 Sigma => {x76:S -> snd(pair(X:S,Y:S))} 0.008/0.008 s => U171(isNatural(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S)),x77:S) 0.008/0.008 t => sel(U181(isLNat(X:S),Y:S),x77:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => sel(x76:S,x77:S) -> U171(isNatural(x76:S),x76:S,x77:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x76:S 0.008/0.008 Pos x76:S in l => [1] 0.008/0.008 Sigma => {x76:S -> splitAt(0,XS:S)} 0.008/0.008 s => U171(isNatural(splitAt(0,XS:S)),splitAt(0,XS:S),x77:S) 0.008/0.008 t => sel(U191(isLNat(XS:S),XS:S),x77:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => sel(x76:S,x77:S) -> U171(isNatural(x76:S),x76:S,x77:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x76:S 0.008/0.008 Pos x76:S in l => [1] 0.008/0.008 Sigma => {x76:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U171(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S)),x77:S) 0.008/0.008 t => sel(U201(isNatural(N:S),N:S,X:S,XS:S),x77:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => sel(x76:S,x77:S) -> U171(isNatural(x76:S),x76:S,x77:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x76:S 0.008/0.008 Pos x76:S in l => [1] 0.008/0.008 Sigma => {x76:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U171(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)),x77:S) 0.008/0.008 t => sel(U211(isNatural(N:S),XS:S),x77:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => sel(x76:S,x77:S) -> U171(isNatural(x76:S),x76:S,x77:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x76:S 0.008/0.008 Pos x76:S in l => [1] 0.008/0.008 Sigma => {x76:S -> take(N:S,XS:S)} 0.008/0.008 s => U171(isNatural(take(N:S,XS:S)),take(N:S,XS:S),x77:S) 0.008/0.008 t => sel(U221(isNatural(N:S),N:S,XS:S),x77:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => snd(pair(x78:S,x79:S)) -> U181(isLNat(x78:S),x79:S) 0.008/0.008 Rule 58 (l' :-> r') => snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 Var => x78:S 0.008/0.008 Pos x78:S in l => [1,1] 0.008/0.008 Sigma => {x78:S -> snd(pair(X:S,Y:S))} 0.008/0.008 s => U181(isLNat(snd(pair(X:S,Y:S))),x79:S) 0.008/0.008 t => snd(pair(U181(isLNat(X:S),Y:S),x79:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => snd(pair(x78:S,x79:S)) -> U181(isLNat(x78:S),x79:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x78:S 0.008/0.008 Pos x78:S in l => [1,1] 0.008/0.008 Sigma => {x78:S -> splitAt(0,XS:S)} 0.008/0.008 s => U181(isLNat(splitAt(0,XS:S)),x79:S) 0.008/0.008 t => snd(pair(U191(isLNat(XS:S),XS:S),x79:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => snd(pair(x78:S,x79:S)) -> U181(isLNat(x78:S),x79:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x78:S 0.008/0.008 Pos x78:S in l => [1,1] 0.008/0.008 Sigma => {x78:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U181(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),x79:S) 0.008/0.008 t => snd(pair(U201(isNatural(N:S),N:S,X:S,XS:S),x79:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => snd(pair(x78:S,x79:S)) -> U181(isLNat(x78:S),x79:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x78:S 0.008/0.008 Pos x78:S in l => [1,1] 0.008/0.008 Sigma => {x78:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U181(isLNat(tail(cons(N:S,XS:S))),x79:S) 0.008/0.008 t => snd(pair(U211(isNatural(N:S),XS:S),x79:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => snd(pair(x78:S,x79:S)) -> U181(isLNat(x78:S),x79:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x78:S 0.008/0.008 Pos x78:S in l => [1,1] 0.008/0.008 Sigma => {x78:S -> take(N:S,XS:S)} 0.008/0.008 s => U181(isLNat(take(N:S,XS:S)),x79:S) 0.008/0.008 t => snd(pair(U221(isNatural(N:S),N:S,XS:S),x79:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => splitAt(0,x80:S) -> U191(isLNat(x80:S),x80:S) 0.008/0.008 Rule 59 (l' :-> r') => splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 Var => x80:S 0.008/0.008 Pos x80:S in l => [2] 0.008/0.008 Sigma => {x80:S -> splitAt(0,XS:S)} 0.008/0.008 s => U191(isLNat(splitAt(0,XS:S)),splitAt(0,XS:S)) 0.008/0.008 t => splitAt(0,U191(isLNat(XS:S),XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => splitAt(0,x80:S) -> U191(isLNat(x80:S),x80:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x80:S 0.008/0.008 Pos x80:S in l => [2] 0.008/0.008 Sigma => {x80:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U191(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S))) 0.008/0.008 t => splitAt(0,U201(isNatural(N:S),N:S,X:S,XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => splitAt(0,x80:S) -> U191(isLNat(x80:S),x80:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x80:S 0.008/0.008 Pos x80:S in l => [2] 0.008/0.008 Sigma => {x80:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U191(isLNat(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))) 0.008/0.008 t => splitAt(0,U211(isNatural(N:S),XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => splitAt(0,x80:S) -> U191(isLNat(x80:S),x80:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x80:S 0.008/0.008 Pos x80:S in l => [2] 0.008/0.008 Sigma => {x80:S -> take(N:S,XS:S)} 0.008/0.008 s => U191(isLNat(take(N:S,XS:S)),take(N:S,XS:S)) 0.008/0.008 t => splitAt(0,U221(isNatural(N:S),N:S,XS:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => splitAt(s(x81:S),cons(x82:S,x83:S)) -> U201(isNatural(x81:S),x81:S,x82:S,x83:S) 0.008/0.008 Rule 60 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 Var => x81:S 0.008/0.008 Pos x81:S in l => [1,1] 0.008/0.008 Sigma => {x81:S -> splitAt(s(N:S),cons(X:S,XS:S))} 0.008/0.008 s => U201(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S)),x82:S,x83:S) 0.008/0.008 t => splitAt(s(U201(isNatural(N:S),N:S,X:S,XS:S)),cons(x82:S,x83:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => splitAt(s(x81:S),cons(x82:S,x83:S)) -> U201(isNatural(x81:S),x81:S,x82:S,x83:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x81:S 0.008/0.008 Pos x81:S in l => [1,1] 0.008/0.008 Sigma => {x81:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U201(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)),x82:S,x83:S) 0.008/0.008 t => splitAt(s(U211(isNatural(N:S),XS:S)),cons(x82:S,x83:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => splitAt(s(x81:S),cons(x82:S,x83:S)) -> U201(isNatural(x81:S),x81:S,x82:S,x83:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x81:S 0.008/0.008 Pos x81:S in l => [1,1] 0.008/0.008 Sigma => {x81:S -> take(N:S,XS:S)} 0.008/0.008 s => U201(isNatural(take(N:S,XS:S)),take(N:S,XS:S),x82:S,x83:S) 0.008/0.008 t => splitAt(s(U221(isNatural(N:S),N:S,XS:S)),cons(x82:S,x83:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => tail(cons(x84:S,x85:S)) -> U211(isNatural(x84:S),x85:S) 0.008/0.008 Rule 61 (l' :-> r') => tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 Var => x84:S 0.008/0.008 Pos x84:S in l => [1,1] 0.008/0.008 Sigma => {x84:S -> tail(cons(N:S,XS:S))} 0.008/0.008 s => U211(isNatural(tail(cons(N:S,XS:S))),x85:S) 0.008/0.008 t => tail(cons(U211(isNatural(N:S),XS:S),x85:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => tail(cons(x84:S,x85:S)) -> U211(isNatural(x84:S),x85:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x84:S 0.008/0.008 Pos x84:S in l => [1,1] 0.008/0.008 Sigma => {x84:S -> take(N:S,XS:S)} 0.008/0.008 s => U211(isNatural(take(N:S,XS:S)),x85:S) 0.008/0.008 t => tail(cons(U221(isNatural(N:S),N:S,XS:S),x85:S)) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 ->Extended u-Critical Pair: 0.008/0.008 Rule 1 (l :-> r) => take(x86:S,x87:S) -> U221(isNatural(x86:S),x86:S,x87:S) 0.008/0.008 Rule 62 (l' :-> r') => take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 Var => x86:S 0.008/0.008 Pos x86:S in l => [1] 0.008/0.008 Sigma => {x86:S -> take(N:S,XS:S)} 0.008/0.008 s => U221(isNatural(take(N:S,XS:S)),take(N:S,XS:S),x87:S) 0.008/0.008 t => take(U221(isNatural(N:S),N:S,XS:S),x87:S) 0.008/0.008 NW => 1 0.008/0.008 0.008/0.008 0.008/0.008 Problem 1: 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 Confluence Problem: 0.008/0.008 (VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S) 0.008/0.008 (STRATEGY CONTEXTSENSITIVE 0.008/0.008 (U101 1) 0.008/0.008 (U102 1) 0.008/0.008 (U11 1) 0.008/0.008 (U111 1) 0.008/0.008 (U12 1) 0.008/0.008 (U121 1) 0.008/0.008 (U131 1) 0.008/0.008 (U132 1) 0.008/0.008 (U141 1) 0.008/0.008 (U142 1) 0.008/0.008 (U151 1) 0.008/0.008 (U152 1) 0.008/0.008 (U161 1) 0.008/0.008 (U171 1) 0.008/0.008 (U172 1) 0.008/0.008 (U181 1) 0.008/0.008 (U182 1) 0.008/0.008 (U191 1) 0.008/0.008 (U201 1) 0.008/0.008 (U202 1) 0.008/0.008 (U203 1) 0.008/0.008 (U204 1) 0.008/0.008 (U21 1) 0.008/0.008 (U211 1) 0.008/0.008 (U212 1) 0.008/0.008 (U22 1) 0.008/0.008 (U221 1) 0.008/0.008 (U222 1) 0.008/0.008 (U31 1) 0.008/0.008 (U32 1) 0.008/0.008 (U41 1) 0.008/0.008 (U42 1) 0.008/0.008 (U51 1) 0.008/0.008 (U52 1) 0.008/0.008 (U61 1) 0.008/0.008 (U71 1) 0.008/0.008 (U81 1) 0.008/0.008 (U91 1) 0.008/0.008 (afterNth 1 2) 0.008/0.008 (fst 1) 0.008/0.008 (head 1) 0.008/0.008 (isLNat) 0.008/0.008 (isNatural) 0.008/0.008 (isPLNat) 0.008/0.008 (natsFrom 1) 0.008/0.008 (sel 1 2) 0.008/0.008 (snd 1) 0.008/0.008 (splitAt 1 2) 0.008/0.008 (tail 1) 0.008/0.008 (take 1 2) 0.008/0.008 (0) 0.008/0.008 (cons 1) 0.008/0.008 (fSNonEmpty) 0.008/0.008 (nil) 0.008/0.008 (pair 1 2) 0.008/0.008 (s 1) 0.008/0.008 (tt) 0.008/0.008 ) 0.008/0.008 (RULES 0.008/0.008 U101(tt,V2:S) -> U102(isLNat(V2:S)) 0.008/0.008 U102(tt) -> tt 0.008/0.008 U11(tt,N:S,XS:S) -> U12(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U111(tt) -> tt 0.008/0.008 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.008/0.008 U121(tt) -> tt 0.008/0.008 U131(tt,V2:S) -> U132(isLNat(V2:S)) 0.008/0.008 U132(tt) -> tt 0.008/0.008 U141(tt,V2:S) -> U142(isLNat(V2:S)) 0.008/0.008 U142(tt) -> tt 0.008/0.008 U151(tt,V2:S) -> U152(isLNat(V2:S)) 0.008/0.008 U152(tt) -> tt 0.008/0.008 U161(tt,N:S) -> cons(N:S,natsFrom(s(N:S))) 0.008/0.008 U171(tt,N:S,XS:S) -> U172(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U172(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.008/0.008 U181(tt,Y:S) -> U182(isLNat(Y:S),Y:S) 0.008/0.008 U182(tt,Y:S) -> Y:S 0.008/0.008 U191(tt,XS:S) -> pair(nil,XS:S) 0.008/0.008 U201(tt,N:S,X:S,XS:S) -> U202(isNatural(X:S),N:S,X:S,XS:S) 0.008/0.008 U202(tt,N:S,X:S,XS:S) -> U203(isLNat(XS:S),N:S,X:S,XS:S) 0.008/0.008 U203(tt,N:S,X:S,XS:S) -> U204(splitAt(N:S,XS:S),X:S) 0.008/0.008 U204(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.008/0.008 U21(tt,X:S,Y:S) -> U22(isLNat(Y:S),X:S) 0.008/0.008 U211(tt,XS:S) -> U212(isLNat(XS:S),XS:S) 0.008/0.008 U212(tt,XS:S) -> XS:S 0.008/0.008 U22(tt,X:S) -> X:S 0.008/0.008 U221(tt,N:S,XS:S) -> U222(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U222(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.008/0.008 U31(tt,N:S,XS:S) -> U32(isLNat(XS:S),N:S) 0.008/0.008 U32(tt,N:S) -> N:S 0.008/0.008 U41(tt,V2:S) -> U42(isLNat(V2:S)) 0.008/0.008 U42(tt) -> tt 0.008/0.008 U51(tt,V2:S) -> U52(isLNat(V2:S)) 0.008/0.008 U52(tt) -> tt 0.008/0.008 U61(tt) -> tt 0.008/0.008 U71(tt) -> tt 0.008/0.008 U81(tt) -> tt 0.008/0.008 U91(tt) -> tt 0.008/0.008 afterNth(N:S,XS:S) -> U11(isNatural(N:S),N:S,XS:S) 0.008/0.008 fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 isNatural(0) -> tt 0.008/0.008 isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 ) 0.008/0.008 Critical Pairs: 0.008/0.008 => Not trivial, Not overlay, NW1, N1 0.008/0.008 => Not trivial, Not overlay, NW1, N2 0.008/0.008 => Not trivial, Not overlay, NW1, N3 0.008/0.008 => Not trivial, Not overlay, NW1, N4 0.008/0.008 => Not trivial, Not overlay, NW1, N5 0.008/0.008 => Not trivial, Not overlay, NW1, N6 0.008/0.008 => Not trivial, Not overlay, NW1, N7 0.008/0.008 => Not trivial, Not overlay, NW1, N8 0.008/0.008 => Not trivial, Not overlay, NW1, N9 0.008/0.008 => Not trivial, Not overlay, NW1, N10 0.008/0.008 => Not trivial, Not overlay, NW1, N11 0.008/0.008 => Not trivial, Not overlay, NW1, N12 0.008/0.008 => Not trivial, Not overlay, NW1, N13 0.008/0.008 => Not trivial, Not overlay, NW1, N14 0.008/0.008 => Not trivial, Not overlay, NW1, N15 0.008/0.008 => Not trivial, Not overlay, NW1, N16 0.008/0.008 => Not trivial, Not overlay, NW1, N17 0.008/0.008 => Not trivial, Not overlay, NW1, N18 0.008/0.008 => Not trivial, Not overlay, NW1, N19 0.008/0.008 => Not trivial, Not overlay, NW1, N20 0.008/0.008 => Not trivial, Not overlay, NW1, N21 0.008/0.008 => Not trivial, Not overlay, NW1, N22 0.008/0.008 => Not trivial, Not overlay, NW1, N23 0.008/0.008 => Not trivial, Not overlay, NW1, N24 0.008/0.008 => Not trivial, Not overlay, NW1, N25 0.008/0.008 => Not trivial, Not overlay, NW1, N26 0.008/0.008 => Not trivial, Not overlay, NW1, N27 0.008/0.008 => Not trivial, Not overlay, NW1, N28 0.008/0.008 => Not trivial, Not overlay, NW1, N29 0.008/0.008 => Not trivial, Not overlay, NW1, N30 0.008/0.008 => Not trivial, Not overlay, NW1, N31 0.008/0.008 => Not trivial, Not overlay, NW1, N32 0.008/0.008 => Not trivial, Not overlay, NW1, N33 0.008/0.008 => Not trivial, Not overlay, NW1, N34 0.008/0.008 => Not trivial, Not overlay, NW1, N35 0.008/0.008 => Not trivial, Not overlay, NW1, N36 0.008/0.008 => Not trivial, Not overlay, NW1, N37 0.008/0.008 => Not trivial, Not overlay, NW1, N38 0.008/0.008 => Not trivial, Not overlay, NW1, N39 0.008/0.008 => Not trivial, Not overlay, NW1, N40 0.008/0.008 => Not trivial, Not overlay, NW1, N41 0.008/0.008 => Not trivial, Not overlay, NW1, N42 0.008/0.008 => Not trivial, Not overlay, NW1, N43 0.008/0.008 => Not trivial, Not overlay, NW0, N44 0.008/0.008 => Not trivial, Not overlay, NW1, N45 0.008/0.008 => Not trivial, Not overlay, NW1, N46 0.008/0.008 => Not trivial, Not overlay, NW1, N47 0.008/0.008 => Not trivial, Not overlay, NW1, N48 0.008/0.008 => Not trivial, Not overlay, NW1, N49 0.008/0.008 => Not trivial, Not overlay, NW1, N50 0.008/0.008 => Not trivial, Not overlay, NW1, N51 0.008/0.008 => Not trivial, Not overlay, NW1, N52 0.008/0.008 => Not trivial, Not overlay, NW1, N53 0.008/0.008 => Not trivial, Not overlay, NW1, N54 0.008/0.008 => Not trivial, Not overlay, NW1, N55 0.008/0.008 => Not trivial, Not overlay, NW1, N56 0.008/0.008 => Not trivial, Not overlay, NW1, N57 0.008/0.008 => Not trivial, Not overlay, NW1, N58 0.008/0.008 => Not trivial, Not overlay, NW1, N59 0.008/0.008 => Not trivial, Not overlay, NW0, N60 0.008/0.008 => Not trivial, Not overlay, NW1, N61 0.008/0.008 => Not trivial, Not overlay, NW1, N62 0.008/0.008 => Not trivial, Not overlay, NW1, N63 0.008/0.008 => Not trivial, Not overlay, NW1, N64 0.008/0.008 => Not trivial, Not overlay, NW1, N65 0.008/0.008 => Not trivial, Not overlay, NW0, N66 0.008/0.008 => Not trivial, Not overlay, NW1, N67 0.008/0.008 => Not trivial, Not overlay, NW1, N68 0.008/0.008 => Not trivial, Not overlay, NW1, N69 0.008/0.008 => Not trivial, Not overlay, NW1, N70 0.008/0.008 => Not trivial, Not overlay, NW1, N71 0.008/0.008 => Not trivial, Not overlay, NW1, N72 0.008/0.008 => Not trivial, Not overlay, NW1, N73 0.008/0.008 => Not trivial, Not overlay, NW1, N74 0.008/0.008 => Not trivial, Not overlay, NW1, N75 0.008/0.008 => Not trivial, Not overlay, NW1, N76 0.008/0.008 => Not trivial, Not overlay, NW1, N77 0.008/0.008 => Not trivial, Not overlay, NW1, N78 0.008/0.008 => Not trivial, Not overlay, NW1, N79 0.008/0.008 => Not trivial, Not overlay, NW1, N80 0.008/0.008 => Not trivial, Not overlay, NW1, N81 0.008/0.008 => Not trivial, Not overlay, NW0, N82 0.008/0.008 => Not trivial, Not overlay, NW1, N83 0.008/0.008 => Not trivial, Not overlay, NW0, N84 0.008/0.008 => Not trivial, Not overlay, NW1, N85 0.008/0.008 => Not trivial, Not overlay, NW1, N86 0.008/0.008 => Not trivial, Not overlay, NW0, N87 0.008/0.008 => Not trivial, Not overlay, NW0, N88 0.008/0.008 => Not trivial, Not overlay, NW0, N89 0.008/0.008 => Not trivial, Not overlay, NW1, N90 0.008/0.008 => Not trivial, Not overlay, NW1, N91 0.008/0.008 => Not trivial, Not overlay, NW1, N92 0.008/0.008 => Not trivial, Not overlay, NW1, N93 0.008/0.008 => Not trivial, Not overlay, NW1, N94 0.008/0.008 => Not trivial, Not overlay, NW1, N95 0.008/0.008 => Not trivial, Not overlay, NW1, N96 0.008/0.008 => Not trivial, Not overlay, NW1, N97 0.008/0.008 => Not trivial, Not overlay, NW1, N98 0.008/0.008 => Not trivial, Not overlay, NW1, N99 0.008/0.008 => Not trivial, Not overlay, NW1, N100 0.008/0.008 => Not trivial, Not overlay, NW1, N101 0.008/0.008 => Not trivial, Not overlay, NW1, N102 0.008/0.008 => Not trivial, Not overlay, NW1, N103 0.008/0.008 => Not trivial, Not overlay, NW1, N104 0.008/0.008 => Not trivial, Not overlay, NW0, N105 0.008/0.008 => Not trivial, Not overlay, NW1, N106 0.008/0.008 => Not trivial, Not overlay, NW1, N107 0.008/0.008 => Not trivial, Not overlay, NW1, N108 0.008/0.008 => Not trivial, Not overlay, NW1, N109 0.008/0.008 => Not trivial, Not overlay, NW1, N110 0.008/0.008 => Not trivial, Not overlay, NW1, N111 0.008/0.008 => Not trivial, Not overlay, NW1, N112 0.008/0.008 => Not trivial, Not overlay, NW1, N113 0.008/0.008 => Not trivial, Not overlay, NW1, N114 0.008/0.008 => Not trivial, Not overlay, NW1, N115 0.008/0.008 => Not trivial, Not overlay, NW1, N116 0.008/0.008 => Not trivial, Not overlay, NW1, N117 0.008/0.008 => Not trivial, Not overlay, NW1, N118 0.008/0.008 => Not trivial, Not overlay, NW1, N119 0.008/0.008 => Not trivial, Not overlay, NW1, N120 0.008/0.008 => Not trivial, Not overlay, NW1, N121 0.008/0.008 => Not trivial, Not overlay, NW1, N122 0.008/0.008 => Not trivial, Not overlay, NW1, N123 0.008/0.008 => Not trivial, Not overlay, NW1, N124 0.008/0.008 => Not trivial, Not overlay, NW1, N125 0.008/0.008 => Not trivial, Not overlay, NW1, N126 0.008/0.008 => Not trivial, Not overlay, NW1, N127 0.008/0.008 => Not trivial, Not overlay, NW1, N128 0.008/0.008 => Not trivial, Not overlay, NW1, N129 0.008/0.008 => Not trivial, Not overlay, NW1, N130 0.008/0.008 => Not trivial, Not overlay, NW1, N131 0.008/0.008 => Not trivial, Not overlay, NW1, N132 0.008/0.008 => Not trivial, Not overlay, NW1, N133 0.008/0.008 => Not trivial, Not overlay, NW1, N134 0.008/0.008 => Not trivial, Not overlay, NW1, N135 0.008/0.008 => Not trivial, Not overlay, NW1, N136 0.008/0.008 => Not trivial, Not overlay, NW1, N137 0.008/0.008 => Not trivial, Not overlay, NW1, N138 0.008/0.008 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.008/0.008 0.008/0.008 Huet Levy Processor: 0.008/0.008 -> Rules: 0.008/0.008 U101(tt,V2:S) -> U102(isLNat(V2:S)) 0.008/0.008 U102(tt) -> tt 0.008/0.008 U11(tt,N:S,XS:S) -> U12(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U111(tt) -> tt 0.008/0.008 U12(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S)) 0.008/0.008 U121(tt) -> tt 0.008/0.008 U131(tt,V2:S) -> U132(isLNat(V2:S)) 0.008/0.008 U132(tt) -> tt 0.008/0.008 U141(tt,V2:S) -> U142(isLNat(V2:S)) 0.008/0.008 U142(tt) -> tt 0.008/0.008 U151(tt,V2:S) -> U152(isLNat(V2:S)) 0.008/0.008 U152(tt) -> tt 0.008/0.008 U161(tt,N:S) -> cons(N:S,natsFrom(s(N:S))) 0.008/0.008 U171(tt,N:S,XS:S) -> U172(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U172(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S)) 0.008/0.008 U181(tt,Y:S) -> U182(isLNat(Y:S),Y:S) 0.008/0.008 U182(tt,Y:S) -> Y:S 0.008/0.008 U191(tt,XS:S) -> pair(nil,XS:S) 0.008/0.008 U201(tt,N:S,X:S,XS:S) -> U202(isNatural(X:S),N:S,X:S,XS:S) 0.008/0.008 U202(tt,N:S,X:S,XS:S) -> U203(isLNat(XS:S),N:S,X:S,XS:S) 0.008/0.008 U203(tt,N:S,X:S,XS:S) -> U204(splitAt(N:S,XS:S),X:S) 0.008/0.008 U204(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S) 0.008/0.008 U21(tt,X:S,Y:S) -> U22(isLNat(Y:S),X:S) 0.008/0.008 U211(tt,XS:S) -> U212(isLNat(XS:S),XS:S) 0.008/0.008 U212(tt,XS:S) -> XS:S 0.008/0.008 U22(tt,X:S) -> X:S 0.008/0.008 U221(tt,N:S,XS:S) -> U222(isLNat(XS:S),N:S,XS:S) 0.008/0.008 U222(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S)) 0.008/0.008 U31(tt,N:S,XS:S) -> U32(isLNat(XS:S),N:S) 0.008/0.008 U32(tt,N:S) -> N:S 0.008/0.008 U41(tt,V2:S) -> U42(isLNat(V2:S)) 0.008/0.008 U42(tt) -> tt 0.008/0.008 U51(tt,V2:S) -> U52(isLNat(V2:S)) 0.008/0.008 U52(tt) -> tt 0.008/0.008 U61(tt) -> tt 0.008/0.008 U71(tt) -> tt 0.008/0.008 U81(tt) -> tt 0.008/0.008 U91(tt) -> tt 0.008/0.008 afterNth(N:S,XS:S) -> U11(isNatural(N:S),N:S,XS:S) 0.008/0.008 fst(pair(X:S,Y:S)) -> U21(isLNat(X:S),X:S,Y:S) 0.008/0.008 head(cons(N:S,XS:S)) -> U31(isNatural(N:S),N:S,XS:S) 0.008/0.008 isLNat(afterNth(V1:S,V2:S)) -> U41(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(fst(V1:S)) -> U61(isPLNat(V1:S)) 0.008/0.008 isLNat(natsFrom(V1:S)) -> U71(isNatural(V1:S)) 0.008/0.008 isLNat(snd(V1:S)) -> U81(isPLNat(V1:S)) 0.008/0.008 isLNat(tail(V1:S)) -> U91(isLNat(V1:S)) 0.008/0.008 isLNat(take(V1:S,V2:S)) -> U101(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(cons(V1:S,V2:S)) -> U51(isNatural(V1:S),V2:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isNatural(head(V1:S)) -> U111(isLNat(V1:S)) 0.008/0.008 isNatural(sel(V1:S,V2:S)) -> U131(isNatural(V1:S),V2:S) 0.008/0.008 isNatural(0) -> tt 0.008/0.008 isNatural(s(V1:S)) -> U121(isNatural(V1:S)) 0.008/0.008 isPLNat(splitAt(V1:S,V2:S)) -> U151(isNatural(V1:S),V2:S) 0.008/0.008 isPLNat(pair(V1:S,V2:S)) -> U141(isLNat(V1:S),V2:S) 0.008/0.008 natsFrom(N:S) -> U161(isNatural(N:S),N:S) 0.008/0.008 sel(N:S,XS:S) -> U171(isNatural(N:S),N:S,XS:S) 0.008/0.008 snd(pair(X:S,Y:S)) -> U181(isLNat(X:S),Y:S) 0.008/0.008 splitAt(0,XS:S) -> U191(isLNat(XS:S),XS:S) 0.008/0.008 splitAt(s(N:S),cons(X:S,XS:S)) -> U201(isNatural(N:S),N:S,X:S,XS:S) 0.008/0.008 tail(cons(N:S,XS:S)) -> U211(isNatural(N:S),XS:S) 0.008/0.008 take(N:S,XS:S) -> U221(isNatural(N:S),N:S,XS:S) 0.008/0.008 -> Vars: 0.008/0.008 V2, N, XS, N, XS, V2, V2, V2, N, N, XS, N, XS, Y, Y, XS, N, X, XS, N, X, XS, N, X, XS, X, YS, ZS, X, Y, XS, XS, X, N, XS, N, XS, N, XS, N, V2, V2, N, XS, X, Y, N, XS, V1, V2, V1, V1, V1, V1, V1, V2, V1, V2, V1, V1, V2, V1, V1, V2, V1, V2, N, N, XS, X, Y, XS, N, X, XS, N, XS, N, XS 0.008/0.008 -> UVars: 0.008/0.008 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.008/0.008 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, XS], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.008/0.008 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.008/0.008 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.008/0.008 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: [N]) 0.008/0.008 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, XS], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [Y], UV-RFrozen: [Y]) 0.008/0.008 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [Y], UV-LFrozen: [Y], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [XS], UV-LFrozen: [XS], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, X, XS], UV-RFrozen: [N, X, XS]) 0.008/0.008 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, X, XS], UV-RFrozen: [N, X, XS]) 0.008/0.008 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, X, XS], UV-RFrozen: [X]) 0.008/0.008 (UV-RuleId: 22, UV-LActive: [YS, ZS], UV-RActive: [X, ZS], UV-LFrozen: [X], UV-RFrozen: [YS]) 0.008/0.008 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X, Y], UV-RFrozen: [X, Y]) 0.008/0.008 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [XS]) 0.008/0.008 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [XS], UV-LFrozen: [XS], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, XS], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N, XS], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.008/0.008 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V2], UV-RFrozen: [V2]) 0.008/0.008 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 39, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 40, UV-LActive: [X, Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [X, Y]) 0.008/0.008 (UV-RuleId: 41, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.008/0.008 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.008/0.008 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.008/0.008 (UV-RuleId: 45, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.008/0.008 (UV-RuleId: 46, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.008/0.008 (UV-RuleId: 47, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.008/0.008 (UV-RuleId: 48, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.008/0.008 (UV-RuleId: 49, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 50, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.008/0.008 (UV-RuleId: 51, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.008/0.008 (UV-RuleId: 52, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1]) 0.008/0.008 (UV-RuleId: 54, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.008/0.008 (UV-RuleId: 55, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2]) 0.008/0.008 (UV-RuleId: 56, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N]) 0.008/0.008 (UV-RuleId: 57, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 58, UV-LActive: [X, Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [X, Y]) 0.008/0.008 (UV-RuleId: 59, UV-LActive: [XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [XS]) 0.008/0.008 (UV-RuleId: 60, UV-LActive: [N, X], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N, X, XS]) 0.008/0.008 (UV-RuleId: 61, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N, XS]) 0.008/0.008 (UV-RuleId: 62, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS]) 0.008/0.008 -> FVars: 0.008/0.008 x9, 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 0.008/0.008 -> PVars: 0.008/0.008 V2: [x9, x14, x15, x16, x49, x50, x58, x64, x66, x69, x72, x74], N: [x10, x12, x17, x18, x20, x25, x28, x31, x42, x44, x46, x48, x51, x55, x75, x76, x81, x84, x86], XS: [x11, x13, x19, x21, x24, x27, x30, x33, x39, x40, x43, x45, x47, x52, x56, x77, x80, x83, x85, x87], Y: [x22, x23, x38, x54, x79], X: [x26, x29, x32, x34, x37, x41, x53, x78, x82], YS: [x35], ZS: [x36], V1: [x57, x59, x60, x61, x62, x63, x65, x67, x68, x70, x71, x73] 0.008/0.008 0.008/0.008 -> Rlps: 0.008/0.008 (rule: U101(tt,x9:S) -> U102(isLNat(x9:S)), id: 1, possubterms: U101(tt,x9:S)->[], tt->[1]) 0.008/0.008 (rule: U102(tt) -> tt, id: 2, possubterms: U102(tt)->[], tt->[1]) 0.008/0.008 (rule: U11(tt,x10:S,x11:S) -> U12(isLNat(x11:S),x10:S,x11:S), id: 3, possubterms: U11(tt,x10:S,x11:S)->[], tt->[1]) 0.008/0.008 (rule: U111(tt) -> tt, id: 4, possubterms: U111(tt)->[], tt->[1]) 0.008/0.008 (rule: U12(tt,x12:S,x13:S) -> snd(splitAt(x12:S,x13:S)), id: 5, possubterms: U12(tt,x12:S,x13:S)->[], tt->[1]) 0.008/0.008 (rule: U121(tt) -> tt, id: 6, possubterms: U121(tt)->[], tt->[1]) 0.008/0.008 (rule: U131(tt,x14:S) -> U132(isLNat(x14:S)), id: 7, possubterms: U131(tt,x14:S)->[], tt->[1]) 0.008/0.008 (rule: U132(tt) -> tt, id: 8, possubterms: U132(tt)->[], tt->[1]) 0.008/0.008 (rule: U141(tt,x15:S) -> U142(isLNat(x15:S)), id: 9, possubterms: U141(tt,x15:S)->[], tt->[1]) 0.008/0.008 (rule: U142(tt) -> tt, id: 10, possubterms: U142(tt)->[], tt->[1]) 0.008/0.008 (rule: U151(tt,x16:S) -> U152(isLNat(x16:S)), id: 11, possubterms: U151(tt,x16:S)->[], tt->[1]) 0.008/0.008 (rule: U152(tt) -> tt, id: 12, possubterms: U152(tt)->[], tt->[1]) 0.008/0.008 (rule: U161(tt,x17:S) -> cons(x17:S,natsFrom(s(x17:S))), id: 13, possubterms: U161(tt,x17:S)->[], tt->[1]) 0.008/0.008 (rule: U171(tt,x18:S,x19:S) -> U172(isLNat(x19:S),x18:S,x19:S), id: 14, possubterms: U171(tt,x18:S,x19:S)->[], tt->[1]) 0.008/0.008 (rule: U172(tt,x20:S,x21:S) -> head(afterNth(x20:S,x21:S)), id: 15, possubterms: U172(tt,x20:S,x21:S)->[], tt->[1]) 0.008/0.008 (rule: U181(tt,x22:S) -> U182(isLNat(x22:S),x22:S), id: 16, possubterms: U181(tt,x22:S)->[], tt->[1]) 0.008/0.008 (rule: U182(tt,x23:S) -> x23:S, id: 17, possubterms: U182(tt,x23:S)->[], tt->[1]) 0.008/0.008 (rule: U191(tt,x24:S) -> pair(nil,x24:S), id: 18, possubterms: U191(tt,x24:S)->[], tt->[1]) 0.008/0.008 (rule: U201(tt,x25:S,x26:S,x27:S) -> U202(isNatural(x26:S),x25:S,x26:S,x27:S), id: 19, possubterms: U201(tt,x25:S,x26:S,x27:S)->[], tt->[1]) 0.008/0.008 (rule: U202(tt,x28:S,x29:S,x30:S) -> U203(isLNat(x30:S),x28:S,x29:S,x30:S), id: 20, possubterms: U202(tt,x28:S,x29:S,x30:S)->[], tt->[1]) 0.008/0.008 (rule: U203(tt,x31:S,x32:S,x33:S) -> U204(splitAt(x31:S,x33:S),x32:S), id: 21, possubterms: U203(tt,x31:S,x32:S,x33:S)->[], tt->[1]) 0.008/0.008 (rule: U204(pair(x35:S,x36:S),x34:S) -> pair(cons(x34:S,x35:S),x36:S), id: 22, possubterms: U204(pair(x35:S,x36:S),x34:S)->[], pair(x35:S,x36:S)->[1]) 0.008/0.008 (rule: U21(tt,x37:S,x38:S) -> U22(isLNat(x38:S),x37:S), id: 23, possubterms: U21(tt,x37:S,x38:S)->[], tt->[1]) 0.008/0.008 (rule: U211(tt,x39:S) -> U212(isLNat(x39:S),x39:S), id: 24, possubterms: U211(tt,x39:S)->[], tt->[1]) 0.008/0.008 (rule: U212(tt,x40:S) -> x40:S, id: 25, possubterms: U212(tt,x40:S)->[], tt->[1]) 0.008/0.008 (rule: U22(tt,x41:S) -> x41:S, id: 26, possubterms: U22(tt,x41:S)->[], tt->[1]) 0.008/0.008 (rule: U221(tt,x42:S,x43:S) -> U222(isLNat(x43:S),x42:S,x43:S), id: 27, possubterms: U221(tt,x42:S,x43:S)->[], tt->[1]) 0.008/0.008 (rule: U222(tt,x44:S,x45:S) -> fst(splitAt(x44:S,x45:S)), id: 28, possubterms: U222(tt,x44:S,x45:S)->[], tt->[1]) 0.008/0.008 (rule: U31(tt,x46:S,x47:S) -> U32(isLNat(x47:S),x46:S), id: 29, possubterms: U31(tt,x46:S,x47:S)->[], tt->[1]) 0.008/0.008 (rule: U32(tt,x48:S) -> x48:S, id: 30, possubterms: U32(tt,x48:S)->[], tt->[1]) 0.008/0.008 (rule: U41(tt,x49:S) -> U42(isLNat(x49:S)), id: 31, possubterms: U41(tt,x49:S)->[], tt->[1]) 0.008/0.008 (rule: U42(tt) -> tt, id: 32, possubterms: U42(tt)->[], tt->[1]) 0.008/0.008 (rule: U51(tt,x50:S) -> U52(isLNat(x50:S)), id: 33, possubterms: U51(tt,x50:S)->[], tt->[1]) 0.008/0.008 (rule: U52(tt) -> tt, id: 34, possubterms: U52(tt)->[], tt->[1]) 0.008/0.008 (rule: U61(tt) -> tt, id: 35, possubterms: U61(tt)->[], tt->[1]) 0.008/0.008 (rule: U71(tt) -> tt, id: 36, possubterms: U71(tt)->[], tt->[1]) 0.008/0.008 (rule: U81(tt) -> tt, id: 37, possubterms: U81(tt)->[], tt->[1]) 0.008/0.008 (rule: U91(tt) -> tt, id: 38, possubterms: U91(tt)->[], tt->[1]) 0.008/0.008 (rule: afterNth(x51:S,x52:S) -> U11(isNatural(x51:S),x51:S,x52:S), id: 39, possubterms: afterNth(x51:S,x52:S)->[]) 0.008/0.008 (rule: fst(pair(x53:S,x54:S)) -> U21(isLNat(x53:S),x53:S,x54:S), id: 40, possubterms: fst(pair(x53:S,x54:S))->[], pair(x53:S,x54:S)->[1]) 0.008/0.008 (rule: head(cons(x55:S,x56:S)) -> U31(isNatural(x55:S),x55:S,x56:S), id: 41, possubterms: head(cons(x55:S,x56:S))->[], cons(x55:S,x56:S)->[1]) 0.008/0.008 (rule: isLNat(afterNth(x57:S,x58:S)) -> U41(isNatural(x57:S),x58:S), id: 42, possubterms: isLNat(afterNth(x57:S,x58:S))->[]) 0.008/0.008 (rule: isLNat(fst(x59:S)) -> U61(isPLNat(x59:S)), id: 43, possubterms: isLNat(fst(x59:S))->[]) 0.008/0.008 (rule: isLNat(natsFrom(x60:S)) -> U71(isNatural(x60:S)), id: 44, possubterms: isLNat(natsFrom(x60:S))->[]) 0.008/0.008 (rule: isLNat(snd(x61:S)) -> U81(isPLNat(x61:S)), id: 45, possubterms: isLNat(snd(x61:S))->[]) 0.008/0.008 (rule: isLNat(tail(x62:S)) -> U91(isLNat(x62:S)), id: 46, possubterms: isLNat(tail(x62:S))->[]) 0.008/0.008 (rule: isLNat(take(x63:S,x64:S)) -> U101(isNatural(x63:S),x64:S), id: 47, possubterms: isLNat(take(x63:S,x64:S))->[]) 0.008/0.008 (rule: isLNat(cons(x65:S,x66:S)) -> U51(isNatural(x65:S),x66:S), id: 48, possubterms: isLNat(cons(x65:S,x66:S))->[]) 0.008/0.008 (rule: isLNat(nil) -> tt, id: 49, possubterms: isLNat(nil)->[]) 0.008/0.008 (rule: isNatural(head(x67:S)) -> U111(isLNat(x67:S)), id: 50, possubterms: isNatural(head(x67:S))->[]) 0.008/0.008 (rule: isNatural(sel(x68:S,x69:S)) -> U131(isNatural(x68:S),x69:S), id: 51, possubterms: isNatural(sel(x68:S,x69:S))->[]) 0.008/0.008 (rule: isNatural(0) -> tt, id: 52, possubterms: isNatural(0)->[]) 0.008/0.008 (rule: isNatural(s(x70:S)) -> U121(isNatural(x70:S)), id: 53, possubterms: isNatural(s(x70:S))->[]) 0.008/0.008 (rule: isPLNat(splitAt(x71:S,x72:S)) -> U151(isNatural(x71:S),x72:S), id: 54, possubterms: isPLNat(splitAt(x71:S,x72:S))->[]) 0.008/0.008 (rule: isPLNat(pair(x73:S,x74:S)) -> U141(isLNat(x73:S),x74:S), id: 55, possubterms: isPLNat(pair(x73:S,x74:S))->[]) 0.008/0.008 (rule: natsFrom(x75:S) -> U161(isNatural(x75:S),x75:S), id: 56, possubterms: natsFrom(x75:S)->[]) 0.008/0.008 (rule: sel(x76:S,x77:S) -> U171(isNatural(x76:S),x76:S,x77:S), id: 57, possubterms: sel(x76:S,x77:S)->[]) 0.008/0.008 (rule: snd(pair(x78:S,x79:S)) -> U181(isLNat(x78:S),x79:S), id: 58, possubterms: snd(pair(x78:S,x79:S))->[], pair(x78:S,x79:S)->[1]) 0.008/0.008 (rule: splitAt(0,x80:S) -> U191(isLNat(x80:S),x80:S), id: 59, possubterms: splitAt(0,x80:S)->[], 0->[1]) 0.008/0.008 (rule: splitAt(s(x81:S),cons(x82:S,x83:S)) -> U201(isNatural(x81:S),x81:S,x82:S,x83:S), id: 60, possubterms: splitAt(s(x81:S),cons(x82:S,x83:S))->[], s(x81:S)->[1], cons(x82:S,x83:S)->[2]) 0.008/0.008 (rule: tail(cons(x84:S,x85:S)) -> U211(isNatural(x84:S),x85:S), id: 61, possubterms: tail(cons(x84:S,x85:S))->[], cons(x84:S,x85:S)->[1]) 0.008/0.008 (rule: take(x86:S,x87:S) -> U221(isNatural(x86:S),x86:S,x87:S), id: 62, possubterms: take(x86:S,x87:S)->[]) 0.008/0.008 0.008/0.008 -> Unifications: 0.008/0.008 0.008/0.008 0.008/0.008 -> Critical pairs info: 0.008/0.008 => Not trivial, Not overlay, NW1, N1 0.008/0.008 => Not trivial, Not overlay, NW1, N2 0.008/0.008 => Not trivial, Not overlay, NW1, N3 0.008/0.008 => Not trivial, Not overlay, NW1, N4 0.008/0.008 => Not trivial, Not overlay, NW1, N5 0.008/0.008 => Not trivial, Not overlay, NW1, N6 0.008/0.008 => Not trivial, Not overlay, NW1, N7 0.008/0.008 => Not trivial, Not overlay, NW1, N8 0.008/0.008 => Not trivial, Not overlay, NW1, N9 0.008/0.008 => Not trivial, Not overlay, NW1, N10 0.008/0.008 => Not trivial, Not overlay, NW1, N11 0.008/0.008 => Not trivial, Not overlay, NW1, N12 0.008/0.008 => Not trivial, Not overlay, NW1, N13 0.008/0.008 => Not trivial, Not overlay, NW1, N14 0.008/0.008 => Not trivial, Not overlay, NW1, N15 0.008/0.008 => Not trivial, Not overlay, NW1, N16 0.008/0.008 => Not trivial, Not overlay, NW1, N17 0.008/0.008 => Not trivial, Not overlay, NW1, N18 0.008/0.008 => Not trivial, Not overlay, NW1, N19 0.008/0.008 => Not trivial, Not overlay, NW1, N20 0.008/0.008 => Not trivial, Not overlay, NW1, N21 0.008/0.008 => Not trivial, Not overlay, NW0, N22 0.008/0.008 => Not trivial, Not overlay, NW1, N23 0.008/0.008 => Not trivial, Not overlay, NW1, N24 0.008/0.008 => Not trivial, Not overlay, NW1, N25 0.008/0.008 => Not trivial, Not overlay, NW1, N26 0.008/0.008 => Not trivial, Not overlay, NW1, N27 0.008/0.008 => Not trivial, Not overlay, NW1, N28 0.008/0.008 => Not trivial, Not overlay, NW1, N29 0.008/0.008 => Not trivial, Not overlay, NW1, N30 0.008/0.008 => Not trivial, Not overlay, NW1, N31 0.008/0.008 => Not trivial, Not overlay, NW1, N32 0.008/0.008 => Not trivial, Not overlay, NW1, N33 0.008/0.008 => Not trivial, Not overlay, NW0, N34 0.008/0.008 => Not trivial, Not overlay, NW1, N35 0.008/0.008 => Not trivial, Not overlay, NW1, N36 0.008/0.008 => Not trivial, Not overlay, NW1, N37 0.008/0.008 => Not trivial, Not overlay, NW1, N38 0.008/0.008 => Not trivial, Not overlay, NW1, N39 0.008/0.008 => Not trivial, Not overlay, NW1, N40 0.008/0.008 => Not trivial, Not overlay, NW1, N41 0.008/0.008 => Not trivial, Not overlay, NW1, N42 0.008/0.008 => Not trivial, Not overlay, NW1, N43 0.008/0.008 => Not trivial, Not overlay, NW1, N44 0.008/0.008 => Not trivial, Not overlay, NW1, N45 0.008/0.008 => Not trivial, Not overlay, NW1, N46 0.008/0.008 => Not trivial, Not overlay, NW1, N47 0.008/0.008 => Not trivial, Not overlay, NW1, N48 0.008/0.008 => Not trivial, Not overlay, NW1, N49 0.008/0.008 => Not trivial, Not overlay, NW1, N50 0.008/0.008 => Not trivial, Not overlay, NW1, N51 0.008/0.008 => Not trivial, Not overlay, NW1, N52 0.008/0.008 => Not trivial, Not overlay, NW1, N53 0.008/0.008 => Not trivial, Not overlay, NW1, N54 0.008/0.008 => Not trivial, Not overlay, NW1, N55 0.008/0.008 => Not trivial, Not overlay, NW1, N56 0.008/0.008 => Not trivial, Not overlay, NW1, N57 0.008/0.008 => Not trivial, Not overlay, NW1, N58 0.008/0.008 => Not trivial, Not overlay, NW0, N59 0.008/0.008 => Not trivial, Not overlay, NW1, N60 0.008/0.008 => Not trivial, Not overlay, NW1, N61 0.008/0.008 => Not trivial, Not overlay, NW1, N62 0.008/0.008 => Not trivial, Not overlay, NW1, N63 0.008/0.008 => Not trivial, Not overlay, NW1, N64 0.008/0.008 => Not trivial, Not overlay, NW1, N65 0.008/0.008 => Not trivial, Not overlay, NW1, N66 0.008/0.008 => Not trivial, Not overlay, NW1, N67 0.008/0.008 => Not trivial, Not overlay, NW1, N68 0.008/0.008 => Not trivial, Not overlay, NW1, N69 0.008/0.008 => Not trivial, Not overlay, NW1, N70 0.008/0.008 => Not trivial, Not overlay, NW1, N71 0.008/0.008 => Not trivial, Not overlay, NW1, N72 0.008/0.008 => Not trivial, Not overlay, NW1, N73 0.008/0.008 => Not trivial, Not overlay, NW1, N74 0.008/0.008 => Not trivial, Not overlay, NW1, N75 0.008/0.008 => Not trivial, Not overlay, NW1, N76 0.008/0.008 => Not trivial, Not overlay, NW1, N77 0.008/0.008 => Not trivial, Not overlay, NW1, N78 0.008/0.008 => Not trivial, Not overlay, NW1, N79 0.008/0.008 => Not trivial, Not overlay, NW1, N80 0.008/0.008 => Not trivial, Not overlay, NW1, N81 0.008/0.008 => Not trivial, Not overlay, NW1, N82 0.008/0.008 => Not trivial, Not overlay, NW1, N83 0.008/0.008 => Not trivial, Not overlay, NW1, N84 0.008/0.008 => Not trivial, Not overlay, NW1, N85 0.008/0.008 => Not trivial, Not overlay, NW1, N86 0.008/0.008 => Not trivial, Not overlay, NW1, N87 0.008/0.008 => Not trivial, Not overlay, NW1, N88 0.008/0.008 => Not trivial, Not overlay, NW1, N89 0.008/0.008 => Not trivial, Not overlay, NW1, N90 0.008/0.008 => Not trivial, Not overlay, NW1, N91 0.008/0.008 => Not trivial, Not overlay, NW1, N92 0.008/0.008 => Not trivial, Not overlay, NW1, N93 0.008/0.008 => Not trivial, Not overlay, NW1, N94 0.008/0.008 => Not trivial, Not overlay, NW1, N95 0.008/0.008 => Not trivial, Not overlay, NW1, N96 0.008/0.008 => Not trivial, Not overlay, NW1, N97 0.008/0.008 => Not trivial, Not overlay, NW1, N98 0.008/0.008 => Not trivial, Not overlay, NW1, N99 0.008/0.008 => Not trivial, Not overlay, NW1, N100 0.008/0.008 => Not trivial, Not overlay, NW1, N101 0.008/0.008 => Not trivial, Not overlay, NW1, N102 0.008/0.008 => Not trivial, Not overlay, NW0, N103 0.008/0.008 => Not trivial, Not overlay, NW1, N104 0.008/0.008 => Not trivial, Not overlay, NW1, N105 0.008/0.008 => Not trivial, Not overlay, NW1, N106 0.008/0.008 => Not trivial, Not overlay, NW1, N107 0.008/0.008 => Not trivial, Not overlay, NW1, N108 0.008/0.008 => Not trivial, Not overlay, NW1, N109 0.008/0.008 => Not trivial, Not overlay, NW1, N110 0.008/0.008 => Not trivial, Not overlay, NW0, N111 0.008/0.008 => Not trivial, Not overlay, NW1, N112 0.008/0.008 => Not trivial, Not overlay, NW1, N113 0.008/0.008 => Not trivial, Not overlay, NW1, N114 0.008/0.008 => Not trivial, Not overlay, NW1, N115 0.008/0.008 => Not trivial, Not overlay, NW1, N116 0.008/0.008 => Not trivial, Not overlay, NW1, N117 0.008/0.008 => Not trivial, Not overlay, NW1, N118 0.008/0.008 => Not trivial, Not overlay, NW1, N119 0.008/0.008 => Not trivial, Not overlay, NW1, N120 0.008/0.008 => Not trivial, Not overlay, NW1, N121 0.008/0.008 => Not trivial, Not overlay, NW1, N122 0.008/0.008 => Not trivial, Not overlay, NW1, N123 0.008/0.008 => Not trivial, Not overlay, NW1, N124 0.008/0.008 => Not trivial, Not overlay, NW0, N125 0.008/0.008 => Not trivial, Not overlay, NW1, N126 0.008/0.008 => Not trivial, Not overlay, NW1, N127 0.008/0.008 => Not trivial, Not overlay, NW1, N128 0.008/0.008 => Not trivial, Not overlay, NW1, N129 0.008/0.008 => Not trivial, Not overlay, NW0, N130 0.008/0.008 => Not trivial, Not overlay, NW1, N131 0.008/0.008 => Not trivial, Not overlay, NW1, N132 0.008/0.008 => Not trivial, Not overlay, NW0, N133 0.008/0.008 => Not trivial, Not overlay, NW1, N134 0.008/0.008 => Not trivial, Not overlay, NW1, N135 0.008/0.008 => Not trivial, Not overlay, NW0, N136 0.008/0.008 => Not trivial, Not overlay, NW1, N137 0.008/0.008 => Not trivial, Not overlay, NW1, N138 0.008/0.008 0.008/0.008 -> Problem conclusions: 0.008/0.008 Left linear, Not right linear, Not linear 0.008/0.008 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.008/0.008 Not Huet-Levy confluent, Not Newman confluent 0.008/0.008 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.008/0.008 0.008/0.008 0.008/0.008 Problem 1: 0.008/0.008 No Convergence Brute Force Processor: 0.008/0.008 -> Rewritings: 0.008/0.008 s: U161(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))) 0.008/0.008 Nodes: [0] 0.008/0.008 Edges: [] 0.008/0.008 ID: 0 => ('U161(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)))', D0) 0.008/0.008 t: natsFrom(U211(isNatural(N:S),XS:S)) 0.008/0.008 Nodes: [0,1] 0.008/0.008 Edges: [(0,1)] 0.008/0.008 ID: 0 => ('natsFrom(U211(isNatural(N:S),XS:S))', D0) 0.008/0.008 ID: 1 => ('U161(isNatural(U211(isNatural(N:S),XS:S)),U211(isNatural(N:S),XS:S))', D1, R56, P[], S{x75:S -> U211(isNatural(N:S),XS:S)}), NR: 'U161(isNatural(U211(isNatural(N:S),XS:S)),U211(isNatural(N:S),XS:S))' 0.008/0.008 U161(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))) ->* no union *<- natsFrom(U211(isNatural(N:S),XS:S)) 0.008/0.008 "Not joinable" 0.008/0.008 0.008/0.008 The problem is not joinable. 0.008/0.008 0.06user 0.01system 0:00.08elapsed 93%CPU (0avgtext+0avgdata 22304maxresident)k 0.008/0.008 0inputs+0outputs (0major+3763minor)pagefaults 0swaps