MAYBE
MAYBE
TRS:
 {
                U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)),
          U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)),
              active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3),
             active(U12(tt(), N, XS)) -> mark(snd(splitAt(N, XS))),
              active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3),
             active(U11(tt(), N, XS)) -> mark(U12(tt(), N, XS)),
                       active(snd(X)) -> snd(active(X)),
              active(snd(pair(X, Y))) -> mark(U51(tt(), 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(U61(tt(), N, X, XS)),
             active(splitAt(0(), XS)) -> mark(pair(nil(), XS)),
                  active(U22(X1, X2)) -> U22(active(X1), X2),
                 active(U22(tt(), X)) -> mark(X),
                  active(U21(X1, X2)) -> U21(active(X1), X2),
                 active(U21(tt(), X)) -> mark(U22(tt(), X)),
                  active(U32(X1, X2)) -> U32(active(X1), X2),
                 active(U32(tt(), N)) -> mark(N),
                  active(U31(X1, X2)) -> U31(active(X1), X2),
                 active(U31(tt(), N)) -> mark(U32(tt(), N)),
              active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3),
             active(U42(tt(), N, XS)) -> mark(head(afterNth(N, XS))),
              active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3),
             active(U41(tt(), N, XS)) -> mark(U42(tt(), N, XS)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(N, XS))) -> mark(U31(tt(), N)),
              active(afterNth(N, XS)) -> mark(U11(tt(), N, XS)),
             active(afterNth(X1, X2)) -> afterNth(X1, active(X2)),
             active(afterNth(X1, X2)) -> afterNth(active(X1), X2),
                  active(U52(X1, X2)) -> U52(active(X1), X2),
                 active(U52(tt(), Y)) -> mark(Y),
                  active(U51(X1, X2)) -> U51(active(X1), X2),
                 active(U51(tt(), Y)) -> mark(U52(tt(), Y)),
          active(U62(X1, X2, X3, X4)) -> U62(active(X1), X2, X3, X4),
          active(U62(tt(), N, X, XS)) -> mark(U63(tt(), N, X, XS)),
          active(U61(X1, X2, X3, X4)) -> U61(active(X1), X2, X3, X4),
          active(U61(tt(), N, X, XS)) -> mark(U62(tt(), N, X, XS)),
          active(U63(X1, X2, X3, X4)) -> U63(active(X1), X2, X3, X4),
          active(U63(tt(), N, X, XS)) -> mark(U64(splitAt(N, XS), X)),
                  active(U64(X1, X2)) -> U64(active(X1), X2),
         active(U64(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
                 active(pair(X1, X2)) -> pair(X1, active(X2)),
                 active(pair(X1, X2)) -> pair(active(X1), X2),
                 active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(U72(X1, X2)) -> U72(active(X1), X2),
                active(U72(tt(), XS)) -> mark(XS),
                  active(U71(X1, X2)) -> U71(active(X1), X2),
                active(U71(tt(), XS)) -> mark(U72(tt(), XS)),
              active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3),
             active(U82(tt(), N, XS)) -> mark(fst(splitAt(N, XS))),
              active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3),
             active(U81(tt(), N, XS)) -> mark(U82(tt(), N, XS)),
                       active(fst(X)) -> fst(active(X)),
              active(fst(pair(X, Y))) -> mark(U21(tt(), X)),
                  active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))),
                  active(natsFrom(X)) -> natsFrom(active(X)),
                         active(s(X)) -> s(active(X)),
                   active(sel(N, XS)) -> mark(U41(tt(), N, XS)),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
                      active(tail(X)) -> tail(active(X)),
            active(tail(cons(N, XS))) -> mark(U71(tt(), XS)),
                  active(take(N, XS)) -> mark(U81(tt(), N, XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
                U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)),
          U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)),
                         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)),
                    U22(mark(X1), X2) -> mark(U22(X1, X2)),
                  U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)),
                    U21(mark(X1), X2) -> mark(U21(X1, X2)),
                  U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)),
                    U32(mark(X1), X2) -> mark(U32(X1, X2)),
                  U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)),
                    U31(mark(X1), X2) -> mark(U31(X1, X2)),
                  U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)),
                U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)),
          U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)),
                U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)),
          U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)),
                        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)),
                    U52(mark(X1), X2) -> mark(U52(X1, X2)),
                  U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)),
                    U51(mark(X1), X2) -> mark(U51(X1, X2)),
                  U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)),
            U62(mark(X1), X2, X3, X4) -> mark(U62(X1, X2, X3, X4)),
  U62(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U62(X1, X2, X3, X4)),
            U61(mark(X1), X2, X3, X4) -> mark(U61(X1, X2, X3, X4)),
  U61(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U61(X1, X2, X3, X4)),
            U63(mark(X1), X2, X3, X4) -> mark(U63(X1, X2, X3, X4)),
  U63(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U63(X1, X2, X3, X4)),
                    U64(mark(X1), X2) -> mark(U64(X1, X2)),
                  U64(ok(X1), ok(X2)) -> ok(U64(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)),
                   cons(mark(X1), X2) -> mark(cons(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    U72(mark(X1), X2) -> mark(U72(X1, X2)),
                  U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)),
                    U71(mark(X1), X2) -> mark(U71(X1, X2)),
                  U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)),
                U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)),
          U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)),
                U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)),
          U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)),
                         fst(mark(X)) -> mark(fst(X)),
                           fst(ok(X)) -> ok(fst(X)),
                    natsFrom(mark(X)) -> mark(natsFrom(X)),
                      natsFrom(ok(X)) -> ok(natsFrom(X)),
                           s(mark(X)) -> mark(s(X)),
                             s(ok(X)) -> ok(s(X)),
                    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)),
                        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)),
              proper(U12(X1, X2, X3)) ->
  U12(proper(X1), proper(X2), proper(X3)),
                         proper(tt()) -> ok(tt()),
              proper(U11(X1, X2, X3)) ->
  U11(proper(X1), proper(X2), proper(X3)),
                       proper(snd(X)) -> snd(proper(X)),
              proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)),
                  proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)),
                  proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)),
                  proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)),
                  proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)),
              proper(U42(X1, X2, X3)) ->
  U42(proper(X1), proper(X2), proper(X3)),
              proper(U41(X1, X2, X3)) ->
  U41(proper(X1), proper(X2), proper(X3)),
                      proper(head(X)) -> head(proper(X)),
             proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)),
                  proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)),
                  proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)),
          proper(U62(X1, X2, X3, X4)) ->
  U62(proper(X1), proper(X2), proper(X3), proper(X4)),
          proper(U61(X1, X2, X3, X4)) ->
  U61(proper(X1), proper(X2), proper(X3), proper(X4)),
          proper(U63(X1, X2, X3, X4)) ->
  U63(proper(X1), proper(X2), proper(X3), proper(X4)),
                  proper(U64(X1, X2)) -> U64(proper(X1), proper(X2)),
                 proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)),
                  proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)),
              proper(U82(X1, X2, X3)) ->
  U82(proper(X1), proper(X2), proper(X3)),
              proper(U81(X1, X2, X3)) ->
  U81(proper(X1), proper(X2), proper(X3)),
                       proper(fst(X)) -> fst(proper(X)),
                  proper(natsFrom(X)) -> natsFrom(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                        proper(nil()) -> ok(nil()),
                          proper(0()) -> ok(0()),
                      proper(tail(X)) -> tail(proper(X)),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)),
            U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)),
                active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3),
               active(U12(tt(), N, XS)) -> mark(snd(splitAt(N, XS))),
                active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3),
               active(U11(tt(), N, XS)) -> mark(U12(tt(), N, XS)),
                         active(snd(X)) -> snd(active(X)),
                active(snd(pair(X, Y))) -> mark(U51(tt(), 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(U61(tt(), N, X, XS)),
               active(splitAt(0(), XS)) -> mark(pair(nil(), XS)),
                    active(U22(X1, X2)) -> U22(active(X1), X2),
                   active(U22(tt(), X)) -> mark(X),
                    active(U21(X1, X2)) -> U21(active(X1), X2),
                   active(U21(tt(), X)) -> mark(U22(tt(), X)),
                    active(U32(X1, X2)) -> U32(active(X1), X2),
                   active(U32(tt(), N)) -> mark(N),
                    active(U31(X1, X2)) -> U31(active(X1), X2),
                   active(U31(tt(), N)) -> mark(U32(tt(), N)),
                active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3),
               active(U42(tt(), N, XS)) -> mark(head(afterNth(N, XS))),
                active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3),
               active(U41(tt(), N, XS)) -> mark(U42(tt(), N, XS)),
                        active(head(X)) -> head(active(X)),
              active(head(cons(N, XS))) -> mark(U31(tt(), N)),
                active(afterNth(N, XS)) -> mark(U11(tt(), N, XS)),
               active(afterNth(X1, X2)) -> afterNth(X1, active(X2)),
               active(afterNth(X1, X2)) -> afterNth(active(X1), X2),
                    active(U52(X1, X2)) -> U52(active(X1), X2),
                   active(U52(tt(), Y)) -> mark(Y),
                    active(U51(X1, X2)) -> U51(active(X1), X2),
                   active(U51(tt(), Y)) -> mark(U52(tt(), Y)),
            active(U62(X1, X2, X3, X4)) -> U62(active(X1), X2, X3, X4),
            active(U62(tt(), N, X, XS)) -> mark(U63(tt(), N, X, XS)),
            active(U61(X1, X2, X3, X4)) -> U61(active(X1), X2, X3, X4),
            active(U61(tt(), N, X, XS)) -> mark(U62(tt(), N, X, XS)),
            active(U63(X1, X2, X3, X4)) -> U63(active(X1), X2, X3, X4),
            active(U63(tt(), N, X, XS)) -> mark(U64(splitAt(N, XS), X)),
                    active(U64(X1, X2)) -> U64(active(X1), X2),
           active(U64(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
                   active(pair(X1, X2)) -> pair(X1, active(X2)),
                   active(pair(X1, X2)) -> pair(active(X1), X2),
                   active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(U72(X1, X2)) -> U72(active(X1), X2),
                  active(U72(tt(), XS)) -> mark(XS),
                    active(U71(X1, X2)) -> U71(active(X1), X2),
                  active(U71(tt(), XS)) -> mark(U72(tt(), XS)),
                active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3),
               active(U82(tt(), N, XS)) -> mark(fst(splitAt(N, XS))),
                active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3),
               active(U81(tt(), N, XS)) -> mark(U82(tt(), N, XS)),
                         active(fst(X)) -> fst(active(X)),
                active(fst(pair(X, Y))) -> mark(U21(tt(), X)),
                    active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))),
                    active(natsFrom(X)) -> natsFrom(active(X)),
                           active(s(X)) -> s(active(X)),
                     active(sel(N, XS)) -> mark(U41(tt(), N, XS)),
                    active(sel(X1, X2)) -> sel(X1, active(X2)),
                    active(sel(X1, X2)) -> sel(active(X1), X2),
                        active(tail(X)) -> tail(active(X)),
              active(tail(cons(N, XS))) -> mark(U71(tt(), XS)),
                    active(take(N, XS)) -> mark(U81(tt(), N, XS)),
                   active(take(X1, X2)) -> take(X1, active(X2)),
                   active(take(X1, X2)) -> take(active(X1), X2),
                  U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)),
            U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)),
                           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)),
                      U22(mark(X1), X2) -> mark(U22(X1, X2)),
                    U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)),
                      U21(mark(X1), X2) -> mark(U21(X1, X2)),
                    U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)),
                      U32(mark(X1), X2) -> mark(U32(X1, X2)),
                    U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)),
                      U31(mark(X1), X2) -> mark(U31(X1, X2)),
                    U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)),
                  U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)),
            U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)),
                  U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)),
            U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)),
                          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)),
                      U52(mark(X1), X2) -> mark(U52(X1, X2)),
                    U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)),
                      U51(mark(X1), X2) -> mark(U51(X1, X2)),
                    U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)),
              U62(mark(X1), X2, X3, X4) -> mark(U62(X1, X2, X3, X4)),
    U62(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U62(X1, X2, X3, X4)),
              U61(mark(X1), X2, X3, X4) -> mark(U61(X1, X2, X3, X4)),
    U61(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U61(X1, X2, X3, X4)),
              U63(mark(X1), X2, X3, X4) -> mark(U63(X1, X2, X3, X4)),
    U63(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U63(X1, X2, X3, X4)),
                      U64(mark(X1), X2) -> mark(U64(X1, X2)),
                    U64(ok(X1), ok(X2)) -> ok(U64(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)),
                     cons(mark(X1), X2) -> mark(cons(X1, X2)),
                   cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      U72(mark(X1), X2) -> mark(U72(X1, X2)),
                    U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)),
                      U71(mark(X1), X2) -> mark(U71(X1, X2)),
                    U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)),
                  U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)),
            U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)),
                  U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)),
            U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)),
                           fst(mark(X)) -> mark(fst(X)),
                             fst(ok(X)) -> ok(fst(X)),
                      natsFrom(mark(X)) -> mark(natsFrom(X)),
                        natsFrom(ok(X)) -> ok(natsFrom(X)),
                             s(mark(X)) -> mark(s(X)),
                               s(ok(X)) -> ok(s(X)),
                      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)),
                          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)),
                proper(U12(X1, X2, X3)) ->
    U12(proper(X1), proper(X2), proper(X3)),
                           proper(tt()) -> ok(tt()),
                proper(U11(X1, X2, X3)) ->
    U11(proper(X1), proper(X2), proper(X3)),
                         proper(snd(X)) -> snd(proper(X)),
                proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)),
                    proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)),
                    proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)),
                    proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)),
                    proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)),
                proper(U42(X1, X2, X3)) ->
    U42(proper(X1), proper(X2), proper(X3)),
                proper(U41(X1, X2, X3)) ->
    U41(proper(X1), proper(X2), proper(X3)),
                        proper(head(X)) -> head(proper(X)),
               proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)),
                    proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)),
                    proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)),
            proper(U62(X1, X2, X3, X4)) ->
    U62(proper(X1), proper(X2), proper(X3), proper(X4)),
            proper(U61(X1, X2, X3, X4)) ->
    U61(proper(X1), proper(X2), proper(X3), proper(X4)),
            proper(U63(X1, X2, X3, X4)) ->
    U63(proper(X1), proper(X2), proper(X3), proper(X4)),
                    proper(U64(X1, X2)) -> U64(proper(X1), proper(X2)),
                   proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)),
                   proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)),
                    proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)),
                proper(U82(X1, X2, X3)) ->
    U82(proper(X1), proper(X2), proper(X3)),
                proper(U81(X1, X2, X3)) ->
    U81(proper(X1), proper(X2), proper(X3)),
                         proper(fst(X)) -> fst(proper(X)),
                    proper(natsFrom(X)) -> natsFrom(proper(X)),
                           proper(s(X)) -> s(proper(X)),
                    proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                          proper(nil()) -> ok(nil()),
                            proper(0()) -> ok(0()),
                        proper(tail(X)) -> tail(proper(X)),
                   proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                           top(mark(X)) -> top(proper(X)),
                             top(ok(X)) -> top(active(X))
   }
  Fail