MAYBE
MAYBE
TRS:
 {
                    U102(mark(X1), X2) -> mark(U102(X1, X2)),
                  U102(ok(X1), ok(X2)) -> ok(U102(X1, X2)),
                      isNatural(ok(X)) -> ok(isNatural(X)),
                  active(U102(X1, X2)) -> U102(active(X1), X2),
                active(U102(tt(), V2)) -> mark(U103(isLNat(V2))),
              active(isNatural(s(V1))) -> mark(U121(isNaturalKind(V1), V1)),
           active(isNatural(head(V1))) -> mark(U111(isLNatKind(V1), V1)),
                active(isNatural(0())) -> mark(tt()),
        active(isNatural(sel(V1, V2))) ->
  mark(U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
              active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3),
            active(U101(tt(), V1, V2)) -> mark(U102(isNatural(V1), V2)),
                       active(U103(X)) -> U103(active(X)),
                    active(U103(tt())) -> mark(tt()),
               active(isLNat(snd(V1))) -> mark(U81(isPLNatKind(V1), V1)),
          active(isLNat(cons(V1, V2))) ->
  mark(U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
          active(isLNat(natsFrom(V1))) -> mark(U71(isNaturalKind(V1), V1)),
      active(isLNat(afterNth(V1, V2))) ->
  mark(U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
                 active(isLNat(nil())) -> mark(tt()),
               active(isLNat(fst(V1))) -> mark(U61(isPLNatKind(V1), V1)),
              active(isLNat(tail(V1))) -> mark(U91(isLNatKind(V1), V1)),
          active(isLNat(take(V1, V2))) ->
  mark(U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
                        active(snd(X)) -> snd(active(X)),
               active(snd(pair(X, Y))) ->
  mark(
      U181(
          and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))),
          Y
      )
  ),
               active(splitAt(X1, X2)) -> splitAt(X1, active(X2)),
               active(splitAt(X1, X2)) -> splitAt(active(X1), X2),
    active(splitAt(s(N), cons(X, XS))) ->
  mark(
      U201(
          and(
             and(isNatural(N), isNaturalKind(N)),
             and(
                and(isNatural(X), isNaturalKind(X)),
                and(isLNat(XS), isLNatKind(XS))
             )
          ), N, X, XS
      )
  ),
              active(splitAt(0(), XS)) ->
  mark(U191(and(isLNat(XS), isLNatKind(XS)), XS)),
               active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3),
              active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))),
                       active(U112(X)) -> U112(active(X)),
                    active(U112(tt())) -> mark(tt()),
                  active(U111(X1, X2)) -> U111(active(X1), X2),
                active(U111(tt(), V1)) -> mark(U112(isLNat(V1))),
                       active(U122(X)) -> U122(active(X)),
                    active(U122(tt())) -> mark(tt()),
                  active(U121(X1, X2)) -> U121(active(X1), X2),
                active(U121(tt(), V1)) -> mark(U122(isNatural(V1))),
                  active(U132(X1, X2)) -> U132(active(X1), X2),
                active(U132(tt(), V2)) -> mark(U133(isLNat(V2))),
              active(U131(X1, X2, X3)) -> U131(active(X1), X2, X3),
            active(U131(tt(), V1, V2)) -> mark(U132(isNatural(V1), V2)),
                       active(U133(X)) -> U133(active(X)),
                    active(U133(tt())) -> mark(tt()),
                  active(U142(X1, X2)) -> U142(active(X1), X2),
                active(U142(tt(), V2)) -> mark(U143(isLNat(V2))),
              active(U141(X1, X2, X3)) -> U141(active(X1), X2, X3),
            active(U141(tt(), V1, V2)) -> mark(U142(isLNat(V1), V2)),
                       active(U143(X)) -> U143(active(X)),
                    active(U143(tt())) -> mark(tt()),
                  active(U152(X1, X2)) -> U152(active(X1), X2),
                active(U152(tt(), V2)) -> mark(U153(isLNat(V2))),
              active(U151(X1, X2, X3)) -> U151(active(X1), X2, X3),
            active(U151(tt(), V1, V2)) -> mark(U152(isNatural(V1), V2)),
                       active(U153(X)) -> U153(active(X)),
                    active(U153(tt())) -> mark(tt()),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                   active(natsFrom(N)) ->
  mark(U161(and(isNatural(N), isNaturalKind(N)), N)),
                   active(natsFrom(X)) -> natsFrom(active(X)),
                          active(s(X)) -> s(active(X)),
                  active(U161(X1, X2)) -> U161(active(X1), X2),
                 active(U161(tt(), N)) -> mark(cons(N, natsFrom(s(N)))),
                       active(head(X)) -> head(active(X)),
             active(head(cons(N, XS))) ->
  mark(
      U31(
         and(
            and(isNatural(N), isNaturalKind(N)),
            and(isLNat(XS), isLNatKind(XS))
         ), N
      )
  ),
               active(afterNth(N, XS)) ->
  mark(
      U11(
         and(
            and(isNatural(N), isNaturalKind(N)),
            and(isLNat(XS), isLNatKind(XS))
         ), N, XS
      )
  ),
              active(afterNth(X1, X2)) -> afterNth(X1, active(X2)),
              active(afterNth(X1, X2)) -> afterNth(active(X1), X2),
              active(U171(X1, X2, X3)) -> U171(active(X1), X2, X3),
             active(U171(tt(), N, XS)) -> mark(head(afterNth(N, XS))),
                  active(U181(X1, X2)) -> U181(active(X1), X2),
                 active(U181(tt(), Y)) -> mark(Y),
                  active(pair(X1, X2)) -> pair(X1, active(X2)),
                  active(pair(X1, X2)) -> pair(active(X1), X2),
                  active(U191(X1, X2)) -> U191(active(X1), X2),
                active(U191(tt(), XS)) -> mark(pair(nil(), XS)),
                  active(U202(X1, X2)) -> U202(active(X1), X2),
         active(U202(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
          active(U201(X1, X2, X3, X4)) -> U201(active(X1), X2, X3, X4),
          active(U201(tt(), N, X, XS)) -> mark(U202(splitAt(N, XS), X)),
                   active(U21(X1, X2)) -> U21(active(X1), X2),
                  active(U21(tt(), X)) -> mark(X),
                  active(U211(X1, X2)) -> U211(active(X1), X2),
                active(U211(tt(), XS)) -> mark(XS),
                        active(fst(X)) -> fst(active(X)),
               active(fst(pair(X, Y))) ->
  mark(
      U21(
         and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X
      )
  ),
              active(U221(X1, X2, X3)) -> U221(active(X1), X2, X3),
             active(U221(tt(), N, XS)) -> mark(fst(splitAt(N, XS))),
                   active(U31(X1, X2)) -> U31(active(X1), X2),
                  active(U31(tt(), N)) -> mark(N),
                   active(U42(X1, X2)) -> U42(active(X1), X2),
                 active(U42(tt(), V2)) -> mark(U43(isLNat(V2))),
               active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3),
             active(U41(tt(), V1, V2)) -> mark(U42(isNatural(V1), V2)),
                        active(U43(X)) -> U43(active(X)),
                     active(U43(tt())) -> mark(tt()),
                   active(U52(X1, X2)) -> U52(active(X1), X2),
                 active(U52(tt(), V2)) -> mark(U53(isLNat(V2))),
               active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3),
             active(U51(tt(), V1, V2)) -> mark(U52(isNatural(V1), V2)),
                        active(U53(X)) -> U53(active(X)),
                     active(U53(tt())) -> mark(tt()),
                        active(U62(X)) -> U62(active(X)),
                     active(U62(tt())) -> mark(tt()),
      active(isPLNat(splitAt(V1, V2))) ->
  mark(U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
         active(isPLNat(pair(V1, V2))) ->
  mark(U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2)),
                   active(U61(X1, X2)) -> U61(active(X1), X2),
                 active(U61(tt(), V1)) -> mark(U62(isPLNat(V1))),
                        active(U72(X)) -> U72(active(X)),
                     active(U72(tt())) -> mark(tt()),
                   active(U71(X1, X2)) -> U71(active(X1), X2),
                 active(U71(tt(), V1)) -> mark(U72(isNatural(V1))),
                        active(U82(X)) -> U82(active(X)),
                     active(U82(tt())) -> mark(tt()),
                   active(U81(X1, X2)) -> U81(active(X1), X2),
                 active(U81(tt(), V1)) -> mark(U82(isPLNat(V1))),
                        active(U92(X)) -> U92(active(X)),
                     active(U92(tt())) -> mark(tt()),
                   active(U91(X1, X2)) -> U91(active(X1), X2),
                 active(U91(tt(), V1)) -> mark(U92(isLNat(V1))),
                   active(and(X1, X2)) -> and(active(X1), X2),
                  active(and(tt(), X)) -> mark(X),
          active(isNaturalKind(s(V1))) -> mark(isNaturalKind(V1)),
       active(isNaturalKind(head(V1))) -> mark(isLNatKind(V1)),
            active(isNaturalKind(0())) -> mark(tt()),
    active(isNaturalKind(sel(V1, V2))) ->
  mark(and(isNaturalKind(V1), isLNatKind(V2))),
           active(isLNatKind(snd(V1))) -> mark(isPLNatKind(V1)),
      active(isLNatKind(cons(V1, V2))) ->
  mark(and(isNaturalKind(V1), isLNatKind(V2))),
      active(isLNatKind(natsFrom(V1))) -> mark(isNaturalKind(V1)),
  active(isLNatKind(afterNth(V1, V2))) ->
  mark(and(isNaturalKind(V1), isLNatKind(V2))),
             active(isLNatKind(nil())) -> mark(tt()),
           active(isLNatKind(fst(V1))) -> mark(isPLNatKind(V1)),
          active(isLNatKind(tail(V1))) -> mark(isLNatKind(V1)),
      active(isLNatKind(take(V1, V2))) ->
  mark(and(isNaturalKind(V1), isLNatKind(V2))),
  active(isPLNatKind(splitAt(V1, V2))) ->
  mark(and(isNaturalKind(V1), isLNatKind(V2))),
     active(isPLNatKind(pair(V1, V2))) ->
  mark(and(isLNatKind(V1), isLNatKind(V2))),
                       active(tail(X)) -> tail(active(X)),
             active(tail(cons(N, XS))) ->
  mark(
      U211(
          and(
             and(isNatural(N), isNaturalKind(N)),
             and(isLNat(XS), isLNatKind(XS))
          ), XS
      )
  ),
                   active(take(N, XS)) ->
  mark(
      U221(
          and(
             and(isNatural(N), isNaturalKind(N)),
             and(isLNat(XS), isLNatKind(XS))
          ), N, XS
      )
  ),
                  active(take(X1, X2)) -> take(X1, active(X2)),
                  active(take(X1, X2)) -> take(active(X1), X2),
                    active(sel(N, XS)) ->
  mark(
      U171(
          and(
             and(isNatural(N), isNaturalKind(N)),
             and(isLNat(XS), isLNatKind(XS))
          ), N, XS
      )
  ),
                   active(sel(X1, X2)) -> sel(X1, active(X2)),
                   active(sel(X1, X2)) -> sel(active(X1), X2),
                U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)),
          U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)),
                         U103(mark(X)) -> mark(U103(X)),
                           U103(ok(X)) -> ok(U103(X)),
                         isLNat(ok(X)) -> ok(isLNat(X)),
                          snd(mark(X)) -> mark(snd(X)),
                            snd(ok(X)) -> ok(snd(X)),
                 splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)),
                 splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)),
               splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)),
                 U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)),
           U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)),
                         U112(mark(X)) -> mark(U112(X)),
                           U112(ok(X)) -> ok(U112(X)),
                    U111(mark(X1), X2) -> mark(U111(X1, X2)),
                  U111(ok(X1), ok(X2)) -> ok(U111(X1, X2)),
                         U122(mark(X)) -> mark(U122(X)),
                           U122(ok(X)) -> ok(U122(X)),
                    U121(mark(X1), X2) -> mark(U121(X1, X2)),
                  U121(ok(X1), ok(X2)) -> ok(U121(X1, X2)),
                    U132(mark(X1), X2) -> mark(U132(X1, X2)),
                  U132(ok(X1), ok(X2)) -> ok(U132(X1, X2)),
                U131(mark(X1), X2, X3) -> mark(U131(X1, X2, X3)),
          U131(ok(X1), ok(X2), ok(X3)) -> ok(U131(X1, X2, X3)),
                         U133(mark(X)) -> mark(U133(X)),
                           U133(ok(X)) -> ok(U133(X)),
                    U142(mark(X1), X2) -> mark(U142(X1, X2)),
                  U142(ok(X1), ok(X2)) -> ok(U142(X1, X2)),
                U141(mark(X1), X2, X3) -> mark(U141(X1, X2, X3)),
          U141(ok(X1), ok(X2), ok(X3)) -> ok(U141(X1, X2, X3)),
                         U143(mark(X)) -> mark(U143(X)),
                           U143(ok(X)) -> ok(U143(X)),
                    U152(mark(X1), X2) -> mark(U152(X1, X2)),
                  U152(ok(X1), ok(X2)) -> ok(U152(X1, X2)),
                U151(mark(X1), X2, X3) -> mark(U151(X1, X2, X3)),
          U151(ok(X1), ok(X2), ok(X3)) -> ok(U151(X1, X2, X3)),
                         U153(mark(X)) -> mark(U153(X)),
                           U153(ok(X)) -> ok(U153(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                     natsFrom(mark(X)) -> mark(natsFrom(X)),
                       natsFrom(ok(X)) -> ok(natsFrom(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                    U161(mark(X1), X2) -> mark(U161(X1, X2)),
                  U161(ok(X1), ok(X2)) -> ok(U161(X1, X2)),
                         head(mark(X)) -> mark(head(X)),
                           head(ok(X)) -> ok(head(X)),
                afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)),
                afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)),
              afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)),
                U171(mark(X1), X2, X3) -> mark(U171(X1, X2, X3)),
          U171(ok(X1), ok(X2), ok(X3)) -> ok(U171(X1, X2, X3)),
                    U181(mark(X1), X2) -> mark(U181(X1, X2)),
                  U181(ok(X1), ok(X2)) -> ok(U181(X1, X2)),
                    pair(X1, mark(X2)) -> mark(pair(X1, X2)),
                    pair(mark(X1), X2) -> mark(pair(X1, X2)),
                  pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)),
                    U191(mark(X1), X2) -> mark(U191(X1, X2)),
                  U191(ok(X1), ok(X2)) -> ok(U191(X1, X2)),
                    U202(mark(X1), X2) -> mark(U202(X1, X2)),
                  U202(ok(X1), ok(X2)) -> ok(U202(X1, X2)),
            U201(mark(X1), X2, X3, X4) -> mark(U201(X1, X2, X3, X4)),
  U201(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U201(X1, X2, X3, X4)),
                     U21(mark(X1), X2) -> mark(U21(X1, X2)),
                   U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)),
                    U211(mark(X1), X2) -> mark(U211(X1, X2)),
                  U211(ok(X1), ok(X2)) -> ok(U211(X1, X2)),
                          fst(mark(X)) -> mark(fst(X)),
                            fst(ok(X)) -> ok(fst(X)),
                U221(mark(X1), X2, X3) -> mark(U221(X1, X2, X3)),
          U221(ok(X1), ok(X2), ok(X3)) -> ok(U221(X1, X2, X3)),
                     U31(mark(X1), X2) -> mark(U31(X1, X2)),
                   U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)),
                     U42(mark(X1), X2) -> mark(U42(X1, X2)),
                   U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)),
                 U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)),
           U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)),
                          U43(mark(X)) -> mark(U43(X)),
                            U43(ok(X)) -> ok(U43(X)),
                     U52(mark(X1), X2) -> mark(U52(X1, X2)),
                   U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)),
                 U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)),
           U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)),
                          U53(mark(X)) -> mark(U53(X)),
                            U53(ok(X)) -> ok(U53(X)),
                          U62(mark(X)) -> mark(U62(X)),
                            U62(ok(X)) -> ok(U62(X)),
                        isPLNat(ok(X)) -> ok(isPLNat(X)),
                     U61(mark(X1), X2) -> mark(U61(X1, X2)),
                   U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)),
                          U72(mark(X)) -> mark(U72(X)),
                            U72(ok(X)) -> ok(U72(X)),
                     U71(mark(X1), X2) -> mark(U71(X1, X2)),
                   U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)),
                          U82(mark(X)) -> mark(U82(X)),
                            U82(ok(X)) -> ok(U82(X)),
                     U81(mark(X1), X2) -> mark(U81(X1, X2)),
                   U81(ok(X1), ok(X2)) -> ok(U81(X1, X2)),
                          U92(mark(X)) -> mark(U92(X)),
                            U92(ok(X)) -> ok(U92(X)),
                     U91(mark(X1), X2) -> mark(U91(X1, X2)),
                   U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)),
                     and(mark(X1), X2) -> mark(and(X1, X2)),
                   and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                  isNaturalKind(ok(X)) -> ok(isNaturalKind(X)),
                     isLNatKind(ok(X)) -> ok(isLNatKind(X)),
                    isPLNatKind(ok(X)) -> ok(isPLNatKind(X)),
                         tail(mark(X)) -> mark(tail(X)),
                           tail(ok(X)) -> ok(tail(X)),
                    take(X1, mark(X2)) -> mark(take(X1, X2)),
                    take(mark(X1), X2) -> mark(take(X1, X2)),
                  take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                     sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                     sel(mark(X1), X2) -> mark(sel(X1, X2)),
                   sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                  proper(U102(X1, X2)) -> U102(proper(X1), proper(X2)),
                  proper(isNatural(X)) -> isNatural(proper(X)),
              proper(U101(X1, X2, X3)) ->
  U101(proper(X1), proper(X2), proper(X3)),
                          proper(tt()) -> ok(tt()),
                       proper(U103(X)) -> U103(proper(X)),
                     proper(isLNat(X)) -> isLNat(proper(X)),
                        proper(snd(X)) -> snd(proper(X)),
               proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)),
               proper(U11(X1, X2, X3)) ->
  U11(proper(X1), proper(X2), proper(X3)),
                       proper(U112(X)) -> U112(proper(X)),
                  proper(U111(X1, X2)) -> U111(proper(X1), proper(X2)),
                       proper(U122(X)) -> U122(proper(X)),
                  proper(U121(X1, X2)) -> U121(proper(X1), proper(X2)),
                  proper(U132(X1, X2)) -> U132(proper(X1), proper(X2)),
              proper(U131(X1, X2, X3)) ->
  U131(proper(X1), proper(X2), proper(X3)),
                       proper(U133(X)) -> U133(proper(X)),
                  proper(U142(X1, X2)) -> U142(proper(X1), proper(X2)),
              proper(U141(X1, X2, X3)) ->
  U141(proper(X1), proper(X2), proper(X3)),
                       proper(U143(X)) -> U143(proper(X)),
                  proper(U152(X1, X2)) -> U152(proper(X1), proper(X2)),
              proper(U151(X1, X2, X3)) ->
  U151(proper(X1), proper(X2), proper(X3)),
                       proper(U153(X)) -> U153(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                   proper(natsFrom(X)) -> natsFrom(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                  proper(U161(X1, X2)) -> U161(proper(X1), proper(X2)),
                       proper(head(X)) -> head(proper(X)),
              proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)),
              proper(U171(X1, X2, X3)) ->
  U171(proper(X1), proper(X2), proper(X3)),
                  proper(U181(X1, X2)) -> U181(proper(X1), proper(X2)),
                  proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)),
                         proper(nil()) -> ok(nil()),
                  proper(U191(X1, X2)) -> U191(proper(X1), proper(X2)),
                  proper(U202(X1, X2)) -> U202(proper(X1), proper(X2)),
          proper(U201(X1, X2, X3, X4)) ->
  U201(proper(X1), proper(X2), proper(X3), proper(X4)),
                   proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)),
                  proper(U211(X1, X2)) -> U211(proper(X1), proper(X2)),
                        proper(fst(X)) -> fst(proper(X)),
              proper(U221(X1, X2, X3)) ->
  U221(proper(X1), proper(X2), proper(X3)),
                   proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)),
                   proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)),
               proper(U41(X1, X2, X3)) ->
  U41(proper(X1), proper(X2), proper(X3)),
                        proper(U43(X)) -> U43(proper(X)),
                   proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)),
               proper(U51(X1, X2, X3)) ->
  U51(proper(X1), proper(X2), proper(X3)),
                        proper(U53(X)) -> U53(proper(X)),
                        proper(U62(X)) -> U62(proper(X)),
                    proper(isPLNat(X)) -> isPLNat(proper(X)),
                   proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)),
                        proper(U72(X)) -> U72(proper(X)),
                   proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)),
                        proper(U82(X)) -> U82(proper(X)),
                   proper(U81(X1, X2)) -> U81(proper(X1), proper(X2)),
                        proper(U92(X)) -> U92(proper(X)),
                   proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)),
                   proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
              proper(isNaturalKind(X)) -> isNaturalKind(proper(X)),
                 proper(isLNatKind(X)) -> isLNatKind(proper(X)),
                proper(isPLNatKind(X)) -> isPLNatKind(proper(X)),
                       proper(tail(X)) -> tail(proper(X)),
                  proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                           proper(0()) -> ok(0()),
                   proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                      U102(mark(X1), X2) -> mark(U102(X1, X2)),
                    U102(ok(X1), ok(X2)) -> ok(U102(X1, X2)),
                        isNatural(ok(X)) -> ok(isNatural(X)),
                    active(U102(X1, X2)) -> U102(active(X1), X2),
                  active(U102(tt(), V2)) -> mark(U103(isLNat(V2))),
                active(isNatural(s(V1))) -> mark(U121(isNaturalKind(V1), V1)),
             active(isNatural(head(V1))) -> mark(U111(isLNatKind(V1), V1)),
                  active(isNatural(0())) -> mark(tt()),
          active(isNatural(sel(V1, V2))) ->
    mark(U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
                active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3),
              active(U101(tt(), V1, V2)) -> mark(U102(isNatural(V1), V2)),
                         active(U103(X)) -> U103(active(X)),
                      active(U103(tt())) -> mark(tt()),
                 active(isLNat(snd(V1))) -> mark(U81(isPLNatKind(V1), V1)),
            active(isLNat(cons(V1, V2))) ->
    mark(U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
            active(isLNat(natsFrom(V1))) -> mark(U71(isNaturalKind(V1), V1)),
        active(isLNat(afterNth(V1, V2))) ->
    mark(U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
                   active(isLNat(nil())) -> mark(tt()),
                 active(isLNat(fst(V1))) -> mark(U61(isPLNatKind(V1), V1)),
                active(isLNat(tail(V1))) -> mark(U91(isLNatKind(V1), V1)),
            active(isLNat(take(V1, V2))) ->
    mark(U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
                          active(snd(X)) -> snd(active(X)),
                 active(snd(pair(X, Y))) ->
    mark(
        U181(
            and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))),
            Y
        )
    ),
                 active(splitAt(X1, X2)) -> splitAt(X1, active(X2)),
                 active(splitAt(X1, X2)) -> splitAt(active(X1), X2),
      active(splitAt(s(N), cons(X, XS))) ->
    mark(
        U201(
            and(
               and(isNatural(N), isNaturalKind(N)),
               and(
                  and(isNatural(X), isNaturalKind(X)),
                  and(isLNat(XS), isLNatKind(XS))
               )
            ), N, X, XS
        )
    ),
                active(splitAt(0(), XS)) ->
    mark(U191(and(isLNat(XS), isLNatKind(XS)), XS)),
                 active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3),
                active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))),
                         active(U112(X)) -> U112(active(X)),
                      active(U112(tt())) -> mark(tt()),
                    active(U111(X1, X2)) -> U111(active(X1), X2),
                  active(U111(tt(), V1)) -> mark(U112(isLNat(V1))),
                         active(U122(X)) -> U122(active(X)),
                      active(U122(tt())) -> mark(tt()),
                    active(U121(X1, X2)) -> U121(active(X1), X2),
                  active(U121(tt(), V1)) -> mark(U122(isNatural(V1))),
                    active(U132(X1, X2)) -> U132(active(X1), X2),
                  active(U132(tt(), V2)) -> mark(U133(isLNat(V2))),
                active(U131(X1, X2, X3)) -> U131(active(X1), X2, X3),
              active(U131(tt(), V1, V2)) -> mark(U132(isNatural(V1), V2)),
                         active(U133(X)) -> U133(active(X)),
                      active(U133(tt())) -> mark(tt()),
                    active(U142(X1, X2)) -> U142(active(X1), X2),
                  active(U142(tt(), V2)) -> mark(U143(isLNat(V2))),
                active(U141(X1, X2, X3)) -> U141(active(X1), X2, X3),
              active(U141(tt(), V1, V2)) -> mark(U142(isLNat(V1), V2)),
                         active(U143(X)) -> U143(active(X)),
                      active(U143(tt())) -> mark(tt()),
                    active(U152(X1, X2)) -> U152(active(X1), X2),
                  active(U152(tt(), V2)) -> mark(U153(isLNat(V2))),
                active(U151(X1, X2, X3)) -> U151(active(X1), X2, X3),
              active(U151(tt(), V1, V2)) -> mark(U152(isNatural(V1), V2)),
                         active(U153(X)) -> U153(active(X)),
                      active(U153(tt())) -> mark(tt()),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                     active(natsFrom(N)) ->
    mark(U161(and(isNatural(N), isNaturalKind(N)), N)),
                     active(natsFrom(X)) -> natsFrom(active(X)),
                            active(s(X)) -> s(active(X)),
                    active(U161(X1, X2)) -> U161(active(X1), X2),
                   active(U161(tt(), N)) -> mark(cons(N, natsFrom(s(N)))),
                         active(head(X)) -> head(active(X)),
               active(head(cons(N, XS))) ->
    mark(
        U31(
           and(
              and(isNatural(N), isNaturalKind(N)),
              and(isLNat(XS), isLNatKind(XS))
           ), N
        )
    ),
                 active(afterNth(N, XS)) ->
    mark(
        U11(
           and(
              and(isNatural(N), isNaturalKind(N)),
              and(isLNat(XS), isLNatKind(XS))
           ), N, XS
        )
    ),
                active(afterNth(X1, X2)) -> afterNth(X1, active(X2)),
                active(afterNth(X1, X2)) -> afterNth(active(X1), X2),
                active(U171(X1, X2, X3)) -> U171(active(X1), X2, X3),
               active(U171(tt(), N, XS)) -> mark(head(afterNth(N, XS))),
                    active(U181(X1, X2)) -> U181(active(X1), X2),
                   active(U181(tt(), Y)) -> mark(Y),
                    active(pair(X1, X2)) -> pair(X1, active(X2)),
                    active(pair(X1, X2)) -> pair(active(X1), X2),
                    active(U191(X1, X2)) -> U191(active(X1), X2),
                  active(U191(tt(), XS)) -> mark(pair(nil(), XS)),
                    active(U202(X1, X2)) -> U202(active(X1), X2),
           active(U202(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
            active(U201(X1, X2, X3, X4)) -> U201(active(X1), X2, X3, X4),
            active(U201(tt(), N, X, XS)) -> mark(U202(splitAt(N, XS), X)),
                     active(U21(X1, X2)) -> U21(active(X1), X2),
                    active(U21(tt(), X)) -> mark(X),
                    active(U211(X1, X2)) -> U211(active(X1), X2),
                  active(U211(tt(), XS)) -> mark(XS),
                          active(fst(X)) -> fst(active(X)),
                 active(fst(pair(X, Y))) ->
    mark(
        U21(
           and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))),
           X
        )
    ),
                active(U221(X1, X2, X3)) -> U221(active(X1), X2, X3),
               active(U221(tt(), N, XS)) -> mark(fst(splitAt(N, XS))),
                     active(U31(X1, X2)) -> U31(active(X1), X2),
                    active(U31(tt(), N)) -> mark(N),
                     active(U42(X1, X2)) -> U42(active(X1), X2),
                   active(U42(tt(), V2)) -> mark(U43(isLNat(V2))),
                 active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3),
               active(U41(tt(), V1, V2)) -> mark(U42(isNatural(V1), V2)),
                          active(U43(X)) -> U43(active(X)),
                       active(U43(tt())) -> mark(tt()),
                     active(U52(X1, X2)) -> U52(active(X1), X2),
                   active(U52(tt(), V2)) -> mark(U53(isLNat(V2))),
                 active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3),
               active(U51(tt(), V1, V2)) -> mark(U52(isNatural(V1), V2)),
                          active(U53(X)) -> U53(active(X)),
                       active(U53(tt())) -> mark(tt()),
                          active(U62(X)) -> U62(active(X)),
                       active(U62(tt())) -> mark(tt()),
        active(isPLNat(splitAt(V1, V2))) ->
    mark(U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)),
           active(isPLNat(pair(V1, V2))) ->
    mark(U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2)),
                     active(U61(X1, X2)) -> U61(active(X1), X2),
                   active(U61(tt(), V1)) -> mark(U62(isPLNat(V1))),
                          active(U72(X)) -> U72(active(X)),
                       active(U72(tt())) -> mark(tt()),
                     active(U71(X1, X2)) -> U71(active(X1), X2),
                   active(U71(tt(), V1)) -> mark(U72(isNatural(V1))),
                          active(U82(X)) -> U82(active(X)),
                       active(U82(tt())) -> mark(tt()),
                     active(U81(X1, X2)) -> U81(active(X1), X2),
                   active(U81(tt(), V1)) -> mark(U82(isPLNat(V1))),
                          active(U92(X)) -> U92(active(X)),
                       active(U92(tt())) -> mark(tt()),
                     active(U91(X1, X2)) -> U91(active(X1), X2),
                   active(U91(tt(), V1)) -> mark(U92(isLNat(V1))),
                     active(and(X1, X2)) -> and(active(X1), X2),
                    active(and(tt(), X)) -> mark(X),
            active(isNaturalKind(s(V1))) -> mark(isNaturalKind(V1)),
         active(isNaturalKind(head(V1))) -> mark(isLNatKind(V1)),
              active(isNaturalKind(0())) -> mark(tt()),
      active(isNaturalKind(sel(V1, V2))) ->
    mark(and(isNaturalKind(V1), isLNatKind(V2))),
             active(isLNatKind(snd(V1))) -> mark(isPLNatKind(V1)),
        active(isLNatKind(cons(V1, V2))) ->
    mark(and(isNaturalKind(V1), isLNatKind(V2))),
        active(isLNatKind(natsFrom(V1))) -> mark(isNaturalKind(V1)),
    active(isLNatKind(afterNth(V1, V2))) ->
    mark(and(isNaturalKind(V1), isLNatKind(V2))),
               active(isLNatKind(nil())) -> mark(tt()),
             active(isLNatKind(fst(V1))) -> mark(isPLNatKind(V1)),
            active(isLNatKind(tail(V1))) -> mark(isLNatKind(V1)),
        active(isLNatKind(take(V1, V2))) ->
    mark(and(isNaturalKind(V1), isLNatKind(V2))),
    active(isPLNatKind(splitAt(V1, V2))) ->
    mark(and(isNaturalKind(V1), isLNatKind(V2))),
       active(isPLNatKind(pair(V1, V2))) ->
    mark(and(isLNatKind(V1), isLNatKind(V2))),
                         active(tail(X)) -> tail(active(X)),
               active(tail(cons(N, XS))) ->
    mark(
        U211(
            and(
               and(isNatural(N), isNaturalKind(N)),
               and(isLNat(XS), isLNatKind(XS))
            ), XS
        )
    ),
                     active(take(N, XS)) ->
    mark(
        U221(
            and(
               and(isNatural(N), isNaturalKind(N)),
               and(isLNat(XS), isLNatKind(XS))
            ), N, XS
        )
    ),
                    active(take(X1, X2)) -> take(X1, active(X2)),
                    active(take(X1, X2)) -> take(active(X1), X2),
                      active(sel(N, XS)) ->
    mark(
        U171(
            and(
               and(isNatural(N), isNaturalKind(N)),
               and(isLNat(XS), isLNatKind(XS))
            ), N, XS
        )
    ),
                     active(sel(X1, X2)) -> sel(X1, active(X2)),
                     active(sel(X1, X2)) -> sel(active(X1), X2),
                  U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)),
            U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)),
                           U103(mark(X)) -> mark(U103(X)),
                             U103(ok(X)) -> ok(U103(X)),
                           isLNat(ok(X)) -> ok(isLNat(X)),
                            snd(mark(X)) -> mark(snd(X)),
                              snd(ok(X)) -> ok(snd(X)),
                   splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)),
                   splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)),
                 splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)),
                   U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)),
             U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)),
                           U112(mark(X)) -> mark(U112(X)),
                             U112(ok(X)) -> ok(U112(X)),
                      U111(mark(X1), X2) -> mark(U111(X1, X2)),
                    U111(ok(X1), ok(X2)) -> ok(U111(X1, X2)),
                           U122(mark(X)) -> mark(U122(X)),
                             U122(ok(X)) -> ok(U122(X)),
                      U121(mark(X1), X2) -> mark(U121(X1, X2)),
                    U121(ok(X1), ok(X2)) -> ok(U121(X1, X2)),
                      U132(mark(X1), X2) -> mark(U132(X1, X2)),
                    U132(ok(X1), ok(X2)) -> ok(U132(X1, X2)),
                  U131(mark(X1), X2, X3) -> mark(U131(X1, X2, X3)),
            U131(ok(X1), ok(X2), ok(X3)) -> ok(U131(X1, X2, X3)),
                           U133(mark(X)) -> mark(U133(X)),
                             U133(ok(X)) -> ok(U133(X)),
                      U142(mark(X1), X2) -> mark(U142(X1, X2)),
                    U142(ok(X1), ok(X2)) -> ok(U142(X1, X2)),
                  U141(mark(X1), X2, X3) -> mark(U141(X1, X2, X3)),
            U141(ok(X1), ok(X2), ok(X3)) -> ok(U141(X1, X2, X3)),
                           U143(mark(X)) -> mark(U143(X)),
                             U143(ok(X)) -> ok(U143(X)),
                      U152(mark(X1), X2) -> mark(U152(X1, X2)),
                    U152(ok(X1), ok(X2)) -> ok(U152(X1, X2)),
                  U151(mark(X1), X2, X3) -> mark(U151(X1, X2, X3)),
            U151(ok(X1), ok(X2), ok(X3)) -> ok(U151(X1, X2, X3)),
                           U153(mark(X)) -> mark(U153(X)),
                             U153(ok(X)) -> ok(U153(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                       natsFrom(mark(X)) -> mark(natsFrom(X)),
                         natsFrom(ok(X)) -> ok(natsFrom(X)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                      U161(mark(X1), X2) -> mark(U161(X1, X2)),
                    U161(ok(X1), ok(X2)) -> ok(U161(X1, X2)),
                           head(mark(X)) -> mark(head(X)),
                             head(ok(X)) -> ok(head(X)),
                  afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)),
                  afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)),
                afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)),
                  U171(mark(X1), X2, X3) -> mark(U171(X1, X2, X3)),
            U171(ok(X1), ok(X2), ok(X3)) -> ok(U171(X1, X2, X3)),
                      U181(mark(X1), X2) -> mark(U181(X1, X2)),
                    U181(ok(X1), ok(X2)) -> ok(U181(X1, X2)),
                      pair(X1, mark(X2)) -> mark(pair(X1, X2)),
                      pair(mark(X1), X2) -> mark(pair(X1, X2)),
                    pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)),
                      U191(mark(X1), X2) -> mark(U191(X1, X2)),
                    U191(ok(X1), ok(X2)) -> ok(U191(X1, X2)),
                      U202(mark(X1), X2) -> mark(U202(X1, X2)),
                    U202(ok(X1), ok(X2)) -> ok(U202(X1, X2)),
              U201(mark(X1), X2, X3, X4) -> mark(U201(X1, X2, X3, X4)),
    U201(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U201(X1, X2, X3, X4)),
                       U21(mark(X1), X2) -> mark(U21(X1, X2)),
                     U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)),
                      U211(mark(X1), X2) -> mark(U211(X1, X2)),
                    U211(ok(X1), ok(X2)) -> ok(U211(X1, X2)),
                            fst(mark(X)) -> mark(fst(X)),
                              fst(ok(X)) -> ok(fst(X)),
                  U221(mark(X1), X2, X3) -> mark(U221(X1, X2, X3)),
            U221(ok(X1), ok(X2), ok(X3)) -> ok(U221(X1, X2, X3)),
                       U31(mark(X1), X2) -> mark(U31(X1, X2)),
                     U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)),
                       U42(mark(X1), X2) -> mark(U42(X1, X2)),
                     U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)),
                   U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)),
             U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)),
                            U43(mark(X)) -> mark(U43(X)),
                              U43(ok(X)) -> ok(U43(X)),
                       U52(mark(X1), X2) -> mark(U52(X1, X2)),
                     U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)),
                   U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)),
             U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)),
                            U53(mark(X)) -> mark(U53(X)),
                              U53(ok(X)) -> ok(U53(X)),
                            U62(mark(X)) -> mark(U62(X)),
                              U62(ok(X)) -> ok(U62(X)),
                          isPLNat(ok(X)) -> ok(isPLNat(X)),
                       U61(mark(X1), X2) -> mark(U61(X1, X2)),
                     U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)),
                            U72(mark(X)) -> mark(U72(X)),
                              U72(ok(X)) -> ok(U72(X)),
                       U71(mark(X1), X2) -> mark(U71(X1, X2)),
                     U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)),
                            U82(mark(X)) -> mark(U82(X)),
                              U82(ok(X)) -> ok(U82(X)),
                       U81(mark(X1), X2) -> mark(U81(X1, X2)),
                     U81(ok(X1), ok(X2)) -> ok(U81(X1, X2)),
                            U92(mark(X)) -> mark(U92(X)),
                              U92(ok(X)) -> ok(U92(X)),
                       U91(mark(X1), X2) -> mark(U91(X1, X2)),
                     U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)),
                       and(mark(X1), X2) -> mark(and(X1, X2)),
                     and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
                    isNaturalKind(ok(X)) -> ok(isNaturalKind(X)),
                       isLNatKind(ok(X)) -> ok(isLNatKind(X)),
                      isPLNatKind(ok(X)) -> ok(isPLNatKind(X)),
                           tail(mark(X)) -> mark(tail(X)),
                             tail(ok(X)) -> ok(tail(X)),
                      take(X1, mark(X2)) -> mark(take(X1, X2)),
                      take(mark(X1), X2) -> mark(take(X1, X2)),
                    take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                       sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                       sel(mark(X1), X2) -> mark(sel(X1, X2)),
                     sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                    proper(U102(X1, X2)) -> U102(proper(X1), proper(X2)),
                    proper(isNatural(X)) -> isNatural(proper(X)),
                proper(U101(X1, X2, X3)) ->
    U101(proper(X1), proper(X2), proper(X3)),
                            proper(tt()) -> ok(tt()),
                         proper(U103(X)) -> U103(proper(X)),
                       proper(isLNat(X)) -> isLNat(proper(X)),
                          proper(snd(X)) -> snd(proper(X)),
                 proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)),
                 proper(U11(X1, X2, X3)) ->
    U11(proper(X1), proper(X2), proper(X3)),
                         proper(U112(X)) -> U112(proper(X)),
                    proper(U111(X1, X2)) -> U111(proper(X1), proper(X2)),
                         proper(U122(X)) -> U122(proper(X)),
                    proper(U121(X1, X2)) -> U121(proper(X1), proper(X2)),
                    proper(U132(X1, X2)) -> U132(proper(X1), proper(X2)),
                proper(U131(X1, X2, X3)) ->
    U131(proper(X1), proper(X2), proper(X3)),
                         proper(U133(X)) -> U133(proper(X)),
                    proper(U142(X1, X2)) -> U142(proper(X1), proper(X2)),
                proper(U141(X1, X2, X3)) ->
    U141(proper(X1), proper(X2), proper(X3)),
                         proper(U143(X)) -> U143(proper(X)),
                    proper(U152(X1, X2)) -> U152(proper(X1), proper(X2)),
                proper(U151(X1, X2, X3)) ->
    U151(proper(X1), proper(X2), proper(X3)),
                         proper(U153(X)) -> U153(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                     proper(natsFrom(X)) -> natsFrom(proper(X)),
                            proper(s(X)) -> s(proper(X)),
                    proper(U161(X1, X2)) -> U161(proper(X1), proper(X2)),
                         proper(head(X)) -> head(proper(X)),
                proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)),
                proper(U171(X1, X2, X3)) ->
    U171(proper(X1), proper(X2), proper(X3)),
                    proper(U181(X1, X2)) -> U181(proper(X1), proper(X2)),
                    proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)),
                           proper(nil()) -> ok(nil()),
                    proper(U191(X1, X2)) -> U191(proper(X1), proper(X2)),
                    proper(U202(X1, X2)) -> U202(proper(X1), proper(X2)),
            proper(U201(X1, X2, X3, X4)) ->
    U201(proper(X1), proper(X2), proper(X3), proper(X4)),
                     proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)),
                    proper(U211(X1, X2)) -> U211(proper(X1), proper(X2)),
                          proper(fst(X)) -> fst(proper(X)),
                proper(U221(X1, X2, X3)) ->
    U221(proper(X1), proper(X2), proper(X3)),
                     proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)),
                     proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)),
                 proper(U41(X1, X2, X3)) ->
    U41(proper(X1), proper(X2), proper(X3)),
                          proper(U43(X)) -> U43(proper(X)),
                     proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)),
                 proper(U51(X1, X2, X3)) ->
    U51(proper(X1), proper(X2), proper(X3)),
                          proper(U53(X)) -> U53(proper(X)),
                          proper(U62(X)) -> U62(proper(X)),
                      proper(isPLNat(X)) -> isPLNat(proper(X)),
                     proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)),
                          proper(U72(X)) -> U72(proper(X)),
                     proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)),
                          proper(U82(X)) -> U82(proper(X)),
                     proper(U81(X1, X2)) -> U81(proper(X1), proper(X2)),
                          proper(U92(X)) -> U92(proper(X)),
                     proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)),
                     proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
                proper(isNaturalKind(X)) -> isNaturalKind(proper(X)),
                   proper(isLNatKind(X)) -> isLNatKind(proper(X)),
                  proper(isPLNatKind(X)) -> isPLNatKind(proper(X)),
                         proper(tail(X)) -> tail(proper(X)),
                    proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                             proper(0()) -> ok(0()),
                     proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))
   }
  Fail