MAYBE
976.21/297.17	MAYBE
976.21/297.17	
976.21/297.17	We are left with following problem, upon which TcT provides the
976.21/297.17	certificate MAYBE.
976.21/297.17	
976.21/297.17	Strict Trs:
976.21/297.17	  { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2))
976.21/297.17	  , U102(tt(), V2) -> U103(isLNat(activate(V2)))
976.21/297.17	  , isNatural(n__0()) -> tt()
976.21/297.17	  , isNatural(n__head(V1)) ->
976.21/297.17	    U111(isLNatKind(activate(V1)), activate(V1))
976.21/297.17	  , isNatural(n__s(V1)) ->
976.21/297.17	    U121(isNaturalKind(activate(V1)), activate(V1))
976.21/297.17	  , isNatural(n__sel(V1, V2)) ->
976.21/297.17	    U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.17	         activate(V1),
976.21/297.17	         activate(V2))
976.21/297.17	  , activate(X) -> X
976.21/297.17	  , activate(n__natsFrom(X)) -> natsFrom(X)
976.21/297.17	  , activate(n__isNaturalKind(X)) -> isNaturalKind(X)
976.21/297.17	  , activate(n__and(X1, X2)) -> and(X1, X2)
976.21/297.17	  , activate(n__isLNatKind(X)) -> isLNatKind(X)
976.21/297.17	  , activate(n__nil()) -> nil()
976.21/297.17	  , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
976.21/297.17	  , activate(n__cons(X1, X2)) -> cons(X1, X2)
976.21/297.17	  , activate(n__fst(X)) -> fst(X)
976.21/297.17	  , activate(n__snd(X)) -> snd(X)
976.21/297.17	  , activate(n__tail(X)) -> tail(X)
976.21/297.17	  , activate(n__take(X1, X2)) -> take(X1, X2)
976.21/297.17	  , activate(n__0()) -> 0()
976.21/297.17	  , activate(n__head(X)) -> head(X)
976.21/297.17	  , activate(n__s(X)) -> s(X)
976.21/297.17	  , activate(n__sel(X1, X2)) -> sel(X1, X2)
976.21/297.17	  , activate(n__pair(X1, X2)) -> pair(X1, X2)
976.21/297.17	  , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
976.21/297.17	  , U103(tt()) -> tt()
976.21/297.17	  , isLNat(n__natsFrom(V1)) ->
976.21/297.17	    U71(isNaturalKind(activate(V1)), activate(V1))
976.21/297.17	  , isLNat(n__nil()) -> tt()
976.21/297.17	  , isLNat(n__afterNth(V1, V2)) ->
976.21/297.17	    U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.17	        activate(V1),
976.21/297.17	        activate(V2))
976.21/297.17	  , isLNat(n__cons(V1, V2)) ->
976.21/297.17	    U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.17	        activate(V1),
976.21/297.17	        activate(V2))
976.21/297.17	  , isLNat(n__fst(V1)) ->
976.21/297.17	    U61(isPLNatKind(activate(V1)), activate(V1))
976.21/297.17	  , isLNat(n__snd(V1)) ->
976.21/297.17	    U81(isPLNatKind(activate(V1)), activate(V1))
976.21/297.17	  , isLNat(n__tail(V1)) ->
976.21/297.17	    U91(isLNatKind(activate(V1)), activate(V1))
976.21/297.17	  , isLNat(n__take(V1, V2)) ->
976.21/297.17	    U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.17	         activate(V1),
976.21/297.17	         activate(V2))
976.21/297.17	  , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
976.21/297.17	  , snd(X) -> n__snd(X)
976.21/297.17	  , snd(pair(X, Y)) ->
976.21/297.17	    U181(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.17	             n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.17	         Y)
976.21/297.17	  , splitAt(X1, X2) -> n__splitAt(X1, X2)
976.21/297.17	  , splitAt(s(N), cons(X, XS)) ->
976.21/297.17	    U201(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	             n__and(and(isNatural(X), n__isNaturalKind(X)),
976.21/297.17	                    n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.21/297.17	         N,
976.21/297.17	         X,
976.21/297.17	         activate(XS))
976.21/297.17	  , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
976.21/297.17	  , U111(tt(), V1) -> U112(isLNat(activate(V1)))
976.21/297.17	  , U112(tt()) -> tt()
976.21/297.17	  , U121(tt(), V1) -> U122(isNatural(activate(V1)))
976.21/297.17	  , U122(tt()) -> tt()
976.21/297.17	  , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2))
976.21/297.17	  , U132(tt(), V2) -> U133(isLNat(activate(V2)))
976.21/297.17	  , U133(tt()) -> tt()
976.21/297.17	  , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2))
976.21/297.17	  , U142(tt(), V2) -> U143(isLNat(activate(V2)))
976.21/297.17	  , U143(tt()) -> tt()
976.21/297.17	  , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2))
976.21/297.17	  , U152(tt(), V2) -> U153(isLNat(activate(V2)))
976.21/297.17	  , U153(tt()) -> tt()
976.21/297.17	  , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
976.21/297.17	  , cons(X1, X2) -> n__cons(X1, X2)
976.21/297.17	  , s(X) -> n__s(X)
976.21/297.17	  , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
976.21/297.17	  , head(X) -> n__head(X)
976.21/297.17	  , head(cons(N, XS)) ->
976.21/297.17	    U31(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	            n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.17	        N)
976.21/297.17	  , afterNth(N, XS) ->
976.21/297.17	    U11(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	            n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.17	        N,
976.21/297.17	        XS)
976.21/297.17	  , afterNth(X1, X2) -> n__afterNth(X1, X2)
976.21/297.17	  , U181(tt(), Y) -> activate(Y)
976.21/297.17	  , U191(tt(), XS) -> pair(nil(), activate(XS))
976.21/297.17	  , pair(X1, X2) -> n__pair(X1, X2)
976.21/297.17	  , nil() -> n__nil()
976.21/297.17	  , U201(tt(), N, X, XS) ->
976.21/297.17	    U202(splitAt(activate(N), activate(XS)), activate(X))
976.21/297.17	  , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
976.21/297.17	  , U21(tt(), X) -> activate(X)
976.21/297.17	  , U211(tt(), XS) -> activate(XS)
976.21/297.17	  , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
976.21/297.17	  , fst(X) -> n__fst(X)
976.21/297.17	  , fst(pair(X, Y)) ->
976.21/297.17	    U21(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.17	            n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.17	        X)
976.21/297.17	  , U31(tt(), N) -> activate(N)
976.21/297.17	  , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2))
976.21/297.17	  , U42(tt(), V2) -> U43(isLNat(activate(V2)))
976.21/297.17	  , U43(tt()) -> tt()
976.21/297.17	  , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2))
976.21/297.17	  , U52(tt(), V2) -> U53(isLNat(activate(V2)))
976.21/297.17	  , U53(tt()) -> tt()
976.21/297.17	  , U61(tt(), V1) -> U62(isPLNat(activate(V1)))
976.21/297.17	  , U62(tt()) -> tt()
976.21/297.17	  , isPLNat(n__pair(V1, V2)) ->
976.21/297.17	    U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.17	         activate(V1),
976.21/297.17	         activate(V2))
976.21/297.17	  , isPLNat(n__splitAt(V1, V2)) ->
976.21/297.17	    U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.17	         activate(V1),
976.21/297.17	         activate(V2))
976.21/297.17	  , U71(tt(), V1) -> U72(isNatural(activate(V1)))
976.21/297.17	  , U72(tt()) -> tt()
976.21/297.17	  , U81(tt(), V1) -> U82(isPLNat(activate(V1)))
976.21/297.17	  , U82(tt()) -> tt()
976.21/297.17	  , U91(tt(), V1) -> U92(isLNat(activate(V1)))
976.21/297.17	  , U92(tt()) -> tt()
976.21/297.17	  , and(X1, X2) -> n__and(X1, X2)
976.21/297.17	  , and(tt(), X) -> activate(X)
976.21/297.17	  , isNaturalKind(X) -> n__isNaturalKind(X)
976.21/297.17	  , isNaturalKind(n__0()) -> tt()
976.21/297.17	  , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
976.21/297.17	  , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
976.21/297.17	  , isNaturalKind(n__sel(V1, V2)) ->
976.21/297.17	    and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.17	  , isPLNatKind(n__pair(V1, V2)) ->
976.21/297.17	    and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.17	  , isPLNatKind(n__splitAt(V1, V2)) ->
976.21/297.17	    and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.17	  , isLNatKind(X) -> n__isLNatKind(X)
976.21/297.17	  , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
976.21/297.17	  , isLNatKind(n__nil()) -> tt()
976.21/297.17	  , isLNatKind(n__afterNth(V1, V2)) ->
976.21/297.17	    and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.17	  , isLNatKind(n__cons(V1, V2)) ->
976.21/297.17	    and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.17	  , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
976.21/297.17	  , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
976.21/297.17	  , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
976.21/297.17	  , isLNatKind(n__take(V1, V2)) ->
976.21/297.17	    and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.17	  , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N)
976.21/297.17	  , natsFrom(X) -> n__natsFrom(X)
976.21/297.17	  , sel(N, XS) ->
976.21/297.17	    U171(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	             n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.17	         N,
976.21/297.17	         XS)
976.21/297.17	  , sel(X1, X2) -> n__sel(X1, X2)
976.21/297.17	  , 0() -> n__0()
976.21/297.17	  , tail(X) -> n__tail(X)
976.21/297.17	  , tail(cons(N, XS)) ->
976.21/297.17	    U211(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	             n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.17	         activate(XS))
976.21/297.17	  , take(N, XS) ->
976.21/297.17	    U221(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	             n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.17	         N,
976.21/297.17	         XS)
976.21/297.17	  , take(X1, X2) -> n__take(X1, X2) }
976.21/297.17	Obligation:
976.21/297.17	  runtime complexity
976.21/297.17	Answer:
976.21/297.17	  MAYBE
976.21/297.17	
976.21/297.17	None of the processors succeeded.
976.21/297.17	
976.21/297.17	Details of failed attempt(s):
976.21/297.17	-----------------------------
976.21/297.17	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
976.21/297.17	   following reason:
976.21/297.17	   
976.21/297.17	   Computation stopped due to timeout after 297.0 seconds.
976.21/297.17	
976.21/297.17	2) 'Best' failed due to the following reason:
976.21/297.17	   
976.21/297.17	   None of the processors succeeded.
976.21/297.17	   
976.21/297.17	   Details of failed attempt(s):
976.21/297.17	   -----------------------------
976.21/297.17	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
976.21/297.17	      seconds)' failed due to the following reason:
976.21/297.17	      
976.21/297.17	      Computation stopped due to timeout after 148.0 seconds.
976.21/297.17	   
976.21/297.17	   2) 'Best' failed due to the following reason:
976.21/297.17	      
976.21/297.17	      None of the processors succeeded.
976.21/297.17	      
976.21/297.17	      Details of failed attempt(s):
976.21/297.17	      -----------------------------
976.21/297.17	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
976.21/297.17	         following reason:
976.21/297.17	         
976.21/297.17	         The processor is inapplicable, reason:
976.21/297.17	           Processor only applicable for innermost runtime complexity analysis
976.21/297.17	      
976.21/297.17	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
976.21/297.17	         to the following reason:
976.21/297.17	         
976.21/297.17	         The processor is inapplicable, reason:
976.21/297.17	           Processor only applicable for innermost runtime complexity analysis
976.21/297.17	      
976.21/297.17	   
976.21/297.17	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
976.21/297.17	      failed due to the following reason:
976.21/297.17	      
976.21/297.17	      None of the processors succeeded.
976.21/297.17	      
976.21/297.17	      Details of failed attempt(s):
976.21/297.17	      -----------------------------
976.21/297.17	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
976.21/297.17	         failed due to the following reason:
976.21/297.17	         
976.21/297.17	         match-boundness of the problem could not be verified.
976.21/297.17	      
976.21/297.17	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
976.21/297.17	         failed due to the following reason:
976.21/297.17	         
976.21/297.17	         match-boundness of the problem could not be verified.
976.21/297.17	      
976.21/297.17	   
976.21/297.17	
976.21/297.17	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
976.21/297.17	   the following reason:
976.21/297.17	   
976.21/297.17	   We add the following weak dependency pairs:
976.21/297.17	   
976.21/297.17	   Strict DPs:
976.21/297.17	     { U101^#(tt(), V1, V2) ->
976.21/297.17	       c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.21/297.17	     , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.21/297.17	     , U103^#(tt()) -> c_25()
976.21/297.17	     , isNatural^#(n__0()) -> c_3()
976.21/297.17	     , isNatural^#(n__head(V1)) ->
976.21/297.17	       c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.17	     , isNatural^#(n__s(V1)) ->
976.21/297.17	       c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.17	     , isNatural^#(n__sel(V1, V2)) ->
976.21/297.17	       c_6(U131^#(and(isNaturalKind(activate(V1)),
976.21/297.17	                      n__isLNatKind(activate(V2))),
976.21/297.17	                  activate(V1),
976.21/297.17	                  activate(V2)))
976.21/297.17	     , U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.21/297.17	     , U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.21/297.17	     , U131^#(tt(), V1, V2) ->
976.21/297.17	       c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.21/297.17	     , activate^#(X) -> c_7(X)
976.21/297.17	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.21/297.17	     , activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.21/297.17	     , activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.21/297.17	     , activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.21/297.17	     , activate^#(n__nil()) -> c_12(nil^#())
976.21/297.17	     , activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.21/297.17	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.21/297.17	     , activate^#(n__fst(X)) -> c_15(fst^#(X))
976.21/297.17	     , activate^#(n__snd(X)) -> c_16(snd^#(X))
976.21/297.17	     , activate^#(n__tail(X)) -> c_17(tail^#(X))
976.21/297.17	     , activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.21/297.17	     , activate^#(n__0()) -> c_19(0^#())
976.21/297.17	     , activate^#(n__head(X)) -> c_20(head^#(X))
976.21/297.17	     , activate^#(n__s(X)) -> c_21(s^#(X))
976.21/297.17	     , activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.21/297.17	     , activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.21/297.17	     , activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.21/297.17	     , natsFrom^#(N) ->
976.21/297.17	       c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.21/297.17	     , natsFrom^#(X) -> c_108(X)
976.21/297.17	     , isNaturalKind^#(X) -> c_91(X)
976.21/297.17	     , isNaturalKind^#(n__0()) -> c_92()
976.21/297.17	     , isNaturalKind^#(n__head(V1)) -> c_93(isLNatKind^#(activate(V1)))
976.21/297.17	     , isNaturalKind^#(n__s(V1)) -> c_94(isNaturalKind^#(activate(V1)))
976.21/297.17	     , isNaturalKind^#(n__sel(V1, V2)) ->
976.21/297.17	       c_95(and^#(isNaturalKind(activate(V1)),
976.21/297.17	                  n__isLNatKind(activate(V2))))
976.21/297.17	     , and^#(X1, X2) -> c_89(X1, X2)
976.21/297.17	     , and^#(tt(), X) -> c_90(activate^#(X))
976.21/297.17	     , isLNatKind^#(X) -> c_98(X)
976.21/297.17	     , isLNatKind^#(n__natsFrom(V1)) ->
976.21/297.17	       c_99(isNaturalKind^#(activate(V1)))
976.21/297.17	     , isLNatKind^#(n__nil()) -> c_100()
976.21/297.17	     , isLNatKind^#(n__afterNth(V1, V2)) ->
976.21/297.17	       c_101(and^#(isNaturalKind(activate(V1)),
976.21/297.17	                   n__isLNatKind(activate(V2))))
976.21/297.17	     , isLNatKind^#(n__cons(V1, V2)) ->
976.21/297.17	       c_102(and^#(isNaturalKind(activate(V1)),
976.21/297.17	                   n__isLNatKind(activate(V2))))
976.21/297.17	     , isLNatKind^#(n__fst(V1)) -> c_103(isPLNatKind^#(activate(V1)))
976.21/297.17	     , isLNatKind^#(n__snd(V1)) -> c_104(isPLNatKind^#(activate(V1)))
976.21/297.17	     , isLNatKind^#(n__tail(V1)) -> c_105(isLNatKind^#(activate(V1)))
976.21/297.17	     , isLNatKind^#(n__take(V1, V2)) ->
976.21/297.17	       c_106(and^#(isNaturalKind(activate(V1)),
976.21/297.17	                   n__isLNatKind(activate(V2))))
976.21/297.17	     , nil^#() -> c_64()
976.21/297.17	     , afterNth^#(N, XS) ->
976.21/297.17	       c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	                      n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.17	                  N,
976.21/297.17	                  XS))
976.21/297.17	     , afterNth^#(X1, X2) -> c_60(X1, X2)
976.21/297.17	     , cons^#(X1, X2) -> c_54(X1, X2)
976.21/297.17	     , fst^#(X) -> c_70(X)
976.21/297.17	     , fst^#(pair(X, Y)) ->
976.21/297.17	       c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.17	                      n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.17	                  X))
976.21/297.17	     , snd^#(X) -> c_35(X)
976.21/297.17	     , snd^#(pair(X, Y)) ->
976.21/297.17	       c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.17	                       n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.17	                   Y))
976.21/297.17	     , tail^#(X) -> c_112(X)
976.21/297.17	     , tail^#(cons(N, XS)) ->
976.21/297.17	       c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	                        n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.17	                    activate(XS)))
976.21/297.17	     , take^#(N, XS) ->
976.21/297.17	       c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.17	                    N,
976.21/297.17	                    XS))
976.21/297.17	     , take^#(X1, X2) -> c_115(X1, X2)
976.21/297.17	     , 0^#() -> c_111()
976.21/297.17	     , head^#(X) -> c_57(X)
976.21/297.17	     , head^#(cons(N, XS)) ->
976.21/297.17	       c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	                      n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.17	                  N))
976.21/297.17	     , s^#(X) -> c_55(X)
976.21/297.17	     , sel^#(N, XS) ->
976.21/297.17	       c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.17	                    N,
976.21/297.17	                    XS))
976.21/297.17	     , sel^#(X1, X2) -> c_110(X1, X2)
976.21/297.17	     , pair^#(X1, X2) -> c_63(X1, X2)
976.21/297.17	     , splitAt^#(X1, X2) -> c_37(X1, X2)
976.21/297.17	     , splitAt^#(s(N), cons(X, XS)) ->
976.21/297.17	       c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.17	                       n__and(and(isNatural(X), n__isNaturalKind(X)),
976.21/297.17	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.21/297.17	                   N,
976.21/297.17	                   X,
976.21/297.17	                   activate(XS)))
976.21/297.17	     , splitAt^#(0(), XS) ->
976.21/297.17	       c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.21/297.17	     , isLNat^#(n__natsFrom(V1)) ->
976.21/297.17	       c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.17	     , isLNat^#(n__nil()) -> c_27()
976.21/297.17	     , isLNat^#(n__afterNth(V1, V2)) ->
976.21/297.17	       c_28(U41^#(and(isNaturalKind(activate(V1)),
976.21/297.17	                      n__isLNatKind(activate(V2))),
976.21/297.17	                  activate(V1),
976.21/297.17	                  activate(V2)))
976.21/297.17	     , isLNat^#(n__cons(V1, V2)) ->
976.21/297.17	       c_29(U51^#(and(isNaturalKind(activate(V1)),
976.21/297.17	                      n__isLNatKind(activate(V2))),
976.21/297.17	                  activate(V1),
976.21/297.17	                  activate(V2)))
976.21/297.17	     , isLNat^#(n__fst(V1)) ->
976.21/297.17	       c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.17	     , isLNat^#(n__snd(V1)) ->
976.21/297.17	       c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.17	     , isLNat^#(n__tail(V1)) ->
976.21/297.17	       c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.17	     , isLNat^#(n__take(V1, V2)) ->
976.21/297.17	       c_33(U101^#(and(isNaturalKind(activate(V1)),
976.21/297.17	                       n__isLNatKind(activate(V2))),
976.21/297.17	                   activate(V1),
976.21/297.17	                   activate(V2)))
976.21/297.17	     , U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.21/297.17	     , U41^#(tt(), V1, V2) ->
976.21/297.17	       c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.21/297.17	     , U51^#(tt(), V1, V2) ->
976.21/297.17	       c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.21/297.17	     , U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.21/297.17	     , U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.21/297.17	     , U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.21/297.17	     , U11^#(tt(), N, XS) ->
976.21/297.17	       c_34(snd^#(splitAt(activate(N), activate(XS))))
976.21/297.17	     , U181^#(tt(), Y) -> c_61(activate^#(Y))
976.21/297.17	     , U201^#(tt(), N, X, XS) ->
976.21/297.18	       c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.21/297.18	     , U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.21/297.18	     , U112^#(tt()) -> c_41()
976.21/297.18	     , U122^#(tt()) -> c_43()
976.21/297.18	     , U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.21/297.18	     , U133^#(tt()) -> c_46()
976.21/297.18	     , U141^#(tt(), V1, V2) ->
976.21/297.18	       c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.21/297.18	     , U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.21/297.18	     , U143^#(tt()) -> c_49()
976.21/297.18	     , U151^#(tt(), V1, V2) ->
976.21/297.18	       c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.21/297.18	     , U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.21/297.18	     , U153^#(tt()) -> c_52()
976.21/297.18	     , U161^#(tt(), N) ->
976.21/297.18	       c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.21/297.18	     , U171^#(tt(), N, XS) ->
976.21/297.18	       c_56(head^#(afterNth(activate(N), activate(XS))))
976.21/297.18	     , U31^#(tt(), N) -> c_72(activate^#(N))
976.21/297.18	     , U202^#(pair(YS, ZS), X) ->
976.21/297.18	       c_66(pair^#(cons(activate(X), YS), ZS))
976.21/297.18	     , U21^#(tt(), X) -> c_67(activate^#(X))
976.21/297.18	     , U211^#(tt(), XS) -> c_68(activate^#(XS))
976.21/297.18	     , U221^#(tt(), N, XS) ->
976.21/297.18	       c_69(fst^#(splitAt(activate(N), activate(XS))))
976.21/297.18	     , U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.21/297.18	     , U43^#(tt()) -> c_75()
976.21/297.18	     , U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.21/297.18	     , U53^#(tt()) -> c_78()
976.21/297.18	     , U62^#(tt()) -> c_80()
976.21/297.18	     , isPLNat^#(n__pair(V1, V2)) ->
976.21/297.18	       c_81(U141^#(and(isLNatKind(activate(V1)),
976.21/297.18	                       n__isLNatKind(activate(V2))),
976.21/297.18	                   activate(V1),
976.21/297.18	                   activate(V2)))
976.21/297.18	     , isPLNat^#(n__splitAt(V1, V2)) ->
976.21/297.18	       c_82(U151^#(and(isNaturalKind(activate(V1)),
976.21/297.18	                       n__isLNatKind(activate(V2))),
976.21/297.18	                   activate(V1),
976.21/297.18	                   activate(V2)))
976.21/297.18	     , U72^#(tt()) -> c_84()
976.21/297.18	     , U82^#(tt()) -> c_86()
976.21/297.18	     , U92^#(tt()) -> c_88()
976.21/297.18	     , isPLNatKind^#(n__pair(V1, V2)) ->
976.21/297.18	       c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.21/297.18	     , isPLNatKind^#(n__splitAt(V1, V2)) ->
976.21/297.18	       c_97(and^#(isNaturalKind(activate(V1)),
976.21/297.18	                  n__isLNatKind(activate(V2)))) }
976.21/297.18	   
976.21/297.18	   and mark the set of starting terms.
976.21/297.18	   
976.21/297.18	   We are left with following problem, upon which TcT provides the
976.21/297.18	   certificate MAYBE.
976.21/297.18	   
976.21/297.18	   Strict DPs:
976.21/297.18	     { U101^#(tt(), V1, V2) ->
976.21/297.18	       c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.21/297.18	     , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.21/297.18	     , U103^#(tt()) -> c_25()
976.21/297.18	     , isNatural^#(n__0()) -> c_3()
976.21/297.18	     , isNatural^#(n__head(V1)) ->
976.21/297.18	       c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.18	     , isNatural^#(n__s(V1)) ->
976.21/297.18	       c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.18	     , isNatural^#(n__sel(V1, V2)) ->
976.21/297.18	       c_6(U131^#(and(isNaturalKind(activate(V1)),
976.21/297.18	                      n__isLNatKind(activate(V2))),
976.21/297.18	                  activate(V1),
976.21/297.18	                  activate(V2)))
976.21/297.18	     , U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.21/297.18	     , U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.21/297.18	     , U131^#(tt(), V1, V2) ->
976.21/297.18	       c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.21/297.18	     , activate^#(X) -> c_7(X)
976.21/297.18	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.21/297.18	     , activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.21/297.18	     , activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.21/297.18	     , activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.21/297.18	     , activate^#(n__nil()) -> c_12(nil^#())
976.21/297.18	     , activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.21/297.18	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.21/297.18	     , activate^#(n__fst(X)) -> c_15(fst^#(X))
976.21/297.18	     , activate^#(n__snd(X)) -> c_16(snd^#(X))
976.21/297.18	     , activate^#(n__tail(X)) -> c_17(tail^#(X))
976.21/297.18	     , activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.21/297.18	     , activate^#(n__0()) -> c_19(0^#())
976.21/297.18	     , activate^#(n__head(X)) -> c_20(head^#(X))
976.21/297.18	     , activate^#(n__s(X)) -> c_21(s^#(X))
976.21/297.18	     , activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.21/297.18	     , activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.21/297.18	     , activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.21/297.18	     , natsFrom^#(N) ->
976.21/297.18	       c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.21/297.18	     , natsFrom^#(X) -> c_108(X)
976.21/297.18	     , isNaturalKind^#(X) -> c_91(X)
976.21/297.18	     , isNaturalKind^#(n__0()) -> c_92()
976.21/297.18	     , isNaturalKind^#(n__head(V1)) -> c_93(isLNatKind^#(activate(V1)))
976.21/297.18	     , isNaturalKind^#(n__s(V1)) -> c_94(isNaturalKind^#(activate(V1)))
976.21/297.18	     , isNaturalKind^#(n__sel(V1, V2)) ->
976.21/297.18	       c_95(and^#(isNaturalKind(activate(V1)),
976.21/297.18	                  n__isLNatKind(activate(V2))))
976.21/297.18	     , and^#(X1, X2) -> c_89(X1, X2)
976.21/297.18	     , and^#(tt(), X) -> c_90(activate^#(X))
976.21/297.18	     , isLNatKind^#(X) -> c_98(X)
976.21/297.18	     , isLNatKind^#(n__natsFrom(V1)) ->
976.21/297.18	       c_99(isNaturalKind^#(activate(V1)))
976.21/297.18	     , isLNatKind^#(n__nil()) -> c_100()
976.21/297.18	     , isLNatKind^#(n__afterNth(V1, V2)) ->
976.21/297.18	       c_101(and^#(isNaturalKind(activate(V1)),
976.21/297.18	                   n__isLNatKind(activate(V2))))
976.21/297.18	     , isLNatKind^#(n__cons(V1, V2)) ->
976.21/297.18	       c_102(and^#(isNaturalKind(activate(V1)),
976.21/297.18	                   n__isLNatKind(activate(V2))))
976.21/297.18	     , isLNatKind^#(n__fst(V1)) -> c_103(isPLNatKind^#(activate(V1)))
976.21/297.18	     , isLNatKind^#(n__snd(V1)) -> c_104(isPLNatKind^#(activate(V1)))
976.21/297.18	     , isLNatKind^#(n__tail(V1)) -> c_105(isLNatKind^#(activate(V1)))
976.21/297.18	     , isLNatKind^#(n__take(V1, V2)) ->
976.21/297.18	       c_106(and^#(isNaturalKind(activate(V1)),
976.21/297.18	                   n__isLNatKind(activate(V2))))
976.21/297.18	     , nil^#() -> c_64()
976.21/297.18	     , afterNth^#(N, XS) ->
976.21/297.18	       c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	                      n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.18	                  N,
976.21/297.18	                  XS))
976.21/297.18	     , afterNth^#(X1, X2) -> c_60(X1, X2)
976.21/297.18	     , cons^#(X1, X2) -> c_54(X1, X2)
976.21/297.18	     , fst^#(X) -> c_70(X)
976.21/297.18	     , fst^#(pair(X, Y)) ->
976.21/297.18	       c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.18	                      n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.18	                  X))
976.21/297.18	     , snd^#(X) -> c_35(X)
976.21/297.18	     , snd^#(pair(X, Y)) ->
976.21/297.18	       c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.18	                       n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.18	                   Y))
976.21/297.18	     , tail^#(X) -> c_112(X)
976.21/297.18	     , tail^#(cons(N, XS)) ->
976.21/297.18	       c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	                        n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.18	                    activate(XS)))
976.21/297.18	     , take^#(N, XS) ->
976.21/297.18	       c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.18	                    N,
976.21/297.18	                    XS))
976.21/297.18	     , take^#(X1, X2) -> c_115(X1, X2)
976.21/297.18	     , 0^#() -> c_111()
976.21/297.18	     , head^#(X) -> c_57(X)
976.21/297.18	     , head^#(cons(N, XS)) ->
976.21/297.18	       c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	                      n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.18	                  N))
976.21/297.18	     , s^#(X) -> c_55(X)
976.21/297.18	     , sel^#(N, XS) ->
976.21/297.18	       c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.18	                    N,
976.21/297.18	                    XS))
976.21/297.18	     , sel^#(X1, X2) -> c_110(X1, X2)
976.21/297.18	     , pair^#(X1, X2) -> c_63(X1, X2)
976.21/297.18	     , splitAt^#(X1, X2) -> c_37(X1, X2)
976.21/297.18	     , splitAt^#(s(N), cons(X, XS)) ->
976.21/297.18	       c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	                       n__and(and(isNatural(X), n__isNaturalKind(X)),
976.21/297.18	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.21/297.18	                   N,
976.21/297.18	                   X,
976.21/297.18	                   activate(XS)))
976.21/297.18	     , splitAt^#(0(), XS) ->
976.21/297.18	       c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.21/297.18	     , isLNat^#(n__natsFrom(V1)) ->
976.21/297.18	       c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.18	     , isLNat^#(n__nil()) -> c_27()
976.21/297.18	     , isLNat^#(n__afterNth(V1, V2)) ->
976.21/297.18	       c_28(U41^#(and(isNaturalKind(activate(V1)),
976.21/297.18	                      n__isLNatKind(activate(V2))),
976.21/297.18	                  activate(V1),
976.21/297.18	                  activate(V2)))
976.21/297.18	     , isLNat^#(n__cons(V1, V2)) ->
976.21/297.18	       c_29(U51^#(and(isNaturalKind(activate(V1)),
976.21/297.18	                      n__isLNatKind(activate(V2))),
976.21/297.18	                  activate(V1),
976.21/297.18	                  activate(V2)))
976.21/297.18	     , isLNat^#(n__fst(V1)) ->
976.21/297.18	       c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.18	     , isLNat^#(n__snd(V1)) ->
976.21/297.18	       c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.18	     , isLNat^#(n__tail(V1)) ->
976.21/297.18	       c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.18	     , isLNat^#(n__take(V1, V2)) ->
976.21/297.18	       c_33(U101^#(and(isNaturalKind(activate(V1)),
976.21/297.18	                       n__isLNatKind(activate(V2))),
976.21/297.18	                   activate(V1),
976.21/297.18	                   activate(V2)))
976.21/297.18	     , U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.21/297.18	     , U41^#(tt(), V1, V2) ->
976.21/297.18	       c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.21/297.18	     , U51^#(tt(), V1, V2) ->
976.21/297.18	       c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.21/297.18	     , U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.21/297.18	     , U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.21/297.18	     , U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.21/297.18	     , U11^#(tt(), N, XS) ->
976.21/297.18	       c_34(snd^#(splitAt(activate(N), activate(XS))))
976.21/297.18	     , U181^#(tt(), Y) -> c_61(activate^#(Y))
976.21/297.18	     , U201^#(tt(), N, X, XS) ->
976.21/297.18	       c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.21/297.18	     , U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.21/297.18	     , U112^#(tt()) -> c_41()
976.21/297.18	     , U122^#(tt()) -> c_43()
976.21/297.18	     , U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.21/297.18	     , U133^#(tt()) -> c_46()
976.21/297.18	     , U141^#(tt(), V1, V2) ->
976.21/297.18	       c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.21/297.18	     , U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.21/297.18	     , U143^#(tt()) -> c_49()
976.21/297.18	     , U151^#(tt(), V1, V2) ->
976.21/297.18	       c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.21/297.18	     , U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.21/297.18	     , U153^#(tt()) -> c_52()
976.21/297.18	     , U161^#(tt(), N) ->
976.21/297.18	       c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.21/297.18	     , U171^#(tt(), N, XS) ->
976.21/297.18	       c_56(head^#(afterNth(activate(N), activate(XS))))
976.21/297.18	     , U31^#(tt(), N) -> c_72(activate^#(N))
976.21/297.18	     , U202^#(pair(YS, ZS), X) ->
976.21/297.18	       c_66(pair^#(cons(activate(X), YS), ZS))
976.21/297.18	     , U21^#(tt(), X) -> c_67(activate^#(X))
976.21/297.18	     , U211^#(tt(), XS) -> c_68(activate^#(XS))
976.21/297.18	     , U221^#(tt(), N, XS) ->
976.21/297.18	       c_69(fst^#(splitAt(activate(N), activate(XS))))
976.21/297.18	     , U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.21/297.18	     , U43^#(tt()) -> c_75()
976.21/297.18	     , U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.21/297.18	     , U53^#(tt()) -> c_78()
976.21/297.18	     , U62^#(tt()) -> c_80()
976.21/297.18	     , isPLNat^#(n__pair(V1, V2)) ->
976.21/297.18	       c_81(U141^#(and(isLNatKind(activate(V1)),
976.21/297.18	                       n__isLNatKind(activate(V2))),
976.21/297.18	                   activate(V1),
976.21/297.18	                   activate(V2)))
976.21/297.18	     , isPLNat^#(n__splitAt(V1, V2)) ->
976.21/297.18	       c_82(U151^#(and(isNaturalKind(activate(V1)),
976.21/297.18	                       n__isLNatKind(activate(V2))),
976.21/297.18	                   activate(V1),
976.21/297.18	                   activate(V2)))
976.21/297.18	     , U72^#(tt()) -> c_84()
976.21/297.18	     , U82^#(tt()) -> c_86()
976.21/297.18	     , U92^#(tt()) -> c_88()
976.21/297.18	     , isPLNatKind^#(n__pair(V1, V2)) ->
976.21/297.18	       c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.21/297.18	     , isPLNatKind^#(n__splitAt(V1, V2)) ->
976.21/297.18	       c_97(and^#(isNaturalKind(activate(V1)),
976.21/297.18	                  n__isLNatKind(activate(V2)))) }
976.21/297.18	   Strict Trs:
976.21/297.18	     { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2))
976.21/297.18	     , U102(tt(), V2) -> U103(isLNat(activate(V2)))
976.21/297.18	     , isNatural(n__0()) -> tt()
976.21/297.18	     , isNatural(n__head(V1)) ->
976.21/297.18	       U111(isLNatKind(activate(V1)), activate(V1))
976.21/297.18	     , isNatural(n__s(V1)) ->
976.21/297.18	       U121(isNaturalKind(activate(V1)), activate(V1))
976.21/297.18	     , isNatural(n__sel(V1, V2)) ->
976.21/297.18	       U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.18	            activate(V1),
976.21/297.18	            activate(V2))
976.21/297.18	     , activate(X) -> X
976.21/297.18	     , activate(n__natsFrom(X)) -> natsFrom(X)
976.21/297.18	     , activate(n__isNaturalKind(X)) -> isNaturalKind(X)
976.21/297.18	     , activate(n__and(X1, X2)) -> and(X1, X2)
976.21/297.18	     , activate(n__isLNatKind(X)) -> isLNatKind(X)
976.21/297.18	     , activate(n__nil()) -> nil()
976.21/297.18	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
976.21/297.18	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
976.21/297.18	     , activate(n__fst(X)) -> fst(X)
976.21/297.18	     , activate(n__snd(X)) -> snd(X)
976.21/297.18	     , activate(n__tail(X)) -> tail(X)
976.21/297.18	     , activate(n__take(X1, X2)) -> take(X1, X2)
976.21/297.18	     , activate(n__0()) -> 0()
976.21/297.18	     , activate(n__head(X)) -> head(X)
976.21/297.18	     , activate(n__s(X)) -> s(X)
976.21/297.18	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
976.21/297.18	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
976.21/297.18	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
976.21/297.18	     , U103(tt()) -> tt()
976.21/297.18	     , isLNat(n__natsFrom(V1)) ->
976.21/297.18	       U71(isNaturalKind(activate(V1)), activate(V1))
976.21/297.18	     , isLNat(n__nil()) -> tt()
976.21/297.18	     , isLNat(n__afterNth(V1, V2)) ->
976.21/297.18	       U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.18	           activate(V1),
976.21/297.18	           activate(V2))
976.21/297.18	     , isLNat(n__cons(V1, V2)) ->
976.21/297.18	       U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.18	           activate(V1),
976.21/297.18	           activate(V2))
976.21/297.18	     , isLNat(n__fst(V1)) ->
976.21/297.18	       U61(isPLNatKind(activate(V1)), activate(V1))
976.21/297.18	     , isLNat(n__snd(V1)) ->
976.21/297.18	       U81(isPLNatKind(activate(V1)), activate(V1))
976.21/297.18	     , isLNat(n__tail(V1)) ->
976.21/297.18	       U91(isLNatKind(activate(V1)), activate(V1))
976.21/297.18	     , isLNat(n__take(V1, V2)) ->
976.21/297.18	       U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.18	            activate(V1),
976.21/297.18	            activate(V2))
976.21/297.18	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
976.21/297.18	     , snd(X) -> n__snd(X)
976.21/297.18	     , snd(pair(X, Y)) ->
976.21/297.18	       U181(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.18	                n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.18	            Y)
976.21/297.18	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
976.21/297.18	     , splitAt(s(N), cons(X, XS)) ->
976.21/297.18	       U201(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	                n__and(and(isNatural(X), n__isNaturalKind(X)),
976.21/297.18	                       n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.21/297.18	            N,
976.21/297.18	            X,
976.21/297.18	            activate(XS))
976.21/297.18	     , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
976.21/297.18	     , U111(tt(), V1) -> U112(isLNat(activate(V1)))
976.21/297.18	     , U112(tt()) -> tt()
976.21/297.18	     , U121(tt(), V1) -> U122(isNatural(activate(V1)))
976.21/297.18	     , U122(tt()) -> tt()
976.21/297.18	     , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2))
976.21/297.18	     , U132(tt(), V2) -> U133(isLNat(activate(V2)))
976.21/297.18	     , U133(tt()) -> tt()
976.21/297.18	     , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2))
976.21/297.18	     , U142(tt(), V2) -> U143(isLNat(activate(V2)))
976.21/297.18	     , U143(tt()) -> tt()
976.21/297.18	     , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2))
976.21/297.18	     , U152(tt(), V2) -> U153(isLNat(activate(V2)))
976.21/297.18	     , U153(tt()) -> tt()
976.21/297.18	     , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
976.21/297.18	     , cons(X1, X2) -> n__cons(X1, X2)
976.21/297.18	     , s(X) -> n__s(X)
976.21/297.18	     , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
976.21/297.18	     , head(X) -> n__head(X)
976.21/297.18	     , head(cons(N, XS)) ->
976.21/297.18	       U31(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	               n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.18	           N)
976.21/297.18	     , afterNth(N, XS) ->
976.21/297.18	       U11(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.18	               n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.18	           N,
976.21/297.18	           XS)
976.21/297.18	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
976.21/297.18	     , U181(tt(), Y) -> activate(Y)
976.21/297.18	     , U191(tt(), XS) -> pair(nil(), activate(XS))
976.21/297.18	     , pair(X1, X2) -> n__pair(X1, X2)
976.21/297.18	     , nil() -> n__nil()
976.21/297.18	     , U201(tt(), N, X, XS) ->
976.21/297.18	       U202(splitAt(activate(N), activate(XS)), activate(X))
976.21/297.18	     , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
976.21/297.18	     , U21(tt(), X) -> activate(X)
976.21/297.18	     , U211(tt(), XS) -> activate(XS)
976.21/297.18	     , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
976.21/297.18	     , fst(X) -> n__fst(X)
976.21/297.18	     , fst(pair(X, Y)) ->
976.21/297.18	       U21(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.18	               n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.18	           X)
976.21/297.18	     , U31(tt(), N) -> activate(N)
976.21/297.18	     , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2))
976.21/297.18	     , U42(tt(), V2) -> U43(isLNat(activate(V2)))
976.21/297.18	     , U43(tt()) -> tt()
976.21/297.18	     , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2))
976.21/297.18	     , U52(tt(), V2) -> U53(isLNat(activate(V2)))
976.21/297.19	     , U53(tt()) -> tt()
976.21/297.19	     , U61(tt(), V1) -> U62(isPLNat(activate(V1)))
976.21/297.19	     , U62(tt()) -> tt()
976.21/297.19	     , isPLNat(n__pair(V1, V2)) ->
976.21/297.19	       U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.19	            activate(V1),
976.21/297.19	            activate(V2))
976.21/297.19	     , isPLNat(n__splitAt(V1, V2)) ->
976.21/297.19	       U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.19	            activate(V1),
976.21/297.19	            activate(V2))
976.21/297.19	     , U71(tt(), V1) -> U72(isNatural(activate(V1)))
976.21/297.19	     , U72(tt()) -> tt()
976.21/297.19	     , U81(tt(), V1) -> U82(isPLNat(activate(V1)))
976.21/297.19	     , U82(tt()) -> tt()
976.21/297.19	     , U91(tt(), V1) -> U92(isLNat(activate(V1)))
976.21/297.19	     , U92(tt()) -> tt()
976.21/297.19	     , and(X1, X2) -> n__and(X1, X2)
976.21/297.19	     , and(tt(), X) -> activate(X)
976.21/297.19	     , isNaturalKind(X) -> n__isNaturalKind(X)
976.21/297.19	     , isNaturalKind(n__0()) -> tt()
976.21/297.19	     , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
976.21/297.19	     , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
976.21/297.19	     , isNaturalKind(n__sel(V1, V2)) ->
976.21/297.19	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.19	     , isPLNatKind(n__pair(V1, V2)) ->
976.21/297.19	       and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.19	     , isPLNatKind(n__splitAt(V1, V2)) ->
976.21/297.19	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.19	     , isLNatKind(X) -> n__isLNatKind(X)
976.21/297.19	     , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
976.21/297.19	     , isLNatKind(n__nil()) -> tt()
976.21/297.19	     , isLNatKind(n__afterNth(V1, V2)) ->
976.21/297.19	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.19	     , isLNatKind(n__cons(V1, V2)) ->
976.21/297.19	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.19	     , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
976.21/297.19	     , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
976.21/297.19	     , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
976.21/297.19	     , isLNatKind(n__take(V1, V2)) ->
976.21/297.19	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.21/297.19	     , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N)
976.21/297.19	     , natsFrom(X) -> n__natsFrom(X)
976.21/297.19	     , sel(N, XS) ->
976.21/297.19	       U171(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	            N,
976.21/297.19	            XS)
976.21/297.19	     , sel(X1, X2) -> n__sel(X1, X2)
976.21/297.19	     , 0() -> n__0()
976.21/297.19	     , tail(X) -> n__tail(X)
976.21/297.19	     , tail(cons(N, XS)) ->
976.21/297.19	       U211(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.19	            activate(XS))
976.21/297.19	     , take(N, XS) ->
976.21/297.19	       U221(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	            N,
976.21/297.19	            XS)
976.21/297.19	     , take(X1, X2) -> n__take(X1, X2) }
976.21/297.19	   Obligation:
976.21/297.19	     runtime complexity
976.21/297.19	   Answer:
976.21/297.19	     MAYBE
976.21/297.19	   
976.21/297.19	   We estimate the number of application of
976.21/297.19	   {3,4,32,40,47,59,70,87,88,90,93,96,105,107,108,111,112,113} by
976.21/297.19	   applications of
976.21/297.19	   Pre({3,4,32,40,47,59,70,87,88,90,93,96,105,107,108,111,112,113}) =
976.21/297.19	   {2,8,9,11,13,15,16,23,30,31,33,34,36,38,39,45,49,50,51,53,55,58,60,62,64,65,66,77,80,81,82,89,92,95,104,106}.
976.21/297.19	   Here rules are labeled as follows:
976.21/297.19	   
976.21/297.19	     DPs:
976.21/297.19	       { 1: U101^#(tt(), V1, V2) ->
976.21/297.19	            c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	       , 2: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.21/297.19	       , 3: U103^#(tt()) -> c_25()
976.21/297.19	       , 4: isNatural^#(n__0()) -> c_3()
976.21/297.19	       , 5: isNatural^#(n__head(V1)) ->
976.21/297.19	            c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.19	       , 6: isNatural^#(n__s(V1)) ->
976.21/297.19	            c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.19	       , 7: isNatural^#(n__sel(V1, V2)) ->
976.21/297.19	            c_6(U131^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                           n__isLNatKind(activate(V2))),
976.21/297.19	                       activate(V1),
976.21/297.19	                       activate(V2)))
976.21/297.19	       , 8: U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.21/297.19	       , 9: U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.21/297.19	       , 10: U131^#(tt(), V1, V2) ->
976.21/297.19	             c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	       , 11: activate^#(X) -> c_7(X)
976.21/297.19	       , 12: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.21/297.19	       , 13: activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.21/297.19	       , 14: activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.21/297.19	       , 15: activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.21/297.19	       , 16: activate^#(n__nil()) -> c_12(nil^#())
976.21/297.19	       , 17: activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.21/297.19	       , 18: activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.21/297.19	       , 19: activate^#(n__fst(X)) -> c_15(fst^#(X))
976.21/297.19	       , 20: activate^#(n__snd(X)) -> c_16(snd^#(X))
976.21/297.19	       , 21: activate^#(n__tail(X)) -> c_17(tail^#(X))
976.21/297.19	       , 22: activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.21/297.19	       , 23: activate^#(n__0()) -> c_19(0^#())
976.21/297.19	       , 24: activate^#(n__head(X)) -> c_20(head^#(X))
976.21/297.19	       , 25: activate^#(n__s(X)) -> c_21(s^#(X))
976.21/297.19	       , 26: activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.21/297.19	       , 27: activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.21/297.19	       , 28: activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.21/297.19	       , 29: natsFrom^#(N) ->
976.21/297.19	             c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.21/297.19	       , 30: natsFrom^#(X) -> c_108(X)
976.21/297.19	       , 31: isNaturalKind^#(X) -> c_91(X)
976.21/297.19	       , 32: isNaturalKind^#(n__0()) -> c_92()
976.21/297.19	       , 33: isNaturalKind^#(n__head(V1)) ->
976.21/297.19	             c_93(isLNatKind^#(activate(V1)))
976.21/297.19	       , 34: isNaturalKind^#(n__s(V1)) ->
976.21/297.19	             c_94(isNaturalKind^#(activate(V1)))
976.21/297.19	       , 35: isNaturalKind^#(n__sel(V1, V2)) ->
976.21/297.19	             c_95(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                        n__isLNatKind(activate(V2))))
976.21/297.19	       , 36: and^#(X1, X2) -> c_89(X1, X2)
976.21/297.19	       , 37: and^#(tt(), X) -> c_90(activate^#(X))
976.21/297.19	       , 38: isLNatKind^#(X) -> c_98(X)
976.21/297.19	       , 39: isLNatKind^#(n__natsFrom(V1)) ->
976.21/297.19	             c_99(isNaturalKind^#(activate(V1)))
976.21/297.19	       , 40: isLNatKind^#(n__nil()) -> c_100()
976.21/297.19	       , 41: isLNatKind^#(n__afterNth(V1, V2)) ->
976.21/297.19	             c_101(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                         n__isLNatKind(activate(V2))))
976.21/297.19	       , 42: isLNatKind^#(n__cons(V1, V2)) ->
976.21/297.19	             c_102(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                         n__isLNatKind(activate(V2))))
976.21/297.19	       , 43: isLNatKind^#(n__fst(V1)) ->
976.21/297.19	             c_103(isPLNatKind^#(activate(V1)))
976.21/297.19	       , 44: isLNatKind^#(n__snd(V1)) ->
976.21/297.19	             c_104(isPLNatKind^#(activate(V1)))
976.21/297.19	       , 45: isLNatKind^#(n__tail(V1)) ->
976.21/297.19	             c_105(isLNatKind^#(activate(V1)))
976.21/297.19	       , 46: isLNatKind^#(n__take(V1, V2)) ->
976.21/297.19	             c_106(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                         n__isLNatKind(activate(V2))))
976.21/297.19	       , 47: nil^#() -> c_64()
976.21/297.19	       , 48: afterNth^#(N, XS) ->
976.21/297.19	             c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                            n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	                        N,
976.21/297.19	                        XS))
976.21/297.19	       , 49: afterNth^#(X1, X2) -> c_60(X1, X2)
976.21/297.19	       , 50: cons^#(X1, X2) -> c_54(X1, X2)
976.21/297.19	       , 51: fst^#(X) -> c_70(X)
976.21/297.19	       , 52: fst^#(pair(X, Y)) ->
976.21/297.19	             c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.19	                            n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.19	                        X))
976.21/297.19	       , 53: snd^#(X) -> c_35(X)
976.21/297.19	       , 54: snd^#(pair(X, Y)) ->
976.21/297.19	             c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.19	                             n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.19	                         Y))
976.21/297.19	       , 55: tail^#(X) -> c_112(X)
976.21/297.19	       , 56: tail^#(cons(N, XS)) ->
976.21/297.19	             c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.19	                          activate(XS)))
976.21/297.19	       , 57: take^#(N, XS) ->
976.21/297.19	             c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	                          N,
976.21/297.19	                          XS))
976.21/297.19	       , 58: take^#(X1, X2) -> c_115(X1, X2)
976.21/297.19	       , 59: 0^#() -> c_111()
976.21/297.19	       , 60: head^#(X) -> c_57(X)
976.21/297.19	       , 61: head^#(cons(N, XS)) ->
976.21/297.19	             c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                            n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.19	                        N))
976.21/297.19	       , 62: s^#(X) -> c_55(X)
976.21/297.19	       , 63: sel^#(N, XS) ->
976.21/297.19	             c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	                          N,
976.21/297.19	                          XS))
976.21/297.19	       , 64: sel^#(X1, X2) -> c_110(X1, X2)
976.21/297.19	       , 65: pair^#(X1, X2) -> c_63(X1, X2)
976.21/297.19	       , 66: splitAt^#(X1, X2) -> c_37(X1, X2)
976.21/297.19	       , 67: splitAt^#(s(N), cons(X, XS)) ->
976.21/297.19	             c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                             n__and(and(isNatural(X), n__isNaturalKind(X)),
976.21/297.19	                                    n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.21/297.19	                         N,
976.21/297.19	                         X,
976.21/297.19	                         activate(XS)))
976.21/297.19	       , 68: splitAt^#(0(), XS) ->
976.21/297.19	             c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.21/297.19	       , 69: isLNat^#(n__natsFrom(V1)) ->
976.21/297.19	             c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.19	       , 70: isLNat^#(n__nil()) -> c_27()
976.21/297.19	       , 71: isLNat^#(n__afterNth(V1, V2)) ->
976.21/297.19	             c_28(U41^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                            n__isLNatKind(activate(V2))),
976.21/297.19	                        activate(V1),
976.21/297.19	                        activate(V2)))
976.21/297.19	       , 72: isLNat^#(n__cons(V1, V2)) ->
976.21/297.19	             c_29(U51^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                            n__isLNatKind(activate(V2))),
976.21/297.19	                        activate(V1),
976.21/297.19	                        activate(V2)))
976.21/297.19	       , 73: isLNat^#(n__fst(V1)) ->
976.21/297.19	             c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.19	       , 74: isLNat^#(n__snd(V1)) ->
976.21/297.19	             c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.19	       , 75: isLNat^#(n__tail(V1)) ->
976.21/297.19	             c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.19	       , 76: isLNat^#(n__take(V1, V2)) ->
976.21/297.19	             c_33(U101^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                             n__isLNatKind(activate(V2))),
976.21/297.19	                         activate(V1),
976.21/297.19	                         activate(V2)))
976.21/297.19	       , 77: U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.21/297.19	       , 78: U41^#(tt(), V1, V2) ->
976.21/297.19	             c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	       , 79: U51^#(tt(), V1, V2) ->
976.21/297.19	             c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	       , 80: U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.21/297.19	       , 81: U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.21/297.19	       , 82: U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.21/297.19	       , 83: U11^#(tt(), N, XS) ->
976.21/297.19	             c_34(snd^#(splitAt(activate(N), activate(XS))))
976.21/297.19	       , 84: U181^#(tt(), Y) -> c_61(activate^#(Y))
976.21/297.19	       , 85: U201^#(tt(), N, X, XS) ->
976.21/297.19	             c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.21/297.19	       , 86: U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.21/297.19	       , 87: U112^#(tt()) -> c_41()
976.21/297.19	       , 88: U122^#(tt()) -> c_43()
976.21/297.19	       , 89: U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.21/297.19	       , 90: U133^#(tt()) -> c_46()
976.21/297.19	       , 91: U141^#(tt(), V1, V2) ->
976.21/297.19	             c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.21/297.19	       , 92: U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.21/297.19	       , 93: U143^#(tt()) -> c_49()
976.21/297.19	       , 94: U151^#(tt(), V1, V2) ->
976.21/297.19	             c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	       , 95: U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.21/297.19	       , 96: U153^#(tt()) -> c_52()
976.21/297.19	       , 97: U161^#(tt(), N) ->
976.21/297.19	             c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.21/297.19	       , 98: U171^#(tt(), N, XS) ->
976.21/297.19	             c_56(head^#(afterNth(activate(N), activate(XS))))
976.21/297.19	       , 99: U31^#(tt(), N) -> c_72(activate^#(N))
976.21/297.19	       , 100: U202^#(pair(YS, ZS), X) ->
976.21/297.19	              c_66(pair^#(cons(activate(X), YS), ZS))
976.21/297.19	       , 101: U21^#(tt(), X) -> c_67(activate^#(X))
976.21/297.19	       , 102: U211^#(tt(), XS) -> c_68(activate^#(XS))
976.21/297.19	       , 103: U221^#(tt(), N, XS) ->
976.21/297.19	              c_69(fst^#(splitAt(activate(N), activate(XS))))
976.21/297.19	       , 104: U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.21/297.19	       , 105: U43^#(tt()) -> c_75()
976.21/297.19	       , 106: U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.21/297.19	       , 107: U53^#(tt()) -> c_78()
976.21/297.19	       , 108: U62^#(tt()) -> c_80()
976.21/297.19	       , 109: isPLNat^#(n__pair(V1, V2)) ->
976.21/297.19	              c_81(U141^#(and(isLNatKind(activate(V1)),
976.21/297.19	                              n__isLNatKind(activate(V2))),
976.21/297.19	                          activate(V1),
976.21/297.19	                          activate(V2)))
976.21/297.19	       , 110: isPLNat^#(n__splitAt(V1, V2)) ->
976.21/297.19	              c_82(U151^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                              n__isLNatKind(activate(V2))),
976.21/297.19	                          activate(V1),
976.21/297.19	                          activate(V2)))
976.21/297.19	       , 111: U72^#(tt()) -> c_84()
976.21/297.19	       , 112: U82^#(tt()) -> c_86()
976.21/297.19	       , 113: U92^#(tt()) -> c_88()
976.21/297.19	       , 114: isPLNatKind^#(n__pair(V1, V2)) ->
976.21/297.19	              c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.21/297.19	       , 115: isPLNatKind^#(n__splitAt(V1, V2)) ->
976.21/297.19	              c_97(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                         n__isLNatKind(activate(V2)))) }
976.21/297.19	   
976.21/297.19	   We are left with following problem, upon which TcT provides the
976.21/297.19	   certificate MAYBE.
976.21/297.19	   
976.21/297.19	   Strict DPs:
976.21/297.19	     { U101^#(tt(), V1, V2) ->
976.21/297.19	       c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	     , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.21/297.19	     , isNatural^#(n__head(V1)) ->
976.21/297.19	       c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.19	     , isNatural^#(n__s(V1)) ->
976.21/297.19	       c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.19	     , isNatural^#(n__sel(V1, V2)) ->
976.21/297.19	       c_6(U131^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                      n__isLNatKind(activate(V2))),
976.21/297.19	                  activate(V1),
976.21/297.19	                  activate(V2)))
976.21/297.19	     , U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.21/297.19	     , U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.21/297.19	     , U131^#(tt(), V1, V2) ->
976.21/297.19	       c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	     , activate^#(X) -> c_7(X)
976.21/297.19	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.21/297.19	     , activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.21/297.19	     , activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.21/297.19	     , activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.21/297.19	     , activate^#(n__nil()) -> c_12(nil^#())
976.21/297.19	     , activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.21/297.19	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.21/297.19	     , activate^#(n__fst(X)) -> c_15(fst^#(X))
976.21/297.19	     , activate^#(n__snd(X)) -> c_16(snd^#(X))
976.21/297.19	     , activate^#(n__tail(X)) -> c_17(tail^#(X))
976.21/297.19	     , activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.21/297.19	     , activate^#(n__0()) -> c_19(0^#())
976.21/297.19	     , activate^#(n__head(X)) -> c_20(head^#(X))
976.21/297.19	     , activate^#(n__s(X)) -> c_21(s^#(X))
976.21/297.19	     , activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.21/297.19	     , activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.21/297.19	     , activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.21/297.19	     , natsFrom^#(N) ->
976.21/297.19	       c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.21/297.19	     , natsFrom^#(X) -> c_108(X)
976.21/297.19	     , isNaturalKind^#(X) -> c_91(X)
976.21/297.19	     , isNaturalKind^#(n__head(V1)) -> c_93(isLNatKind^#(activate(V1)))
976.21/297.19	     , isNaturalKind^#(n__s(V1)) -> c_94(isNaturalKind^#(activate(V1)))
976.21/297.19	     , isNaturalKind^#(n__sel(V1, V2)) ->
976.21/297.19	       c_95(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                  n__isLNatKind(activate(V2))))
976.21/297.19	     , and^#(X1, X2) -> c_89(X1, X2)
976.21/297.19	     , and^#(tt(), X) -> c_90(activate^#(X))
976.21/297.19	     , isLNatKind^#(X) -> c_98(X)
976.21/297.19	     , isLNatKind^#(n__natsFrom(V1)) ->
976.21/297.19	       c_99(isNaturalKind^#(activate(V1)))
976.21/297.19	     , isLNatKind^#(n__afterNth(V1, V2)) ->
976.21/297.19	       c_101(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                   n__isLNatKind(activate(V2))))
976.21/297.19	     , isLNatKind^#(n__cons(V1, V2)) ->
976.21/297.19	       c_102(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                   n__isLNatKind(activate(V2))))
976.21/297.19	     , isLNatKind^#(n__fst(V1)) -> c_103(isPLNatKind^#(activate(V1)))
976.21/297.19	     , isLNatKind^#(n__snd(V1)) -> c_104(isPLNatKind^#(activate(V1)))
976.21/297.19	     , isLNatKind^#(n__tail(V1)) -> c_105(isLNatKind^#(activate(V1)))
976.21/297.19	     , isLNatKind^#(n__take(V1, V2)) ->
976.21/297.19	       c_106(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                   n__isLNatKind(activate(V2))))
976.21/297.19	     , afterNth^#(N, XS) ->
976.21/297.19	       c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                      n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	                  N,
976.21/297.19	                  XS))
976.21/297.19	     , afterNth^#(X1, X2) -> c_60(X1, X2)
976.21/297.19	     , cons^#(X1, X2) -> c_54(X1, X2)
976.21/297.19	     , fst^#(X) -> c_70(X)
976.21/297.19	     , fst^#(pair(X, Y)) ->
976.21/297.19	       c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.19	                      n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.19	                  X))
976.21/297.19	     , snd^#(X) -> c_35(X)
976.21/297.19	     , snd^#(pair(X, Y)) ->
976.21/297.19	       c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.21/297.19	                       n__and(isLNat(Y), n__isLNatKind(Y))),
976.21/297.19	                   Y))
976.21/297.19	     , tail^#(X) -> c_112(X)
976.21/297.19	     , tail^#(cons(N, XS)) ->
976.21/297.19	       c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                        n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.19	                    activate(XS)))
976.21/297.19	     , take^#(N, XS) ->
976.21/297.19	       c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	                    N,
976.21/297.19	                    XS))
976.21/297.19	     , take^#(X1, X2) -> c_115(X1, X2)
976.21/297.19	     , head^#(X) -> c_57(X)
976.21/297.19	     , head^#(cons(N, XS)) ->
976.21/297.19	       c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                      n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.21/297.19	                  N))
976.21/297.19	     , s^#(X) -> c_55(X)
976.21/297.19	     , sel^#(N, XS) ->
976.21/297.19	       c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.21/297.19	                    N,
976.21/297.19	                    XS))
976.21/297.19	     , sel^#(X1, X2) -> c_110(X1, X2)
976.21/297.19	     , pair^#(X1, X2) -> c_63(X1, X2)
976.21/297.19	     , splitAt^#(X1, X2) -> c_37(X1, X2)
976.21/297.19	     , splitAt^#(s(N), cons(X, XS)) ->
976.21/297.19	       c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.21/297.19	                       n__and(and(isNatural(X), n__isNaturalKind(X)),
976.21/297.19	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.21/297.19	                   N,
976.21/297.19	                   X,
976.21/297.19	                   activate(XS)))
976.21/297.19	     , splitAt^#(0(), XS) ->
976.21/297.19	       c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.21/297.19	     , isLNat^#(n__natsFrom(V1)) ->
976.21/297.19	       c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.21/297.19	     , isLNat^#(n__afterNth(V1, V2)) ->
976.21/297.19	       c_28(U41^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                      n__isLNatKind(activate(V2))),
976.21/297.19	                  activate(V1),
976.21/297.19	                  activate(V2)))
976.21/297.19	     , isLNat^#(n__cons(V1, V2)) ->
976.21/297.19	       c_29(U51^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                      n__isLNatKind(activate(V2))),
976.21/297.19	                  activate(V1),
976.21/297.19	                  activate(V2)))
976.21/297.19	     , isLNat^#(n__fst(V1)) ->
976.21/297.19	       c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.19	     , isLNat^#(n__snd(V1)) ->
976.21/297.19	       c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.21/297.19	     , isLNat^#(n__tail(V1)) ->
976.21/297.19	       c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.21/297.19	     , isLNat^#(n__take(V1, V2)) ->
976.21/297.19	       c_33(U101^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                       n__isLNatKind(activate(V2))),
976.21/297.19	                   activate(V1),
976.21/297.19	                   activate(V2)))
976.21/297.19	     , U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.21/297.19	     , U41^#(tt(), V1, V2) ->
976.21/297.19	       c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	     , U51^#(tt(), V1, V2) ->
976.21/297.19	       c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	     , U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.21/297.19	     , U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.21/297.19	     , U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.21/297.19	     , U11^#(tt(), N, XS) ->
976.21/297.19	       c_34(snd^#(splitAt(activate(N), activate(XS))))
976.21/297.19	     , U181^#(tt(), Y) -> c_61(activate^#(Y))
976.21/297.19	     , U201^#(tt(), N, X, XS) ->
976.21/297.19	       c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.21/297.19	     , U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.21/297.19	     , U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.21/297.19	     , U141^#(tt(), V1, V2) ->
976.21/297.19	       c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.21/297.19	     , U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.21/297.19	     , U151^#(tt(), V1, V2) ->
976.21/297.19	       c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.21/297.19	     , U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.21/297.19	     , U161^#(tt(), N) ->
976.21/297.19	       c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.21/297.19	     , U171^#(tt(), N, XS) ->
976.21/297.19	       c_56(head^#(afterNth(activate(N), activate(XS))))
976.21/297.19	     , U31^#(tt(), N) -> c_72(activate^#(N))
976.21/297.19	     , U202^#(pair(YS, ZS), X) ->
976.21/297.19	       c_66(pair^#(cons(activate(X), YS), ZS))
976.21/297.19	     , U21^#(tt(), X) -> c_67(activate^#(X))
976.21/297.19	     , U211^#(tt(), XS) -> c_68(activate^#(XS))
976.21/297.19	     , U221^#(tt(), N, XS) ->
976.21/297.19	       c_69(fst^#(splitAt(activate(N), activate(XS))))
976.21/297.19	     , U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.21/297.19	     , U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.21/297.19	     , isPLNat^#(n__pair(V1, V2)) ->
976.21/297.19	       c_81(U141^#(and(isLNatKind(activate(V1)),
976.21/297.19	                       n__isLNatKind(activate(V2))),
976.21/297.19	                   activate(V1),
976.21/297.19	                   activate(V2)))
976.21/297.19	     , isPLNat^#(n__splitAt(V1, V2)) ->
976.21/297.19	       c_82(U151^#(and(isNaturalKind(activate(V1)),
976.21/297.19	                       n__isLNatKind(activate(V2))),
976.21/297.19	                   activate(V1),
976.21/297.19	                   activate(V2)))
976.21/297.19	     , isPLNatKind^#(n__pair(V1, V2)) ->
976.21/297.19	       c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.21/297.19	     , isPLNatKind^#(n__splitAt(V1, V2)) ->
976.21/297.19	       c_97(and^#(isNaturalKind(activate(V1)),
976.21/297.19	                  n__isLNatKind(activate(V2)))) }
976.21/297.19	   Strict Trs:
976.21/297.19	     { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2))
976.21/297.19	     , U102(tt(), V2) -> U103(isLNat(activate(V2)))
976.21/297.19	     , isNatural(n__0()) -> tt()
976.21/297.19	     , isNatural(n__head(V1)) ->
976.21/297.19	       U111(isLNatKind(activate(V1)), activate(V1))
976.21/297.19	     , isNatural(n__s(V1)) ->
976.21/297.19	       U121(isNaturalKind(activate(V1)), activate(V1))
976.21/297.19	     , isNatural(n__sel(V1, V2)) ->
976.21/297.19	       U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.19	            activate(V1),
976.21/297.19	            activate(V2))
976.21/297.19	     , activate(X) -> X
976.21/297.19	     , activate(n__natsFrom(X)) -> natsFrom(X)
976.21/297.19	     , activate(n__isNaturalKind(X)) -> isNaturalKind(X)
976.21/297.19	     , activate(n__and(X1, X2)) -> and(X1, X2)
976.21/297.19	     , activate(n__isLNatKind(X)) -> isLNatKind(X)
976.21/297.19	     , activate(n__nil()) -> nil()
976.21/297.19	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
976.21/297.19	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
976.21/297.19	     , activate(n__fst(X)) -> fst(X)
976.21/297.19	     , activate(n__snd(X)) -> snd(X)
976.21/297.19	     , activate(n__tail(X)) -> tail(X)
976.21/297.19	     , activate(n__take(X1, X2)) -> take(X1, X2)
976.21/297.19	     , activate(n__0()) -> 0()
976.21/297.19	     , activate(n__head(X)) -> head(X)
976.21/297.19	     , activate(n__s(X)) -> s(X)
976.21/297.19	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
976.21/297.19	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
976.21/297.19	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
976.21/297.19	     , U103(tt()) -> tt()
976.21/297.19	     , isLNat(n__natsFrom(V1)) ->
976.21/297.19	       U71(isNaturalKind(activate(V1)), activate(V1))
976.21/297.19	     , isLNat(n__nil()) -> tt()
976.21/297.19	     , isLNat(n__afterNth(V1, V2)) ->
976.21/297.19	       U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.19	           activate(V1),
976.21/297.19	           activate(V2))
976.21/297.19	     , isLNat(n__cons(V1, V2)) ->
976.21/297.19	       U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.19	           activate(V1),
976.21/297.19	           activate(V2))
976.21/297.19	     , isLNat(n__fst(V1)) ->
976.21/297.19	       U61(isPLNatKind(activate(V1)), activate(V1))
976.21/297.19	     , isLNat(n__snd(V1)) ->
976.21/297.19	       U81(isPLNatKind(activate(V1)), activate(V1))
976.21/297.19	     , isLNat(n__tail(V1)) ->
976.21/297.19	       U91(isLNatKind(activate(V1)), activate(V1))
976.21/297.19	     , isLNat(n__take(V1, V2)) ->
976.21/297.19	       U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.21/297.19	            activate(V1),
976.21/297.19	            activate(V2))
976.21/297.19	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
976.21/297.19	     , snd(X) -> n__snd(X)
976.21/297.19	     , snd(pair(X, Y)) ->
976.48/297.20	       U181(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.20	                n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.20	            Y)
976.48/297.20	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
976.48/297.20	     , splitAt(s(N), cons(X, XS)) ->
976.48/297.20	       U201(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.20	                       n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.20	            N,
976.48/297.20	            X,
976.48/297.20	            activate(XS))
976.48/297.20	     , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
976.48/297.20	     , U111(tt(), V1) -> U112(isLNat(activate(V1)))
976.48/297.20	     , U112(tt()) -> tt()
976.48/297.20	     , U121(tt(), V1) -> U122(isNatural(activate(V1)))
976.48/297.20	     , U122(tt()) -> tt()
976.48/297.20	     , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2))
976.48/297.20	     , U132(tt(), V2) -> U133(isLNat(activate(V2)))
976.48/297.20	     , U133(tt()) -> tt()
976.48/297.20	     , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2))
976.48/297.20	     , U142(tt(), V2) -> U143(isLNat(activate(V2)))
976.48/297.20	     , U143(tt()) -> tt()
976.48/297.20	     , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2))
976.48/297.20	     , U152(tt(), V2) -> U153(isLNat(activate(V2)))
976.48/297.20	     , U153(tt()) -> tt()
976.48/297.20	     , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
976.48/297.20	     , cons(X1, X2) -> n__cons(X1, X2)
976.48/297.20	     , s(X) -> n__s(X)
976.48/297.20	     , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
976.48/297.20	     , head(X) -> n__head(X)
976.48/297.20	     , head(cons(N, XS)) ->
976.48/297.20	       U31(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	               n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.20	           N)
976.48/297.20	     , afterNth(N, XS) ->
976.48/297.20	       U11(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	               n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.20	           N,
976.48/297.20	           XS)
976.48/297.20	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
976.48/297.20	     , U181(tt(), Y) -> activate(Y)
976.48/297.20	     , U191(tt(), XS) -> pair(nil(), activate(XS))
976.48/297.20	     , pair(X1, X2) -> n__pair(X1, X2)
976.48/297.20	     , nil() -> n__nil()
976.48/297.20	     , U201(tt(), N, X, XS) ->
976.48/297.20	       U202(splitAt(activate(N), activate(XS)), activate(X))
976.48/297.20	     , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
976.48/297.20	     , U21(tt(), X) -> activate(X)
976.48/297.20	     , U211(tt(), XS) -> activate(XS)
976.48/297.20	     , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
976.48/297.20	     , fst(X) -> n__fst(X)
976.48/297.20	     , fst(pair(X, Y)) ->
976.48/297.20	       U21(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.20	               n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.20	           X)
976.48/297.20	     , U31(tt(), N) -> activate(N)
976.48/297.20	     , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2))
976.48/297.20	     , U42(tt(), V2) -> U43(isLNat(activate(V2)))
976.48/297.20	     , U43(tt()) -> tt()
976.48/297.20	     , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2))
976.48/297.20	     , U52(tt(), V2) -> U53(isLNat(activate(V2)))
976.48/297.20	     , U53(tt()) -> tt()
976.48/297.20	     , U61(tt(), V1) -> U62(isPLNat(activate(V1)))
976.48/297.20	     , U62(tt()) -> tt()
976.48/297.20	     , isPLNat(n__pair(V1, V2)) ->
976.48/297.20	       U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.20	            activate(V1),
976.48/297.20	            activate(V2))
976.48/297.20	     , isPLNat(n__splitAt(V1, V2)) ->
976.48/297.20	       U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.20	            activate(V1),
976.48/297.20	            activate(V2))
976.48/297.20	     , U71(tt(), V1) -> U72(isNatural(activate(V1)))
976.48/297.20	     , U72(tt()) -> tt()
976.48/297.20	     , U81(tt(), V1) -> U82(isPLNat(activate(V1)))
976.48/297.20	     , U82(tt()) -> tt()
976.48/297.20	     , U91(tt(), V1) -> U92(isLNat(activate(V1)))
976.48/297.20	     , U92(tt()) -> tt()
976.48/297.20	     , and(X1, X2) -> n__and(X1, X2)
976.48/297.20	     , and(tt(), X) -> activate(X)
976.48/297.20	     , isNaturalKind(X) -> n__isNaturalKind(X)
976.48/297.20	     , isNaturalKind(n__0()) -> tt()
976.48/297.20	     , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
976.48/297.20	     , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
976.48/297.20	     , isNaturalKind(n__sel(V1, V2)) ->
976.48/297.20	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.20	     , isPLNatKind(n__pair(V1, V2)) ->
976.48/297.20	       and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.20	     , isPLNatKind(n__splitAt(V1, V2)) ->
976.48/297.20	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.20	     , isLNatKind(X) -> n__isLNatKind(X)
976.48/297.20	     , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
976.48/297.20	     , isLNatKind(n__nil()) -> tt()
976.48/297.20	     , isLNatKind(n__afterNth(V1, V2)) ->
976.48/297.20	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.20	     , isLNatKind(n__cons(V1, V2)) ->
976.48/297.20	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.20	     , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
976.48/297.20	     , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
976.48/297.20	     , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
976.48/297.20	     , isLNatKind(n__take(V1, V2)) ->
976.48/297.20	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.20	     , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N)
976.48/297.20	     , natsFrom(X) -> n__natsFrom(X)
976.48/297.20	     , sel(N, XS) ->
976.48/297.20	       U171(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.20	            N,
976.48/297.20	            XS)
976.48/297.20	     , sel(X1, X2) -> n__sel(X1, X2)
976.48/297.20	     , 0() -> n__0()
976.48/297.20	     , tail(X) -> n__tail(X)
976.48/297.20	     , tail(cons(N, XS)) ->
976.48/297.20	       U211(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.20	            activate(XS))
976.48/297.20	     , take(N, XS) ->
976.48/297.20	       U221(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.20	            N,
976.48/297.20	            XS)
976.48/297.20	     , take(X1, X2) -> n__take(X1, X2) }
976.48/297.20	   Weak DPs:
976.48/297.20	     { U103^#(tt()) -> c_25()
976.48/297.20	     , isNatural^#(n__0()) -> c_3()
976.48/297.20	     , isNaturalKind^#(n__0()) -> c_92()
976.48/297.20	     , isLNatKind^#(n__nil()) -> c_100()
976.48/297.20	     , nil^#() -> c_64()
976.48/297.20	     , 0^#() -> c_111()
976.48/297.20	     , isLNat^#(n__nil()) -> c_27()
976.48/297.20	     , U112^#(tt()) -> c_41()
976.48/297.20	     , U122^#(tt()) -> c_43()
976.48/297.20	     , U133^#(tt()) -> c_46()
976.48/297.20	     , U143^#(tt()) -> c_49()
976.48/297.20	     , U153^#(tt()) -> c_52()
976.48/297.20	     , U43^#(tt()) -> c_75()
976.48/297.20	     , U53^#(tt()) -> c_78()
976.48/297.20	     , U62^#(tt()) -> c_80()
976.48/297.20	     , U72^#(tt()) -> c_84()
976.48/297.20	     , U82^#(tt()) -> c_86()
976.48/297.20	     , U92^#(tt()) -> c_88() }
976.48/297.20	   Obligation:
976.48/297.20	     runtime complexity
976.48/297.20	   Answer:
976.48/297.20	     MAYBE
976.48/297.20	   
976.48/297.20	   We estimate the number of application of
976.48/297.20	   {2,6,7,14,21,70,73,74,75,80,82,84,92,93} by applications of
976.48/297.20	   Pre({2,6,7,14,21,70,73,74,75,80,82,84,92,93}) =
976.48/297.20	   {1,3,4,8,9,28,29,33,34,35,44,45,46,48,50,53,54,56,58,59,60,63,66,67,68,71,72,77,81,83,87,89,90}.
976.48/297.20	   Here rules are labeled as follows:
976.48/297.20	   
976.48/297.20	     DPs:
976.48/297.20	       { 1: U101^#(tt(), V1, V2) ->
976.48/297.20	            c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.48/297.20	       , 2: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.48/297.20	       , 3: isNatural^#(n__head(V1)) ->
976.48/297.20	            c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.20	       , 4: isNatural^#(n__s(V1)) ->
976.48/297.20	            c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.20	       , 5: isNatural^#(n__sel(V1, V2)) ->
976.48/297.20	            c_6(U131^#(and(isNaturalKind(activate(V1)),
976.48/297.20	                           n__isLNatKind(activate(V2))),
976.48/297.20	                       activate(V1),
976.48/297.20	                       activate(V2)))
976.48/297.20	       , 6: U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.48/297.20	       , 7: U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.48/297.20	       , 8: U131^#(tt(), V1, V2) ->
976.48/297.20	            c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.48/297.20	       , 9: activate^#(X) -> c_7(X)
976.48/297.20	       , 10: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.48/297.20	       , 11: activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.48/297.20	       , 12: activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.48/297.20	       , 13: activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.48/297.20	       , 14: activate^#(n__nil()) -> c_12(nil^#())
976.48/297.20	       , 15: activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.48/297.20	       , 16: activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.48/297.20	       , 17: activate^#(n__fst(X)) -> c_15(fst^#(X))
976.48/297.20	       , 18: activate^#(n__snd(X)) -> c_16(snd^#(X))
976.48/297.20	       , 19: activate^#(n__tail(X)) -> c_17(tail^#(X))
976.48/297.20	       , 20: activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.48/297.20	       , 21: activate^#(n__0()) -> c_19(0^#())
976.48/297.20	       , 22: activate^#(n__head(X)) -> c_20(head^#(X))
976.48/297.20	       , 23: activate^#(n__s(X)) -> c_21(s^#(X))
976.48/297.20	       , 24: activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.48/297.20	       , 25: activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.48/297.20	       , 26: activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.48/297.20	       , 27: natsFrom^#(N) ->
976.48/297.20	             c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.48/297.20	       , 28: natsFrom^#(X) -> c_108(X)
976.48/297.20	       , 29: isNaturalKind^#(X) -> c_91(X)
976.48/297.20	       , 30: isNaturalKind^#(n__head(V1)) ->
976.48/297.20	             c_93(isLNatKind^#(activate(V1)))
976.48/297.20	       , 31: isNaturalKind^#(n__s(V1)) ->
976.48/297.20	             c_94(isNaturalKind^#(activate(V1)))
976.48/297.20	       , 32: isNaturalKind^#(n__sel(V1, V2)) ->
976.48/297.20	             c_95(and^#(isNaturalKind(activate(V1)),
976.48/297.20	                        n__isLNatKind(activate(V2))))
976.48/297.20	       , 33: and^#(X1, X2) -> c_89(X1, X2)
976.48/297.20	       , 34: and^#(tt(), X) -> c_90(activate^#(X))
976.48/297.20	       , 35: isLNatKind^#(X) -> c_98(X)
976.48/297.20	       , 36: isLNatKind^#(n__natsFrom(V1)) ->
976.48/297.20	             c_99(isNaturalKind^#(activate(V1)))
976.48/297.20	       , 37: isLNatKind^#(n__afterNth(V1, V2)) ->
976.48/297.20	             c_101(and^#(isNaturalKind(activate(V1)),
976.48/297.20	                         n__isLNatKind(activate(V2))))
976.48/297.20	       , 38: isLNatKind^#(n__cons(V1, V2)) ->
976.48/297.20	             c_102(and^#(isNaturalKind(activate(V1)),
976.48/297.20	                         n__isLNatKind(activate(V2))))
976.48/297.20	       , 39: isLNatKind^#(n__fst(V1)) ->
976.48/297.20	             c_103(isPLNatKind^#(activate(V1)))
976.48/297.20	       , 40: isLNatKind^#(n__snd(V1)) ->
976.48/297.20	             c_104(isPLNatKind^#(activate(V1)))
976.48/297.20	       , 41: isLNatKind^#(n__tail(V1)) ->
976.48/297.20	             c_105(isLNatKind^#(activate(V1)))
976.48/297.20	       , 42: isLNatKind^#(n__take(V1, V2)) ->
976.48/297.20	             c_106(and^#(isNaturalKind(activate(V1)),
976.48/297.20	                         n__isLNatKind(activate(V2))))
976.48/297.20	       , 43: afterNth^#(N, XS) ->
976.48/297.20	             c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                            n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.20	                        N,
976.48/297.20	                        XS))
976.48/297.20	       , 44: afterNth^#(X1, X2) -> c_60(X1, X2)
976.48/297.20	       , 45: cons^#(X1, X2) -> c_54(X1, X2)
976.48/297.20	       , 46: fst^#(X) -> c_70(X)
976.48/297.20	       , 47: fst^#(pair(X, Y)) ->
976.48/297.20	             c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.20	                            n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.20	                        X))
976.48/297.20	       , 48: snd^#(X) -> c_35(X)
976.48/297.20	       , 49: snd^#(pair(X, Y)) ->
976.48/297.20	             c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.20	                             n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.20	                         Y))
976.48/297.20	       , 50: tail^#(X) -> c_112(X)
976.48/297.20	       , 51: tail^#(cons(N, XS)) ->
976.48/297.20	             c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.20	                          activate(XS)))
976.48/297.20	       , 52: take^#(N, XS) ->
976.48/297.20	             c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.20	                          N,
976.48/297.20	                          XS))
976.48/297.20	       , 53: take^#(X1, X2) -> c_115(X1, X2)
976.48/297.20	       , 54: head^#(X) -> c_57(X)
976.48/297.20	       , 55: head^#(cons(N, XS)) ->
976.48/297.20	             c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                            n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.20	                        N))
976.48/297.20	       , 56: s^#(X) -> c_55(X)
976.48/297.20	       , 57: sel^#(N, XS) ->
976.48/297.20	             c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.20	                          N,
976.48/297.20	                          XS))
976.48/297.20	       , 58: sel^#(X1, X2) -> c_110(X1, X2)
976.48/297.20	       , 59: pair^#(X1, X2) -> c_63(X1, X2)
976.48/297.20	       , 60: splitAt^#(X1, X2) -> c_37(X1, X2)
976.48/297.20	       , 61: splitAt^#(s(N), cons(X, XS)) ->
976.48/297.20	             c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.20	                             n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.20	                                    n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.20	                         N,
976.48/297.20	                         X,
976.48/297.20	                         activate(XS)))
976.48/297.20	       , 62: splitAt^#(0(), XS) ->
976.48/297.20	             c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.48/297.20	       , 63: isLNat^#(n__natsFrom(V1)) ->
976.48/297.20	             c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.20	       , 64: isLNat^#(n__afterNth(V1, V2)) ->
976.48/297.20	             c_28(U41^#(and(isNaturalKind(activate(V1)),
976.48/297.20	                            n__isLNatKind(activate(V2))),
976.48/297.20	                        activate(V1),
976.48/297.20	                        activate(V2)))
976.48/297.20	       , 65: isLNat^#(n__cons(V1, V2)) ->
976.48/297.20	             c_29(U51^#(and(isNaturalKind(activate(V1)),
976.48/297.20	                            n__isLNatKind(activate(V2))),
976.48/297.20	                        activate(V1),
976.48/297.20	                        activate(V2)))
976.48/297.20	       , 66: isLNat^#(n__fst(V1)) ->
976.48/297.20	             c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.20	       , 67: isLNat^#(n__snd(V1)) ->
976.48/297.20	             c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.20	       , 68: isLNat^#(n__tail(V1)) ->
976.48/297.20	             c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.20	       , 69: isLNat^#(n__take(V1, V2)) ->
976.48/297.20	             c_33(U101^#(and(isNaturalKind(activate(V1)),
976.48/297.20	                             n__isLNatKind(activate(V2))),
976.48/297.20	                         activate(V1),
976.48/297.20	                         activate(V2)))
976.48/297.20	       , 70: U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.48/297.20	       , 71: U41^#(tt(), V1, V2) ->
976.48/297.20	             c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.48/297.20	       , 72: U51^#(tt(), V1, V2) ->
976.48/297.20	             c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.48/297.20	       , 73: U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.48/297.20	       , 74: U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.48/297.20	       , 75: U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.48/297.20	       , 76: U11^#(tt(), N, XS) ->
976.48/297.20	             c_34(snd^#(splitAt(activate(N), activate(XS))))
976.48/297.20	       , 77: U181^#(tt(), Y) -> c_61(activate^#(Y))
976.48/297.20	       , 78: U201^#(tt(), N, X, XS) ->
976.48/297.20	             c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.48/297.20	       , 79: U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.48/297.20	       , 80: U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.48/297.20	       , 81: U141^#(tt(), V1, V2) ->
976.48/297.20	             c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.48/297.20	       , 82: U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.48/297.20	       , 83: U151^#(tt(), V1, V2) ->
976.48/297.20	             c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.48/297.20	       , 84: U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.48/297.20	       , 85: U161^#(tt(), N) ->
976.48/297.20	             c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.48/297.20	       , 86: U171^#(tt(), N, XS) ->
976.48/297.20	             c_56(head^#(afterNth(activate(N), activate(XS))))
976.48/297.20	       , 87: U31^#(tt(), N) -> c_72(activate^#(N))
976.48/297.20	       , 88: U202^#(pair(YS, ZS), X) ->
976.48/297.20	             c_66(pair^#(cons(activate(X), YS), ZS))
976.48/297.20	       , 89: U21^#(tt(), X) -> c_67(activate^#(X))
976.48/297.20	       , 90: U211^#(tt(), XS) -> c_68(activate^#(XS))
976.48/297.20	       , 91: U221^#(tt(), N, XS) ->
976.48/297.20	             c_69(fst^#(splitAt(activate(N), activate(XS))))
976.48/297.20	       , 92: U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.48/297.20	       , 93: U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.48/297.20	       , 94: isPLNat^#(n__pair(V1, V2)) ->
976.48/297.20	             c_81(U141^#(and(isLNatKind(activate(V1)),
976.48/297.20	                             n__isLNatKind(activate(V2))),
976.48/297.20	                         activate(V1),
976.48/297.20	                         activate(V2)))
976.48/297.20	       , 95: isPLNat^#(n__splitAt(V1, V2)) ->
976.48/297.20	             c_82(U151^#(and(isNaturalKind(activate(V1)),
976.48/297.20	                             n__isLNatKind(activate(V2))),
976.48/297.20	                         activate(V1),
976.48/297.20	                         activate(V2)))
976.48/297.20	       , 96: isPLNatKind^#(n__pair(V1, V2)) ->
976.48/297.20	             c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.48/297.20	       , 97: isPLNatKind^#(n__splitAt(V1, V2)) ->
976.48/297.20	             c_97(and^#(isNaturalKind(activate(V1)),
976.48/297.20	                        n__isLNatKind(activate(V2))))
976.48/297.20	       , 98: U103^#(tt()) -> c_25()
976.48/297.20	       , 99: isNatural^#(n__0()) -> c_3()
976.48/297.20	       , 100: isNaturalKind^#(n__0()) -> c_92()
976.48/297.20	       , 101: isLNatKind^#(n__nil()) -> c_100()
976.48/297.20	       , 102: nil^#() -> c_64()
976.48/297.20	       , 103: 0^#() -> c_111()
976.48/297.20	       , 104: isLNat^#(n__nil()) -> c_27()
976.48/297.20	       , 105: U112^#(tt()) -> c_41()
976.48/297.21	       , 106: U122^#(tt()) -> c_43()
976.48/297.21	       , 107: U133^#(tt()) -> c_46()
976.48/297.21	       , 108: U143^#(tt()) -> c_49()
976.48/297.21	       , 109: U153^#(tt()) -> c_52()
976.48/297.21	       , 110: U43^#(tt()) -> c_75()
976.48/297.21	       , 111: U53^#(tt()) -> c_78()
976.48/297.21	       , 112: U62^#(tt()) -> c_80()
976.48/297.21	       , 113: U72^#(tt()) -> c_84()
976.48/297.21	       , 114: U82^#(tt()) -> c_86()
976.48/297.21	       , 115: U92^#(tt()) -> c_88() }
976.48/297.21	   
976.48/297.21	   We are left with following problem, upon which TcT provides the
976.48/297.21	   certificate MAYBE.
976.48/297.21	   
976.48/297.21	   Strict DPs:
976.48/297.21	     { U101^#(tt(), V1, V2) ->
976.48/297.21	       c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	     , isNatural^#(n__head(V1)) ->
976.48/297.21	       c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.21	     , isNatural^#(n__s(V1)) ->
976.48/297.21	       c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.21	     , isNatural^#(n__sel(V1, V2)) ->
976.48/297.21	       c_6(U131^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                      n__isLNatKind(activate(V2))),
976.48/297.21	                  activate(V1),
976.48/297.21	                  activate(V2)))
976.48/297.21	     , U131^#(tt(), V1, V2) ->
976.48/297.21	       c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	     , activate^#(X) -> c_7(X)
976.48/297.21	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.48/297.21	     , activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.48/297.21	     , activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.48/297.21	     , activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.48/297.21	     , activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.48/297.21	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.48/297.21	     , activate^#(n__fst(X)) -> c_15(fst^#(X))
976.48/297.21	     , activate^#(n__snd(X)) -> c_16(snd^#(X))
976.48/297.21	     , activate^#(n__tail(X)) -> c_17(tail^#(X))
976.48/297.21	     , activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.48/297.21	     , activate^#(n__head(X)) -> c_20(head^#(X))
976.48/297.21	     , activate^#(n__s(X)) -> c_21(s^#(X))
976.48/297.21	     , activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.48/297.21	     , activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.48/297.21	     , activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.48/297.21	     , natsFrom^#(N) ->
976.48/297.21	       c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.48/297.21	     , natsFrom^#(X) -> c_108(X)
976.48/297.21	     , isNaturalKind^#(X) -> c_91(X)
976.48/297.21	     , isNaturalKind^#(n__head(V1)) -> c_93(isLNatKind^#(activate(V1)))
976.48/297.21	     , isNaturalKind^#(n__s(V1)) -> c_94(isNaturalKind^#(activate(V1)))
976.48/297.21	     , isNaturalKind^#(n__sel(V1, V2)) ->
976.48/297.21	       c_95(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                  n__isLNatKind(activate(V2))))
976.48/297.21	     , and^#(X1, X2) -> c_89(X1, X2)
976.48/297.21	     , and^#(tt(), X) -> c_90(activate^#(X))
976.48/297.21	     , isLNatKind^#(X) -> c_98(X)
976.48/297.21	     , isLNatKind^#(n__natsFrom(V1)) ->
976.48/297.21	       c_99(isNaturalKind^#(activate(V1)))
976.48/297.21	     , isLNatKind^#(n__afterNth(V1, V2)) ->
976.48/297.21	       c_101(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                   n__isLNatKind(activate(V2))))
976.48/297.21	     , isLNatKind^#(n__cons(V1, V2)) ->
976.48/297.21	       c_102(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                   n__isLNatKind(activate(V2))))
976.48/297.21	     , isLNatKind^#(n__fst(V1)) -> c_103(isPLNatKind^#(activate(V1)))
976.48/297.21	     , isLNatKind^#(n__snd(V1)) -> c_104(isPLNatKind^#(activate(V1)))
976.48/297.21	     , isLNatKind^#(n__tail(V1)) -> c_105(isLNatKind^#(activate(V1)))
976.48/297.21	     , isLNatKind^#(n__take(V1, V2)) ->
976.48/297.21	       c_106(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                   n__isLNatKind(activate(V2))))
976.48/297.21	     , afterNth^#(N, XS) ->
976.48/297.21	       c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                      n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	                  N,
976.48/297.21	                  XS))
976.48/297.21	     , afterNth^#(X1, X2) -> c_60(X1, X2)
976.48/297.21	     , cons^#(X1, X2) -> c_54(X1, X2)
976.48/297.21	     , fst^#(X) -> c_70(X)
976.48/297.21	     , fst^#(pair(X, Y)) ->
976.48/297.21	       c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.21	                      n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.21	                  X))
976.48/297.21	     , snd^#(X) -> c_35(X)
976.48/297.21	     , snd^#(pair(X, Y)) ->
976.48/297.21	       c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.21	                       n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.21	                   Y))
976.48/297.21	     , tail^#(X) -> c_112(X)
976.48/297.21	     , tail^#(cons(N, XS)) ->
976.48/297.21	       c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                        n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.21	                    activate(XS)))
976.48/297.21	     , take^#(N, XS) ->
976.48/297.21	       c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	                    N,
976.48/297.21	                    XS))
976.48/297.21	     , take^#(X1, X2) -> c_115(X1, X2)
976.48/297.21	     , head^#(X) -> c_57(X)
976.48/297.21	     , head^#(cons(N, XS)) ->
976.48/297.21	       c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                      n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.21	                  N))
976.48/297.21	     , s^#(X) -> c_55(X)
976.48/297.21	     , sel^#(N, XS) ->
976.48/297.21	       c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	                    N,
976.48/297.21	                    XS))
976.48/297.21	     , sel^#(X1, X2) -> c_110(X1, X2)
976.48/297.21	     , pair^#(X1, X2) -> c_63(X1, X2)
976.48/297.21	     , splitAt^#(X1, X2) -> c_37(X1, X2)
976.48/297.21	     , splitAt^#(s(N), cons(X, XS)) ->
976.48/297.21	       c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                       n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.21	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.21	                   N,
976.48/297.21	                   X,
976.48/297.21	                   activate(XS)))
976.48/297.21	     , splitAt^#(0(), XS) ->
976.48/297.21	       c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.48/297.21	     , isLNat^#(n__natsFrom(V1)) ->
976.48/297.21	       c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.21	     , isLNat^#(n__afterNth(V1, V2)) ->
976.48/297.21	       c_28(U41^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                      n__isLNatKind(activate(V2))),
976.48/297.21	                  activate(V1),
976.48/297.21	                  activate(V2)))
976.48/297.21	     , isLNat^#(n__cons(V1, V2)) ->
976.48/297.21	       c_29(U51^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                      n__isLNatKind(activate(V2))),
976.48/297.21	                  activate(V1),
976.48/297.21	                  activate(V2)))
976.48/297.21	     , isLNat^#(n__fst(V1)) ->
976.48/297.21	       c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.21	     , isLNat^#(n__snd(V1)) ->
976.48/297.21	       c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.21	     , isLNat^#(n__tail(V1)) ->
976.48/297.21	       c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.21	     , isLNat^#(n__take(V1, V2)) ->
976.48/297.21	       c_33(U101^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                       n__isLNatKind(activate(V2))),
976.48/297.21	                   activate(V1),
976.48/297.21	                   activate(V2)))
976.48/297.21	     , U41^#(tt(), V1, V2) ->
976.48/297.21	       c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	     , U51^#(tt(), V1, V2) ->
976.48/297.21	       c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	     , U11^#(tt(), N, XS) ->
976.48/297.21	       c_34(snd^#(splitAt(activate(N), activate(XS))))
976.48/297.21	     , U181^#(tt(), Y) -> c_61(activate^#(Y))
976.48/297.21	     , U201^#(tt(), N, X, XS) ->
976.48/297.21	       c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.48/297.21	     , U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.48/297.21	     , U141^#(tt(), V1, V2) ->
976.48/297.21	       c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.48/297.21	     , U151^#(tt(), V1, V2) ->
976.48/297.21	       c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	     , U161^#(tt(), N) ->
976.48/297.21	       c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.48/297.21	     , U171^#(tt(), N, XS) ->
976.48/297.21	       c_56(head^#(afterNth(activate(N), activate(XS))))
976.48/297.21	     , U31^#(tt(), N) -> c_72(activate^#(N))
976.48/297.21	     , U202^#(pair(YS, ZS), X) ->
976.48/297.21	       c_66(pair^#(cons(activate(X), YS), ZS))
976.48/297.21	     , U21^#(tt(), X) -> c_67(activate^#(X))
976.48/297.21	     , U211^#(tt(), XS) -> c_68(activate^#(XS))
976.48/297.21	     , U221^#(tt(), N, XS) ->
976.48/297.21	       c_69(fst^#(splitAt(activate(N), activate(XS))))
976.48/297.21	     , isPLNat^#(n__pair(V1, V2)) ->
976.48/297.21	       c_81(U141^#(and(isLNatKind(activate(V1)),
976.48/297.21	                       n__isLNatKind(activate(V2))),
976.48/297.21	                   activate(V1),
976.48/297.21	                   activate(V2)))
976.48/297.21	     , isPLNat^#(n__splitAt(V1, V2)) ->
976.48/297.21	       c_82(U151^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                       n__isLNatKind(activate(V2))),
976.48/297.21	                   activate(V1),
976.48/297.21	                   activate(V2)))
976.48/297.21	     , isPLNatKind^#(n__pair(V1, V2)) ->
976.48/297.21	       c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.48/297.21	     , isPLNatKind^#(n__splitAt(V1, V2)) ->
976.48/297.21	       c_97(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                  n__isLNatKind(activate(V2)))) }
976.48/297.21	   Strict Trs:
976.48/297.21	     { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2))
976.48/297.21	     , U102(tt(), V2) -> U103(isLNat(activate(V2)))
976.48/297.21	     , isNatural(n__0()) -> tt()
976.48/297.21	     , isNatural(n__head(V1)) ->
976.48/297.21	       U111(isLNatKind(activate(V1)), activate(V1))
976.48/297.21	     , isNatural(n__s(V1)) ->
976.48/297.21	       U121(isNaturalKind(activate(V1)), activate(V1))
976.48/297.21	     , isNatural(n__sel(V1, V2)) ->
976.48/297.21	       U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.21	            activate(V1),
976.48/297.21	            activate(V2))
976.48/297.21	     , activate(X) -> X
976.48/297.21	     , activate(n__natsFrom(X)) -> natsFrom(X)
976.48/297.21	     , activate(n__isNaturalKind(X)) -> isNaturalKind(X)
976.48/297.21	     , activate(n__and(X1, X2)) -> and(X1, X2)
976.48/297.21	     , activate(n__isLNatKind(X)) -> isLNatKind(X)
976.48/297.21	     , activate(n__nil()) -> nil()
976.48/297.21	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
976.48/297.21	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
976.48/297.21	     , activate(n__fst(X)) -> fst(X)
976.48/297.21	     , activate(n__snd(X)) -> snd(X)
976.48/297.21	     , activate(n__tail(X)) -> tail(X)
976.48/297.21	     , activate(n__take(X1, X2)) -> take(X1, X2)
976.48/297.21	     , activate(n__0()) -> 0()
976.48/297.21	     , activate(n__head(X)) -> head(X)
976.48/297.21	     , activate(n__s(X)) -> s(X)
976.48/297.21	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
976.48/297.21	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
976.48/297.21	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
976.48/297.21	     , U103(tt()) -> tt()
976.48/297.21	     , isLNat(n__natsFrom(V1)) ->
976.48/297.21	       U71(isNaturalKind(activate(V1)), activate(V1))
976.48/297.21	     , isLNat(n__nil()) -> tt()
976.48/297.21	     , isLNat(n__afterNth(V1, V2)) ->
976.48/297.21	       U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.21	           activate(V1),
976.48/297.21	           activate(V2))
976.48/297.21	     , isLNat(n__cons(V1, V2)) ->
976.48/297.21	       U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.21	           activate(V1),
976.48/297.21	           activate(V2))
976.48/297.21	     , isLNat(n__fst(V1)) ->
976.48/297.21	       U61(isPLNatKind(activate(V1)), activate(V1))
976.48/297.21	     , isLNat(n__snd(V1)) ->
976.48/297.21	       U81(isPLNatKind(activate(V1)), activate(V1))
976.48/297.21	     , isLNat(n__tail(V1)) ->
976.48/297.21	       U91(isLNatKind(activate(V1)), activate(V1))
976.48/297.21	     , isLNat(n__take(V1, V2)) ->
976.48/297.21	       U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.21	            activate(V1),
976.48/297.21	            activate(V2))
976.48/297.21	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
976.48/297.21	     , snd(X) -> n__snd(X)
976.48/297.21	     , snd(pair(X, Y)) ->
976.48/297.21	       U181(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.21	                n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.21	            Y)
976.48/297.21	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
976.48/297.21	     , splitAt(s(N), cons(X, XS)) ->
976.48/297.21	       U201(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.21	                       n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.21	            N,
976.48/297.21	            X,
976.48/297.21	            activate(XS))
976.48/297.21	     , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
976.48/297.21	     , U111(tt(), V1) -> U112(isLNat(activate(V1)))
976.48/297.21	     , U112(tt()) -> tt()
976.48/297.21	     , U121(tt(), V1) -> U122(isNatural(activate(V1)))
976.48/297.21	     , U122(tt()) -> tt()
976.48/297.21	     , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2))
976.48/297.21	     , U132(tt(), V2) -> U133(isLNat(activate(V2)))
976.48/297.21	     , U133(tt()) -> tt()
976.48/297.21	     , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2))
976.48/297.21	     , U142(tt(), V2) -> U143(isLNat(activate(V2)))
976.48/297.21	     , U143(tt()) -> tt()
976.48/297.21	     , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2))
976.48/297.21	     , U152(tt(), V2) -> U153(isLNat(activate(V2)))
976.48/297.21	     , U153(tt()) -> tt()
976.48/297.21	     , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
976.48/297.21	     , cons(X1, X2) -> n__cons(X1, X2)
976.48/297.21	     , s(X) -> n__s(X)
976.48/297.21	     , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
976.48/297.21	     , head(X) -> n__head(X)
976.48/297.21	     , head(cons(N, XS)) ->
976.48/297.21	       U31(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	               n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.21	           N)
976.48/297.21	     , afterNth(N, XS) ->
976.48/297.21	       U11(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	               n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	           N,
976.48/297.21	           XS)
976.48/297.21	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
976.48/297.21	     , U181(tt(), Y) -> activate(Y)
976.48/297.21	     , U191(tt(), XS) -> pair(nil(), activate(XS))
976.48/297.21	     , pair(X1, X2) -> n__pair(X1, X2)
976.48/297.21	     , nil() -> n__nil()
976.48/297.21	     , U201(tt(), N, X, XS) ->
976.48/297.21	       U202(splitAt(activate(N), activate(XS)), activate(X))
976.48/297.21	     , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
976.48/297.21	     , U21(tt(), X) -> activate(X)
976.48/297.21	     , U211(tt(), XS) -> activate(XS)
976.48/297.21	     , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
976.48/297.21	     , fst(X) -> n__fst(X)
976.48/297.21	     , fst(pair(X, Y)) ->
976.48/297.21	       U21(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.21	               n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.21	           X)
976.48/297.21	     , U31(tt(), N) -> activate(N)
976.48/297.21	     , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2))
976.48/297.21	     , U42(tt(), V2) -> U43(isLNat(activate(V2)))
976.48/297.21	     , U43(tt()) -> tt()
976.48/297.21	     , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2))
976.48/297.21	     , U52(tt(), V2) -> U53(isLNat(activate(V2)))
976.48/297.21	     , U53(tt()) -> tt()
976.48/297.21	     , U61(tt(), V1) -> U62(isPLNat(activate(V1)))
976.48/297.21	     , U62(tt()) -> tt()
976.48/297.21	     , isPLNat(n__pair(V1, V2)) ->
976.48/297.21	       U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.21	            activate(V1),
976.48/297.21	            activate(V2))
976.48/297.21	     , isPLNat(n__splitAt(V1, V2)) ->
976.48/297.21	       U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.21	            activate(V1),
976.48/297.21	            activate(V2))
976.48/297.21	     , U71(tt(), V1) -> U72(isNatural(activate(V1)))
976.48/297.21	     , U72(tt()) -> tt()
976.48/297.21	     , U81(tt(), V1) -> U82(isPLNat(activate(V1)))
976.48/297.21	     , U82(tt()) -> tt()
976.48/297.21	     , U91(tt(), V1) -> U92(isLNat(activate(V1)))
976.48/297.21	     , U92(tt()) -> tt()
976.48/297.21	     , and(X1, X2) -> n__and(X1, X2)
976.48/297.21	     , and(tt(), X) -> activate(X)
976.48/297.21	     , isNaturalKind(X) -> n__isNaturalKind(X)
976.48/297.21	     , isNaturalKind(n__0()) -> tt()
976.48/297.21	     , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
976.48/297.21	     , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
976.48/297.21	     , isNaturalKind(n__sel(V1, V2)) ->
976.48/297.21	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.21	     , isPLNatKind(n__pair(V1, V2)) ->
976.48/297.21	       and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.21	     , isPLNatKind(n__splitAt(V1, V2)) ->
976.48/297.21	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.21	     , isLNatKind(X) -> n__isLNatKind(X)
976.48/297.21	     , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
976.48/297.21	     , isLNatKind(n__nil()) -> tt()
976.48/297.21	     , isLNatKind(n__afterNth(V1, V2)) ->
976.48/297.21	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.21	     , isLNatKind(n__cons(V1, V2)) ->
976.48/297.21	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.21	     , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
976.48/297.21	     , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
976.48/297.21	     , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
976.48/297.21	     , isLNatKind(n__take(V1, V2)) ->
976.48/297.21	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.21	     , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N)
976.48/297.21	     , natsFrom(X) -> n__natsFrom(X)
976.48/297.21	     , sel(N, XS) ->
976.48/297.21	       U171(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	            N,
976.48/297.21	            XS)
976.48/297.21	     , sel(X1, X2) -> n__sel(X1, X2)
976.48/297.21	     , 0() -> n__0()
976.48/297.21	     , tail(X) -> n__tail(X)
976.48/297.21	     , tail(cons(N, XS)) ->
976.48/297.21	       U211(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.21	            activate(XS))
976.48/297.21	     , take(N, XS) ->
976.48/297.21	       U221(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	            N,
976.48/297.21	            XS)
976.48/297.21	     , take(X1, X2) -> n__take(X1, X2) }
976.48/297.21	   Weak DPs:
976.48/297.21	     { U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.48/297.21	     , U103^#(tt()) -> c_25()
976.48/297.21	     , isNatural^#(n__0()) -> c_3()
976.48/297.21	     , U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.48/297.21	     , U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.48/297.21	     , activate^#(n__nil()) -> c_12(nil^#())
976.48/297.21	     , activate^#(n__0()) -> c_19(0^#())
976.48/297.21	     , isNaturalKind^#(n__0()) -> c_92()
976.48/297.21	     , isLNatKind^#(n__nil()) -> c_100()
976.48/297.21	     , nil^#() -> c_64()
976.48/297.21	     , 0^#() -> c_111()
976.48/297.21	     , isLNat^#(n__nil()) -> c_27()
976.48/297.21	     , U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.48/297.21	     , U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.48/297.21	     , U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.48/297.21	     , U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.48/297.21	     , U112^#(tt()) -> c_41()
976.48/297.21	     , U122^#(tt()) -> c_43()
976.48/297.21	     , U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.48/297.21	     , U133^#(tt()) -> c_46()
976.48/297.21	     , U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.48/297.21	     , U143^#(tt()) -> c_49()
976.48/297.21	     , U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.48/297.21	     , U153^#(tt()) -> c_52()
976.48/297.21	     , U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.48/297.21	     , U43^#(tt()) -> c_75()
976.48/297.21	     , U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.48/297.21	     , U53^#(tt()) -> c_78()
976.48/297.21	     , U62^#(tt()) -> c_80()
976.48/297.21	     , U72^#(tt()) -> c_84()
976.48/297.21	     , U82^#(tt()) -> c_86()
976.48/297.21	     , U92^#(tt()) -> c_88() }
976.48/297.21	   Obligation:
976.48/297.21	     runtime complexity
976.48/297.21	   Answer:
976.48/297.21	     MAYBE
976.48/297.21	   
976.48/297.21	   We estimate the number of application of
976.48/297.21	   {1,2,3,5,58,61,62,63,65,66,71,72} by applications of
976.48/297.21	   Pre({1,2,3,5,58,61,62,63,65,66,71,72}) =
976.48/297.21	   {4,6,23,24,28,30,39,40,41,43,45,48,49,51,53,54,55,59,60,64,80,81}.
976.48/297.21	   Here rules are labeled as follows:
976.48/297.21	   
976.48/297.21	     DPs:
976.48/297.21	       { 1: U101^#(tt(), V1, V2) ->
976.48/297.21	            c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	       , 2: isNatural^#(n__head(V1)) ->
976.48/297.21	            c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.21	       , 3: isNatural^#(n__s(V1)) ->
976.48/297.21	            c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.21	       , 4: isNatural^#(n__sel(V1, V2)) ->
976.48/297.21	            c_6(U131^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                           n__isLNatKind(activate(V2))),
976.48/297.21	                       activate(V1),
976.48/297.21	                       activate(V2)))
976.48/297.21	       , 5: U131^#(tt(), V1, V2) ->
976.48/297.21	            c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	       , 6: activate^#(X) -> c_7(X)
976.48/297.21	       , 7: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.48/297.21	       , 8: activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.48/297.21	       , 9: activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.48/297.21	       , 10: activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.48/297.21	       , 11: activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.48/297.21	       , 12: activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.48/297.21	       , 13: activate^#(n__fst(X)) -> c_15(fst^#(X))
976.48/297.21	       , 14: activate^#(n__snd(X)) -> c_16(snd^#(X))
976.48/297.21	       , 15: activate^#(n__tail(X)) -> c_17(tail^#(X))
976.48/297.21	       , 16: activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.48/297.21	       , 17: activate^#(n__head(X)) -> c_20(head^#(X))
976.48/297.21	       , 18: activate^#(n__s(X)) -> c_21(s^#(X))
976.48/297.21	       , 19: activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.48/297.21	       , 20: activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.48/297.21	       , 21: activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.48/297.21	       , 22: natsFrom^#(N) ->
976.48/297.21	             c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.48/297.21	       , 23: natsFrom^#(X) -> c_108(X)
976.48/297.21	       , 24: isNaturalKind^#(X) -> c_91(X)
976.48/297.21	       , 25: isNaturalKind^#(n__head(V1)) ->
976.48/297.21	             c_93(isLNatKind^#(activate(V1)))
976.48/297.21	       , 26: isNaturalKind^#(n__s(V1)) ->
976.48/297.21	             c_94(isNaturalKind^#(activate(V1)))
976.48/297.21	       , 27: isNaturalKind^#(n__sel(V1, V2)) ->
976.48/297.21	             c_95(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                        n__isLNatKind(activate(V2))))
976.48/297.21	       , 28: and^#(X1, X2) -> c_89(X1, X2)
976.48/297.21	       , 29: and^#(tt(), X) -> c_90(activate^#(X))
976.48/297.21	       , 30: isLNatKind^#(X) -> c_98(X)
976.48/297.21	       , 31: isLNatKind^#(n__natsFrom(V1)) ->
976.48/297.21	             c_99(isNaturalKind^#(activate(V1)))
976.48/297.21	       , 32: isLNatKind^#(n__afterNth(V1, V2)) ->
976.48/297.21	             c_101(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                         n__isLNatKind(activate(V2))))
976.48/297.21	       , 33: isLNatKind^#(n__cons(V1, V2)) ->
976.48/297.21	             c_102(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                         n__isLNatKind(activate(V2))))
976.48/297.21	       , 34: isLNatKind^#(n__fst(V1)) ->
976.48/297.21	             c_103(isPLNatKind^#(activate(V1)))
976.48/297.21	       , 35: isLNatKind^#(n__snd(V1)) ->
976.48/297.21	             c_104(isPLNatKind^#(activate(V1)))
976.48/297.21	       , 36: isLNatKind^#(n__tail(V1)) ->
976.48/297.21	             c_105(isLNatKind^#(activate(V1)))
976.48/297.21	       , 37: isLNatKind^#(n__take(V1, V2)) ->
976.48/297.21	             c_106(and^#(isNaturalKind(activate(V1)),
976.48/297.21	                         n__isLNatKind(activate(V2))))
976.48/297.21	       , 38: afterNth^#(N, XS) ->
976.48/297.21	             c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                            n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	                        N,
976.48/297.21	                        XS))
976.48/297.21	       , 39: afterNth^#(X1, X2) -> c_60(X1, X2)
976.48/297.21	       , 40: cons^#(X1, X2) -> c_54(X1, X2)
976.48/297.21	       , 41: fst^#(X) -> c_70(X)
976.48/297.21	       , 42: fst^#(pair(X, Y)) ->
976.48/297.21	             c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.21	                            n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.21	                        X))
976.48/297.21	       , 43: snd^#(X) -> c_35(X)
976.48/297.21	       , 44: snd^#(pair(X, Y)) ->
976.48/297.21	             c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.21	                             n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.21	                         Y))
976.48/297.21	       , 45: tail^#(X) -> c_112(X)
976.48/297.21	       , 46: tail^#(cons(N, XS)) ->
976.48/297.21	             c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.21	                          activate(XS)))
976.48/297.21	       , 47: take^#(N, XS) ->
976.48/297.21	             c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	                          N,
976.48/297.21	                          XS))
976.48/297.21	       , 48: take^#(X1, X2) -> c_115(X1, X2)
976.48/297.21	       , 49: head^#(X) -> c_57(X)
976.48/297.21	       , 50: head^#(cons(N, XS)) ->
976.48/297.21	             c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                            n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.21	                        N))
976.48/297.21	       , 51: s^#(X) -> c_55(X)
976.48/297.21	       , 52: sel^#(N, XS) ->
976.48/297.21	             c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.21	                          N,
976.48/297.21	                          XS))
976.48/297.21	       , 53: sel^#(X1, X2) -> c_110(X1, X2)
976.48/297.21	       , 54: pair^#(X1, X2) -> c_63(X1, X2)
976.48/297.21	       , 55: splitAt^#(X1, X2) -> c_37(X1, X2)
976.48/297.21	       , 56: splitAt^#(s(N), cons(X, XS)) ->
976.48/297.21	             c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.21	                             n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.21	                                    n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.21	                         N,
976.48/297.21	                         X,
976.48/297.21	                         activate(XS)))
976.48/297.21	       , 57: splitAt^#(0(), XS) ->
976.48/297.21	             c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.48/297.21	       , 58: isLNat^#(n__natsFrom(V1)) ->
976.48/297.21	             c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.21	       , 59: isLNat^#(n__afterNth(V1, V2)) ->
976.48/297.21	             c_28(U41^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                            n__isLNatKind(activate(V2))),
976.48/297.21	                        activate(V1),
976.48/297.21	                        activate(V2)))
976.48/297.21	       , 60: isLNat^#(n__cons(V1, V2)) ->
976.48/297.21	             c_29(U51^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                            n__isLNatKind(activate(V2))),
976.48/297.21	                        activate(V1),
976.48/297.21	                        activate(V2)))
976.48/297.21	       , 61: isLNat^#(n__fst(V1)) ->
976.48/297.21	             c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.21	       , 62: isLNat^#(n__snd(V1)) ->
976.48/297.21	             c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.21	       , 63: isLNat^#(n__tail(V1)) ->
976.48/297.21	             c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.21	       , 64: isLNat^#(n__take(V1, V2)) ->
976.48/297.21	             c_33(U101^#(and(isNaturalKind(activate(V1)),
976.48/297.21	                             n__isLNatKind(activate(V2))),
976.48/297.21	                         activate(V1),
976.48/297.21	                         activate(V2)))
976.48/297.21	       , 65: U41^#(tt(), V1, V2) ->
976.48/297.21	             c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.48/297.21	       , 66: U51^#(tt(), V1, V2) ->
976.48/297.21	             c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.48/297.22	       , 67: U11^#(tt(), N, XS) ->
976.48/297.22	             c_34(snd^#(splitAt(activate(N), activate(XS))))
976.48/297.22	       , 68: U181^#(tt(), Y) -> c_61(activate^#(Y))
976.48/297.22	       , 69: U201^#(tt(), N, X, XS) ->
976.48/297.22	             c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.48/297.22	       , 70: U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.48/297.22	       , 71: U141^#(tt(), V1, V2) ->
976.48/297.22	             c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.48/297.22	       , 72: U151^#(tt(), V1, V2) ->
976.48/297.22	             c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.48/297.22	       , 73: U161^#(tt(), N) ->
976.48/297.22	             c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.48/297.22	       , 74: U171^#(tt(), N, XS) ->
976.48/297.22	             c_56(head^#(afterNth(activate(N), activate(XS))))
976.48/297.22	       , 75: U31^#(tt(), N) -> c_72(activate^#(N))
976.48/297.22	       , 76: U202^#(pair(YS, ZS), X) ->
976.48/297.22	             c_66(pair^#(cons(activate(X), YS), ZS))
976.48/297.22	       , 77: U21^#(tt(), X) -> c_67(activate^#(X))
976.48/297.22	       , 78: U211^#(tt(), XS) -> c_68(activate^#(XS))
976.48/297.22	       , 79: U221^#(tt(), N, XS) ->
976.48/297.22	             c_69(fst^#(splitAt(activate(N), activate(XS))))
976.48/297.22	       , 80: isPLNat^#(n__pair(V1, V2)) ->
976.48/297.22	             c_81(U141^#(and(isLNatKind(activate(V1)),
976.48/297.22	                             n__isLNatKind(activate(V2))),
976.48/297.22	                         activate(V1),
976.48/297.22	                         activate(V2)))
976.48/297.22	       , 81: isPLNat^#(n__splitAt(V1, V2)) ->
976.48/297.22	             c_82(U151^#(and(isNaturalKind(activate(V1)),
976.48/297.22	                             n__isLNatKind(activate(V2))),
976.48/297.22	                         activate(V1),
976.48/297.22	                         activate(V2)))
976.48/297.22	       , 82: isPLNatKind^#(n__pair(V1, V2)) ->
976.48/297.22	             c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.48/297.22	       , 83: isPLNatKind^#(n__splitAt(V1, V2)) ->
976.48/297.22	             c_97(and^#(isNaturalKind(activate(V1)),
976.48/297.22	                        n__isLNatKind(activate(V2))))
976.48/297.22	       , 84: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.48/297.22	       , 85: U103^#(tt()) -> c_25()
976.48/297.22	       , 86: isNatural^#(n__0()) -> c_3()
976.48/297.22	       , 87: U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.48/297.22	       , 88: U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.48/297.22	       , 89: activate^#(n__nil()) -> c_12(nil^#())
976.48/297.22	       , 90: activate^#(n__0()) -> c_19(0^#())
976.48/297.22	       , 91: isNaturalKind^#(n__0()) -> c_92()
976.48/297.22	       , 92: isLNatKind^#(n__nil()) -> c_100()
976.48/297.22	       , 93: nil^#() -> c_64()
976.48/297.22	       , 94: 0^#() -> c_111()
976.48/297.22	       , 95: isLNat^#(n__nil()) -> c_27()
976.48/297.22	       , 96: U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.48/297.22	       , 97: U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.48/297.22	       , 98: U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.48/297.22	       , 99: U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.48/297.22	       , 100: U112^#(tt()) -> c_41()
976.48/297.22	       , 101: U122^#(tt()) -> c_43()
976.48/297.22	       , 102: U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.48/297.22	       , 103: U133^#(tt()) -> c_46()
976.48/297.22	       , 104: U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.48/297.22	       , 105: U143^#(tt()) -> c_49()
976.48/297.22	       , 106: U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.48/297.22	       , 107: U153^#(tt()) -> c_52()
976.48/297.22	       , 108: U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.48/297.22	       , 109: U43^#(tt()) -> c_75()
976.48/297.22	       , 110: U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.48/297.22	       , 111: U53^#(tt()) -> c_78()
976.48/297.22	       , 112: U62^#(tt()) -> c_80()
976.48/297.22	       , 113: U72^#(tt()) -> c_84()
976.48/297.22	       , 114: U82^#(tt()) -> c_86()
976.48/297.22	       , 115: U92^#(tt()) -> c_88() }
976.48/297.22	   
976.48/297.22	   We are left with following problem, upon which TcT provides the
976.48/297.22	   certificate MAYBE.
976.48/297.22	   
976.48/297.22	   Strict DPs:
976.48/297.22	     { isNatural^#(n__sel(V1, V2)) ->
976.48/297.22	       c_6(U131^#(and(isNaturalKind(activate(V1)),
976.48/297.22	                      n__isLNatKind(activate(V2))),
976.48/297.22	                  activate(V1),
976.48/297.22	                  activate(V2)))
976.48/297.22	     , activate^#(X) -> c_7(X)
976.48/297.22	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.48/297.22	     , activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.48/297.22	     , activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.48/297.22	     , activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.48/297.22	     , activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.48/297.22	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.48/297.22	     , activate^#(n__fst(X)) -> c_15(fst^#(X))
976.48/297.22	     , activate^#(n__snd(X)) -> c_16(snd^#(X))
976.48/297.22	     , activate^#(n__tail(X)) -> c_17(tail^#(X))
976.48/297.22	     , activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.48/297.22	     , activate^#(n__head(X)) -> c_20(head^#(X))
976.48/297.22	     , activate^#(n__s(X)) -> c_21(s^#(X))
976.48/297.22	     , activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.48/297.22	     , activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.48/297.22	     , activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.48/297.22	     , natsFrom^#(N) ->
976.48/297.22	       c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.48/297.22	     , natsFrom^#(X) -> c_108(X)
976.48/297.22	     , isNaturalKind^#(X) -> c_91(X)
976.48/297.22	     , isNaturalKind^#(n__head(V1)) -> c_93(isLNatKind^#(activate(V1)))
976.48/297.22	     , isNaturalKind^#(n__s(V1)) -> c_94(isNaturalKind^#(activate(V1)))
976.48/297.22	     , isNaturalKind^#(n__sel(V1, V2)) ->
976.48/297.22	       c_95(and^#(isNaturalKind(activate(V1)),
976.48/297.22	                  n__isLNatKind(activate(V2))))
976.48/297.22	     , and^#(X1, X2) -> c_89(X1, X2)
976.48/297.22	     , and^#(tt(), X) -> c_90(activate^#(X))
976.48/297.22	     , isLNatKind^#(X) -> c_98(X)
976.48/297.22	     , isLNatKind^#(n__natsFrom(V1)) ->
976.48/297.22	       c_99(isNaturalKind^#(activate(V1)))
976.48/297.22	     , isLNatKind^#(n__afterNth(V1, V2)) ->
976.48/297.22	       c_101(and^#(isNaturalKind(activate(V1)),
976.48/297.22	                   n__isLNatKind(activate(V2))))
976.48/297.22	     , isLNatKind^#(n__cons(V1, V2)) ->
976.48/297.22	       c_102(and^#(isNaturalKind(activate(V1)),
976.48/297.22	                   n__isLNatKind(activate(V2))))
976.48/297.22	     , isLNatKind^#(n__fst(V1)) -> c_103(isPLNatKind^#(activate(V1)))
976.48/297.22	     , isLNatKind^#(n__snd(V1)) -> c_104(isPLNatKind^#(activate(V1)))
976.48/297.22	     , isLNatKind^#(n__tail(V1)) -> c_105(isLNatKind^#(activate(V1)))
976.48/297.22	     , isLNatKind^#(n__take(V1, V2)) ->
976.48/297.22	       c_106(and^#(isNaturalKind(activate(V1)),
976.48/297.22	                   n__isLNatKind(activate(V2))))
976.48/297.22	     , afterNth^#(N, XS) ->
976.48/297.22	       c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	                      n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.22	                  N,
976.48/297.22	                  XS))
976.48/297.22	     , afterNth^#(X1, X2) -> c_60(X1, X2)
976.48/297.22	     , cons^#(X1, X2) -> c_54(X1, X2)
976.48/297.22	     , fst^#(X) -> c_70(X)
976.48/297.22	     , fst^#(pair(X, Y)) ->
976.48/297.22	       c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.22	                      n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.22	                  X))
976.48/297.22	     , snd^#(X) -> c_35(X)
976.48/297.22	     , snd^#(pair(X, Y)) ->
976.48/297.22	       c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.22	                       n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.22	                   Y))
976.48/297.22	     , tail^#(X) -> c_112(X)
976.48/297.22	     , tail^#(cons(N, XS)) ->
976.48/297.22	       c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	                        n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.22	                    activate(XS)))
976.48/297.22	     , take^#(N, XS) ->
976.48/297.22	       c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.22	                    N,
976.48/297.22	                    XS))
976.48/297.22	     , take^#(X1, X2) -> c_115(X1, X2)
976.48/297.22	     , head^#(X) -> c_57(X)
976.48/297.22	     , head^#(cons(N, XS)) ->
976.48/297.22	       c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	                      n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.22	                  N))
976.48/297.22	     , s^#(X) -> c_55(X)
976.48/297.22	     , sel^#(N, XS) ->
976.48/297.22	       c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.22	                    N,
976.48/297.22	                    XS))
976.48/297.22	     , sel^#(X1, X2) -> c_110(X1, X2)
976.48/297.22	     , pair^#(X1, X2) -> c_63(X1, X2)
976.48/297.22	     , splitAt^#(X1, X2) -> c_37(X1, X2)
976.48/297.22	     , splitAt^#(s(N), cons(X, XS)) ->
976.48/297.22	       c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	                       n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.22	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.22	                   N,
976.48/297.22	                   X,
976.48/297.22	                   activate(XS)))
976.48/297.22	     , splitAt^#(0(), XS) ->
976.48/297.22	       c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.48/297.22	     , isLNat^#(n__afterNth(V1, V2)) ->
976.48/297.22	       c_28(U41^#(and(isNaturalKind(activate(V1)),
976.48/297.22	                      n__isLNatKind(activate(V2))),
976.48/297.22	                  activate(V1),
976.48/297.22	                  activate(V2)))
976.48/297.22	     , isLNat^#(n__cons(V1, V2)) ->
976.48/297.22	       c_29(U51^#(and(isNaturalKind(activate(V1)),
976.48/297.22	                      n__isLNatKind(activate(V2))),
976.48/297.22	                  activate(V1),
976.48/297.22	                  activate(V2)))
976.48/297.22	     , isLNat^#(n__take(V1, V2)) ->
976.48/297.22	       c_33(U101^#(and(isNaturalKind(activate(V1)),
976.48/297.22	                       n__isLNatKind(activate(V2))),
976.48/297.22	                   activate(V1),
976.48/297.22	                   activate(V2)))
976.48/297.22	     , U11^#(tt(), N, XS) ->
976.48/297.22	       c_34(snd^#(splitAt(activate(N), activate(XS))))
976.48/297.22	     , U181^#(tt(), Y) -> c_61(activate^#(Y))
976.48/297.22	     , U201^#(tt(), N, X, XS) ->
976.48/297.22	       c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.48/297.22	     , U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.48/297.22	     , U161^#(tt(), N) ->
976.48/297.22	       c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.48/297.22	     , U171^#(tt(), N, XS) ->
976.48/297.22	       c_56(head^#(afterNth(activate(N), activate(XS))))
976.48/297.22	     , U31^#(tt(), N) -> c_72(activate^#(N))
976.48/297.22	     , U202^#(pair(YS, ZS), X) ->
976.48/297.22	       c_66(pair^#(cons(activate(X), YS), ZS))
976.48/297.22	     , U21^#(tt(), X) -> c_67(activate^#(X))
976.48/297.22	     , U211^#(tt(), XS) -> c_68(activate^#(XS))
976.48/297.22	     , U221^#(tt(), N, XS) ->
976.48/297.22	       c_69(fst^#(splitAt(activate(N), activate(XS))))
976.48/297.22	     , isPLNat^#(n__pair(V1, V2)) ->
976.48/297.22	       c_81(U141^#(and(isLNatKind(activate(V1)),
976.48/297.22	                       n__isLNatKind(activate(V2))),
976.48/297.22	                   activate(V1),
976.48/297.22	                   activate(V2)))
976.48/297.22	     , isPLNat^#(n__splitAt(V1, V2)) ->
976.48/297.22	       c_82(U151^#(and(isNaturalKind(activate(V1)),
976.48/297.22	                       n__isLNatKind(activate(V2))),
976.48/297.22	                   activate(V1),
976.48/297.22	                   activate(V2)))
976.48/297.22	     , isPLNatKind^#(n__pair(V1, V2)) ->
976.48/297.22	       c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.48/297.22	     , isPLNatKind^#(n__splitAt(V1, V2)) ->
976.48/297.22	       c_97(and^#(isNaturalKind(activate(V1)),
976.48/297.22	                  n__isLNatKind(activate(V2)))) }
976.48/297.22	   Strict Trs:
976.48/297.22	     { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2))
976.48/297.22	     , U102(tt(), V2) -> U103(isLNat(activate(V2)))
976.48/297.22	     , isNatural(n__0()) -> tt()
976.48/297.22	     , isNatural(n__head(V1)) ->
976.48/297.22	       U111(isLNatKind(activate(V1)), activate(V1))
976.48/297.22	     , isNatural(n__s(V1)) ->
976.48/297.22	       U121(isNaturalKind(activate(V1)), activate(V1))
976.48/297.22	     , isNatural(n__sel(V1, V2)) ->
976.48/297.22	       U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.22	            activate(V1),
976.48/297.22	            activate(V2))
976.48/297.22	     , activate(X) -> X
976.48/297.22	     , activate(n__natsFrom(X)) -> natsFrom(X)
976.48/297.22	     , activate(n__isNaturalKind(X)) -> isNaturalKind(X)
976.48/297.22	     , activate(n__and(X1, X2)) -> and(X1, X2)
976.48/297.22	     , activate(n__isLNatKind(X)) -> isLNatKind(X)
976.48/297.22	     , activate(n__nil()) -> nil()
976.48/297.22	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
976.48/297.22	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
976.48/297.22	     , activate(n__fst(X)) -> fst(X)
976.48/297.22	     , activate(n__snd(X)) -> snd(X)
976.48/297.22	     , activate(n__tail(X)) -> tail(X)
976.48/297.22	     , activate(n__take(X1, X2)) -> take(X1, X2)
976.48/297.22	     , activate(n__0()) -> 0()
976.48/297.22	     , activate(n__head(X)) -> head(X)
976.48/297.22	     , activate(n__s(X)) -> s(X)
976.48/297.22	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
976.48/297.22	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
976.48/297.22	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
976.48/297.22	     , U103(tt()) -> tt()
976.48/297.22	     , isLNat(n__natsFrom(V1)) ->
976.48/297.22	       U71(isNaturalKind(activate(V1)), activate(V1))
976.48/297.22	     , isLNat(n__nil()) -> tt()
976.48/297.22	     , isLNat(n__afterNth(V1, V2)) ->
976.48/297.22	       U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.22	           activate(V1),
976.48/297.22	           activate(V2))
976.48/297.22	     , isLNat(n__cons(V1, V2)) ->
976.48/297.22	       U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.22	           activate(V1),
976.48/297.22	           activate(V2))
976.48/297.22	     , isLNat(n__fst(V1)) ->
976.48/297.22	       U61(isPLNatKind(activate(V1)), activate(V1))
976.48/297.22	     , isLNat(n__snd(V1)) ->
976.48/297.22	       U81(isPLNatKind(activate(V1)), activate(V1))
976.48/297.22	     , isLNat(n__tail(V1)) ->
976.48/297.22	       U91(isLNatKind(activate(V1)), activate(V1))
976.48/297.22	     , isLNat(n__take(V1, V2)) ->
976.48/297.22	       U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.22	            activate(V1),
976.48/297.22	            activate(V2))
976.48/297.22	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
976.48/297.22	     , snd(X) -> n__snd(X)
976.48/297.22	     , snd(pair(X, Y)) ->
976.48/297.22	       U181(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.22	                n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.22	            Y)
976.48/297.22	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
976.48/297.22	     , splitAt(s(N), cons(X, XS)) ->
976.48/297.22	       U201(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	                n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.22	                       n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.22	            N,
976.48/297.22	            X,
976.48/297.22	            activate(XS))
976.48/297.22	     , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
976.48/297.22	     , U111(tt(), V1) -> U112(isLNat(activate(V1)))
976.48/297.22	     , U112(tt()) -> tt()
976.48/297.22	     , U121(tt(), V1) -> U122(isNatural(activate(V1)))
976.48/297.22	     , U122(tt()) -> tt()
976.48/297.22	     , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2))
976.48/297.22	     , U132(tt(), V2) -> U133(isLNat(activate(V2)))
976.48/297.22	     , U133(tt()) -> tt()
976.48/297.22	     , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2))
976.48/297.22	     , U142(tt(), V2) -> U143(isLNat(activate(V2)))
976.48/297.22	     , U143(tt()) -> tt()
976.48/297.22	     , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2))
976.48/297.22	     , U152(tt(), V2) -> U153(isLNat(activate(V2)))
976.48/297.22	     , U153(tt()) -> tt()
976.48/297.22	     , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
976.48/297.22	     , cons(X1, X2) -> n__cons(X1, X2)
976.48/297.22	     , s(X) -> n__s(X)
976.48/297.22	     , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
976.48/297.22	     , head(X) -> n__head(X)
976.48/297.22	     , head(cons(N, XS)) ->
976.48/297.22	       U31(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	               n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.22	           N)
976.48/297.22	     , afterNth(N, XS) ->
976.48/297.22	       U11(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.22	               n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.22	           N,
976.48/297.22	           XS)
976.48/297.22	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
976.48/297.22	     , U181(tt(), Y) -> activate(Y)
976.48/297.22	     , U191(tt(), XS) -> pair(nil(), activate(XS))
976.48/297.22	     , pair(X1, X2) -> n__pair(X1, X2)
976.48/297.22	     , nil() -> n__nil()
976.48/297.22	     , U201(tt(), N, X, XS) ->
976.48/297.22	       U202(splitAt(activate(N), activate(XS)), activate(X))
976.48/297.22	     , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
976.48/297.22	     , U21(tt(), X) -> activate(X)
976.48/297.22	     , U211(tt(), XS) -> activate(XS)
976.48/297.22	     , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
976.48/297.22	     , fst(X) -> n__fst(X)
976.48/297.22	     , fst(pair(X, Y)) ->
976.48/297.22	       U21(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.22	               n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.22	           X)
976.48/297.22	     , U31(tt(), N) -> activate(N)
976.48/297.22	     , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2))
976.48/297.22	     , U42(tt(), V2) -> U43(isLNat(activate(V2)))
976.48/297.22	     , U43(tt()) -> tt()
976.48/297.22	     , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2))
976.48/297.22	     , U52(tt(), V2) -> U53(isLNat(activate(V2)))
976.48/297.22	     , U53(tt()) -> tt()
976.48/297.22	     , U61(tt(), V1) -> U62(isPLNat(activate(V1)))
976.48/297.22	     , U62(tt()) -> tt()
976.48/297.22	     , isPLNat(n__pair(V1, V2)) ->
976.48/297.22	       U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.22	            activate(V1),
976.48/297.22	            activate(V2))
976.48/297.22	     , isPLNat(n__splitAt(V1, V2)) ->
976.48/297.22	       U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.22	            activate(V1),
976.48/297.22	            activate(V2))
976.48/297.22	     , U71(tt(), V1) -> U72(isNatural(activate(V1)))
976.48/297.22	     , U72(tt()) -> tt()
976.48/297.22	     , U81(tt(), V1) -> U82(isPLNat(activate(V1)))
976.48/297.22	     , U82(tt()) -> tt()
976.48/297.22	     , U91(tt(), V1) -> U92(isLNat(activate(V1)))
976.48/297.22	     , U92(tt()) -> tt()
976.48/297.22	     , and(X1, X2) -> n__and(X1, X2)
976.48/297.22	     , and(tt(), X) -> activate(X)
976.48/297.22	     , isNaturalKind(X) -> n__isNaturalKind(X)
976.48/297.22	     , isNaturalKind(n__0()) -> tt()
976.48/297.22	     , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
976.48/297.22	     , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
976.48/297.22	     , isNaturalKind(n__sel(V1, V2)) ->
976.48/297.22	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.22	     , isPLNatKind(n__pair(V1, V2)) ->
976.48/297.22	       and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.23	     , isPLNatKind(n__splitAt(V1, V2)) ->
976.48/297.23	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.23	     , isLNatKind(X) -> n__isLNatKind(X)
976.48/297.23	     , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
976.48/297.23	     , isLNatKind(n__nil()) -> tt()
976.48/297.23	     , isLNatKind(n__afterNth(V1, V2)) ->
976.48/297.23	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.23	     , isLNatKind(n__cons(V1, V2)) ->
976.48/297.23	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.23	     , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
976.48/297.23	     , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
976.48/297.23	     , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
976.48/297.23	     , isLNatKind(n__take(V1, V2)) ->
976.48/297.23	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.23	     , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N)
976.48/297.23	     , natsFrom(X) -> n__natsFrom(X)
976.48/297.23	     , sel(N, XS) ->
976.48/297.23	       U171(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.23	            N,
976.48/297.23	            XS)
976.48/297.23	     , sel(X1, X2) -> n__sel(X1, X2)
976.48/297.23	     , 0() -> n__0()
976.48/297.23	     , tail(X) -> n__tail(X)
976.48/297.23	     , tail(cons(N, XS)) ->
976.48/297.23	       U211(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.23	            activate(XS))
976.48/297.23	     , take(N, XS) ->
976.48/297.23	       U221(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.23	            N,
976.48/297.23	            XS)
976.48/297.23	     , take(X1, X2) -> n__take(X1, X2) }
976.48/297.23	   Weak DPs:
976.48/297.23	     { U101^#(tt(), V1, V2) ->
976.48/297.23	       c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	     , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.48/297.23	     , U103^#(tt()) -> c_25()
976.48/297.23	     , isNatural^#(n__0()) -> c_3()
976.48/297.23	     , isNatural^#(n__head(V1)) ->
976.48/297.23	       c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.23	     , isNatural^#(n__s(V1)) ->
976.48/297.23	       c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.23	     , U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.48/297.23	     , U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.48/297.23	     , U131^#(tt(), V1, V2) ->
976.48/297.23	       c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	     , activate^#(n__nil()) -> c_12(nil^#())
976.48/297.23	     , activate^#(n__0()) -> c_19(0^#())
976.48/297.23	     , isNaturalKind^#(n__0()) -> c_92()
976.48/297.23	     , isLNatKind^#(n__nil()) -> c_100()
976.48/297.23	     , nil^#() -> c_64()
976.48/297.23	     , 0^#() -> c_111()
976.48/297.23	     , isLNat^#(n__natsFrom(V1)) ->
976.48/297.23	       c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.23	     , isLNat^#(n__nil()) -> c_27()
976.48/297.23	     , isLNat^#(n__fst(V1)) ->
976.48/297.23	       c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.23	     , isLNat^#(n__snd(V1)) ->
976.48/297.23	       c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.23	     , isLNat^#(n__tail(V1)) ->
976.48/297.23	       c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.23	     , U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.48/297.23	     , U41^#(tt(), V1, V2) ->
976.48/297.23	       c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	     , U51^#(tt(), V1, V2) ->
976.48/297.23	       c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	     , U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.48/297.23	     , U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.48/297.23	     , U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.48/297.23	     , U112^#(tt()) -> c_41()
976.48/297.23	     , U122^#(tt()) -> c_43()
976.48/297.23	     , U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.48/297.23	     , U133^#(tt()) -> c_46()
976.48/297.23	     , U141^#(tt(), V1, V2) ->
976.48/297.23	       c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.48/297.23	     , U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.48/297.23	     , U143^#(tt()) -> c_49()
976.48/297.23	     , U151^#(tt(), V1, V2) ->
976.48/297.23	       c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	     , U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.48/297.23	     , U153^#(tt()) -> c_52()
976.48/297.23	     , U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.48/297.23	     , U43^#(tt()) -> c_75()
976.48/297.23	     , U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.48/297.23	     , U53^#(tt()) -> c_78()
976.48/297.23	     , U62^#(tt()) -> c_80()
976.48/297.23	     , U72^#(tt()) -> c_84()
976.48/297.23	     , U82^#(tt()) -> c_86()
976.48/297.23	     , U92^#(tt()) -> c_88() }
976.48/297.23	   Obligation:
976.48/297.23	     runtime complexity
976.48/297.23	   Answer:
976.48/297.23	     MAYBE
976.48/297.23	   
976.48/297.23	   We estimate the number of application of {1,54,55,56,68,69} by
976.48/297.23	   applications of Pre({1,54,55,56,68,69}) =
976.48/297.23	   {2,19,20,24,26,35,36,37,39,41,44,45,47,49,50,51}. Here rules are
976.48/297.23	   labeled as follows:
976.48/297.23	   
976.48/297.23	     DPs:
976.48/297.23	       { 1: isNatural^#(n__sel(V1, V2)) ->
976.48/297.23	            c_6(U131^#(and(isNaturalKind(activate(V1)),
976.48/297.23	                           n__isLNatKind(activate(V2))),
976.48/297.23	                       activate(V1),
976.48/297.23	                       activate(V2)))
976.48/297.23	       , 2: activate^#(X) -> c_7(X)
976.48/297.23	       , 3: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.48/297.23	       , 4: activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.48/297.23	       , 5: activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.48/297.23	       , 6: activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.48/297.23	       , 7: activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.48/297.23	       , 8: activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.48/297.23	       , 9: activate^#(n__fst(X)) -> c_15(fst^#(X))
976.48/297.23	       , 10: activate^#(n__snd(X)) -> c_16(snd^#(X))
976.48/297.23	       , 11: activate^#(n__tail(X)) -> c_17(tail^#(X))
976.48/297.23	       , 12: activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.48/297.23	       , 13: activate^#(n__head(X)) -> c_20(head^#(X))
976.48/297.23	       , 14: activate^#(n__s(X)) -> c_21(s^#(X))
976.48/297.23	       , 15: activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.48/297.23	       , 16: activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.48/297.23	       , 17: activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.48/297.23	       , 18: natsFrom^#(N) ->
976.48/297.23	             c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.48/297.23	       , 19: natsFrom^#(X) -> c_108(X)
976.48/297.23	       , 20: isNaturalKind^#(X) -> c_91(X)
976.48/297.23	       , 21: isNaturalKind^#(n__head(V1)) ->
976.48/297.23	             c_93(isLNatKind^#(activate(V1)))
976.48/297.23	       , 22: isNaturalKind^#(n__s(V1)) ->
976.48/297.23	             c_94(isNaturalKind^#(activate(V1)))
976.48/297.23	       , 23: isNaturalKind^#(n__sel(V1, V2)) ->
976.48/297.23	             c_95(and^#(isNaturalKind(activate(V1)),
976.48/297.23	                        n__isLNatKind(activate(V2))))
976.48/297.23	       , 24: and^#(X1, X2) -> c_89(X1, X2)
976.48/297.23	       , 25: and^#(tt(), X) -> c_90(activate^#(X))
976.48/297.23	       , 26: isLNatKind^#(X) -> c_98(X)
976.48/297.23	       , 27: isLNatKind^#(n__natsFrom(V1)) ->
976.48/297.23	             c_99(isNaturalKind^#(activate(V1)))
976.48/297.23	       , 28: isLNatKind^#(n__afterNth(V1, V2)) ->
976.48/297.23	             c_101(and^#(isNaturalKind(activate(V1)),
976.48/297.23	                         n__isLNatKind(activate(V2))))
976.48/297.23	       , 29: isLNatKind^#(n__cons(V1, V2)) ->
976.48/297.23	             c_102(and^#(isNaturalKind(activate(V1)),
976.48/297.23	                         n__isLNatKind(activate(V2))))
976.48/297.23	       , 30: isLNatKind^#(n__fst(V1)) ->
976.48/297.23	             c_103(isPLNatKind^#(activate(V1)))
976.48/297.23	       , 31: isLNatKind^#(n__snd(V1)) ->
976.48/297.23	             c_104(isPLNatKind^#(activate(V1)))
976.48/297.23	       , 32: isLNatKind^#(n__tail(V1)) ->
976.48/297.23	             c_105(isLNatKind^#(activate(V1)))
976.48/297.23	       , 33: isLNatKind^#(n__take(V1, V2)) ->
976.48/297.23	             c_106(and^#(isNaturalKind(activate(V1)),
976.48/297.23	                         n__isLNatKind(activate(V2))))
976.48/297.23	       , 34: afterNth^#(N, XS) ->
976.48/297.23	             c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                            n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.23	                        N,
976.48/297.23	                        XS))
976.48/297.23	       , 35: afterNth^#(X1, X2) -> c_60(X1, X2)
976.48/297.23	       , 36: cons^#(X1, X2) -> c_54(X1, X2)
976.48/297.23	       , 37: fst^#(X) -> c_70(X)
976.48/297.23	       , 38: fst^#(pair(X, Y)) ->
976.48/297.23	             c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.23	                            n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.23	                        X))
976.48/297.23	       , 39: snd^#(X) -> c_35(X)
976.48/297.23	       , 40: snd^#(pair(X, Y)) ->
976.48/297.23	             c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.23	                             n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.23	                         Y))
976.48/297.23	       , 41: tail^#(X) -> c_112(X)
976.48/297.23	       , 42: tail^#(cons(N, XS)) ->
976.48/297.23	             c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.23	                          activate(XS)))
976.48/297.23	       , 43: take^#(N, XS) ->
976.48/297.23	             c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.23	                          N,
976.48/297.23	                          XS))
976.48/297.23	       , 44: take^#(X1, X2) -> c_115(X1, X2)
976.48/297.23	       , 45: head^#(X) -> c_57(X)
976.48/297.23	       , 46: head^#(cons(N, XS)) ->
976.48/297.23	             c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                            n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.23	                        N))
976.48/297.23	       , 47: s^#(X) -> c_55(X)
976.48/297.23	       , 48: sel^#(N, XS) ->
976.48/297.23	             c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                              n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.23	                          N,
976.48/297.23	                          XS))
976.48/297.23	       , 49: sel^#(X1, X2) -> c_110(X1, X2)
976.48/297.23	       , 50: pair^#(X1, X2) -> c_63(X1, X2)
976.48/297.23	       , 51: splitAt^#(X1, X2) -> c_37(X1, X2)
976.48/297.23	       , 52: splitAt^#(s(N), cons(X, XS)) ->
976.48/297.23	             c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.23	                             n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.23	                                    n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.23	                         N,
976.48/297.23	                         X,
976.48/297.23	                         activate(XS)))
976.48/297.23	       , 53: splitAt^#(0(), XS) ->
976.48/297.23	             c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.48/297.23	       , 54: isLNat^#(n__afterNth(V1, V2)) ->
976.48/297.23	             c_28(U41^#(and(isNaturalKind(activate(V1)),
976.48/297.23	                            n__isLNatKind(activate(V2))),
976.48/297.23	                        activate(V1),
976.48/297.23	                        activate(V2)))
976.48/297.23	       , 55: isLNat^#(n__cons(V1, V2)) ->
976.48/297.23	             c_29(U51^#(and(isNaturalKind(activate(V1)),
976.48/297.23	                            n__isLNatKind(activate(V2))),
976.48/297.23	                        activate(V1),
976.48/297.23	                        activate(V2)))
976.48/297.23	       , 56: isLNat^#(n__take(V1, V2)) ->
976.48/297.23	             c_33(U101^#(and(isNaturalKind(activate(V1)),
976.48/297.23	                             n__isLNatKind(activate(V2))),
976.48/297.23	                         activate(V1),
976.48/297.23	                         activate(V2)))
976.48/297.23	       , 57: U11^#(tt(), N, XS) ->
976.48/297.23	             c_34(snd^#(splitAt(activate(N), activate(XS))))
976.48/297.23	       , 58: U181^#(tt(), Y) -> c_61(activate^#(Y))
976.48/297.23	       , 59: U201^#(tt(), N, X, XS) ->
976.48/297.23	             c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.48/297.23	       , 60: U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.48/297.23	       , 61: U161^#(tt(), N) ->
976.48/297.23	             c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.48/297.23	       , 62: U171^#(tt(), N, XS) ->
976.48/297.23	             c_56(head^#(afterNth(activate(N), activate(XS))))
976.48/297.23	       , 63: U31^#(tt(), N) -> c_72(activate^#(N))
976.48/297.23	       , 64: U202^#(pair(YS, ZS), X) ->
976.48/297.23	             c_66(pair^#(cons(activate(X), YS), ZS))
976.48/297.23	       , 65: U21^#(tt(), X) -> c_67(activate^#(X))
976.48/297.23	       , 66: U211^#(tt(), XS) -> c_68(activate^#(XS))
976.48/297.23	       , 67: U221^#(tt(), N, XS) ->
976.48/297.23	             c_69(fst^#(splitAt(activate(N), activate(XS))))
976.48/297.23	       , 68: isPLNat^#(n__pair(V1, V2)) ->
976.48/297.23	             c_81(U141^#(and(isLNatKind(activate(V1)),
976.48/297.23	                             n__isLNatKind(activate(V2))),
976.48/297.23	                         activate(V1),
976.48/297.23	                         activate(V2)))
976.48/297.23	       , 69: isPLNat^#(n__splitAt(V1, V2)) ->
976.48/297.23	             c_82(U151^#(and(isNaturalKind(activate(V1)),
976.48/297.23	                             n__isLNatKind(activate(V2))),
976.48/297.23	                         activate(V1),
976.48/297.23	                         activate(V2)))
976.48/297.23	       , 70: isPLNatKind^#(n__pair(V1, V2)) ->
976.48/297.23	             c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.48/297.23	       , 71: isPLNatKind^#(n__splitAt(V1, V2)) ->
976.48/297.23	             c_97(and^#(isNaturalKind(activate(V1)),
976.48/297.23	                        n__isLNatKind(activate(V2))))
976.48/297.23	       , 72: U101^#(tt(), V1, V2) ->
976.48/297.23	             c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	       , 73: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.48/297.23	       , 74: U103^#(tt()) -> c_25()
976.48/297.23	       , 75: isNatural^#(n__0()) -> c_3()
976.48/297.23	       , 76: isNatural^#(n__head(V1)) ->
976.48/297.23	             c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.23	       , 77: isNatural^#(n__s(V1)) ->
976.48/297.23	             c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.23	       , 78: U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.48/297.23	       , 79: U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.48/297.23	       , 80: U131^#(tt(), V1, V2) ->
976.48/297.23	             c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	       , 81: activate^#(n__nil()) -> c_12(nil^#())
976.48/297.23	       , 82: activate^#(n__0()) -> c_19(0^#())
976.48/297.23	       , 83: isNaturalKind^#(n__0()) -> c_92()
976.48/297.23	       , 84: isLNatKind^#(n__nil()) -> c_100()
976.48/297.23	       , 85: nil^#() -> c_64()
976.48/297.23	       , 86: 0^#() -> c_111()
976.48/297.23	       , 87: isLNat^#(n__natsFrom(V1)) ->
976.48/297.23	             c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.23	       , 88: isLNat^#(n__nil()) -> c_27()
976.48/297.23	       , 89: isLNat^#(n__fst(V1)) ->
976.48/297.23	             c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.23	       , 90: isLNat^#(n__snd(V1)) ->
976.48/297.23	             c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.23	       , 91: isLNat^#(n__tail(V1)) ->
976.48/297.23	             c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.23	       , 92: U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.48/297.23	       , 93: U41^#(tt(), V1, V2) ->
976.48/297.23	             c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	       , 94: U51^#(tt(), V1, V2) ->
976.48/297.23	             c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	       , 95: U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.48/297.23	       , 96: U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.48/297.23	       , 97: U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.48/297.23	       , 98: U112^#(tt()) -> c_41()
976.48/297.23	       , 99: U122^#(tt()) -> c_43()
976.48/297.23	       , 100: U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.48/297.23	       , 101: U133^#(tt()) -> c_46()
976.48/297.23	       , 102: U141^#(tt(), V1, V2) ->
976.48/297.23	              c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.48/297.23	       , 103: U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.48/297.23	       , 104: U143^#(tt()) -> c_49()
976.48/297.23	       , 105: U151^#(tt(), V1, V2) ->
976.48/297.23	              c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.48/297.23	       , 106: U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.48/297.23	       , 107: U153^#(tt()) -> c_52()
976.48/297.23	       , 108: U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.48/297.23	       , 109: U43^#(tt()) -> c_75()
976.48/297.23	       , 110: U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.48/297.23	       , 111: U53^#(tt()) -> c_78()
976.48/297.23	       , 112: U62^#(tt()) -> c_80()
976.48/297.23	       , 113: U72^#(tt()) -> c_84()
976.48/297.23	       , 114: U82^#(tt()) -> c_86()
976.48/297.23	       , 115: U92^#(tt()) -> c_88() }
976.48/297.23	   
976.48/297.23	   We are left with following problem, upon which TcT provides the
976.48/297.23	   certificate MAYBE.
976.48/297.23	   
976.48/297.23	   Strict DPs:
976.48/297.23	     { activate^#(X) -> c_7(X)
976.48/297.23	     , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(X))
976.48/297.23	     , activate^#(n__isNaturalKind(X)) -> c_9(isNaturalKind^#(X))
976.48/297.23	     , activate^#(n__and(X1, X2)) -> c_10(and^#(X1, X2))
976.48/297.23	     , activate^#(n__isLNatKind(X)) -> c_11(isLNatKind^#(X))
976.48/297.23	     , activate^#(n__afterNth(X1, X2)) -> c_13(afterNth^#(X1, X2))
976.48/297.23	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(X1, X2))
976.48/297.23	     , activate^#(n__fst(X)) -> c_15(fst^#(X))
976.48/297.23	     , activate^#(n__snd(X)) -> c_16(snd^#(X))
976.48/297.23	     , activate^#(n__tail(X)) -> c_17(tail^#(X))
976.48/297.23	     , activate^#(n__take(X1, X2)) -> c_18(take^#(X1, X2))
976.48/297.23	     , activate^#(n__head(X)) -> c_20(head^#(X))
976.48/297.23	     , activate^#(n__s(X)) -> c_21(s^#(X))
976.48/297.23	     , activate^#(n__sel(X1, X2)) -> c_22(sel^#(X1, X2))
976.48/297.23	     , activate^#(n__pair(X1, X2)) -> c_23(pair^#(X1, X2))
976.48/297.23	     , activate^#(n__splitAt(X1, X2)) -> c_24(splitAt^#(X1, X2))
976.48/297.23	     , natsFrom^#(N) ->
976.48/297.23	       c_107(U161^#(and(isNatural(N), n__isNaturalKind(N)), N))
976.48/297.23	     , natsFrom^#(X) -> c_108(X)
976.48/297.23	     , isNaturalKind^#(X) -> c_91(X)
976.48/297.23	     , isNaturalKind^#(n__head(V1)) -> c_93(isLNatKind^#(activate(V1)))
976.48/297.23	     , isNaturalKind^#(n__s(V1)) -> c_94(isNaturalKind^#(activate(V1)))
976.48/297.23	     , isNaturalKind^#(n__sel(V1, V2)) ->
976.48/297.23	       c_95(and^#(isNaturalKind(activate(V1)),
976.48/297.23	                  n__isLNatKind(activate(V2))))
976.48/297.23	     , and^#(X1, X2) -> c_89(X1, X2)
976.48/297.23	     , and^#(tt(), X) -> c_90(activate^#(X))
976.48/297.23	     , isLNatKind^#(X) -> c_98(X)
976.48/297.23	     , isLNatKind^#(n__natsFrom(V1)) ->
976.48/297.23	       c_99(isNaturalKind^#(activate(V1)))
976.48/297.24	     , isLNatKind^#(n__afterNth(V1, V2)) ->
976.48/297.24	       c_101(and^#(isNaturalKind(activate(V1)),
976.48/297.24	                   n__isLNatKind(activate(V2))))
976.48/297.24	     , isLNatKind^#(n__cons(V1, V2)) ->
976.48/297.24	       c_102(and^#(isNaturalKind(activate(V1)),
976.48/297.24	                   n__isLNatKind(activate(V2))))
976.48/297.24	     , isLNatKind^#(n__fst(V1)) -> c_103(isPLNatKind^#(activate(V1)))
976.48/297.24	     , isLNatKind^#(n__snd(V1)) -> c_104(isPLNatKind^#(activate(V1)))
976.48/297.24	     , isLNatKind^#(n__tail(V1)) -> c_105(isLNatKind^#(activate(V1)))
976.48/297.24	     , isLNatKind^#(n__take(V1, V2)) ->
976.48/297.24	       c_106(and^#(isNaturalKind(activate(V1)),
976.48/297.24	                   n__isLNatKind(activate(V2))))
976.48/297.24	     , afterNth^#(N, XS) ->
976.48/297.24	       c_59(U11^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                      n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.24	                  N,
976.48/297.24	                  XS))
976.48/297.24	     , afterNth^#(X1, X2) -> c_60(X1, X2)
976.48/297.24	     , cons^#(X1, X2) -> c_54(X1, X2)
976.48/297.24	     , fst^#(X) -> c_70(X)
976.48/297.24	     , fst^#(pair(X, Y)) ->
976.48/297.24	       c_71(U21^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.24	                      n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.24	                  X))
976.48/297.24	     , snd^#(X) -> c_35(X)
976.48/297.24	     , snd^#(pair(X, Y)) ->
976.48/297.24	       c_36(U181^#(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.24	                       n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.24	                   Y))
976.48/297.24	     , tail^#(X) -> c_112(X)
976.48/297.24	     , tail^#(cons(N, XS)) ->
976.48/297.24	       c_113(U211^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                        n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.24	                    activate(XS)))
976.48/297.24	     , take^#(N, XS) ->
976.48/297.24	       c_114(U221^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.24	                    N,
976.48/297.24	                    XS))
976.48/297.24	     , take^#(X1, X2) -> c_115(X1, X2)
976.48/297.24	     , head^#(X) -> c_57(X)
976.48/297.24	     , head^#(cons(N, XS)) ->
976.48/297.24	       c_58(U31^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                      n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.24	                  N))
976.48/297.24	     , s^#(X) -> c_55(X)
976.48/297.24	     , sel^#(N, XS) ->
976.48/297.24	       c_109(U171^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                        n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.24	                    N,
976.48/297.24	                    XS))
976.48/297.24	     , sel^#(X1, X2) -> c_110(X1, X2)
976.48/297.24	     , pair^#(X1, X2) -> c_63(X1, X2)
976.48/297.24	     , splitAt^#(X1, X2) -> c_37(X1, X2)
976.48/297.24	     , splitAt^#(s(N), cons(X, XS)) ->
976.48/297.24	       c_38(U201^#(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                       n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.24	                              n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.24	                   N,
976.48/297.24	                   X,
976.48/297.24	                   activate(XS)))
976.48/297.24	     , splitAt^#(0(), XS) ->
976.48/297.24	       c_39(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS))
976.48/297.24	     , U11^#(tt(), N, XS) ->
976.48/297.24	       c_34(snd^#(splitAt(activate(N), activate(XS))))
976.48/297.24	     , U181^#(tt(), Y) -> c_61(activate^#(Y))
976.48/297.24	     , U201^#(tt(), N, X, XS) ->
976.48/297.24	       c_65(U202^#(splitAt(activate(N), activate(XS)), activate(X)))
976.48/297.24	     , U191^#(tt(), XS) -> c_62(pair^#(nil(), activate(XS)))
976.48/297.24	     , U161^#(tt(), N) ->
976.48/297.24	       c_53(cons^#(activate(N), n__natsFrom(s(activate(N)))))
976.48/297.24	     , U171^#(tt(), N, XS) ->
976.48/297.24	       c_56(head^#(afterNth(activate(N), activate(XS))))
976.48/297.24	     , U31^#(tt(), N) -> c_72(activate^#(N))
976.48/297.24	     , U202^#(pair(YS, ZS), X) ->
976.48/297.24	       c_66(pair^#(cons(activate(X), YS), ZS))
976.48/297.24	     , U21^#(tt(), X) -> c_67(activate^#(X))
976.48/297.24	     , U211^#(tt(), XS) -> c_68(activate^#(XS))
976.48/297.24	     , U221^#(tt(), N, XS) ->
976.48/297.24	       c_69(fst^#(splitAt(activate(N), activate(XS))))
976.48/297.24	     , isPLNatKind^#(n__pair(V1, V2)) ->
976.48/297.24	       c_96(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))))
976.48/297.24	     , isPLNatKind^#(n__splitAt(V1, V2)) ->
976.48/297.24	       c_97(and^#(isNaturalKind(activate(V1)),
976.48/297.24	                  n__isLNatKind(activate(V2)))) }
976.48/297.24	   Strict Trs:
976.48/297.24	     { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2))
976.48/297.24	     , U102(tt(), V2) -> U103(isLNat(activate(V2)))
976.48/297.24	     , isNatural(n__0()) -> tt()
976.48/297.24	     , isNatural(n__head(V1)) ->
976.48/297.24	       U111(isLNatKind(activate(V1)), activate(V1))
976.48/297.24	     , isNatural(n__s(V1)) ->
976.48/297.24	       U121(isNaturalKind(activate(V1)), activate(V1))
976.48/297.24	     , isNatural(n__sel(V1, V2)) ->
976.48/297.24	       U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.24	            activate(V1),
976.48/297.24	            activate(V2))
976.48/297.24	     , activate(X) -> X
976.48/297.24	     , activate(n__natsFrom(X)) -> natsFrom(X)
976.48/297.24	     , activate(n__isNaturalKind(X)) -> isNaturalKind(X)
976.48/297.24	     , activate(n__and(X1, X2)) -> and(X1, X2)
976.48/297.24	     , activate(n__isLNatKind(X)) -> isLNatKind(X)
976.48/297.24	     , activate(n__nil()) -> nil()
976.48/297.24	     , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
976.48/297.24	     , activate(n__cons(X1, X2)) -> cons(X1, X2)
976.48/297.24	     , activate(n__fst(X)) -> fst(X)
976.48/297.24	     , activate(n__snd(X)) -> snd(X)
976.48/297.24	     , activate(n__tail(X)) -> tail(X)
976.48/297.24	     , activate(n__take(X1, X2)) -> take(X1, X2)
976.48/297.24	     , activate(n__0()) -> 0()
976.48/297.24	     , activate(n__head(X)) -> head(X)
976.48/297.24	     , activate(n__s(X)) -> s(X)
976.48/297.24	     , activate(n__sel(X1, X2)) -> sel(X1, X2)
976.48/297.24	     , activate(n__pair(X1, X2)) -> pair(X1, X2)
976.48/297.24	     , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
976.48/297.24	     , U103(tt()) -> tt()
976.48/297.24	     , isLNat(n__natsFrom(V1)) ->
976.48/297.24	       U71(isNaturalKind(activate(V1)), activate(V1))
976.48/297.24	     , isLNat(n__nil()) -> tt()
976.48/297.24	     , isLNat(n__afterNth(V1, V2)) ->
976.48/297.24	       U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.24	           activate(V1),
976.48/297.24	           activate(V2))
976.48/297.24	     , isLNat(n__cons(V1, V2)) ->
976.48/297.24	       U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.24	           activate(V1),
976.48/297.24	           activate(V2))
976.48/297.24	     , isLNat(n__fst(V1)) ->
976.48/297.24	       U61(isPLNatKind(activate(V1)), activate(V1))
976.48/297.24	     , isLNat(n__snd(V1)) ->
976.48/297.24	       U81(isPLNatKind(activate(V1)), activate(V1))
976.48/297.24	     , isLNat(n__tail(V1)) ->
976.48/297.24	       U91(isLNatKind(activate(V1)), activate(V1))
976.48/297.24	     , isLNat(n__take(V1, V2)) ->
976.48/297.24	       U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.24	            activate(V1),
976.48/297.24	            activate(V2))
976.48/297.24	     , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
976.48/297.24	     , snd(X) -> n__snd(X)
976.48/297.24	     , snd(pair(X, Y)) ->
976.48/297.24	       U181(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.24	                n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.24	            Y)
976.48/297.24	     , splitAt(X1, X2) -> n__splitAt(X1, X2)
976.48/297.24	     , splitAt(s(N), cons(X, XS)) ->
976.48/297.24	       U201(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                n__and(and(isNatural(X), n__isNaturalKind(X)),
976.48/297.24	                       n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))),
976.48/297.24	            N,
976.48/297.24	            X,
976.48/297.24	            activate(XS))
976.48/297.24	     , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
976.48/297.24	     , U111(tt(), V1) -> U112(isLNat(activate(V1)))
976.48/297.24	     , U112(tt()) -> tt()
976.48/297.24	     , U121(tt(), V1) -> U122(isNatural(activate(V1)))
976.48/297.24	     , U122(tt()) -> tt()
976.48/297.24	     , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2))
976.48/297.24	     , U132(tt(), V2) -> U133(isLNat(activate(V2)))
976.48/297.24	     , U133(tt()) -> tt()
976.48/297.24	     , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2))
976.48/297.24	     , U142(tt(), V2) -> U143(isLNat(activate(V2)))
976.48/297.24	     , U143(tt()) -> tt()
976.48/297.24	     , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2))
976.48/297.24	     , U152(tt(), V2) -> U153(isLNat(activate(V2)))
976.48/297.24	     , U153(tt()) -> tt()
976.48/297.24	     , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N))))
976.48/297.24	     , cons(X1, X2) -> n__cons(X1, X2)
976.48/297.24	     , s(X) -> n__s(X)
976.48/297.24	     , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
976.48/297.24	     , head(X) -> n__head(X)
976.48/297.24	     , head(cons(N, XS)) ->
976.48/297.24	       U31(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	               n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.24	           N)
976.48/297.24	     , afterNth(N, XS) ->
976.48/297.24	       U11(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	               n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.24	           N,
976.48/297.24	           XS)
976.48/297.24	     , afterNth(X1, X2) -> n__afterNth(X1, X2)
976.48/297.24	     , U181(tt(), Y) -> activate(Y)
976.48/297.24	     , U191(tt(), XS) -> pair(nil(), activate(XS))
976.48/297.24	     , pair(X1, X2) -> n__pair(X1, X2)
976.48/297.24	     , nil() -> n__nil()
976.48/297.24	     , U201(tt(), N, X, XS) ->
976.48/297.24	       U202(splitAt(activate(N), activate(XS)), activate(X))
976.48/297.24	     , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
976.48/297.24	     , U21(tt(), X) -> activate(X)
976.48/297.24	     , U211(tt(), XS) -> activate(XS)
976.48/297.24	     , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
976.48/297.24	     , fst(X) -> n__fst(X)
976.48/297.24	     , fst(pair(X, Y)) ->
976.48/297.24	       U21(and(and(isLNat(X), n__isLNatKind(X)),
976.48/297.24	               n__and(isLNat(Y), n__isLNatKind(Y))),
976.48/297.24	           X)
976.48/297.24	     , U31(tt(), N) -> activate(N)
976.48/297.24	     , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2))
976.48/297.24	     , U42(tt(), V2) -> U43(isLNat(activate(V2)))
976.48/297.24	     , U43(tt()) -> tt()
976.48/297.24	     , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2))
976.48/297.24	     , U52(tt(), V2) -> U53(isLNat(activate(V2)))
976.48/297.24	     , U53(tt()) -> tt()
976.48/297.24	     , U61(tt(), V1) -> U62(isPLNat(activate(V1)))
976.48/297.24	     , U62(tt()) -> tt()
976.48/297.24	     , isPLNat(n__pair(V1, V2)) ->
976.48/297.24	       U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.24	            activate(V1),
976.48/297.24	            activate(V2))
976.48/297.24	     , isPLNat(n__splitAt(V1, V2)) ->
976.48/297.24	       U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),
976.48/297.24	            activate(V1),
976.48/297.24	            activate(V2))
976.48/297.24	     , U71(tt(), V1) -> U72(isNatural(activate(V1)))
976.48/297.24	     , U72(tt()) -> tt()
976.48/297.24	     , U81(tt(), V1) -> U82(isPLNat(activate(V1)))
976.48/297.24	     , U82(tt()) -> tt()
976.48/297.24	     , U91(tt(), V1) -> U92(isLNat(activate(V1)))
976.48/297.24	     , U92(tt()) -> tt()
976.48/297.24	     , and(X1, X2) -> n__and(X1, X2)
976.48/297.24	     , and(tt(), X) -> activate(X)
976.48/297.24	     , isNaturalKind(X) -> n__isNaturalKind(X)
976.48/297.24	     , isNaturalKind(n__0()) -> tt()
976.48/297.24	     , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
976.48/297.24	     , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
976.48/297.24	     , isNaturalKind(n__sel(V1, V2)) ->
976.48/297.24	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.24	     , isPLNatKind(n__pair(V1, V2)) ->
976.48/297.24	       and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.24	     , isPLNatKind(n__splitAt(V1, V2)) ->
976.48/297.24	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.24	     , isLNatKind(X) -> n__isLNatKind(X)
976.48/297.24	     , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
976.48/297.24	     , isLNatKind(n__nil()) -> tt()
976.48/297.24	     , isLNatKind(n__afterNth(V1, V2)) ->
976.48/297.24	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.24	     , isLNatKind(n__cons(V1, V2)) ->
976.48/297.24	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.24	     , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
976.48/297.24	     , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
976.48/297.24	     , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
976.48/297.24	     , isLNatKind(n__take(V1, V2)) ->
976.48/297.24	       and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
976.48/297.24	     , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N)
976.48/297.24	     , natsFrom(X) -> n__natsFrom(X)
976.48/297.24	     , sel(N, XS) ->
976.48/297.24	       U171(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.24	            N,
976.48/297.24	            XS)
976.48/297.24	     , sel(X1, X2) -> n__sel(X1, X2)
976.48/297.24	     , 0() -> n__0()
976.48/297.24	     , tail(X) -> n__tail(X)
976.48/297.24	     , tail(cons(N, XS)) ->
976.48/297.24	       U211(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),
976.48/297.24	            activate(XS))
976.48/297.24	     , take(N, XS) ->
976.48/297.24	       U221(and(and(isNatural(N), n__isNaturalKind(N)),
976.48/297.24	                n__and(isLNat(XS), n__isLNatKind(XS))),
976.48/297.24	            N,
976.48/297.24	            XS)
976.48/297.24	     , take(X1, X2) -> n__take(X1, X2) }
976.48/297.24	   Weak DPs:
976.48/297.24	     { U101^#(tt(), V1, V2) ->
976.48/297.24	       c_1(U102^#(isNatural(activate(V1)), activate(V2)))
976.48/297.24	     , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2))))
976.48/297.24	     , U103^#(tt()) -> c_25()
976.48/297.24	     , isNatural^#(n__0()) -> c_3()
976.48/297.24	     , isNatural^#(n__head(V1)) ->
976.48/297.24	       c_4(U111^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.24	     , isNatural^#(n__s(V1)) ->
976.48/297.24	       c_5(U121^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.24	     , isNatural^#(n__sel(V1, V2)) ->
976.48/297.24	       c_6(U131^#(and(isNaturalKind(activate(V1)),
976.48/297.24	                      n__isLNatKind(activate(V2))),
976.48/297.24	                  activate(V1),
976.48/297.24	                  activate(V2)))
976.48/297.24	     , U111^#(tt(), V1) -> c_40(U112^#(isLNat(activate(V1))))
976.48/297.24	     , U121^#(tt(), V1) -> c_42(U122^#(isNatural(activate(V1))))
976.48/297.24	     , U131^#(tt(), V1, V2) ->
976.48/297.24	       c_44(U132^#(isNatural(activate(V1)), activate(V2)))
976.48/297.24	     , activate^#(n__nil()) -> c_12(nil^#())
976.48/297.24	     , activate^#(n__0()) -> c_19(0^#())
976.48/297.24	     , isNaturalKind^#(n__0()) -> c_92()
976.48/297.24	     , isLNatKind^#(n__nil()) -> c_100()
976.48/297.24	     , nil^#() -> c_64()
976.48/297.24	     , 0^#() -> c_111()
976.48/297.24	     , isLNat^#(n__natsFrom(V1)) ->
976.48/297.24	       c_26(U71^#(isNaturalKind(activate(V1)), activate(V1)))
976.48/297.24	     , isLNat^#(n__nil()) -> c_27()
976.48/297.24	     , isLNat^#(n__afterNth(V1, V2)) ->
976.48/297.24	       c_28(U41^#(and(isNaturalKind(activate(V1)),
976.48/297.24	                      n__isLNatKind(activate(V2))),
976.48/297.24	                  activate(V1),
976.48/297.24	                  activate(V2)))
976.48/297.24	     , isLNat^#(n__cons(V1, V2)) ->
976.48/297.24	       c_29(U51^#(and(isNaturalKind(activate(V1)),
976.48/297.24	                      n__isLNatKind(activate(V2))),
976.48/297.24	                  activate(V1),
976.48/297.24	                  activate(V2)))
976.48/297.24	     , isLNat^#(n__fst(V1)) ->
976.48/297.24	       c_30(U61^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.24	     , isLNat^#(n__snd(V1)) ->
976.48/297.24	       c_31(U81^#(isPLNatKind(activate(V1)), activate(V1)))
976.48/297.24	     , isLNat^#(n__tail(V1)) ->
976.48/297.24	       c_32(U91^#(isLNatKind(activate(V1)), activate(V1)))
976.48/297.24	     , isLNat^#(n__take(V1, V2)) ->
976.48/297.24	       c_33(U101^#(and(isNaturalKind(activate(V1)),
976.48/297.24	                       n__isLNatKind(activate(V2))),
976.48/297.24	                   activate(V1),
976.48/297.24	                   activate(V2)))
976.48/297.24	     , U71^#(tt(), V1) -> c_83(U72^#(isNatural(activate(V1))))
976.48/297.24	     , U41^#(tt(), V1, V2) ->
976.48/297.24	       c_73(U42^#(isNatural(activate(V1)), activate(V2)))
976.48/297.24	     , U51^#(tt(), V1, V2) ->
976.48/297.24	       c_76(U52^#(isNatural(activate(V1)), activate(V2)))
976.48/297.24	     , U61^#(tt(), V1) -> c_79(U62^#(isPLNat(activate(V1))))
976.48/297.24	     , U81^#(tt(), V1) -> c_85(U82^#(isPLNat(activate(V1))))
976.48/297.24	     , U91^#(tt(), V1) -> c_87(U92^#(isLNat(activate(V1))))
976.48/297.24	     , U112^#(tt()) -> c_41()
976.48/297.24	     , U122^#(tt()) -> c_43()
976.48/297.24	     , U132^#(tt(), V2) -> c_45(U133^#(isLNat(activate(V2))))
976.48/297.24	     , U133^#(tt()) -> c_46()
976.48/297.24	     , U141^#(tt(), V1, V2) ->
976.48/297.24	       c_47(U142^#(isLNat(activate(V1)), activate(V2)))
976.48/297.24	     , U142^#(tt(), V2) -> c_48(U143^#(isLNat(activate(V2))))
976.48/297.24	     , U143^#(tt()) -> c_49()
976.48/297.24	     , U151^#(tt(), V1, V2) ->
976.48/297.24	       c_50(U152^#(isNatural(activate(V1)), activate(V2)))
976.48/297.24	     , U152^#(tt(), V2) -> c_51(U153^#(isLNat(activate(V2))))
976.48/297.24	     , U153^#(tt()) -> c_52()
976.48/297.24	     , U42^#(tt(), V2) -> c_74(U43^#(isLNat(activate(V2))))
976.48/297.24	     , U43^#(tt()) -> c_75()
976.48/297.24	     , U52^#(tt(), V2) -> c_77(U53^#(isLNat(activate(V2))))
976.48/297.24	     , U53^#(tt()) -> c_78()
976.48/297.24	     , U62^#(tt()) -> c_80()
976.48/297.24	     , isPLNat^#(n__pair(V1, V2)) ->
976.48/297.24	       c_81(U141^#(and(isLNatKind(activate(V1)),
976.48/297.24	                       n__isLNatKind(activate(V2))),
976.48/297.24	                   activate(V1),
976.48/297.24	                   activate(V2)))
976.48/297.24	     , isPLNat^#(n__splitAt(V1, V2)) ->
976.48/297.24	       c_82(U151^#(and(isNaturalKind(activate(V1)),
976.48/297.24	                       n__isLNatKind(activate(V2))),
976.48/297.24	                   activate(V1),
976.48/297.24	                   activate(V2)))
976.48/297.24	     , U72^#(tt()) -> c_84()
976.48/297.24	     , U82^#(tt()) -> c_86()
976.48/297.24	     , U92^#(tt()) -> c_88() }
976.48/297.24	   Obligation:
976.48/297.24	     runtime complexity
976.48/297.24	   Answer:
976.48/297.24	     MAYBE
976.48/297.24	   
976.48/297.24	   Empty strict component of the problem is NOT empty.
976.48/297.24	
976.48/297.24	
976.48/297.24	Arrrr..
976.48/297.24	EOF