NO 0.19/0.25 NO 0.19/0.25 0.19/0.25 Problem: 0.19/0.25 U14(tt()) -> snd(splitAt(N,XS)) 0.19/0.25 U24(tt()) -> X 0.19/0.25 U282(tt()) -> cons(N) 0.19/0.25 U294(tt()) -> head(afterNth(N,XS)) 0.19/0.25 U304(tt()) -> Y 0.19/0.25 U312(tt()) -> pair(nil(),XS) 0.19/0.25 U326(tt()) -> U327(splitAt(N,XS)) 0.19/0.25 U327(pair(YS,ZS)) -> pair(cons(X),ZS) 0.19/0.25 U334(tt()) -> XS 0.19/0.25 U34(tt()) -> N 0.19/0.25 U344(tt()) -> fst(splitAt(N,XS)) 0.19/0.25 U101(tt()) -> U102(isNaturalKind()) 0.19/0.25 U102(tt()) -> U103(isLNatKind()) 0.19/0.25 U103(tt()) -> U104(isLNatKind()) 0.19/0.25 U104(tt()) -> U105(isNatural()) 0.19/0.25 U105(tt()) -> U106(isLNat()) 0.19/0.25 U106(tt()) -> tt() 0.19/0.25 U11(tt()) -> U12(isNaturalKind()) 0.19/0.25 U111(tt()) -> U112(isLNatKind()) 0.19/0.25 U112(tt()) -> tt() 0.19/0.25 U12(tt()) -> U13(isLNat()) 0.19/0.25 U121(tt()) -> U122(isLNatKind()) 0.19/0.25 U122(tt()) -> tt() 0.19/0.25 U13(tt()) -> U14(isLNatKind()) 0.19/0.25 U131(tt()) -> tt() 0.19/0.25 U141(tt()) -> tt() 0.19/0.25 U151(tt()) -> tt() 0.19/0.25 U161(tt()) -> tt() 0.19/0.25 U171(tt()) -> U172(isLNatKind()) 0.19/0.25 U172(tt()) -> tt() 0.19/0.25 U181(tt()) -> U182(isLNatKind()) 0.19/0.25 U182(tt()) -> U183(isLNat()) 0.19/0.25 U183(tt()) -> tt() 0.19/0.25 U191(tt()) -> U192(isNaturalKind()) 0.19/0.25 U192(tt()) -> U193(isNatural()) 0.19/0.25 U193(tt()) -> tt() 0.19/0.25 U201(tt()) -> U202(isNaturalKind()) 0.19/0.25 U202(tt()) -> U203(isLNatKind()) 0.19/0.25 U203(tt()) -> U204(isLNatKind()) 0.19/0.25 U204(tt()) -> U205(isNatural()) 0.19/0.25 U205(tt()) -> U206(isLNat()) 0.19/0.25 U206(tt()) -> tt() 0.19/0.25 U21(tt()) -> U22(isLNatKind()) 0.19/0.25 U211(tt()) -> tt() 0.19/0.25 U22(tt()) -> U23(isLNat()) 0.19/0.25 U221(tt()) -> tt() 0.19/0.25 U23(tt()) -> U24(isLNatKind()) 0.19/0.25 U231(tt()) -> U232(isLNatKind()) 0.19/0.25 U232(tt()) -> tt() 0.19/0.25 U241(tt()) -> U242(isLNatKind()) 0.19/0.25 U242(tt()) -> U243(isLNatKind()) 0.19/0.25 U243(tt()) -> U244(isLNatKind()) 0.19/0.25 U244(tt()) -> U245(isLNat()) 0.19/0.25 U245(tt()) -> U246(isLNat()) 0.19/0.25 U246(tt()) -> tt() 0.19/0.25 U251(tt()) -> U252(isNaturalKind()) 0.19/0.25 U252(tt()) -> U253(isLNatKind()) 0.19/0.25 U253(tt()) -> U254(isLNatKind()) 0.19/0.25 U254(tt()) -> U255(isNatural()) 0.19/0.25 U255(tt()) -> U256(isLNat()) 0.19/0.25 U256(tt()) -> tt() 0.19/0.25 U261(tt()) -> U262(isLNatKind()) 0.19/0.25 U262(tt()) -> tt() 0.19/0.25 U271(tt()) -> U272(isLNatKind()) 0.19/0.25 U272(tt()) -> tt() 0.19/0.25 U281(tt()) -> U282(isNaturalKind()) 0.19/0.25 U291(tt()) -> U292(isNaturalKind()) 0.19/0.25 U292(tt()) -> U293(isLNat()) 0.19/0.25 U293(tt()) -> U294(isLNatKind()) 0.19/0.25 U301(tt()) -> U302(isLNatKind()) 0.19/0.25 U302(tt()) -> U303(isLNat()) 0.19/0.25 U303(tt()) -> U304(isLNatKind()) 0.19/0.25 U31(tt()) -> U32(isNaturalKind()) 0.19/0.25 U311(tt()) -> U312(isLNatKind()) 0.19/0.25 U32(tt()) -> U33(isLNat()) 0.19/0.25 U321(tt()) -> U322(isNaturalKind()) 0.19/0.25 U322(tt()) -> U323(isNatural()) 0.19/0.25 U323(tt()) -> U324(isNaturalKind()) 0.19/0.25 U324(tt()) -> U325(isLNat()) 0.19/0.25 U325(tt()) -> U326(isLNatKind()) 0.19/0.25 U33(tt()) -> U34(isLNatKind()) 0.19/0.25 U331(tt()) -> U332(isNaturalKind()) 0.19/0.25 U332(tt()) -> U333(isLNat()) 0.19/0.25 U333(tt()) -> U334(isLNatKind()) 0.19/0.25 U341(tt()) -> U342(isNaturalKind()) 0.19/0.25 U342(tt()) -> U343(isLNat()) 0.19/0.25 U343(tt()) -> U344(isLNatKind()) 0.19/0.25 U41(tt()) -> U42(isNaturalKind()) 0.19/0.25 U42(tt()) -> U43(isLNatKind()) 0.19/0.25 U43(tt()) -> U44(isLNatKind()) 0.19/0.25 U44(tt()) -> U45(isNatural()) 0.19/0.25 U45(tt()) -> U46(isLNat()) 0.19/0.25 U46(tt()) -> tt() 0.19/0.25 U51(tt()) -> U52(isNaturalKind()) 0.19/0.25 U52(tt()) -> U53(isLNatKind()) 0.19/0.25 U53(tt()) -> U54(isLNatKind()) 0.19/0.25 U54(tt()) -> U55(isNatural()) 0.19/0.25 U55(tt()) -> U56(isLNat()) 0.19/0.25 U56(tt()) -> tt() 0.19/0.25 U61(tt()) -> U62(isPLNatKind()) 0.19/0.25 U62(tt()) -> U63(isPLNat()) 0.19/0.25 U63(tt()) -> tt() 0.19/0.25 U71(tt()) -> U72(isNaturalKind()) 0.19/0.25 U72(tt()) -> U73(isNatural()) 0.19/0.25 U73(tt()) -> tt() 0.19/0.25 U81(tt()) -> U82(isPLNatKind()) 0.19/0.25 U82(tt()) -> U83(isPLNat()) 0.19/0.25 U83(tt()) -> tt() 0.19/0.25 U91(tt()) -> U92(isLNatKind()) 0.19/0.25 U92(tt()) -> U93(isLNat()) 0.19/0.25 U93(tt()) -> tt() 0.19/0.25 afterNth(N,XS) -> U11(isNatural()) 0.19/0.25 fst(pair(X,Y)) -> U21(isLNat()) 0.19/0.25 head(cons(N)) -> U31(isNatural()) 0.19/0.25 isLNat() -> tt() 0.19/0.25 isLNat() -> U41(isNaturalKind()) 0.19/0.25 isLNat() -> U51(isNaturalKind()) 0.19/0.25 isLNat() -> U61(isPLNatKind()) 0.19/0.25 isLNat() -> U71(isNaturalKind()) 0.19/0.25 isLNat() -> U81(isPLNatKind()) 0.19/0.25 isLNat() -> U91(isLNatKind()) 0.19/0.25 isLNat() -> U101(isNaturalKind()) 0.19/0.25 isLNatKind() -> tt() 0.19/0.25 isLNatKind() -> U111(isNaturalKind()) 0.19/0.25 isLNatKind() -> U121(isNaturalKind()) 0.19/0.25 isLNatKind() -> U131(isPLNatKind()) 0.19/0.25 isLNatKind() -> U141(isNaturalKind()) 0.19/0.25 isLNatKind() -> U151(isPLNatKind()) 0.19/0.25 isLNatKind() -> U161(isLNatKind()) 0.19/0.25 isLNatKind() -> U171(isNaturalKind()) 0.19/0.25 isNatural() -> tt() 0.19/0.25 isNatural() -> U181(isLNatKind()) 0.19/0.25 isNatural() -> U191(isNaturalKind()) 0.19/0.25 isNatural() -> U201(isNaturalKind()) 0.19/0.25 isNaturalKind() -> tt() 0.19/0.25 isNaturalKind() -> U211(isLNatKind()) 0.19/0.25 isNaturalKind() -> U221(isNaturalKind()) 0.19/0.25 isNaturalKind() -> U231(isNaturalKind()) 0.19/0.25 isPLNat() -> U241(isLNatKind()) 0.19/0.25 isPLNat() -> U251(isNaturalKind()) 0.19/0.25 isPLNatKind() -> U261(isLNatKind()) 0.19/0.25 isPLNatKind() -> U271(isNaturalKind()) 0.19/0.25 natsFrom(N) -> U281(isNatural()) 0.19/0.25 sel(N,XS) -> U291(isNatural()) 0.19/0.25 snd(pair(X,Y)) -> U301(isLNat()) 0.19/0.25 splitAt(0(),XS) -> U311(isLNat()) 0.19/0.25 splitAt(s(N),cons(X)) -> U321(isNatural()) 0.19/0.25 tail(cons(N)) -> U331(isNatural()) 0.19/0.25 take(N,XS) -> U341(isNatural()) 0.19/0.25 0.19/0.25 Proof: 0.19/0.25 Fresh Variable Processor: 0.19/0.25 loop length: 1 0.19/0.25 terms: 0.19/0.25 U14(tt()) 0.19/0.25 context: snd(splitAt([],XS)) 0.19/0.25 substitution: 0.19/0.25 N -> U14(tt()) 0.19/0.25 Qed 0.19/0.26 EOF