MAYBE
MAYBE
TRS:
 {
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(zeros()) -> mark(cons(0(), zeros())),
                   active(U12(X1, X2)) -> U12(active(X1), X2),
                 active(U12(tt(), V1)) -> mark(U13(isNatList(V1))),
  active(isNatIListKind(cons(V1, V2))) -> mark(U51(isNatKind(V1), V2)),
       active(isNatIListKind(zeros())) -> mark(tt()),
         active(isNatIListKind(nil())) -> mark(tt()),
                   active(U11(X1, X2)) -> U11(active(X1), X2),
                 active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)),
                        active(U13(X)) -> U13(active(X)),
                     active(U13(tt())) -> mark(tt()),
       active(isNatList(cons(V1, V2))) -> mark(U81(isNatKind(V1), V1, V2)),
              active(isNatList(nil())) -> mark(tt()),
                   active(U22(X1, X2)) -> U22(active(X1), X2),
                 active(U22(tt(), V1)) -> mark(U23(isNat(V1))),
                active(isNatKind(0())) -> mark(tt()),
              active(isNatKind(s(V1))) -> mark(U71(isNatKind(V1))),
         active(isNatKind(length(V1))) -> mark(U61(isNatIListKind(V1))),
                   active(U21(X1, X2)) -> U21(active(X1), X2),
                 active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)),
                        active(U23(X)) -> U23(active(X)),
                     active(U23(tt())) -> mark(tt()),
                    active(isNat(0())) -> mark(tt()),
                  active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)),
             active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)),
                   active(U32(X1, X2)) -> U32(active(X1), X2),
                  active(U32(tt(), V)) -> mark(U33(isNatList(V))),
                   active(U31(X1, X2)) -> U31(active(X1), X2),
                  active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)),
                        active(U33(X)) -> U33(active(X)),
                     active(U33(tt())) -> mark(tt()),
               active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3),
             active(U42(tt(), V1, V2)) ->
  mark(U43(isNatIListKind(V2), V1, V2)),
               active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3),
             active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)),
               active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3),
             active(U43(tt(), V1, V2)) ->
  mark(U44(isNatIListKind(V2), V1, V2)),
               active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3),
             active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)),
                   active(U45(X1, X2)) -> U45(active(X1), X2),
                 active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))),
                        active(U46(X)) -> U46(active(X)),
                     active(U46(tt())) -> mark(tt()),
                 active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)),
      active(isNatIList(cons(V1, V2))) -> mark(U41(isNatKind(V1), V1, V2)),
           active(isNatIList(zeros())) -> mark(tt()),
                        active(U52(X)) -> U52(active(X)),
                     active(U52(tt())) -> mark(tt()),
                   active(U51(X1, X2)) -> U51(active(X1), X2),
                 active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))),
                        active(U61(X)) -> U61(active(X)),
                     active(U61(tt())) -> mark(tt()),
                        active(U71(X)) -> U71(active(X)),
                     active(U71(tt())) -> mark(tt()),
               active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3),
             active(U82(tt(), V1, V2)) ->
  mark(U83(isNatIListKind(V2), V1, V2)),
               active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3),
             active(U81(tt(), V1, V2)) -> mark(U82(isNatKind(V1), V1, V2)),
               active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3),
             active(U83(tt(), V1, V2)) ->
  mark(U84(isNatIListKind(V2), V1, V2)),
               active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3),
             active(U84(tt(), V1, V2)) -> mark(U85(isNat(V1), V2)),
                   active(U85(X1, X2)) -> U85(active(X1), X2),
                 active(U85(tt(), V2)) -> mark(U86(isNatList(V2))),
                        active(U86(X)) -> U86(active(X)),
                     active(U86(tt())) -> mark(tt()),
               active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3),
               active(U92(tt(), L, N)) -> mark(U93(isNat(N), L, N)),
               active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3),
               active(U91(tt(), L, N)) -> mark(U92(isNatIListKind(L), L, N)),
               active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3),
               active(U93(tt(), L, N)) -> mark(U94(isNatKind(N), L)),
                   active(U94(X1, X2)) -> U94(active(X1), X2),
                  active(U94(tt(), L)) -> mark(s(length(L))),
                          active(s(X)) -> s(active(X)),
                     active(length(X)) -> length(active(X)),
            active(length(cons(N, L))) -> mark(U91(isNatList(L), L, N)),
                 active(length(nil())) -> mark(0()),
                     U12(mark(X1), X2) -> mark(U12(X1, X2)),
                   U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)),
                 isNatIListKind(ok(X)) -> ok(isNatIListKind(X)),
                     U11(mark(X1), X2) -> mark(U11(X1, X2)),
                   U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)),
                          U13(mark(X)) -> mark(U13(X)),
                            U13(ok(X)) -> ok(U13(X)),
                      isNatList(ok(X)) -> ok(isNatList(X)),
                     U22(mark(X1), X2) -> mark(U22(X1, X2)),
                   U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)),
                      isNatKind(ok(X)) -> ok(isNatKind(X)),
                     U21(mark(X1), X2) -> mark(U21(X1, X2)),
                   U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)),
                          U23(mark(X)) -> mark(U23(X)),
                            U23(ok(X)) -> ok(U23(X)),
                          isNat(ok(X)) -> ok(isNat(X)),
                     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)),
                          U33(mark(X)) -> mark(U33(X)),
                            U33(ok(X)) -> ok(U33(X)),
                 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)),
                 U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)),
           U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)),
                 U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)),
           U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)),
                     U45(mark(X1), X2) -> mark(U45(X1, X2)),
                   U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)),
                          U46(mark(X)) -> mark(U46(X)),
                            U46(ok(X)) -> ok(U46(X)),
                     isNatIList(ok(X)) -> ok(isNatIList(X)),
                          U52(mark(X)) -> mark(U52(X)),
                            U52(ok(X)) -> ok(U52(X)),
                     U51(mark(X1), X2) -> mark(U51(X1, X2)),
                   U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)),
                          U61(mark(X)) -> mark(U61(X)),
                            U61(ok(X)) -> ok(U61(X)),
                          U71(mark(X)) -> mark(U71(X)),
                            U71(ok(X)) -> ok(U71(X)),
                 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)),
                 U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)),
           U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)),
                 U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)),
           U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)),
                     U85(mark(X1), X2) -> mark(U85(X1, X2)),
                   U85(ok(X1), ok(X2)) -> ok(U85(X1, X2)),
                          U86(mark(X)) -> mark(U86(X)),
                            U86(ok(X)) -> ok(U86(X)),
                 U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)),
           U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)),
                 U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)),
           U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)),
                 U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)),
           U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)),
                     U94(mark(X1), X2) -> mark(U94(X1, X2)),
                   U94(ok(X1), ok(X2)) -> ok(U94(X1, X2)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                       length(mark(X)) -> mark(length(X)),
                         length(ok(X)) -> ok(length(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(0()) -> ok(0()),
                       proper(zeros()) -> ok(zeros()),
                   proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)),
             proper(isNatIListKind(X)) -> isNatIListKind(proper(X)),
                   proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)),
                          proper(tt()) -> ok(tt()),
                        proper(U13(X)) -> U13(proper(X)),
                  proper(isNatList(X)) -> isNatList(proper(X)),
                   proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)),
                  proper(isNatKind(X)) -> isNatKind(proper(X)),
                   proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)),
                        proper(U23(X)) -> U23(proper(X)),
                      proper(isNat(X)) -> isNat(proper(X)),
                   proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)),
                   proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)),
                        proper(U33(X)) -> U33(proper(X)),
               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(U43(X1, X2, X3)) ->
  U43(proper(X1), proper(X2), proper(X3)),
               proper(U44(X1, X2, X3)) ->
  U44(proper(X1), proper(X2), proper(X3)),
                   proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)),
                        proper(U46(X)) -> U46(proper(X)),
                 proper(isNatIList(X)) -> isNatIList(proper(X)),
                        proper(U52(X)) -> U52(proper(X)),
                   proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)),
                        proper(U61(X)) -> U61(proper(X)),
                        proper(U71(X)) -> U71(proper(X)),
               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(U83(X1, X2, X3)) ->
  U83(proper(X1), proper(X2), proper(X3)),
               proper(U84(X1, X2, X3)) ->
  U84(proper(X1), proper(X2), proper(X3)),
                   proper(U85(X1, X2)) -> U85(proper(X1), proper(X2)),
                        proper(U86(X)) -> U86(proper(X)),
               proper(U92(X1, X2, X3)) ->
  U92(proper(X1), proper(X2), proper(X3)),
               proper(U91(X1, X2, X3)) ->
  U91(proper(X1), proper(X2), proper(X3)),
               proper(U93(X1, X2, X3)) ->
  U93(proper(X1), proper(X2), proper(X3)),
                   proper(U94(X1, X2)) -> U94(proper(X1), proper(X2)),
                          proper(s(X)) -> s(proper(X)),
                     proper(length(X)) -> length(proper(X)),
                         proper(nil()) -> ok(nil()),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                         active(zeros()) -> mark(cons(0(), zeros())),
                     active(U12(X1, X2)) -> U12(active(X1), X2),
                   active(U12(tt(), V1)) -> mark(U13(isNatList(V1))),
    active(isNatIListKind(cons(V1, V2))) -> mark(U51(isNatKind(V1), V2)),
         active(isNatIListKind(zeros())) -> mark(tt()),
           active(isNatIListKind(nil())) -> mark(tt()),
                     active(U11(X1, X2)) -> U11(active(X1), X2),
                   active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)),
                          active(U13(X)) -> U13(active(X)),
                       active(U13(tt())) -> mark(tt()),
         active(isNatList(cons(V1, V2))) -> mark(U81(isNatKind(V1), V1, V2)),
                active(isNatList(nil())) -> mark(tt()),
                     active(U22(X1, X2)) -> U22(active(X1), X2),
                   active(U22(tt(), V1)) -> mark(U23(isNat(V1))),
                  active(isNatKind(0())) -> mark(tt()),
                active(isNatKind(s(V1))) -> mark(U71(isNatKind(V1))),
           active(isNatKind(length(V1))) -> mark(U61(isNatIListKind(V1))),
                     active(U21(X1, X2)) -> U21(active(X1), X2),
                   active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)),
                          active(U23(X)) -> U23(active(X)),
                       active(U23(tt())) -> mark(tt()),
                      active(isNat(0())) -> mark(tt()),
                    active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)),
               active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)),
                     active(U32(X1, X2)) -> U32(active(X1), X2),
                    active(U32(tt(), V)) -> mark(U33(isNatList(V))),
                     active(U31(X1, X2)) -> U31(active(X1), X2),
                    active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)),
                          active(U33(X)) -> U33(active(X)),
                       active(U33(tt())) -> mark(tt()),
                 active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3),
               active(U42(tt(), V1, V2)) ->
    mark(U43(isNatIListKind(V2), V1, V2)),
                 active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3),
               active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)),
                 active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3),
               active(U43(tt(), V1, V2)) ->
    mark(U44(isNatIListKind(V2), V1, V2)),
                 active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3),
               active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)),
                     active(U45(X1, X2)) -> U45(active(X1), X2),
                   active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))),
                          active(U46(X)) -> U46(active(X)),
                       active(U46(tt())) -> mark(tt()),
                   active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)),
        active(isNatIList(cons(V1, V2))) -> mark(U41(isNatKind(V1), V1, V2)),
             active(isNatIList(zeros())) -> mark(tt()),
                          active(U52(X)) -> U52(active(X)),
                       active(U52(tt())) -> mark(tt()),
                     active(U51(X1, X2)) -> U51(active(X1), X2),
                   active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))),
                          active(U61(X)) -> U61(active(X)),
                       active(U61(tt())) -> mark(tt()),
                          active(U71(X)) -> U71(active(X)),
                       active(U71(tt())) -> mark(tt()),
                 active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3),
               active(U82(tt(), V1, V2)) ->
    mark(U83(isNatIListKind(V2), V1, V2)),
                 active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3),
               active(U81(tt(), V1, V2)) -> mark(U82(isNatKind(V1), V1, V2)),
                 active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3),
               active(U83(tt(), V1, V2)) ->
    mark(U84(isNatIListKind(V2), V1, V2)),
                 active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3),
               active(U84(tt(), V1, V2)) -> mark(U85(isNat(V1), V2)),
                     active(U85(X1, X2)) -> U85(active(X1), X2),
                   active(U85(tt(), V2)) -> mark(U86(isNatList(V2))),
                          active(U86(X)) -> U86(active(X)),
                       active(U86(tt())) -> mark(tt()),
                 active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3),
                 active(U92(tt(), L, N)) -> mark(U93(isNat(N), L, N)),
                 active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3),
                 active(U91(tt(), L, N)) ->
    mark(U92(isNatIListKind(L), L, N)),
                 active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3),
                 active(U93(tt(), L, N)) -> mark(U94(isNatKind(N), L)),
                     active(U94(X1, X2)) -> U94(active(X1), X2),
                    active(U94(tt(), L)) -> mark(s(length(L))),
                            active(s(X)) -> s(active(X)),
                       active(length(X)) -> length(active(X)),
              active(length(cons(N, L))) -> mark(U91(isNatList(L), L, N)),
                   active(length(nil())) -> mark(0()),
                       U12(mark(X1), X2) -> mark(U12(X1, X2)),
                     U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)),
                   isNatIListKind(ok(X)) -> ok(isNatIListKind(X)),
                       U11(mark(X1), X2) -> mark(U11(X1, X2)),
                     U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)),
                            U13(mark(X)) -> mark(U13(X)),
                              U13(ok(X)) -> ok(U13(X)),
                        isNatList(ok(X)) -> ok(isNatList(X)),
                       U22(mark(X1), X2) -> mark(U22(X1, X2)),
                     U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)),
                        isNatKind(ok(X)) -> ok(isNatKind(X)),
                       U21(mark(X1), X2) -> mark(U21(X1, X2)),
                     U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)),
                            U23(mark(X)) -> mark(U23(X)),
                              U23(ok(X)) -> ok(U23(X)),
                            isNat(ok(X)) -> ok(isNat(X)),
                       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)),
                            U33(mark(X)) -> mark(U33(X)),
                              U33(ok(X)) -> ok(U33(X)),
                   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)),
                   U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)),
             U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)),
                   U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)),
             U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)),
                       U45(mark(X1), X2) -> mark(U45(X1, X2)),
                     U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)),
                            U46(mark(X)) -> mark(U46(X)),
                              U46(ok(X)) -> ok(U46(X)),
                       isNatIList(ok(X)) -> ok(isNatIList(X)),
                            U52(mark(X)) -> mark(U52(X)),
                              U52(ok(X)) -> ok(U52(X)),
                       U51(mark(X1), X2) -> mark(U51(X1, X2)),
                     U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)),
                            U61(mark(X)) -> mark(U61(X)),
                              U61(ok(X)) -> ok(U61(X)),
                            U71(mark(X)) -> mark(U71(X)),
                              U71(ok(X)) -> ok(U71(X)),
                   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)),
                   U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)),
             U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)),
                   U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)),
             U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)),
                       U85(mark(X1), X2) -> mark(U85(X1, X2)),
                     U85(ok(X1), ok(X2)) -> ok(U85(X1, X2)),
                            U86(mark(X)) -> mark(U86(X)),
                              U86(ok(X)) -> ok(U86(X)),
                   U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)),
             U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)),
                   U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)),
             U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)),
                   U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)),
             U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)),
                       U94(mark(X1), X2) -> mark(U94(X1, X2)),
                     U94(ok(X1), ok(X2)) -> ok(U94(X1, X2)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                         length(mark(X)) -> mark(length(X)),
                           length(ok(X)) -> ok(length(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                             proper(0()) -> ok(0()),
                         proper(zeros()) -> ok(zeros()),
                     proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)),
               proper(isNatIListKind(X)) -> isNatIListKind(proper(X)),
                     proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)),
                            proper(tt()) -> ok(tt()),
                          proper(U13(X)) -> U13(proper(X)),
                    proper(isNatList(X)) -> isNatList(proper(X)),
                     proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)),
                    proper(isNatKind(X)) -> isNatKind(proper(X)),
                     proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)),
                          proper(U23(X)) -> U23(proper(X)),
                        proper(isNat(X)) -> isNat(proper(X)),
                     proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)),
                     proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)),
                          proper(U33(X)) -> U33(proper(X)),
                 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(U43(X1, X2, X3)) ->
    U43(proper(X1), proper(X2), proper(X3)),
                 proper(U44(X1, X2, X3)) ->
    U44(proper(X1), proper(X2), proper(X3)),
                     proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)),
                          proper(U46(X)) -> U46(proper(X)),
                   proper(isNatIList(X)) -> isNatIList(proper(X)),
                          proper(U52(X)) -> U52(proper(X)),
                     proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)),
                          proper(U61(X)) -> U61(proper(X)),
                          proper(U71(X)) -> U71(proper(X)),
                 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(U83(X1, X2, X3)) ->
    U83(proper(X1), proper(X2), proper(X3)),
                 proper(U84(X1, X2, X3)) ->
    U84(proper(X1), proper(X2), proper(X3)),
                     proper(U85(X1, X2)) -> U85(proper(X1), proper(X2)),
                          proper(U86(X)) -> U86(proper(X)),
                 proper(U92(X1, X2, X3)) ->
    U92(proper(X1), proper(X2), proper(X3)),
                 proper(U91(X1, X2, X3)) ->
    U91(proper(X1), proper(X2), proper(X3)),
                 proper(U93(X1, X2, X3)) ->
    U93(proper(X1), proper(X2), proper(X3)),
                     proper(U94(X1, X2)) -> U94(proper(X1), proper(X2)),
                            proper(s(X)) -> s(proper(X)),
                       proper(length(X)) -> length(proper(X)),
                           proper(nil()) -> ok(nil()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))
   }
  Fail