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